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