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