]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/lambda/terms/delifting_substitution.ma
7926c3948bec077d2a8ecb69e4b49b0d1d914f6d
[helm.git] / matita / matita / contribs / lambda / terms / 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 "terms/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 lemma dsubst_vref_lt: ∀i,d,D. i < d → [d ↙ D] #i = #i.
30 normalize /2 width=1/
31 qed.
32
33 lemma dsubst_vref_eq: ∀i,D. [i ↙ D] #i = ↑[i]D.
34 normalize //
35 qed.
36
37 lemma dsubst_vref_gt: ∀i,d,D. d < i → [d ↙ D] #i = #(i-1).
38 normalize /2 width=1/
39 qed.
40
41 theorem dsubst_lift_le: ∀h,D,M,d1,d2. d2 ≤ d1 →
42                         [d2 ↙ ↑[d1 - d2, h] D] ↑[d1 + 1, h] M = ↑[d1, h] [d2 ↙ D] M.
43 #h #D #M elim M -M
44 [ #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     >(dsubst_vref_lt … Hid2) >(lift_vref_lt … Hid1) >lift_vref_lt /2 width=1/
47   | destruct >dsubst_vref_eq >lift_vref_lt /2 width=1/
48   | >(dsubst_vref_gt … Hid2) -Hd21 elim (lt_or_ge (i-1) d1) #Hi1d1
49     [ >(lift_vref_lt … Hi1d1) >lift_vref_lt /2 width=1/
50     | lapply (ltn_to_ltO … Hid2) #Hi
51       >(lift_vref_ge … Hi1d1) >lift_vref_ge /2 width=1/ -Hi1d1 >plus_minus // /3 width=1/
52     ]
53   ]
54 | normalize #A #IHA #d1 #d2 #Hd21
55   lapply (IHA (d1+1) (d2+1) ?) -IHA /2 width=1/
56 | normalize #B #A #IHB #IHA #d1 #d2 #Hd21
57   >IHB -IHB // >IHA -IHA //
58 ]
59 qed.
60
61 theorem dsubst_lift_be: ∀h,D,M,d1,d2. d1 ≤ d2 → d2 ≤ d1 + h →
62                         [d2 ↙ D] ↑[d1, h + 1] M = ↑[d1, h] M.
63 #h #D #M elim M -M
64 [ #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     >(lift_vref_lt … Hid1) >(lift_vref_lt … Hid1) /2 width=1/
67   | lapply (transitive_le … (i+h) Hd21 ?) -Hd12 -Hd21 /2 width=1/ #Hd2
68     >(lift_vref_ge … Hid1) >(lift_vref_ge … Hid1) -Hid1
69     >dsubst_vref_gt // /2 width=1/
70   ]
71 | normalize #A #IHA #d1 #d2 #Hd12 #Hd21
72   >IHA -IHA // /2 width=1/
73 | normalize #B #A #IHB #IHA #d1 #d2 #Hd12 #Hd21
74   >IHB -IHB // >IHA -IHA //
75 ]
76 qed.
77
78 theorem dsubst_lift_ge: ∀h,D,M,d1,d2. d1 + h ≤ d2 →
79                         [d2 ↙ D] ↑[d1, h] M = ↑[d1, h] [d2 - h ↙ D] M.
80 #h #D #M elim M -M
81 [ #i #d1 #d2 #Hd12 elim (lt_or_eq_or_gt i (d2-h)) #Hid2h
82   [ >(dsubst_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       >(lift_vref_lt … Hid1) -Hid1 /2 width=1/
86     | >(lift_vref_ge … Hid1) -Hid1 -Hd12 /3 width=1/
87     ]
88   | destruct elim (le_inv_plus_l … Hd12) -Hd12 #Hd12 #Hhd2
89     >dsubst_vref_eq >lift_vref_ge // >lift_lift_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     >(dsubst_vref_gt … Hid2h)
94     >lift_vref_ge /2 width=1/ >lift_vref_ge /2 width=1/ -Hid1
95     >dsubst_vref_gt /2 width=1/ -Hid2h >plus_minus //
96   ]
97 | normalize #A #IHA #d1 #d2 #Hd12
98   elim (le_inv_plus_l … Hd12) #_ #Hhd2
99   >IHA -IHA /2 width=1/ <plus_minus //
100 | normalize #B #A #IHB #IHA #d1 #d2 #Hd12
101   >IHB -IHB // >IHA -IHA //
102 ]
103 qed.
104
105 theorem dsubst_dsubst_ge: ∀D1,D2,M,d1,d2. d1 ≤ d2 →
106                           [d2 ↙ D2] [d1 ↙ D1] M = [d1 ↙ [d2 - d1 ↙ D2] D1] [d2 + 1 ↙ D2] M.
107 #D1 #D2 #M elim M -M
108 [ #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     >(dsubst_vref_lt … Hid1) >(dsubst_vref_lt … Hid2) >dsubst_vref_lt /2 width=1/
111   | destruct >dsubst_vref_eq >dsubst_vref_lt /2 width=1/
112   | >(dsubst_vref_gt … Hid1) elim (lt_or_eq_or_gt i (d2+1)) #Hid2
113     [ lapply (ltn_to_ltO … Hid1) #Hi
114       >(dsubst_vref_lt … Hid2) >dsubst_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       >(dsubst_vref_gt … Hid2) >dsubst_vref_gt /2 width=1/
118       >dsubst_vref_gt // /2 width=1/
119     ]
120   ]
121 | normalize #A #IHA #d1 #d2 #Hd12
122   lapply (IHA (d1+1) (d2+1) ?) -IHA /2 width=1/
123 | normalize #B #A #IHB #IHA #d1 #d2 #Hd12
124   >IHB -IHB // >IHA -IHA //
125 ]
126 qed.
127
128 theorem dsubst_dsubst_lt: ∀D1,D2,M,d1,d2. d2 < d1 →
129                           [d2 ↙ [d1 - d2 -1 ↙ D1] D2] [d1 ↙ D1] M = [d1 - 1 ↙ D1] [d2 ↙ D2] M.
130 #D1 #D2 #M #d1 #d2 #Hd21
131 lapply (ltn_to_ltO … Hd21) #Hd1
132 >dsubst_dsubst_ge in ⊢ (???%); /2 width=1/ <plus_minus_m_m //
133 qed.
134
135 definition dsubstable_dx: predicate (relation term) ≝ λR.
136                           ∀D,M1,M2. R M1 M2 → ∀d. R ([d ↙ D] M1) ([d ↙ D] M2).
137
138 definition dsubstable: predicate (relation term) ≝ λR.
139                        ∀D1,D2. R D1 D2 → ∀M1,M2. R M1 M2 → ∀d. R ([d ↙ D1] M1) ([d ↙ D2] M2).
140
141 lemma star_dsubstable_dx: ∀R. dsubstable_dx R → dsubstable_dx (star … R).
142 #R #HR #D #M1 #M2 #H elim H -M2 // /3 width=3/
143 qed.
144
145 lemma lstar_dsubstable_dx: ∀S,R. (∀a. dsubstable_dx (R a)) →
146                            ∀l. dsubstable_dx (lstar S … R l).
147 #S #R #HR #l #D #M1 #M2 #H
148 @(lstar_ind_l ????????? H) -l -M1 // /3 width=3/
149 qed.
150
151 lemma star_dsubstable: ∀R. reflexive ? R →
152                        dsubstable R → dsubstable (star … R).
153 #R #H1R #H2 #D1 #D2 #H elim H -D2 /3 width=1/ /3 width=5/
154 qed.