matita/matita/contribs/lambdadelta/basic_2/etc/llpx_sn_alt2.etc

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 include "basic_2/substitution/cofrees_lift.ma".
  16 include "basic_2/substitution/llpx_sn_alt1.ma".
  17
  18 (* LAZY SN POINTWISE EXTENSION OF A CONTEXT-SENSITIVE REALTION FOR TERMS ****)
  19
  20 (* alternative definition of llpx_sn (not recursive) *)
  21 definition llpx_sn_alt2: relation4 bind2 lenv term term → relation4 ynat term lenv lenv ≝
  22                          λR,d,T,L1,L2. |L1| = |L2| ∧
  23                          (∀I1,I2,K1,K2,V1,V2,i. d ≤ yinj i → (L1 ⊢ i ~ϵ 𝐅*[d]⦃T⦄ → ⊥) →
  24                             ⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L2 ≡ K2.ⓑ{I2}V2 →
  25                             I1 = I2 ∧ R I1 K1 V1 V2
  26                          ).
  27
  28 (* Main properties **********************************************************)
  29
  30 lemma cpy_inv_nlift2_be: ∀G,L,U1,U2,d. ⦃G, L⦄ ⊢ U1 ▶[d, ∞] U2 → ∀i. d ≤ yinj i →
  31                          ∀K,s. ⇩[s, i, 1] L ≡ K →
  32                          (∀T2. ⇧[i, 1] T2 ≡ U2 → ⊥) → (∀T1. ⇧[i, 1] T1 ≡ U1 → ⊥).
  33 #G #L #U1 #U2 #d #HU12 #i #Hdi #K #s #HLK #HnU2 #T1 #HTU1
  34 elim (cpy_inv_lift1_be … HU12 … HLK … HTU1) /2 width=2 by/
  35 qed-.
  36
  37 lemma cpy_inv_nlift2_ge: ∀G,L,U1,U2,d,e. ⦃G, L⦄ ⊢ U1 ▶[d, e] U2 →
  38                          ∀i. d ≤ yinj i → (* yinj i + yinj 1 ≤ d + e → *)
  39                          (∀T2. ⇧[i, 1] T2 ≡ U2 → ⊥) →
  40                          ∃∃j. d ≤ yinj j & j ≤ i & (∀T1. ⇧[j, 1] T1 ≡ U1 → ⊥).
  41 #G #L #U1 #U2 #d #e #H elim H -G -L -U1 -U2 -d -e
  42 [ #I #G #L #d #e #i #Hdi (* #Hide *) #H @(ex3_intro … i) /2 width=2 by/
  43 | #I #G #L #K #V #W #j #d #e #Hdj #Hjde #HLK #HVW #i #Hdi (* #Hide *) #HnW
  44   elim (le_or_ge i j) #Hij [2: @(ex3_intro … j) /2 width=7 by lift_inv_lref2_be/ ]
  45   elim (lift_split … HVW i j) -HVW //
  46   #X #_ #H elim HnW -HnW //
  47 | #a #I #G #L #W1 #W2 #U1 #U2 #d #e #_ #_ #IHW12 #IHU12 #i #Hdi #H elim (nlift_inv_bind … H) -H
  48   [ #HnW2 elim (IHW12 … HnW2) -IHW12 -HnW2 -IHU12 //
  49     #j #Hdj #Hji #HnW1 @(ex3_intro … j) /3 width=9 by nlift_bind_sn/
  50   | #HnU2 elim (IHU12 … HnU2) -IHU12 -HnU2 -IHW12 /2 width=1 by yle_succ/
  51     #j #Hdj #Hji
  52     >(plus_minus_m_m j 1) in ⊢ (%→?); [2: /3 width=3 by yle_trans, yle_inv_inj/ ]
  53     #HnW1 @(ex3_intro … (j-1)) /3 width=9 by nlift_bind_dx, yle_pred, monotonic_pred/
  54   ]
  55 | #I #G #L #W1 #W2 #U1 #U2 #d #e #_ #_ #IHW12 #IHU12 #i #Hdi #H elim (nlift_inv_flat … H) -H
  56   [ #HnW2 elim (IHW12 … HnW2) -IHW12 -HnW2 -IHU12 //
  57     #j #Hdj #Hji #HnW1 @(ex3_intro … j) /3 width=8 by nlift_flat_sn/
  58   | #HnU2 elim (IHU12 … HnU2) -IHU12 -HnU2 -IHW12 //
  59     #j #Hdj #Hji #HnW1 @(ex3_intro … j) /3 width=8 by nlift_flat_dx/
  60   ]
  61 ]
  62 qed-.
  63
  64 axiom frees_fwd_nlift_ge: ∀L,U,d,i. (L ⊢ i ~ϵ 𝐅*[d]⦃U⦄ → ⊥) → d ≤ yinj i →
  65                           ∃∃j. d ≤ yinj j & j ≤ i & (∀T. ⇧[j, 1] T ≡ U → ⊥).
  66
  67 (*
  68 lemma frees_ind_nlift: ∀L,d. ∀R:relation2 term nat.
  69                        (∀U1,i. d ≤ yinj i → (∀T1. ⇧[i, 1] T1 ≡ U1 → ⊥) → R U1 i) →
  70                        (∀U1,U2,i,j. d ≤ yinj j → j ≤ i → ⦃⋆, L⦄ ⊢ U1 ▶[d, ∞] U2 → (∀T2. ⇧[i, 1] T2 ≡ U2 → ⊥) → R U2 i → R U1 j) →
  71                        ∀U,i. d ≤ yinj i → (L ⊢ i ~ϵ 𝐅*[d]⦃U⦄ → ⊥) → R U i.
  72 #L #d #R #IH1 #IH2 #U1 #i #Hdi #H @(frees_ind … H) -U1 /3 width=4 by/
  73 #U1 #U2 #HU12 #HnU2 #HU2 @(IH2 … HU12 … HU2)
  74
  75 qed-.
  76 *)(*
  77 lemma frees_fwd_nlift: ∀L,d. ∀R:relation2 term nat. (
  78                           ∀U1,j. (∀T1. ⇧[j, 1] T1 ≡ U1 → ⊥) ∨
  79                                  (∃∃U2,i. d ≤ yinj j → j < i & (L ⊢ j ~ϵ 𝐅*[d]⦃U1⦄ → ⊥) & ⦃⋆, L⦄ ⊢ U1 ▶[d, ∞] U2 & R U1 i
  80                                  ) →
  81                           d ≤ yinj j → R U1 j
  82                        ) →
  83                        ∀U,i. d ≤ yinj i → (L ⊢ i ~ϵ 𝐅*[d]⦃U⦄ → ⊥) → R U i.
  84 #L #d #R #IHR #U1 #j #Hdj #H elim (frees_inv_gen … H) -H
  85 #U2 #H generalize in match Hdj; -Hdj generalize in match j; -j @(cpys_ind … H) -U2
  86 [ #j #Hdj #HnU1 @IHR -IHR /3 width=2 by or_introl/
  87 | #U0 #U2 #HU10 #HU02 #IHU10 #j #Hdj #HnU2 elim (cpy_inv_nlift2_ge … HU02 … Hdj HnU2) -HU02 -HnU2
  88   #i #Hdi #Hij #HnU0 lapply (IHU10 … HnU0) // -IHU10
  89   #Hi @IHR -IHR // -Hdj @or_intror
  90
  91 lemma frees_fwd_nlift: ∀L,U,d,i. d ≤ yinj i → (L ⊢ i ~ϵ 𝐅*[d]⦃U⦄ → ⊥) →
  92                        ∃∃j. d ≤ yinj j & j ≤ i & (∀T. ⇧[j, 1] T ≡ U → ⊥).
  93 #L #U1 #d #i #Hdi  #H
  94 #U2 #H #HnU2 @(cpys_ind_dx … H) -U1 [ @(ex3_intro … i) /2 width=2 by/ ] -Hdi -HnU2
  95 #U1 #U0 #HU10 #_ * #j #Hdj #Hji #HnU0 elim (cpy_inv_nlift2_ge … HU10 … Hdj HnU0) -U0 -Hdj
  96 /3 width=5 by transitive_le, ex3_intro/
  97 qed-.
  98 *)
  99
 100 theorem llpx_sn_llpx_sn_alt2: ∀R,L1,L2,T,d. llpx_sn R d T L1 L2 → llpx_sn_alt2 R d T L1 L2.
 101 #R #L1 #L2 #U1 #d #H elim (llpx_sn_inv_alt1 … H) -H
 102 #HL12 #IH @conj // -HL12
 103 #I1 #I2 #K1 #K2 #V1 #V2 #i #Hdi #H #HLK1 #HLK2
 104 elim (frees_fwd_nlift_ge … H Hdi) -H -Hdi #j #Hdj #Hji #HnU1
 105 lapply (ldrop_fwd_length_lt2 … HLK1) #HL1
 106 lapply (ldrop_fwd_length_lt2 … HLK2) #HL2
 107 lapply (le_to_lt_to_lt … Hji HL1) -HL1 #HL1
 108 lapply (le_to_lt_to_lt … Hji HL2) -HL2 #HL2
 109 elim (ldrop_O1_lt L1 j) // #Z1 #Y1 #X1 #HLY1
 110 elim (ldrop_O1_lt L2 j) // #Z2 #Y2 #X2 #HLY2
 111
 112
 113
 114
 115 generalize in match V2; -V2 generalize in match V1; -V1
 116 generalize in match K2; -K2 generalize in match K1; -K1
 117 generalize in match I2; -I2 generalize in match I1; -I1
 118 generalize in match IH; -IH
 119 @(frees_ind_nlift … Hdi H) -U1 -i
 120 [ #U1 #i #Hdi #HnU1 #IH #I1 #I2 #K1 #K2 #V1 #V2 #HLK1 #HLK2 elim (IH … HnU1 HLK1 HLK2) -IH -HnU1 -HLK1 -HLK2 /2 width=1 by conj/
 121 | #U1 #U2 #i #j #Hdj #Hji #HU12 #HnU2 #IHU12 #IH #I1 #I2 #K1 #K2 #V1 #V2 #HLK1 #HLK2
 122 (*
 123 *)
 124   @(IHU12) … HLK1 HLK2)
 125
 126   @(IHU12 … HLK1 HLK2) -IHU02 -I1 -I2 -K1 -K2 -V1 -V2
 127   #I1 #I2 #K1 #K2 #V1 #V2 #j #Hdj #HnU0 #HLK1 #HLK2 @(IH … HLK1 HLK2) -IH -HLK1 -HLK2 //
 128
 129
 130
 131  elim (frees_fwd_nlift … HnU1) // -HnU1 -Hdi
 132 #j #Hdj #Hji #HnU1
 133 lapply (ldrop_fwd_length_lt2 … HLK1) #HL1
 134 lapply (ldrop_fwd_length_lt2 … HLK2) #HL2
 135 lapply (le_to_lt_to_lt … Hji HL1) -HL1 #HL1
 136 lapply (le_to_lt_to_lt … Hji HL2) -HL2 #HL2
 137 elim (ldrop_O1_lt L1 j) // #Z1 #Y1 #X1 #HLY1
 138 elim (ldrop_O1_lt L2 j) // #Z2 #Y2 #X2 #HLY2
 139 elim (IH … HnU1 HLY1 HLY2) // #H #HX12 #HY12 destruct
 140
 141
 142
 143
 144
 145
 146
 147
 148
 149
 150
 151
 152
 153
 154
 155
 156
 157
 158
 159
 160
 161
 162 theorem llpx_sn_llpx_sn_alt2: ∀R,L1,L2,T,d. llpx_sn R d T L1 L2 → llpx_sn_alt2 R d T L1 L2.
 163 #R #L1 #L2 #U1 #d #H @(llpx_sn_ind_alt1 … H) -L1 -L2 -U1 -d
 164 #L1 #L2 #U1 #d #HL12 #IH @conj // -HL12
 165 #I1 #I2 #K1 #K2 #V1 #V2 #i #Hdi #HnU1 #HLK1 #HLK2 elim (frees_inv_gen … HnU1) -HnU1
 166 #U2 #H generalize in match IH; -IH @(cpys_ind_dx … H) -U1
 167 [ #IH #HnU2 elim (IH … HnU2 … HLK1 HLK2) -L1 -L2 -U2 /2 width=1 by conj/
 168 | #U1 #U0 #HU10 #_ #IHU02 #IH #HnU2 @IHU02 /2 width=2 by/ -I1 -I2 -K1 -K2 -V1 -V2 -U2 -i
 169   #I1 #I2 #K1 #K2 #V1 #V2 #i #Hdi #HnU0 #HLK1 #HLK2 @(IH … HLK1 HLK2) -IH // -R -I2 -L2 -K2 -V2
 170   @(cpy_inv_nlift2_be … HU10) /2 width=3 by/
 171
 172 theorem llpx_sn_llpx_sn_alt2: ∀R,L1,L2,T2,d. llpx_sn R d T2 L1 L2 →
 173                               ∀T1. ⦃⋆, L1⦄ ⊢ T1 ▶*[d, ∞] T2 → llpx_sn_alt2 R d T1 L1 L2.
 174 #R #L1 #L2 #U2 #d #H elim (llpx_sn_inv_alt1 … H) -H
 175 #HL12 #IH #U1 #HU12 @conj // -HL12
 176 #I1 #I2 #K1 #K2 #V1 #V2 #i #Hdi #HnU1 #HLK1 #HLK2 elim (frees_inv_gen … HnU1) -HnU1
 177 #U2 #H generalize in match IH; -IH @(cpys_ind_dx … H) -U1
 178 [ #IH #HnU2 elim (IH … HnU2 … HLK1 HLK2) -L1 -L2 -U2 /2 width=1 by conj/
 179 | #U1 #U0 #HU10 #_ #IHU02 #IH #HnU2 @IHU02 /2 width=2 by/ -I1 -I2 -K1 -K2 -V1 -V2 -U2 -i
 180   #I1 #I2 #K1 #K2 #V1 #V2 #i #Hdi #HnU0 #HLK1 #HLK2 @(IH … HLK1 HLK2) -IH // -R -I2 -L2 -K2 -V2
 181   @(cpy_inv_nlift2_be … HU10) /2 width=3 by/
 182
 183
 184 theorem llpx_sn_llpx_sn_alt2: ∀R,L1,L2,T,d. llpx_sn R d T L1 L2 → llpx_sn_alt2 R d T L1 L2.
 185 #R #L1 #L2 #U1 #d #H elim (llpx_sn_inv_alt1 … H) -H
 186 #HL12 #IH @conj // -HL12
 187 #I1 #I2 #K1 #K2 #V1 #V2 #i #Hdi #HnU1 #HLK1 #HLK2 elim (frees_inv_gen … HnU1) -HnU1
 188 #U2 #H generalize in match IH; -IH @(cpys_ind_dx … H) -U1
 189 [ #IH #HnU2 elim (IH … HnU2 … HLK1 HLK2) -L1 -L2 -U2 /2 width=1 by conj/
 190 | #U1 #U0 #HU10 #_ #IHU02 #IH #HnU2 @IHU02 /2 width=2 by/ -I1 -I2 -K1 -K2 -V1 -V2 -U2 -i
 191   #I1 #I2 #K1 #K2 #V1 #V2 #i #Hdi #HnU0 #HLK1 #HLK2 @(IH … HLK1 HLK2) -IH // -R -I2 -L2 -K2 -V2
 192   @(cpy_inv_nlift2_be … HU10) /2 width=3 by/