matita/matita/lib/lambda/terms/relocating_substitution.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/relocation.ma".
  16
  17 include "lambda/notation/functions/dsubst_3.ma".
  18
  19 (* RELOCATING SUBSTITUTION **************************************************)
  20
  21 (* Policy: depth (level) metavariables: d, e (as for lift) *)
  22 let rec dsubst N d M on M ≝ match M with
  23 [ VRef i   ⇒ tri … i d (#i) (↑[i] N) (#(i-1))
  24 | Abst A   ⇒ 𝛌. (dsubst N (d+1) A)
  25 | Appl B A ⇒ @ (dsubst N d B). (dsubst N d A)
  26 ].
  27
  28 interpretation "relocating substitution"
  29    'DSubst N d M = (dsubst N d M).
  30
  31 lemma dsubst_vref_lt: ∀i,d,N. i < d → [d ↙ N] #i = #i.
  32 normalize /2 width=1/
  33 qed.
  34
  35 lemma dsubst_vref_eq: ∀i,N. [i ↙ N] #i = ↑[i]N.
  36 normalize //
  37 qed.
  38
  39 lemma dsubst_vref_gt: ∀i,d,N. d < i → [d ↙ N] #i = #(i-1).
  40 normalize /2 width=1/
  41 qed.
  42
  43 theorem dsubst_lift_le: ∀h,N,M,d1,d2. d2 ≤ d1 →
  44                         [d2 ↙ ↑[d1 - d2, h] N] ↑[d1 + 1, h] M = ↑[d1, h] [d2 ↙ N] M.
  45 #h #N #M elim M -M
  46 [ #i #d1 #d2 #Hd21 elim (lt_or_eq_or_gt i d2) #Hid2
  47   [ lapply (lt_to_le_to_lt … Hid2 Hd21) -Hd21 #Hid1
  48     >(dsubst_vref_lt … Hid2) >(lift_vref_lt … Hid1) >lift_vref_lt /2 width=1/
  49   | destruct >dsubst_vref_eq >lift_vref_lt /2 width=1/
  50   | >(dsubst_vref_gt … Hid2) -Hd21 elim (lt_or_ge (i-1) d1) #Hi1d1
  51     [ >(lift_vref_lt … Hi1d1) >lift_vref_lt /2 width=1/
  52     | lapply (ltn_to_ltO … Hid2) #Hi
  53       >(lift_vref_ge … Hi1d1) >lift_vref_ge /2 width=1/ -Hi1d1 >plus_minus // /3 width=1/
  54     ]
  55   ]
  56 | normalize #A #IHA #d1 #d2 #Hd21
  57   lapply (IHA (d1+1) (d2+1) ?) -IHA /2 width=1/
  58 | normalize #B #A #IHB #IHA #d1 #d2 #Hd21
  59   >IHB -IHB // >IHA -IHA //
  60 ]
  61 qed.
  62
  63 theorem dsubst_lift_be: ∀h,N,M,d1,d2. d1 ≤ d2 → d2 ≤ d1 + h →
  64                         [d2 ↙ N] ↑[d1, h + 1] M = ↑[d1, h] M.
  65 #h #N #M elim M -M
  66 [ #i #d1 #d2 #Hd12 #Hd21 elim (lt_or_ge i d1) #Hid1
  67   [ lapply (lt_to_le_to_lt … Hid1 Hd12) -Hd12 -Hd21 #Hid2
  68     >(lift_vref_lt … Hid1) >(lift_vref_lt … Hid1) /2 width=1/
  69   | lapply (transitive_le … (i+h) Hd21 ?) -Hd12 -Hd21 /2 width=1/ #Hd2
  70     >(lift_vref_ge … Hid1) >(lift_vref_ge … Hid1) -Hid1
  71     >dsubst_vref_gt // /2 width=1/
  72   ]
  73 | normalize #A #IHA #d1 #d2 #Hd12 #Hd21
  74   >IHA -IHA // /2 width=1/
  75 | normalize #B #A #IHB #IHA #d1 #d2 #Hd12 #Hd21
  76   >IHB -IHB // >IHA -IHA //
  77 ]
  78 qed.
  79
  80 theorem dsubst_lift_ge: ∀h,N,M,d1,d2. d1 + h ≤ d2 →
  81                         [d2 ↙ N] ↑[d1, h] M = ↑[d1, h] [d2 - h ↙ N] M.
  82 #h #N #M elim M -M
  83 [ #i #d1 #d2 #Hd12 elim (lt_or_eq_or_gt i (d2-h)) #Hid2h
  84   [ >(dsubst_vref_lt … Hid2h) elim (lt_or_ge i d1) #Hid1
  85     [ lapply (lt_to_le_to_lt … (d1+h) Hid1 ?) -Hid2h // #Hid1h
  86       lapply (lt_to_le_to_lt … Hid1h Hd12) -Hid1h -Hd12 #Hid2
  87       >(lift_vref_lt … Hid1) -Hid1 /2 width=1/
  88     | >(lift_vref_ge … Hid1) -Hid1 -Hd12 /3 width=1/
  89     ]
  90   | destruct elim (le_inv_plus_l … Hd12) -Hd12 #Hd12 #Hhd2
  91     >dsubst_vref_eq >lift_vref_ge // >lift_lift_be // <plus_minus_m_m //
  92   | elim (le_inv_plus_l … Hd12) -Hd12 #Hd12 #_
  93     lapply (le_to_lt_to_lt … Hd12 Hid2h) -Hd12 #Hid1
  94     lapply (ltn_to_ltO … Hid2h) #Hi
  95     >(dsubst_vref_gt … Hid2h)
  96     >lift_vref_ge /2 width=1/ >lift_vref_ge /2 width=1/ -Hid1
  97     >dsubst_vref_gt /2 width=1/ -Hid2h >plus_minus //
  98   ]
  99 | normalize #A #IHA #d1 #d2 #Hd12
 100   elim (le_inv_plus_l … Hd12) #_ #Hhd2
 101   >IHA -IHA /2 width=1/ <plus_minus //
 102 | normalize #B #A #IHB #IHA #d1 #d2 #Hd12
 103   >IHB -IHB // >IHA -IHA //
 104 ]
 105 qed.
 106
 107 theorem dsubst_dsubst_ge: ∀N1,N2,M,d1,d2. d1 ≤ d2 →
 108                           [d2 ↙ N2] [d1 ↙ N1] M = [d1 ↙ [d2 - d1 ↙ N2] N1] [d2 + 1 ↙ N2] M.
 109 #N1 #N2 #M elim M -M
 110 [ #i #d1 #d2 #Hd12 elim (lt_or_eq_or_gt i d1) #Hid1
 111   [ lapply (lt_to_le_to_lt … Hid1 Hd12) -Hd12 #Hid2
 112     >(dsubst_vref_lt … Hid1) >(dsubst_vref_lt … Hid2) >dsubst_vref_lt /2 width=1/
 113   | destruct >dsubst_vref_eq >dsubst_vref_lt /2 width=1/
 114   | >(dsubst_vref_gt … Hid1) elim (lt_or_eq_or_gt i (d2+1)) #Hid2
 115     [ lapply (ltn_to_ltO … Hid1) #Hi
 116       >(dsubst_vref_lt … Hid2) >dsubst_vref_lt /2 width=1/
 117     | destruct /2 width=1/
 118     | lapply (le_to_lt_to_lt (d1+1) … Hid2) -Hid1 /2 width=1/ -Hd12 #Hid1
 119       >(dsubst_vref_gt … Hid2) >dsubst_vref_gt /2 width=1/
 120       >dsubst_vref_gt // /2 width=1/
 121     ]
 122   ]
 123 | normalize #A #IHA #d1 #d2 #Hd12
 124   lapply (IHA (d1+1) (d2+1) ?) -IHA /2 width=1/
 125 | normalize #B #A #IHB #IHA #d1 #d2 #Hd12
 126   >IHB -IHB // >IHA -IHA //
 127 ]
 128 qed.
 129
 130 theorem dsubst_dsubst_lt: ∀N1,N2,M,d1,d2. d2 < d1 →
 131                           [d2 ↙ [d1 - d2 -1 ↙ N1] N2] [d1 ↙ N1] M = [d1 - 1 ↙ N1] [d2 ↙ N2] M.
 132 #N1 #N2 #M #d1 #d2 #Hd21
 133 lapply (ltn_to_ltO … Hd21) #Hd1
 134 >dsubst_dsubst_ge in ⊢ (???%); /2 width=1/ <plus_minus_m_m //
 135 qed.
 136
 137 definition dsubstable_dx: predicate (relation term) ≝ λR.
 138                           ∀N,M1,M2. R M1 M2 → ∀d. R ([d ↙ N] M1) ([d ↙ N] M2).
 139
 140 definition dsubstable: predicate (relation term) ≝ λR.
 141                        ∀N1,N2. R N1 N2 → ∀M1,M2. R M1 M2 → ∀d. R ([d ↙ N1] M1) ([d ↙ N2] M2).
 142
 143 lemma star_dsubstable_dx: ∀R. dsubstable_dx R → dsubstable_dx (star … R).
 144 #R #HR #N #M1 #M2 #H elim H -M2 // /3 width=3/
 145 qed.
 146
 147 lemma lstar_dsubstable_dx: ∀S,R. (∀a. dsubstable_dx (R a)) →
 148                            ∀l. dsubstable_dx (lstar S … R l).
 149 #S #R #HR #l #N #M1 #M2 #H
 150 @(lstar_ind_l … l M1 H) -l -M1 // /3 width=3/
 151 qed.
 152
 153 lemma star_dsubstable: ∀R. reflexive ? R →
 154                        dsubstable R → dsubstable (star … R).
 155 #R #H1R #H2 #N1 #N2 #H elim H -N2 /3 width=1/ /3 width=5/
 156 qed.