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 (**************************************************************************)
15 include "subterms/relocation.ma".
17 (* RELOCATING SUBSTITUTION **************************************************)
19 (* Policy: depth (level) metavariables: d, e (as for lift) *)
20 let rec sdsubst G d F on F ≝ match F with
21 [ SVRef b i ⇒ tri … i d ({b}#i) (↑[i] G) ({b}#(i-1))
22 | SAbst b T ⇒ {b}𝛌. (sdsubst G (d+1) T)
23 | SAppl b V T ⇒ {b}@ (sdsubst G d V). (sdsubst G d T)
26 interpretation "relocating substitution for subterms"
27 'DSubst G d F = (sdsubst G d F).
29 lemma sdsubst_vref_lt: ∀b,i,d,G. i < d → [d ↙ G] {b}#i = {b}#i.
33 lemma sdsubst_vref_eq: ∀b,i,G. [i ↙ G] {b}#i = ↑[i]G.
37 lemma sdsubst_vref_gt: ∀b,i,d,G. d < i → [d ↙ G] {b}#i = {b}#(i-1).
41 theorem sdsubst_slift_le: ∀h,G,F,d1,d2. d2 ≤ d1 →
42 [d2 ↙ ↑[d1 - d2, h] G] ↑[d1 + 1, h] F = ↑[d1, h] [d2 ↙ G] F.
44 [ #b #i #d1 #d2 #Hd21 elim (lt_or_eq_or_gt i d2) #Hid2
45 [ lapply (lt_to_le_to_lt … Hid2 Hd21) -Hd21 #Hid1
46 >(sdsubst_vref_lt … Hid2) >(slift_vref_lt … Hid1) >slift_vref_lt /2 width=1/
47 | destruct >sdsubst_vref_eq >slift_vref_lt /2 width=1/
48 | >(sdsubst_vref_gt … Hid2) -Hd21 elim (lt_or_ge (i-1) d1) #Hi1d1
49 [ >(slift_vref_lt … Hi1d1) >slift_vref_lt /2 width=1/
50 | lapply (ltn_to_ltO … Hid2) #Hi
51 >(slift_vref_ge … Hi1d1) >slift_vref_ge /2 width=1/ -Hi1d1 >plus_minus // /3 width=1/
54 | normalize #b #T #IHT #d1 #d2 #Hd21
55 lapply (IHT (d1+1) (d2+1) ?) -IHT /2 width=1/
56 | normalize #b #V #T #IHV #IHT #d1 #d2 #Hd21
57 >IHV -IHV // >IHT -IHT //
61 theorem sdsubst_slift_be: ∀h,G,F,d1,d2. d1 ≤ d2 → d2 ≤ d1 + h →
62 [d2 ↙ G] ↑[d1, h + 1] F = ↑[d1, h] F.
64 [ #b #i #d1 #d2 #Hd12 #Hd21 elim (lt_or_ge i d1) #Hid1
65 [ lapply (lt_to_le_to_lt … Hid1 Hd12) -Hd12 -Hd21 #Hid2
66 >(slift_vref_lt … Hid1) >(slift_vref_lt … Hid1) /2 width=1/
67 | lapply (transitive_le … (i+h) Hd21 ?) -Hd12 -Hd21 /2 width=1/ #Hd2
68 >(slift_vref_ge … Hid1) >(slift_vref_ge … Hid1) -Hid1
69 >sdsubst_vref_gt // /2 width=1/
71 | normalize #b #T #IHT #d1 #d2 #Hd12 #Hd21
72 >IHT -IHT // /2 width=1/
73 | normalize #b #V #T #IHV #IHT #d1 #d2 #Hd12 #Hd21
74 >IHV -IHV // >IHT -IHT //
78 theorem sdsubst_slift_ge: ∀h,G,F,d1,d2. d1 + h ≤ d2 →
79 [d2 ↙ G] ↑[d1, h] F = ↑[d1, h] [d2 - h ↙ G] F.
81 [ #b #i #d1 #d2 #Hd12 elim (lt_or_eq_or_gt i (d2-h)) #Hid2h
82 [ >(sdsubst_vref_lt … Hid2h) elim (lt_or_ge i d1) #Hid1
83 [ lapply (lt_to_le_to_lt … (d1+h) Hid1 ?) -Hid2h // #Hid1h
84 lapply (lt_to_le_to_lt … Hid1h Hd12) -Hid1h -Hd12 #Hid2
85 >(slift_vref_lt … Hid1) -Hid1 /2 width=1/
86 | >(slift_vref_ge … Hid1) -Hid1 -Hd12 /3 width=1/
88 | destruct elim (le_inv_plus_l … Hd12) -Hd12 #Hd12 #Hhd2
89 >sdsubst_vref_eq >slift_vref_ge // >slift_slift_be // <plus_minus_m_m //
90 | elim (le_inv_plus_l … Hd12) -Hd12 #Hd12 #_
91 lapply (le_to_lt_to_lt … Hd12 Hid2h) -Hd12 #Hid1
92 lapply (ltn_to_ltO … Hid2h) #Hi
93 >(sdsubst_vref_gt … Hid2h)
94 >slift_vref_ge /2 width=1/ >slift_vref_ge /2 width=1/ -Hid1
95 >sdsubst_vref_gt /2 width=1/ -Hid2h >plus_minus //
97 | normalize #b #T #IHT #d1 #d2 #Hd12
98 elim (le_inv_plus_l … Hd12) #_ #Hhd2
99 >IHT -IHT /2 width=1/ <plus_minus //
100 | normalize #b #V #T #IHV #IHT #d1 #d2 #Hd12
101 >IHV -IHV // >IHT -IHT //
105 theorem sdsubst_sdsubst_ge: ∀G1,G2,F,d1,d2. d1 ≤ d2 →
106 [d2 ↙ G2] [d1 ↙ G1] F = [d1 ↙ [d2 - d1 ↙ G2] G1] [d2 + 1 ↙ G2] F.
108 [ #b #i #d1 #d2 #Hd12 elim (lt_or_eq_or_gt i d1) #Hid1
109 [ lapply (lt_to_le_to_lt … Hid1 Hd12) -Hd12 #Hid2
110 >(sdsubst_vref_lt … Hid1) >(sdsubst_vref_lt … Hid2) >sdsubst_vref_lt /2 width=1/
111 | destruct >sdsubst_vref_eq >sdsubst_vref_lt /2 width=1/
112 | >(sdsubst_vref_gt … Hid1) elim (lt_or_eq_or_gt i (d2+1)) #Hid2
113 [ lapply (ltn_to_ltO … Hid1) #Hi
114 >(sdsubst_vref_lt … Hid2) >sdsubst_vref_lt /2 width=1/
115 | destruct /2 width=1/
116 | lapply (le_to_lt_to_lt (d1+1) … Hid2) -Hid1 /2 width=1/ -Hd12 #Hid1
117 >(sdsubst_vref_gt … Hid2) >sdsubst_vref_gt /2 width=1/
118 >sdsubst_vref_gt // /2 width=1/
121 | normalize #b #T #IHT #d1 #d2 #Hd12
122 lapply (IHT (d1+1) (d2+1) ?) -IHT /2 width=1/
123 | normalize #b #V #T #IHV #IHT #d1 #d2 #Hd12
124 >IHV -IHV // >IHT -IHT //
128 theorem sdsubst_sdsubst_lt: ∀G1,G2,F,d1,d2. d2 < d1 →
129 [d2 ↙ [d1 - d2 -1 ↙ G1] G2] [d1 ↙ G1] F = [d1 - 1 ↙ G1] [d2 ↙ G2] F.
130 #G1 #G2 #F #d1 #d2 #Hd21
131 lapply (ltn_to_ltO … Hd21) #Hd1
132 >sdsubst_sdsubst_ge in ⊢ (???%); /2 width=1/ <plus_minus_m_m //
135 definition sdsubstable_f_dx: ∀S:Type[0]. (S → ?) → predicate (relation subterms) ≝ λS,f,R.
136 ∀G,F1,F2. R F1 F2 → ∀d. R ([d ↙ (f G)] F1) ([d ↙ (f G)] F2).
138 lemma lstar_sdsubstable_f_dx: ∀S1,f,S2,R. (∀a. sdsubstable_f_dx S1 f (R a)) →
139 ∀l. sdsubstable_f_dx S1 f (lstar S2 … R l).
140 #S1 #f #S2 #R #HR #l #G #F1 #F2 #H
141 @(lstar_ind_l ????????? H) -l -F1 // /3 width=3/
144 definition sdsubstable_dx: predicate (relation subterms) ≝ λR.
145 ∀G,F1,F2. R F1 F2 → ∀d. R ([d ↙ G] F1) ([d ↙ G] F2).
147 definition sdsubstable: predicate (relation subterms) ≝ λR.
148 ∀G1,G2. R G1 G2 → ∀F1,F2. R F1 F2 → ∀d. R ([d ↙ G1] F1) ([d ↙ G2] F2).
150 lemma star_sdsubstable_dx: ∀R. sdsubstable_dx R → sdsubstable_dx (star … R).
151 #R #HR #G #F1 #F2 #H elim H -F2 // /3 width=3/
154 lemma lstar_sdsubstable_dx: ∀S,R. (∀a. sdsubstable_dx (R a)) →
155 ∀l. sdsubstable_dx (lstar S … R l).
156 #S #R #HR #l #G #F1 #F2 #H
157 @(lstar_ind_l ????????? H) -l -F1 // /3 width=3/
160 lemma star_sdsubstable: ∀R. reflexive ? R →
161 sdsubstable R → sdsubstable (star … R).
162 #R #H1R #H2 #G1 #G2 #H elim H -G2 /3 width=1/ /3 width=5/