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 lemma le_plus_xSy_O_false: ∀x,y. x + S y ≤ 0 → ⊥.
  19 #x #y #H lapply (le_n_O_to_eq … H) -H <plus_n_Sm #H destruct
  20 qed-.
  21
  22 lemma ldrop_fwd_length_ge: ∀L1,L2,d,e,s. ⇩[s, d, e] L1 ≡ L2 → |L1| ≤ d → |L2| = |L1|.
  23 #L1 #L2 #d #e #s #H elim H -L1 -L2 -d -e // normalize
  24 [ #I #L1 #L2 #V #e #_ #_ #H elim (le_plus_xSy_O_false … H)
  25 | /4 width=2 by le_plus_to_le_r, eq_f/
  26 ]
  27 qed-.
  28
  29 lemma ldrop_fwd_length_le_le: ∀L1,L2,d,e,s. ⇩[s, d, e] L1 ≡ L2 → d ≤ |L1| → e ≤ |L1| - d → |L2| = |L1| - e.
  30 #L1 #L2 #d #e #s #H elim H -L1 -L2 -d -e // normalize
  31 [ /3 width=2 by le_plus_to_le_r/
  32 | #I #L1 #L2 #V1 #V2 #d #e #_ #_ #IHL12 >minus_plus_plus_l
  33   #Hd #He lapply (le_plus_to_le_r … Hd) -Hd
  34   #Hd >IHL12 // -L2 >plus_minus /2 width=3 by transitive_le/
  35 ]
  36 qed-.
  37
  38 lemma ldrop_fwd_length_le_ge: ∀L1,L2,d,e,s. ⇩[s, d, e] L1 ≡ L2 → d ≤ |L1| → |L1| - d ≤ e → |L2| = d.
  39 #L1 #L2 #d #e #s #H elim H -L1 -L2 -d -e normalize
  40 [ /2 width=1 by le_n_O_to_eq/
  41 | #I #L #V #_ <minus_n_O #H elim (le_plus_xSy_O_false … H)
  42 | /3 width=2 by le_plus_to_le_r/
  43 | /4 width=2 by le_plus_to_le_r, eq_f/
  44 ]
  45 qed-.
  46
  47 lemma ldrop_O1_le: ∀s,e,L. e ≤ |L| → ∃K. ⇩[s, 0, e] L ≡ K.
  48 #s #e @(nat_ind_plus … e) -e /2 width=2 by ex_intro/
  49 #e #IHe *
  50 [ #H elim (le_plus_xSy_O_false … H)
  51 | #L #I #V normalize #H elim (IHe L) -IHe /3 width=2 by ldrop_drop, monotonic_pred, ex_intro/
  52 ]
  53 qed-.
  54
  55 lemma ldrop_O1_lt: ∀s,L,e. e < |L| → ∃∃I,K,V. ⇩[s, 0, e] L ≡ K.ⓑ{I}V.
  56 #s #L elim L -L
  57 [ #e #H elim (lt_zero_false … H)
  58 | #L #I #V #IHL #e @(nat_ind_plus … e) -e /2 width=4 by ldrop_pair, ex1_3_intro/
  59   #e #_ normalize #H elim (IHL e) -IHL /3 width=4 by ldrop_drop, lt_plus_to_minus_r, lt_plus_to_lt_l, ex1_3_intro/
  60 ]
  61 qed-.
  62
  63 lemma ldrop_O1_pair: ∀L,K,e,s. ⇩[s, 0, e] L ≡ K → e ≤ |L| → ∀I,V.
  64                      ∃∃J,W. ⇩[s, 0, e] L.ⓑ{I}V ≡ K.ⓑ{J}W.
  65 #L elim L -L [| #L #Z #X #IHL ] #K #e #s #H normalize #He #I #V
  66 [ elim (ldrop_inv_atom1 … H) -H #H <(le_n_O_to_eq … He) -e
  67   #Hs destruct /2 width=3 by ex1_2_intro/
  68 | elim (ldrop_inv_O1_pair1 … H) -H * #He #HLK destruct /2 width=3 by ex1_2_intro/
  69   elim (IHL … HLK … Z X) -IHL -HLK
  70   /3 width=3 by ldrop_drop_lt, le_plus_to_minus, ex1_2_intro/
  71 ]
  72 qed-.
  73
  74 lemma ldrop_inv_O1_gt: ∀L,K,e,s. ⇩[s, 0, e] L ≡ K → |L| < e →
  75                        s = Ⓣ ∧ K = ⋆.
  76 #L elim L -L [| #L #Z #X #IHL ] #K #e #s #H normalize in ⊢ (?%?→?); #H1e
  77 [ elim (ldrop_inv_atom1 … H) -H elim s -s /2 width=1 by conj/
  78   #_ #Hs lapply (Hs ?) // -Hs #H destruct elim (lt_zero_false … H1e)
  79 | elim (ldrop_inv_O1_pair1 … H) -H * #H2e #HLK destruct
  80   [ elim (lt_zero_false … H1e)
  81   | elim (IHL … HLK) -IHL -HLK /2 width=1 by lt_plus_to_minus_r, conj/
  82   ]
  83 ]
  84 qed-.
  85
  86 lemma ldrop_O1_ge: ∀L,e. |L| ≤ e → ⇩[Ⓣ, 0, e] L ≡ ⋆.
  87 #L elim L -L [ #e #_ @ldrop_atom #H destruct ]
  88 #L #I #V #IHL #e @(nat_ind_plus … e) -e [ #H elim (le_plus_xSy_O_false … H) ]
  89 normalize /4 width=1 by ldrop_drop, monotonic_pred/
  90 qed.
  91
  92 lemma ldrop_split: ∀L1,L2,d,e2,s. ⇩[s, d, e2] L1 ≡ L2 → ∀e1. e1 ≤ e2 →
  93                    ∃∃L. ⇩[s, d, e2 - e1] L1 ≡ L & ⇩[s, d, e1] L ≡ L2.
  94 #L1 #L2 #d #e2 #s #H elim H -L1 -L2 -d -e2
  95 [ #d #e2 #Hs #e1 #He12 @(ex2_intro … (⋆))
  96   @ldrop_atom #H lapply (Hs H) -s #H destruct /2 width=1 by le_n_O_to_eq/
  97 | #I #L1 #V #e1 #He1 lapply (le_n_O_to_eq … He1) -He1
  98   #H destruct /2 width=3 by ex2_intro/
  99 | #I #L1 #L2 #V #e2 #HL12 #IHL12 #e1 @(nat_ind_plus … e1) -e1
 100   [ /3 width=3 by ldrop_drop, ex2_intro/
 101   | -HL12 #e1 #_ #He12 lapply (le_plus_to_le_r … He12) -He12
 102     #He12 elim (IHL12 … He12) -IHL12 >minus_plus_plus_l
 103     #L #HL1 #HL2 elim (lt_or_ge (|L1|) (e2-e1)) #H0
 104     [ elim (ldrop_inv_O1_gt … HL1 H0) -HL1 #H1 #H2 destruct
 105       elim (ldrop_inv_atom1 … HL2) -HL2 #H #_ destruct
 106       @(ex2_intro … (⋆)) [ @ldrop_O1_ge normalize // ]
 107       @ldrop_atom #H destruct
 108     | elim (ldrop_O1_pair … HL1 H0 I V) -HL1 -H0 /3 width=5 by ldrop_drop, ex2_intro/
 109     ]
 110   ]
 111 | #I #L1 #L2 #V1 #V2 #d #e2 #_ #HV21 #IHL12 #e1 #He12 elim (IHL12 … He12) -IHL12
 112   #L #HL1 #HL2 elim (lift_split … HV21 d e1) -HV21 /3 width=5 by ldrop_skip, ex2_intro/
 113 ]
 114 qed-.
 115
 116 (* LAZY SN POINTWISE EXTENSION OF A CONTEXT-SENSITIVE REALTION FOR TERMS ****)
 117
 118 (* alternative definition of llpx_sn (not recursive) *)
 119 definition llpx_sn_alt2: relation4 bind2 lenv term term → relation4 ynat term lenv lenv ≝
 120                          λR,d,T,L1,L2. |L1| = |L2| ∧
 121                          (∀I1,I2,K1,K2,V1,V2,i. d ≤ yinj i → (L1 ⊢ i ~ϵ 𝐅*[d]⦃T⦄ → ⊥) →
 122                             ⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L2 ≡ K2.ⓑ{I2}V2 →
 123                             I1 = I2 ∧ R I1 K1 V1 V2
 124                          ).
 125
 126 (* Main properties **********************************************************)
 127
 128 lemma cpy_inv_nlift2_be: ∀G,L,U1,U2,d. ⦃G, L⦄ ⊢ U1 ▶[d, ∞] U2 → ∀i. d ≤ yinj i →
 129                          ∀K,s. ⇩[s, i, 1] L ≡ K →
 130                          (∀T2. ⇧[i, 1] T2 ≡ U2 → ⊥) → (∀T1. ⇧[i, 1] T1 ≡ U1 → ⊥).
 131 #G #L #U1 #U2 #d #HU12 #i #Hdi #K #s #HLK #HnU2 #T1 #HTU1
 132 elim (cpy_inv_lift1_be … HU12 … HLK … HTU1) /2 width=2 by/
 133 qed-.
 134
 135 lemma cpy_inv_nlift2_ge: ∀G,L,U1,U2,d,e. ⦃G, L⦄ ⊢ U1 ▶[d, e] U2 →
 136                          ∀i. d ≤ yinj i → (* yinj i + yinj 1 ≤ d + e → *)
 137                          (∀T2. ⇧[i, 1] T2 ≡ U2 → ⊥) →
 138                          ∃∃j. d ≤ yinj j & j ≤ i & (∀T1. ⇧[j, 1] T1 ≡ U1 → ⊥).
 139 #G #L #U1 #U2 #d #e #H elim H -G -L -U1 -U2 -d -e
 140 [ #I #G #L #d #e #i #Hdi (* #Hide *) #H @(ex3_intro … i) /2 width=2 by/
 141 | #I #G #L #K #V #W #j #d #e #Hdj #Hjde #HLK #HVW #i #Hdi (* #Hide *) #HnW
 142   elim (le_or_ge i j) #Hij [2: @(ex3_intro … j) /2 width=7 by lift_inv_lref2_be/ ]
 143   elim (lift_split … HVW i j) -HVW //
 144   #X #_ #H elim HnW -HnW //
 145 | #a #I #G #L #W1 #W2 #U1 #U2 #d #e #_ #_ #IHW12 #IHU12 #i #Hdi #H elim (nlift_inv_bind … H) -H
 146   [ #HnW2 elim (IHW12 … HnW2) -IHW12 -HnW2 -IHU12 //
 147     #j #Hdj #Hji #HnW1 @(ex3_intro … j) /3 width=9 by nlift_bind_sn/
 148   | #HnU2 elim (IHU12 … HnU2) -IHU12 -HnU2 -IHW12 /2 width=1 by yle_succ/
 149     #j #Hdj #Hji
 150     >(plus_minus_m_m j 1) in ⊢ (%→?); [2: /3 width=3 by yle_trans, yle_inv_inj/ ]
 151     #HnW1 @(ex3_intro … (j-1)) /3 width=9 by nlift_bind_dx, yle_pred, monotonic_pred/
 152   ]
 153 | #I #G #L #W1 #W2 #U1 #U2 #d #e #_ #_ #IHW12 #IHU12 #i #Hdi #H elim (nlift_inv_flat … H) -H
 154   [ #HnW2 elim (IHW12 … HnW2) -IHW12 -HnW2 -IHU12 //
 155     #j #Hdj #Hji #HnW1 @(ex3_intro … j) /3 width=8 by nlift_flat_sn/
 156   | #HnU2 elim (IHU12 … HnU2) -IHU12 -HnU2 -IHW12 //
 157     #j #Hdj #Hji #HnW1 @(ex3_intro … j) /3 width=8 by nlift_flat_dx/
 158   ]
 159 ]
 160 qed-.
 161
 162 axiom frees_fwd_nlift_ge: ∀L,U,d,i. (L ⊢ i ~ϵ 𝐅*[d]⦃U⦄ → ⊥) → d ≤ yinj i →
 163                           ∃∃j. d ≤ yinj j & j ≤ i & (∀T. ⇧[j, 1] T ≡ U → ⊥).
 164
 165 (*
 166 lemma frees_ind_nlift: ∀L,d. ∀R:relation2 term nat.
 167                        (∀U1,i. d ≤ yinj i → (∀T1. ⇧[i, 1] T1 ≡ U1 → ⊥) → R U1 i) →
 168                        (∀U1,U2,i,j. d ≤ yinj j → j ≤ i → ⦃⋆, L⦄ ⊢ U1 ▶[d, ∞] U2 → (∀T2. ⇧[i, 1] T2 ≡ U2 → ⊥) → R U2 i → R U1 j) →
 169                        ∀U,i. d ≤ yinj i → (L ⊢ i ~ϵ 𝐅*[d]⦃U⦄ → ⊥) → R U i.
 170 #L #d #R #IH1 #IH2 #U1 #i #Hdi #H @(frees_ind … H) -U1 /3 width=4 by/
 171 #U1 #U2 #HU12 #HnU2 #HU2 @(IH2 … HU12 … HU2)
 172
 173 qed-.
 174 *)(*
 175 lemma frees_fwd_nlift: ∀L,d. ∀R:relation2 term nat. (
 176                           ∀U1,j. (∀T1. ⇧[j, 1] T1 ≡ U1 → ⊥) ∨
 177                                  (∃∃U2,i. d ≤ yinj j → j < i & (L ⊢ j ~ϵ 𝐅*[d]⦃U1⦄ → ⊥) & ⦃⋆, L⦄ ⊢ U1 ▶[d, ∞] U2 & R U1 i
 178                                  ) →
 179                           d ≤ yinj j → R U1 j
 180                        ) →
 181                        ∀U,i. d ≤ yinj i → (L ⊢ i ~ϵ 𝐅*[d]⦃U⦄ → ⊥) → R U i.
 182 #L #d #R #IHR #U1 #j #Hdj #H elim (frees_inv_gen … H) -H
 183 #U2 #H generalize in match Hdj; -Hdj generalize in match j; -j @(cpys_ind … H) -U2
 184 [ #j #Hdj #HnU1 @IHR -IHR /3 width=2 by or_introl/
 185 | #U0 #U2 #HU10 #HU02 #IHU10 #j #Hdj #HnU2 elim (cpy_inv_nlift2_ge … HU02 … Hdj HnU2) -HU02 -HnU2
 186   #i #Hdi #Hij #HnU0 lapply (IHU10 … HnU0) // -IHU10
 187   #Hi @IHR -IHR // -Hdj @or_intror
 188
 189 lemma frees_fwd_nlift: ∀L,U,d,i. d ≤ yinj i → (L ⊢ i ~ϵ 𝐅*[d]⦃U⦄ → ⊥) →
 190                        ∃∃j. d ≤ yinj j & j ≤ i & (∀T. ⇧[j, 1] T ≡ U → ⊥).
 191 #L #U1 #d #i #Hdi  #H
 192 #U2 #H #HnU2 @(cpys_ind_dx … H) -U1 [ @(ex3_intro … i) /2 width=2 by/ ] -Hdi -HnU2
 193 #U1 #U0 #HU10 #_ * #j #Hdj #Hji #HnU0 elim (cpy_inv_nlift2_ge … HU10 … Hdj HnU0) -U0 -Hdj
 194 /3 width=5 by transitive_le, ex3_intro/
 195 qed-.
 196 *)
 197
 198 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.
 199 #R #L1 #L2 #U1 #d #H elim (llpx_sn_inv_alt1 … H) -H
 200 #HL12 #IH @conj // -HL12
 201 #I1 #I2 #K1 #K2 #V1 #V2 #i #Hdi #H #HLK1 #HLK2
 202 elim (frees_fwd_nlift_ge … H Hdi) -H -Hdi #j #Hdj #Hji #HnU1
 203 lapply (ldrop_fwd_length_lt2 … HLK1) #HL1
 204 lapply (ldrop_fwd_length_lt2 … HLK2) #HL2
 205 lapply (le_to_lt_to_lt … Hji HL1) -HL1 #HL1
 206 lapply (le_to_lt_to_lt … Hji HL2) -HL2 #HL2
 207 elim (ldrop_O1_lt L1 j) // #Z1 #Y1 #X1 #HLY1
 208 elim (ldrop_O1_lt L2 j) // #Z2 #Y2 #X2 #HLY2
 209
 210
 211
 212
 213 generalize in match V2; -V2 generalize in match V1; -V1
 214 generalize in match K2; -K2 generalize in match K1; -K1
 215 generalize in match I2; -I2 generalize in match I1; -I1
 216 generalize in match IH; -IH
 217 @(frees_ind_nlift … Hdi H) -U1 -i
 218 [ #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/
 219 | #U1 #U2 #i #j #Hdj #Hji #HU12 #HnU2 #IHU12 #IH #I1 #I2 #K1 #K2 #V1 #V2 #HLK1 #HLK2
 220 (*
 221 *)
 222   @(IHU12) … HLK1 HLK2)
 223
 224   @(IHU12 … HLK1 HLK2) -IHU02 -I1 -I2 -K1 -K2 -V1 -V2
 225   #I1 #I2 #K1 #K2 #V1 #V2 #j #Hdj #HnU0 #HLK1 #HLK2 @(IH … HLK1 HLK2) -IH -HLK1 -HLK2 //
 226
 227
 228
 229  elim (frees_fwd_nlift … HnU1) // -HnU1 -Hdi
 230 #j #Hdj #Hji #HnU1
 231 lapply (ldrop_fwd_length_lt2 … HLK1) #HL1
 232 lapply (ldrop_fwd_length_lt2 … HLK2) #HL2
 233 lapply (le_to_lt_to_lt … Hji HL1) -HL1 #HL1
 234 lapply (le_to_lt_to_lt … Hji HL2) -HL2 #HL2
 235 elim (ldrop_O1_lt L1 j) // #Z1 #Y1 #X1 #HLY1
 236 elim (ldrop_O1_lt L2 j) // #Z2 #Y2 #X2 #HLY2
 237 elim (IH … HnU1 HLY1 HLY2) // #H #HX12 #HY12 destruct
 238
 239
 240
 241
 242
 243
 244
 245
 246
 247
 248
 249
 250
 251
 252
 253
 254
 255
 256
 257
 258
 259
 260 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.
 261 #R #L1 #L2 #U1 #d #H @(llpx_sn_ind_alt1 … H) -L1 -L2 -U1 -d
 262 #L1 #L2 #U1 #d #HL12 #IH @conj // -HL12
 263 #I1 #I2 #K1 #K2 #V1 #V2 #i #Hdi #HnU1 #HLK1 #HLK2 elim (frees_inv_gen … HnU1) -HnU1
 264 #U2 #H generalize in match IH; -IH @(cpys_ind_dx … H) -U1
 265 [ #IH #HnU2 elim (IH … HnU2 … HLK1 HLK2) -L1 -L2 -U2 /2 width=1 by conj/
 266 | #U1 #U0 #HU10 #_ #IHU02 #IH #HnU2 @IHU02 /2 width=2 by/ -I1 -I2 -K1 -K2 -V1 -V2 -U2 -i
 267   #I1 #I2 #K1 #K2 #V1 #V2 #i #Hdi #HnU0 #HLK1 #HLK2 @(IH … HLK1 HLK2) -IH // -R -I2 -L2 -K2 -V2
 268   @(cpy_inv_nlift2_be … HU10) /2 width=3 by/
 269
 270 theorem llpx_sn_llpx_sn_alt2: ∀R,L1,L2,T2,d. llpx_sn R d T2 L1 L2 →
 271                               ∀T1. ⦃⋆, L1⦄ ⊢ T1 ▶*[d, ∞] T2 → llpx_sn_alt2 R d T1 L1 L2.
 272 #R #L1 #L2 #U2 #d #H elim (llpx_sn_inv_alt1 … H) -H
 273 #HL12 #IH #U1 #HU12 @conj // -HL12
 274 #I1 #I2 #K1 #K2 #V1 #V2 #i #Hdi #HnU1 #HLK1 #HLK2 elim (frees_inv_gen … HnU1) -HnU1
 275 #U2 #H generalize in match IH; -IH @(cpys_ind_dx … H) -U1
 276 [ #IH #HnU2 elim (IH … HnU2 … HLK1 HLK2) -L1 -L2 -U2 /2 width=1 by conj/
 277 | #U1 #U0 #HU10 #_ #IHU02 #IH #HnU2 @IHU02 /2 width=2 by/ -I1 -I2 -K1 -K2 -V1 -V2 -U2 -i
 278   #I1 #I2 #K1 #K2 #V1 #V2 #i #Hdi #HnU0 #HLK1 #HLK2 @(IH … HLK1 HLK2) -IH // -R -I2 -L2 -K2 -V2
 279   @(cpy_inv_nlift2_be … HU10) /2 width=3 by/
 280
 281
 282 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.
 283 #R #L1 #L2 #U1 #d #H elim (llpx_sn_inv_alt1 … H) -H
 284 #HL12 #IH @conj // -HL12
 285 #I1 #I2 #K1 #K2 #V1 #V2 #i #Hdi #HnU1 #HLK1 #HLK2 elim (frees_inv_gen … HnU1) -HnU1
 286 #U2 #H generalize in match IH; -IH @(cpys_ind_dx … H) -U1
 287 [ #IH #HnU2 elim (IH … HnU2 … HLK1 HLK2) -L1 -L2 -U2 /2 width=1 by conj/
 288 | #U1 #U0 #HU10 #_ #IHU02 #IH #HnU2 @IHU02 /2 width=2 by/ -I1 -I2 -K1 -K2 -V1 -V2 -U2 -i
 289   #I1 #I2 #K1 #K2 #V1 #V2 #i #Hdi #HnU0 #HLK1 #HLK2 @(IH … HLK1 HLK2) -IH // -R -I2 -L2 -K2 -V2
 290   @(cpy_inv_nlift2_be … HU10) /2 width=3 by/