]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/lambdadelta/basic_2/etc/cpr/tpss_lift.etc
- basic_2: induction for preservation results now uses supclosure
[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / etc / cpr / tpss_lift.etc
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 "basic_2/substitution/tps_lift.ma".
16 include "basic_2/unfold/tpss.ma".
17
18 (* PARTIAL UNFOLD ON TERMS **************************************************)
19
20 (* Advanced properties ******************************************************)
21
22 lemma tpss_subst: ∀L,K,V,U1,i,d,e.
23                   d ≤ i → i < d + e →
24                   ⇩[0, i] L ≡ K. ⓓV → K ⊢ V ▶* [0, d + e - i - 1] U1 →
25                   ∀U2. ⇧[0, i + 1] U1 ≡ U2 → L ⊢ #i ▶* [d, e] U2.
26 #L #K #V #U1 #i #d #e #Hdi #Hide #HLK #H @(tpss_ind … H) -U1
27 [ /3 width=4/
28 | #U #U1 #_ #HU1 #IHU #U2 #HU12
29   elim (lift_total U 0 (i+1)) #U0 #HU0
30   lapply (IHU … HU0) -IHU #H
31   lapply (ldrop_fwd_ldrop2 … HLK) -HLK #HLK
32   lapply (tps_lift_ge … HU1 … HLK HU0 HU12 ?) -HU1 -HLK -HU0 -HU12 // normalize #HU02
33   lapply (tps_weak … HU02 d e ? ?) -HU02 [ >minus_plus >commutative_plus /2 width=1/ | /2 width=1/ | /2 width=3/ ]
34 ]
35 qed.
36
37 (* Advanced inverion lemmas *************************************************)
38
39 lemma tpss_inv_atom1: ∀L,T2,I,d,e. L ⊢ ⓪{I} ▶* [d, e] T2 →
40                       T2 = ⓪{I} ∨
41                       ∃∃K,V1,V2,i. d ≤ i & i < d + e &
42                                    ⇩[O, i] L ≡ K. ⓓV1 &
43                                    K ⊢ V1 ▶* [0, d + e - i - 1] V2 &
44                                    ⇧[O, i + 1] V2 ≡ T2 &
45                                    I = LRef i.
46 #L #T2 #I #d #e #H @(tpss_ind … H) -T2
47 [ /2 width=1/
48 | #T #T2 #_ #HT2 *
49   [ #H destruct
50     elim (tps_inv_atom1 … HT2) -HT2 [ /2 width=1/ | * /3 width=10/ ]
51   | * #K #V1 #V #i #Hdi #Hide #HLK #HV1 #HVT #HI
52     lapply (ldrop_fwd_ldrop2 … HLK) #H
53     elim (tps_inv_lift1_ge_up … HT2 … H … HVT ? ? ?) normalize -HT2 -H -HVT [2,3,4: /2 width=1/ ] #V2 <minus_plus #HV2 #HVT2
54     @or_intror @(ex6_4_intro … Hdi Hide HLK … HVT2 HI) /2 width=3/ (**) (* /4 width=10/ is too slow *)
55   ]
56 ]
57 qed-.
58
59 lemma tpss_inv_lref1: ∀L,T2,i,d,e. L ⊢ #i ▶* [d, e] T2 →
60                       T2 = #i ∨
61                       ∃∃K,V1,V2. d ≤ i & i < d + e &
62                                  ⇩[O, i] L ≡ K. ⓓV1 &
63                                  K ⊢ V1 ▶* [0, d + e - i - 1] V2 &
64                                  ⇧[O, i + 1] V2 ≡ T2.
65 #L #T2 #i #d #e #H
66 elim (tpss_inv_atom1 … H) -H /2 width=1/
67 * #K #V1 #V2 #j #Hdj #Hjde #HLK #HV12 #HVT2 #H destruct /3 width=6/
68 qed-.
69
70 lemma tpss_inv_S2: ∀L,T1,T2,d,e. L ⊢ T1 ▶* [d, e + 1] T2 →
71                    ∀K,V. ⇩[0, d] L ≡ K. ⓛV → L ⊢ T1 ▶* [d + 1, e] T2.
72 #L #T1 #T2 #d #e #H #K #V #HLK @(tpss_ind … H) -T2 //
73 #T #T2 #_ #HT2 #IHT
74 lapply (tps_inv_S2 … HT2 … HLK) -HT2 -HLK /2 width=3/
75 qed-.
76
77 lemma tpss_inv_refl_SO2: ∀L,T1,T2,d. L ⊢ T1 ▶* [d, 1] T2 →
78                          ∀K,V. ⇩[0, d] L ≡ K. ⓛV → T1 = T2.
79 #L #T1 #T2 #d #H #K #V #HLK @(tpss_ind … H) -T2 //
80 #T #T2 #_ #HT2 #IHT <(tps_inv_refl_SO2 … HT2 … HLK) //
81 qed-.
82
83 (* Relocation properties ****************************************************)
84
85 lemma tpss_lift_le: ∀K,T1,T2,dt,et. K ⊢ T1 ▶* [dt, et] T2 →
86                     ∀L,U1,d,e. dt + et ≤ d → ⇩[d, e] L ≡ K →
87                     ⇧[d, e] T1 ≡ U1 → ∀U2. ⇧[d, e] T2 ≡ U2 →
88                     L ⊢ U1 ▶* [dt, et] U2.
89 #K #T1 #T2 #dt #et #H #L #U1 #d #e #Hdetd #HLK #HTU1 @(tpss_ind … H) -T2
90 [ #U2 #H >(lift_mono … HTU1 … H) -H //
91 | -HTU1 #T #T2 #_ #HT2 #IHT #U2 #HTU2
92   elim (lift_total T d e) #U #HTU
93   lapply (IHT … HTU) -IHT #HU1
94   lapply (tps_lift_le … HT2 … HLK HTU HTU2 ?) -HT2 -HLK -HTU -HTU2 // /2 width=3/
95 ]
96 qed.
97
98 lemma tpss_lift_be: ∀K,T1,T2,dt,et. K ⊢ T1 ▶* [dt, et] T2 →
99                     ∀L,U1,d,e. dt ≤ d → d ≤ dt + et →
100                     ⇩[d, e] L ≡ K → ⇧[d, e] T1 ≡ U1 →
101                     ∀U2. ⇧[d, e] T2 ≡ U2 → L ⊢ U1 ▶* [dt, et + e] U2.
102 #K #T1 #T2 #dt #et #H #L #U1 #d #e #Hdtd #Hddet #HLK #HTU1 @(tpss_ind … H) -T2
103 [ #U2 #H >(lift_mono … HTU1 … H) -H //
104 | -HTU1 #T #T2 #_ #HT2 #IHT #U2 #HTU2
105   elim (lift_total T d e) #U #HTU
106   lapply (IHT … HTU) -IHT #HU1
107   lapply (tps_lift_be … HT2 … HLK HTU HTU2 ? ?) -HT2 -HLK -HTU -HTU2 // /2 width=3/
108 ]
109 qed.
110
111 lemma tpss_lift_ge: ∀K,T1,T2,dt,et. K ⊢ T1 ▶* [dt, et] T2 →
112                     ∀L,U1,d,e. d ≤ dt → ⇩[d, e] L ≡ K →
113                     ⇧[d, e] T1 ≡ U1 → ∀U2. ⇧[d, e] T2 ≡ U2 →
114                     L ⊢ U1 ▶* [dt + e, et] U2.
115 #K #T1 #T2 #dt #et #H #L #U1 #d #e #Hddt #HLK #HTU1 @(tpss_ind … H) -T2
116 [ #U2 #H >(lift_mono … HTU1 … H) -H //
117 | -HTU1 #T #T2 #_ #HT2 #IHT #U2 #HTU2
118   elim (lift_total T d e) #U #HTU
119   lapply (IHT … HTU) -IHT #HU1
120   lapply (tps_lift_ge … HT2 … HLK HTU HTU2 ?) -HT2 -HLK -HTU -HTU2 // /2 width=3/
121 ]
122 qed.
123
124 lemma tpss_inv_lift1_le: ∀L,U1,U2,dt,et. L ⊢ U1 ▶* [dt, et] U2 →
125                          ∀K,d,e. ⇩[d, e] L ≡ K → ∀T1. ⇧[d, e] T1 ≡ U1 →
126                          dt + et ≤ d →
127                          ∃∃T2. K ⊢ T1 ▶* [dt, et] T2 & ⇧[d, e] T2 ≡ U2.
128 #L #U1 #U2 #dt #et #H #K #d #e #HLK #T1 #HTU1 #Hdetd @(tpss_ind … H) -U2
129 [ /2 width=3/
130 | -HTU1 #U #U2 #_ #HU2 * #T #HT1 #HTU
131   elim (tps_inv_lift1_le … HU2 … HLK … HTU ?) -HU2 -HLK -HTU // /3 width=3/
132 ]
133 qed.
134
135 lemma tpss_inv_lift1_be: ∀L,U1,U2,dt,et. L ⊢ U1 ▶* [dt, et] U2 →
136                          ∀K,d,e. ⇩[d, e] L ≡ K → ∀T1. ⇧[d, e] T1 ≡ U1 →
137                          dt ≤ d → d + e ≤ dt + et →
138                          ∃∃T2. K ⊢ T1 ▶* [dt, et - e] T2 & ⇧[d, e] T2 ≡ U2.
139 #L #U1 #U2 #dt #et #H #K #d #e #HLK #T1 #HTU1 #Hdtd #Hdedet @(tpss_ind … H) -U2
140 [ /2 width=3/
141 | -HTU1 #U #U2 #_ #HU2 * #T #HT1 #HTU
142   elim (tps_inv_lift1_be … HU2 … HLK … HTU ? ?) -HU2 -HLK -HTU // /3 width=3/
143 ]
144 qed.
145
146 lemma tpss_inv_lift1_ge: ∀L,U1,U2,dt,et. L ⊢ U1 ▶* [dt, et] U2 →
147                          ∀K,d,e. ⇩[d, e] L ≡ K → ∀T1. ⇧[d, e] T1 ≡ U1 →
148                          d + e ≤ dt →
149                          ∃∃T2. K ⊢ T1 ▶* [dt - e, et] T2 & ⇧[d, e] T2 ≡ U2.
150 #L #U1 #U2 #dt #et #H #K #d #e #HLK #T1 #HTU1 #Hdedt @(tpss_ind … H) -U2
151 [ /2 width=3/
152 | -HTU1 #U #U2 #_ #HU2 * #T #HT1 #HTU
153   elim (tps_inv_lift1_ge … HU2 … HLK … HTU ?) -HU2 -HLK -HTU // /3 width=3/
154 ]
155 qed.
156
157 lemma tpss_inv_lift1_eq: ∀L,U1,U2,d,e.
158                          L ⊢ U1 ▶* [d, e] U2 → ∀T1. ⇧[d, e] T1 ≡ U1 → U1 = U2.
159 #L #U1 #U2 #d #e #H #T1 #HTU1 @(tpss_ind … H) -U2 //
160 #U #U2 #_ #HU2 #IHU destruct
161 <(tps_inv_lift1_eq … HU2 … HTU1) -HU2 -HTU1 //
162 qed.
163
164 lemma tpss_inv_lift1_ge_up: ∀L,U1,U2,dt,et. L ⊢ U1 ▶* [dt, et] U2 →
165                             ∀K,d,e. ⇩[d, e] L ≡ K → ∀T1. ⇧[d, e] T1 ≡ U1 →
166                             d ≤ dt → dt ≤ d + e → d + e ≤ dt + et →
167                             ∃∃T2. K ⊢ T1 ▶* [d, dt + et - (d + e)] T2 &
168                                  ⇧[d, e] T2 ≡ U2.
169 #L #U1 #U2 #dt #et #H #K #d #e #HLK #T1 #HTU1 #Hddt #Hdtde #Hdedet @(tpss_ind … H) -U2
170 [ /2 width=3/
171 | -HTU1 #U #U2 #_ #HU2 * #T #HT1 #HTU
172   elim (tps_inv_lift1_ge_up … HU2 … HLK … HTU ? ? ?) -HU2 -HLK -HTU // /3 width=3/
173 ]
174 qed.
175
176 lemma tpss_inv_lift1_be_up: ∀L,U1,U2,dt,et. L ⊢ U1 ▶* [dt, et] U2 →
177                             ∀K,d,e. ⇩[d, e] L ≡ K → ∀T1. ⇧[d, e] T1 ≡ U1 →
178                             dt ≤ d → dt + et ≤ d + e →
179                             ∃∃T2. K ⊢ T1 ▶* [dt, d - dt] T2 & ⇧[d, e] T2 ≡ U2.
180 #L #U1 #U2 #dt #et #H #K #d #e #HLK #T1 #HTU1 #Hdtd #Hdetde @(tpss_ind … H) -U2
181 [ /2 width=3/
182 | -HTU1 #U #U2 #_ #HU2 * #T #HT1 #HTU
183   elim (tps_inv_lift1_be_up … HU2 … HLK … HTU ? ?) -HU2 -HLK -HTU // /3 width=3/
184 ]
185 qed.
186
187 lemma tpss_inv_lift1_le_up: ∀L,U1,U2,dt,et. L ⊢ U1 ▶* [dt, et] U2 →
188                             ∀K,d,e. ⇩[d, e] L ≡ K → ∀T1. ⇧[d, e] T1 ≡ U1 →
189                             dt ≤ d → d ≤ dt + et → dt + et ≤ d + e →
190                             ∃∃T2. K ⊢ T1 ▶* [dt, d - dt] T2 & ⇧[d, e] T2 ≡ U2.
191 #L #U1 #U2 #dt #et #H #K #d #e #HLK #T1 #HTU1 #Hdtd #Hddet #Hdetde @(tpss_ind … H) -U2
192 [ /2 width=3/
193 | -HTU1 #U #U2 #_ #HU2 * #T #HT1 #HTU
194   elim (tps_inv_lift1_le_up … HU2 … HLK … HTU ? ? ?) -HU2 -HLK -HTU // /3 width=3/
195 ]
196 qed.