matita/matita/contribs/lambda/subterms/lift.ma

   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 "subterms/subterms.ma".
  16
  17 (* RELOCATION FOR SUBTERMS **************************************************)
  18
  19 let rec slift h d E on E ≝ match E with
  20 [ SVRef b i   ⇒ {b}#(tri … i d i (i + h) (i + h))
  21 | SAbst b T   ⇒ {b}𝛌.(slift h (d+1) T)
  22 | SAppl b V T ⇒ {b}@(slift h d V).(slift h d T)
  23 ].
  24
  25 interpretation "relocation for subterms" 'Lift h d E = (slift h d E).
  26
  27 lemma slift_vref_lt: ∀b,d,h,i. i < d → ↑[d, h] {b}#i = {b}#i.
  28 normalize /3 width=1/
  29 qed.
  30
  31 lemma slift_vref_ge: ∀b,d,h,i. d ≤ i → ↑[d, h] {b}#i = {b}#(i+h).
  32 #b #d #h #i #H elim (le_to_or_lt_eq … H) -H
  33 normalize // /3 width=1/
  34 qed.
  35
  36 lemma slift_id: ∀E,d. ↑[d, 0] E = E.
  37 #E elim E -E
  38 [ #b #i #d elim (lt_or_ge i d) /2 width=1/
  39 | /3 width=1/
  40 | /3 width=1/
  41 ]
  42 qed.
  43
  44 lemma slift_inv_vref_lt: ∀b0,j,d. j < d → ∀h,E. ↑[d, h] E = {b0}#j → E = {b0}#j.
  45 #b0 #j #d #Hjd #h * normalize
  46 [ #b #i elim (lt_or_eq_or_gt i d) #Hid
  47   [ >(tri_lt ???? … Hid) -Hid -Hjd //
  48   | #H destruct >tri_eq in Hjd; #H
  49     elim (plus_lt_false … H)
  50   | >(tri_gt ???? … Hid)
  51     lapply (transitive_lt … Hjd Hid) -d #H #H0 destruct
  52     elim (plus_lt_false … H)
  53   ]
  54 | #b #T #H destruct
  55 | #b #V #T #H destruct
  56 ]
  57 qed.
  58
  59 lemma slift_inv_vref_ge: ∀b0,j,d. d ≤ j → ∀h,E. ↑[d, h] E = {b0}#j →
  60                          d + h ≤ j ∧ E = {b0}#(j-h).
  61 #b0 #j #d #Hdj #h * normalize
  62 [ #b #i elim (lt_or_eq_or_gt i d) #Hid
  63   [ >(tri_lt ???? … Hid) #H destruct
  64     lapply (le_to_lt_to_lt … Hdj Hid) -Hdj -Hid #H
  65     elim (lt_refl_false … H)
  66   | #H -Hdj destruct /2 width=1/
  67   | >(tri_gt ???? … Hid) #H -Hdj destruct /4 width=1/
  68   ]
  69 | #b #T #H destruct
  70 | #b #V #T #H destruct
  71 ]
  72 qed-.
  73
  74 lemma slift_inv_vref_be: ∀b0,j,d,h. d ≤ j → j < d + h → ∀E. ↑[d, h] E = {b0}#j → ⊥.
  75 #b0 #j #d #h #Hdj #Hjdh #E #H elim (slift_inv_vref_ge … H) -H // -Hdj #Hdhj #_ -E
  76 lapply (lt_to_le_to_lt … Hjdh Hdhj) -d -h #H
  77 elim (lt_refl_false … H)
  78 qed-.
  79
  80 lemma slift_inv_vref_ge_plus: ∀b0,j,d,h. d + h ≤ j →
  81                               ∀E. ↑[d, h] E = {b0}#j → E = {b0}#(j-h).
  82 #b0 #j #d #h #Hdhj #E #H elim (slift_inv_vref_ge … H) -H // -E /2 width=2/
  83 qed.
  84
  85 lemma slift_inv_abst: ∀b0,U,d,h,E. ↑[d, h] E = {b0}𝛌.U →
  86                       ∃∃T. ↑[d+1, h] T = U & E = {b0}𝛌.T.
  87 #b0 #U #d #h * normalize
  88 [ #b #i #H destruct
  89 | #b #T #H destruct /2 width=3/
  90 | #b #V #T #H destruct
  91 ]
  92 qed-.
  93
  94 lemma slift_inv_appl: ∀b0,W,U,d,h,E. ↑[d, h] E = {b0}@W.U →
  95                       ∃∃V,T. ↑[d, h] V = W & ↑[d, h] T = U & E = {b0}@V.T.
  96 #b0 #W #U #d #h * normalize
  97 [ #b #i #H destruct
  98 | #b #T #H destruct
  99 | #b #V #T #H destruct /2 width=5/
 100 ]
 101 qed-.
 102
 103 theorem slift_slift_le: ∀h1,h2,E,d1,d2. d2 ≤ d1 →
 104                         ↑[d2, h2] ↑[d1, h1] E = ↑[d1 + h2, h1] ↑[d2, h2] E.
 105 #h1 #h2 #E elim E -E
 106 [ #b #i #d1 #d2 #Hd21 elim (lt_or_ge i d2) #Hid2
 107   [ lapply (lt_to_le_to_lt … Hid2 Hd21) -Hd21 #Hid1
 108     >(slift_vref_lt … Hid1) >(slift_vref_lt … Hid2)
 109     >slift_vref_lt // /2 width=1/
 110   | >(slift_vref_ge … Hid2) elim (lt_or_ge i d1) #Hid1
 111     [ >(slift_vref_lt … Hid1) >(slift_vref_ge … Hid2)
 112       >slift_vref_lt // -d2 /2 width=1/
 113     | >(slift_vref_ge … Hid1) >slift_vref_ge /2 width=1/
 114       >slift_vref_ge // /2 width=1/
 115     ]
 116   ]
 117 | normalize #b #T #IHT #d1 #d2 #Hd21 >IHT // /2 width=1/
 118 | normalize #b #V #T #IHV #IHT #d1 #d2 #Hd21 >IHV >IHT //
 119 ]
 120 qed.
 121
 122 theorem slift_slift_be: ∀h1,h2,E,d1,d2. d1 ≤ d2 → d2 ≤ d1 + h1 →
 123                         ↑[d2, h2] ↑[d1, h1] E = ↑[d1, h1 + h2] E.
 124 #h1 #h2 #E elim E -E
 125 [ #b #i #d1 #d2 #Hd12 #Hd21 elim (lt_or_ge i d1) #Hid1
 126   [ lapply (lt_to_le_to_lt … Hid1 Hd12) -Hd12 -Hd21 #Hid2
 127     >(slift_vref_lt … Hid1) >(slift_vref_lt … Hid1) /2 width=1/
 128   | lapply (transitive_le … (i+h1) Hd21 ?) -Hd21 -Hd12 /2 width=1/ #Hd2
 129     >(slift_vref_ge … Hid1) >(slift_vref_ge … Hid1) /2 width=1/
 130   ]
 131 | normalize #b #T #IHT #d1 #d2 #Hd12 #Hd21 >IHT // /2 width=1/
 132 | normalize #b #V #T #IHV #IHT #d1 #d2 #Hd12 #Hd21 >IHV >IHT //
 133 ]
 134 qed.
 135
 136 theorem slift_slift_ge: ∀h1,h2,E,d1,d2. d1 + h1 ≤ d2 →
 137                         ↑[d2, h2] ↑[d1, h1] E = ↑[d1, h1] ↑[d2 - h1, h2] E.
 138 #h1 #h2 #E #d1 #d2 #Hd12
 139 >(slift_slift_le h2 h1) /2 width=1/ <plus_minus_m_m // /2 width=2/
 140 qed.
 141
 142 (* Note: this is "∀h,d. injective … (slift h d)" *)
 143 theorem slift_inj: ∀h,E1,E2,d. ↑[d, h] E2 = ↑[d, h] E1 → E2 = E1.
 144 #h #E1 elim E1 -E1
 145 [ #b #i #E2 #d #H elim (lt_or_ge i d) #Hid
 146   [ >(slift_vref_lt … Hid) in H; #H
 147     >(slift_inv_vref_lt … Hid … H) -E2 -d -h //
 148   | >(slift_vref_ge … Hid) in H; #H
 149     >(slift_inv_vref_ge_plus … H) -E2 // /2 width=1/
 150   ]
 151 | normalize #b #T1 #IHT1 #E2 #d #H
 152   elim (slift_inv_abst … H) -H #T2 #HT12 #H destruct
 153   >(IHT1 … HT12) -IHT1 -T2 //
 154 | normalize #b #V1 #T1 #IHV1 #IHT1 #E2 #d #H
 155   elim (slift_inv_appl … H) -H #V2 #T2 #HV12 #HT12 #H destruct
 156   >(IHV1 … HV12) -IHV1 -V2 >(IHT1 … HT12) -IHT1 -T2 //
 157 ]
 158 qed-.
 159
 160 theorem slift_inv_slift_le: ∀h1,h2,E1,E2,d1,d2. d2 ≤ d1 →
 161                             ↑[d2, h2] E2 = ↑[d1 + h2, h1] E1 →
 162                             ∃∃E. ↑[d1, h1] E = E2 & ↑[d2, h2] E = E1.
 163 #h1 #h2 #E1 elim E1 -E1
 164 [ #b #i #E2 #d1 #d2 #Hd21 elim (lt_or_ge i (d1+h2)) #Hid1
 165   [ >(slift_vref_lt … Hid1) elim (lt_or_ge i d2) #Hid2 #H
 166     [ lapply (lt_to_le_to_lt … Hid2 Hd21) -Hd21 -Hid1 #Hid1
 167       >(slift_inv_vref_lt … Hid2 … H) -E2 /3 width=3/
 168     | elim (slift_inv_vref_ge … H) -H -Hd21 // -Hid2 #Hdh2i #H destruct
 169       elim (le_inv_plus_l … Hdh2i) -Hdh2i #Hd2i #Hh2i
 170       @(ex2_intro … ({b}#(i-h2))) [ /4 width=1/ ] -Hid1
 171       >slift_vref_ge // -Hd2i /3 width=1/ (**) (* auto: needs some help here *)
 172     ]
 173   | elim (le_inv_plus_l … Hid1) #Hd1i #Hh2i
 174     lapply (transitive_le (d2+h2) … Hid1) /2 width=1/ -Hd21 #Hdh2i
 175     elim (le_inv_plus_l … Hdh2i) #Hd2i #_
 176     >(slift_vref_ge … Hid1) #H -Hid1
 177     >(slift_inv_vref_ge_plus … H) -H /2 width=3/ -Hdh2i
 178     @(ex2_intro … ({b}#(i-h2))) (**) (* auto: needs some help here *)
 179     [ >slift_vref_ge // -Hd1i /3 width=1/
 180     | >slift_vref_ge // -Hd2i -Hd1i /3 width=1/
 181     ]
 182   ]
 183 | normalize #b #T1 #IHT1 #E2 #d1 #d2 #Hd21 #H
 184   elim (slift_inv_abst … H) -H >plus_plus_comm_23 #T2 #HT12 #H destruct
 185   elim (IHT1 … HT12) -IHT1 -HT12 /2 width=1/ -Hd21 #T #HT2 #HT1
 186   @(ex2_intro … ({b}𝛌.T)) normalize //
 187 | normalize #b #V1 #T1 #IHV1 #IHT1 #E2 #d1 #d2 #Hd21 #H
 188   elim (slift_inv_appl … H) -H #V2 #T2 #HV12 #HT12 #H destruct
 189   elim (IHV1 … HV12) -IHV1 -HV12 // #V #HV2 #HV1
 190   elim (IHT1 … HT12) -IHT1 -HT12 // -Hd21 #T #HT2 #HT1
 191   @(ex2_intro … ({b}@V.T)) normalize //
 192 ]
 193 qed-.
 194
 195 theorem slift_inv_slift_be: ∀h1,h2,E1,E2,d1,d2. d1 ≤ d2 → d2 ≤ d1 + h1 →
 196                             ↑[d2, h2] E2 = ↑[d1, h1 + h2] E1 → ↑[d1, h1] E1 = E2.
 197 #h1 #h2 #E1 elim E1 -E1
 198 [ #b #i #E2 #d1 #d2 #Hd12 #Hd21 elim (lt_or_ge i d1) #Hid1
 199   [ lapply (lt_to_le_to_lt … Hid1 Hd12) -Hd12 -Hd21 #Hid2
 200     >(slift_vref_lt … Hid1) #H >(slift_inv_vref_lt … Hid2 … H) -h2 -E2 -d2 /2 width=1/
 201   | lapply (transitive_le … (i+h1) Hd21 ?) -Hd12 -Hd21 /2 width=1/ #Hd2
 202     >(slift_vref_ge … Hid1) #H >(slift_inv_vref_ge_plus … H) -E2 /2 width=1/
 203   ]
 204 | normalize #b #T1 #IHT1 #E2 #d1 #d2 #Hd12 #Hd21 #H
 205   elim (slift_inv_abst … H) -H #T #HT12 #H destruct
 206   >(IHT1 … HT12) -IHT1 -HT12 // /2 width=1/
 207 | normalize #b #V1 #T1 #IHV1 #IHT1 #E2 #d1 #d2 #Hd12 #Hd21 #H
 208   elim (slift_inv_appl … H) -H #V #T #HV12 #HT12 #H destruct
 209   >(IHV1 … HV12) -IHV1 -HV12 // >(IHT1 … HT12) -IHT1 -HT12 //
 210 ]
 211 qed-.
 212
 213 theorem slift_inv_slift_ge: ∀h1,h2,E1,E2,d1,d2. d1 + h1 ≤ d2 →
 214                             ↑[d2, h2] E2 = ↑[d1, h1] E1 →
 215                             ∃∃E. ↑[d1, h1] E = E2 & ↑[d2 - h1, h2] E = E1.
 216 #h1 #h2 #E1 #E2 #d1 #d2 #Hd12 #H
 217 elim (le_inv_plus_l … Hd12) -Hd12 #Hd12 #Hh1d2
 218 lapply (sym_eq subterms … H) -H >(plus_minus_m_m … Hh1d2) in ⊢ (???%→?); -Hh1d2 #H
 219 elim (slift_inv_slift_le … Hd12 … H) -H -Hd12 /2 width=3/
 220 qed-.
 221 (*
 222 definition liftable: predicate (relation term) ≝ λR.
 223                      ∀h,M1,M2. R M1 M2 → ∀d. R (↑[d, h] M1) (↑[d, h] M2).
 224
 225 definition deliftable_sn: predicate (relation term) ≝ λR.
 226                           ∀h,N1,N2. R N1 N2 → ∀d,M1. ↑[d, h] M1 = N1 →
 227                           ∃∃M2. R M1 M2 & ↑[d, h] M2 = N2.
 228
 229 lemma star_liftable: ∀R. liftable R → liftable (star … R).
 230 #R #HR #h #M1 #M2 #H elim H -M2 // /3 width=3/
 231 qed.
 232
 233 lemma star_deliftable_sn: ∀R. deliftable_sn R → deliftable_sn (star … R).
 234 #R #HR #h #N1 #N2 #H elim H -N2 /2 width=3/
 235 #N #N2 #_ #HN2 #IHN1 #d #M1 #HMN1
 236 elim (IHN1 … HMN1) -N1 #M #HM1 #HMN
 237 elim (HR … HN2 … HMN) -N /3 width=3/
 238 qed-.
 239
 240 lemma lstar_liftable: ∀S,R. (∀a. liftable (R a)) →
 241                       ∀l. liftable (lstar S … R l).
 242 #S #R #HR #l #h #M1 #M2 #H
 243 @(lstar_ind_l ????????? H) -l -M1 // /3 width=3/
 244 qed.
 245
 246 lemma lstar_deliftable_sn: ∀S,R. (∀a. deliftable_sn (R a)) →
 247                            ∀l. deliftable_sn (lstar S … R l).
 248 #S #R #HR #l #h #N1 #N2 #H
 249 @(lstar_ind_l ????????? H) -l -N1 /2 width=3/
 250 #a #l #N1 #N #HN1 #_ #IHN2 #d #M1 #HMN1
 251 elim (HR … HN1 … HMN1) -N1 #M #HM1 #HMN
 252 elim (IHN2 … HMN) -N /3 width=3/
 253 qed-.
 254 *)