matita/matita/lib/lambda/terms/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/terms/term.ma".
  16
  17 include "lambda/notation/functions/lift_3.ma".
  18
  19 (* RELOCATION ***************************************************************)
  20
  21 (* Policy: level metavariables : d, e
  22            height metavariables: h, k
  23 *)
  24 (* Note: indexes start at zero *)
  25 let rec lift h d M on M ≝ match M with
  26 [ VRef i   ⇒ #(tri … i d i (i + h) (i + h))
  27 | Abst A   ⇒ 𝛌. (lift h (d+1) A)
  28 | Appl B A ⇒ @(lift h d B). (lift h d A)
  29 ].
  30
  31 interpretation "relocation" 'Lift h d M = (lift h d M).
  32
  33 lemma lift_vref_lt: ∀d,h,i. i < d → ↑[d, h] #i = #i.
  34 normalize /3 width=1/
  35 qed.
  36
  37 lemma lift_vref_ge: ∀d,h,i. d ≤ i → ↑[d, h] #i = #(i+h).
  38 #d #h #i #H elim (le_to_or_lt_eq … H) -H
  39 normalize // /3 width=1/
  40 qed.
  41
  42 lemma lift_id: ∀M,d. ↑[d, 0] M = M.
  43 #M elim M -M
  44 [ #i #d elim (lt_or_ge i d) /2 width=1/
  45 | /3 width=1/
  46 | /3 width=1/
  47 ]
  48 qed.
  49
  50 lemma lift_inv_vref_lt: ∀j,d. j < d → ∀h,M. ↑[d, h] M = #j → M = #j.
  51 #j #d #Hjd #h * normalize
  52 [ #i elim (lt_or_eq_or_gt i d) #Hid
  53   [ >(tri_lt ???? … Hid) -Hid -Hjd //
  54   | #H destruct >tri_eq in Hjd; #H
  55     elim (plus_lt_false … H)
  56   | >(tri_gt ???? … Hid)
  57     lapply (transitive_lt … Hjd Hid) -d #H #H0 destruct
  58     elim (plus_lt_false … H)
  59   ]
  60 | #A #H destruct
  61 | #B #A #H destruct
  62 ]
  63 qed.
  64
  65 lemma lift_inv_vref_ge: ∀j,d. d ≤ j → ∀h,M. ↑[d, h] M = #j →
  66                         d + h ≤ j ∧ M = #(j-h).
  67 #j #d #Hdj #h * normalize
  68 [ #i elim (lt_or_eq_or_gt i d) #Hid
  69   [ >(tri_lt ???? … Hid) #H destruct
  70     lapply (le_to_lt_to_lt … Hdj Hid) -Hdj -Hid #H
  71     elim (lt_refl_false … H)
  72   | #H -Hdj destruct /2 width=1/
  73   | >(tri_gt ???? … Hid) #H -Hdj destruct /4 width=1/
  74   ]
  75 | #A #H destruct
  76 | #B #A #H destruct
  77 ]
  78 qed-.
  79
  80 lemma lift_inv_vref_be: ∀j,d,h. d ≤ j → j < d + h → ∀M. ↑[d, h] M = #j → ⊥.
  81 #j #d #h #Hdj #Hjdh #M #H elim (lift_inv_vref_ge … H) -H // -Hdj #Hdhj #_ -M
  82 lapply (lt_to_le_to_lt … Hjdh Hdhj) -d -h #H
  83 elim (lt_refl_false … H)
  84 qed-.
  85
  86 lemma lift_inv_vref_ge_plus: ∀j,d,h. d + h ≤ j →
  87                              ∀M. ↑[d, h] M = #j → M = #(j-h).
  88 #j #d #h #Hdhj #M #H elim (lift_inv_vref_ge … H) -H // -M /2 width=2/
  89 qed.
  90
  91 lemma lift_inv_abst: ∀C,d,h,M. ↑[d, h] M = 𝛌.C →
  92                      ∃∃A. ↑[d+1, h] A = C & M = 𝛌.A.
  93 #C #d #h * normalize
  94 [ #i #H destruct
  95 | #A #H destruct /2 width=3/
  96 | #B #A #H destruct
  97 ]
  98 qed-.
  99
 100 lemma lift_inv_appl: ∀D,C,d,h,M. ↑[d, h] M = @D.C →
 101                      ∃∃B,A. ↑[d, h] B = D & ↑[d, h] A = C & M = @B.A.
 102 #D #C #d #h * normalize
 103 [ #i #H destruct
 104 | #A #H destruct
 105 | #B #A #H destruct /2 width=5/
 106 ]
 107 qed-.
 108
 109 theorem lift_lift_le: ∀h1,h2,M,d1,d2. d2 ≤ d1 →
 110                       ↑[d2, h2] ↑[d1, h1] M = ↑[d1 + h2, h1] ↑[d2, h2] M.
 111 #h1 #h2 #M elim M -M
 112 [ #i #d1 #d2 #Hd21 elim (lt_or_ge i d2) #Hid2
 113   [ lapply (lt_to_le_to_lt … Hid2 Hd21) -Hd21 #Hid1
 114     >(lift_vref_lt … Hid1) >(lift_vref_lt … Hid2)
 115     >lift_vref_lt // /2 width=1/
 116   | >(lift_vref_ge … Hid2) elim (lt_or_ge i d1) #Hid1
 117     [ >(lift_vref_lt … Hid1) >(lift_vref_ge … Hid2)
 118       >lift_vref_lt // -d2 /2 width=1/
 119     | >(lift_vref_ge … Hid1) >lift_vref_ge /2 width=1/
 120       >lift_vref_ge // /2 width=1/
 121     ]
 122   ]
 123 | normalize #A #IHA #d1 #d2 #Hd21 >IHA // /2 width=1/
 124 | normalize #B #A #IHB #IHA #d1 #d2 #Hd21 >IHB >IHA //
 125 ]
 126 qed.
 127
 128 theorem lift_lift_be: ∀h1,h2,M,d1,d2. d1 ≤ d2 → d2 ≤ d1 + h1 →
 129                       ↑[d2, h2] ↑[d1, h1] M = ↑[d1, h1 + h2] M.
 130 #h1 #h2 #M elim M -M
 131 [ #i #d1 #d2 #Hd12 #Hd21 elim (lt_or_ge i d1) #Hid1
 132   [ lapply (lt_to_le_to_lt … Hid1 Hd12) -Hd12 -Hd21 #Hid2
 133     >(lift_vref_lt … Hid1) >(lift_vref_lt … Hid1) /2 width=1/
 134   | lapply (transitive_le … (i+h1) Hd21 ?) -Hd21 -Hd12 /2 width=1/ #Hd2
 135     >(lift_vref_ge … Hid1) >(lift_vref_ge … Hid1) /2 width=1/
 136   ]
 137 | normalize #A #IHA #d1 #d2 #Hd12 #Hd21 >IHA // /2 width=1/
 138 | normalize #B #A #IHB #IHA #d1 #d2 #Hd12 #Hd21 >IHB >IHA //
 139 ]
 140 qed.
 141
 142 theorem lift_lift_ge: ∀h1,h2,M,d1,d2. d1 + h1 ≤ d2 →
 143                       ↑[d2, h2] ↑[d1, h1] M = ↑[d1, h1] ↑[d2 - h1, h2] M.
 144 #h1 #h2 #M #d1 #d2 #Hd12
 145 >(lift_lift_le h2 h1) /2 width=1/ <plus_minus_m_m // /2 width=2/
 146 qed.
 147
 148 (* Note: this is "∀h,d. injective … (lift h d)" *)
 149 theorem lift_inj: ∀h,M1,M2,d. ↑[d, h] M2 = ↑[d, h] M1 → M2 = M1.
 150 #h #M1 elim M1 -M1
 151 [ #i #M2 #d #H elim (lt_or_ge i d) #Hid
 152   [ >(lift_vref_lt … Hid) in H; #H
 153     >(lift_inv_vref_lt … Hid … H) -M2 -d -h //
 154   | >(lift_vref_ge … Hid) in H; #H
 155     >(lift_inv_vref_ge_plus … H) -M2 // /2 width=1/
 156   ]
 157 | normalize #A1 #IHA1 #M2 #d #H
 158   elim (lift_inv_abst … H) -H #A2 #HA12 #H destruct
 159   >(IHA1 … HA12) -IHA1 -A2 //
 160 | normalize #B1 #A1 #IHB1 #IHA1 #M2 #d #H
 161   elim (lift_inv_appl … H) -H #B2 #A2 #HB12 #HA12 #H destruct
 162   >(IHB1 … HB12) -IHB1 -B2 >(IHA1 … HA12) -IHA1 -A2 //
 163 ]
 164 qed-.
 165
 166 theorem lift_inv_lift_le: ∀h1,h2,M1,M2,d1,d2. d2 ≤ d1 →
 167                           ↑[d2, h2] M2 = ↑[d1 + h2, h1] M1 →
 168                           ∃∃M. ↑[d1, h1] M = M2 & ↑[d2, h2] M = M1.
 169 #h1 #h2 #M1 elim M1 -M1
 170 [ #i #M2 #d1 #d2 #Hd21 elim (lt_or_ge i (d1+h2)) #Hid1
 171   [ >(lift_vref_lt … Hid1) elim (lt_or_ge i d2) #Hid2 #H
 172     [ lapply (lt_to_le_to_lt … Hid2 Hd21) -Hd21 -Hid1 #Hid1
 173       >(lift_inv_vref_lt … Hid2 … H) -M2 /3 width=3/
 174     | elim (lift_inv_vref_ge … H) -H -Hd21 // -Hid2 #Hdh2i #H destruct
 175       elim (le_inv_plus_l … Hdh2i) -Hdh2i #Hd2i #Hh2i
 176       @(ex2_intro … (#(i-h2))) [ /4 width=1/ ] -Hid1
 177       >lift_vref_ge // -Hd2i /3 width=1/ (**) (* auto: needs some help here *)
 178     ]
 179   | elim (le_inv_plus_l … Hid1) #Hd1i #Hh2i
 180     lapply (transitive_le (d2+h2) … Hid1) /2 width=1/ -Hd21 #Hdh2i
 181     elim (le_inv_plus_l … Hdh2i) #Hd2i #_
 182     >(lift_vref_ge … Hid1) #H -Hid1
 183     >(lift_inv_vref_ge_plus … H) -H /2 width=3/ -Hdh2i
 184     @(ex2_intro … (#(i-h2))) (**) (* auto: needs some help here *)
 185     [ >lift_vref_ge // -Hd1i /3 width=1/
 186     | >lift_vref_ge // -Hd2i -Hd1i /3 width=1/
 187     ]
 188   ]
 189 | normalize #A1 #IHA1 #M2 #d1 #d2 #Hd21 #H
 190   elim (lift_inv_abst … H) -H >plus_plus_comm_23 #A2 #HA12 #H destruct
 191   elim (IHA1 … HA12) -IHA1 -HA12 /2 width=1/ -Hd21 #A #HA2 #HA1
 192   @(ex2_intro … (𝛌.A)) normalize //
 193 | normalize #B1 #A1 #IHB1 #IHA1 #M2 #d1 #d2 #Hd21 #H
 194   elim (lift_inv_appl … H) -H #B2 #A2 #HB12 #HA12 #H destruct
 195   elim (IHB1 … HB12) -IHB1 -HB12 // #B #HB2 #HB1
 196   elim (IHA1 … HA12) -IHA1 -HA12 // -Hd21 #A #HA2 #HA1
 197   @(ex2_intro … (@B.A)) normalize //
 198 ]
 199 qed-.
 200
 201 theorem lift_inv_lift_be: ∀h1,h2,M1,M2,d1,d2. d1 ≤ d2 → d2 ≤ d1 + h1 →
 202                           ↑[d2, h2] M2 = ↑[d1, h1 + h2] M1 → ↑[d1, h1] M1 = M2.
 203 #h1 #h2 #M1 elim M1 -M1
 204 [ #i #M2 #d1 #d2 #Hd12 #Hd21 elim (lt_or_ge i d1) #Hid1
 205   [ lapply (lt_to_le_to_lt … Hid1 Hd12) -Hd12 -Hd21 #Hid2
 206     >(lift_vref_lt … Hid1) #H >(lift_inv_vref_lt … Hid2 … H) -h2 -M2 -d2 /2 width=1/
 207   | lapply (transitive_le … (i+h1) Hd21 ?) -Hd12 -Hd21 /2 width=1/ #Hd2
 208     >(lift_vref_ge … Hid1) #H >(lift_inv_vref_ge_plus … H) -M2 /2 width=1/
 209   ]
 210 | normalize #A1 #IHA1 #M2 #d1 #d2 #Hd12 #Hd21 #H
 211   elim (lift_inv_abst … H) -H #A #HA12 #H destruct
 212   >(IHA1 … HA12) -IHA1 -HA12 // /2 width=1/
 213 | normalize #B1 #A1 #IHB1 #IHA1 #M2 #d1 #d2 #Hd12 #Hd21 #H
 214   elim (lift_inv_appl … H) -H #B #A #HB12 #HA12 #H destruct
 215   >(IHB1 … HB12) -IHB1 -HB12 // >(IHA1 … HA12) -IHA1 -HA12 //
 216 ]
 217 qed-.
 218
 219 theorem lift_inv_lift_ge: ∀h1,h2,M1,M2,d1,d2. d1 + h1 ≤ d2 →
 220                           ↑[d2, h2] M2 = ↑[d1, h1] M1 →
 221                           ∃∃M. ↑[d1, h1] M = M2 & ↑[d2 - h1, h2] M = M1.
 222 #h1 #h2 #M1 #M2 #d1 #d2 #Hd12 #H
 223 elim (le_inv_plus_l … Hd12) -Hd12 #Hd12 #Hh1d2
 224 lapply (sym_eq term … H) -H >(plus_minus_m_m … Hh1d2) in ⊢ (???%→?); -Hh1d2 #H
 225 elim (lift_inv_lift_le … Hd12 … H) -H -Hd12 /2 width=3/
 226 qed-.
 227
 228 definition liftable: predicate (relation term) ≝ λR.
 229                      ∀h,M1,M2. R M1 M2 → ∀d. R (↑[d, h] M1) (↑[d, h] M2).
 230
 231 definition deliftable_sn: predicate (relation term) ≝ λR.
 232                           ∀h,N1,N2. R N1 N2 → ∀d,M1. ↑[d, h] M1 = N1 →
 233                           ∃∃M2. R M1 M2 & ↑[d, h] M2 = N2.
 234
 235 lemma star_liftable: ∀R. liftable R → liftable (star … R).
 236 #R #HR #h #M1 #M2 #H elim H -M2 // /3 width=3/
 237 qed.
 238
 239 lemma star_deliftable_sn: ∀R. deliftable_sn R → deliftable_sn (star … R).
 240 #R #HR #h #N1 #N2 #H elim H -N2 /2 width=3/
 241 #N #N2 #_ #HN2 #IHN1 #d #M1 #HMN1
 242 elim (IHN1 … HMN1) -N1 #M #HM1 #HMN
 243 elim (HR … HN2 … HMN) -N /3 width=3/
 244 qed-.
 245
 246 lemma lstar_liftable: ∀S,R. (∀a. liftable (R a)) →
 247                       ∀l. liftable (lstar S … R l).
 248 #S #R #HR #l #h #M1 #M2 #H
 249 @(lstar_ind_l … l M1 H) -l -M1 // /3 width=3/
 250 qed.
 251
 252 lemma lstar_deliftable_sn: ∀S,R. (∀a. deliftable_sn (R a)) →
 253                            ∀l. deliftable_sn (lstar S … R l).
 254 #S #R #HR #l #h #N1 #N2 #H
 255 @(lstar_ind_l … l N1 H) -l -N1 /2 width=3/
 256 #a #l #N1 #N #HN1 #_ #IHN2 #d #M1 #HMN1
 257 elim (HR … HN1 … HMN1) -N1 #M #HM1 #HMN
 258 elim (IHN2 … HMN) -N /3 width=3/
 259 qed-.