1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
17 (* DELIFTING SUBSTITUTION ***************************************************)
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)
26 interpretation "delifting substitution"
27 'DSubst D d M = (dsubst D d M).
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 }.
34 notation > "hvbox( [ ⬐ term 46 D ] break term 46 M )"
35 non associative with precedence 46
36 for @{ 'DSubst $D 0 $M }.
38 lemma dsubst_vref_lt: ∀i,d,D. i < d → [d ⬐ D] #i = #i.
42 lemma dsubst_vref_eq: ∀d,D. [d ⬐ D] #d = ↑[d]D.
46 lemma dsubst_vref_gt: ∀i,d,D. d < i → [d ⬐ D] #i = #(i-1).
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.
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/
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 //
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.
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/
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 //
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.
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/
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 //
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 //
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.
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/
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 //
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 //
144 definition dsubstable_dx: predicate (relation term) ≝ λR.
145 ∀D,M1,M2. R M1 M2 → ∀d. R ([d ⬐ D] M1) ([d ⬐ D] M2).
147 definition dsubstable_sn: predicate (relation term) ≝ λR.
148 ∀D1,D2. R D1 D2 → ∀M,d. R ([d ⬐ D1] M) ([d ⬐ D2] M).
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).