]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/lambdadelta/basic_2/etc/snta/snta_lift.etc
- extended multiple substitutions now uses bounds in ynat (ie. they
[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / etc / snta / snta_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/equivalence/cpcs_cpcs.ma".
16 include "basic_2/dynamic/snta.ma".
17
18 (* NATIVE TYPE ASSIGNMENT ON TERMS ******************************************)
19
20 (* Advanced inversion lemmas ************************************************)
21
22 fact snta_inv_sort1_aux: ∀h,L,T,U,l. ⦃h, L⦄ ⊢ T :[l] U → ∀k0. T = ⋆k0 →
23                          l = 0 ∧ L ⊢ ⋆(next h k0) ⬌* U.
24 #h #L #T #U #l #H elim H -L -T -U -l
25 [ #L #k #k0 #H destruct /2 width=1/
26 | #L #K #V #W #U #i #l #_ #_ #_ #_ #k0 #H destruct
27 | #L #K #W #V #U #i #l #_ #_ #_ #_ #k0 #H destruct
28 | #I #L #V #W #T #U #l1 #l2 #_ #_ #_ #_ #k0 #H destruct
29 | #L #V #W1 #W2 #T #U #l1 #l2 #_ #_ #_ #_ #k0 #H destruct
30 | #L #V #T #U #W #l #_ #_ #_ #_ #k0 #H destruct
31 | #L #T #U #W #l1 #l2 #_ #_ #_ #_ #k0 #H destruct
32 | #L #T #U1 #U2 #V2 #l #_ #HU12 #_ #IHTU1 #_ #k0 #H destruct
33   elim (IHTU1 ??) -IHTU1 [3: // |2: skip ] #H #Hk0
34   lapply (cpcs_trans … Hk0 … HU12) -U1 /2 width=1/
35 ]
36 qed.
37
38 lemma snta_inv_sort1: ∀h,L,U,k,l. ⦃h, L⦄ ⊢ ⋆k :[l] U →
39                       l = 0 ∧ L ⊢ ⋆(next h k) ⬌* U.
40 /2 width=4/ qed-.
41
42 fact snta_inv_lref1_aux: ∀h,L,T,U,l. ⦃h, L⦄ ⊢ T :[l] U → ∀j. T = #j →
43                          (∃∃K,V,W,U0. ⇩[0, j] L ≡ K. ⓓV & ⦃h, K⦄ ⊢ V :[l] W &
44                                       ⇧[0, j + 1] W ≡ U0 & L ⊢ U0 ⬌* U
45                          ) ∨
46                          (∃∃K,W,V,U0. ⇩[0, j] L ≡ K. ⓛW & ⦃h, K⦄ ⊢ W :[l-1] V &
47                                       ⇧[0, j + 1] W ≡ U0 & l > 0 & L ⊢ U0 ⬌* U
48                          ).
49 #h #L #T #U #l #H elim H -L -T -U -l
50 [ #L #k #j #H destruct
51 | #L #K #V #W #U #i #l #HLK #HVW #HWU #_ #j #H destruct /3 width=8/
52 | #L #K #W #V #U #i #l #HLK #HWV #HWU #_ #j #H destruct /3 width=8/
53 | #I #L #V #W #T #U #l1 #l2 #_ #_ #_ #_ #j #H destruct
54 | #L #V #W1 #W2 #T #U #l1 #l2 #_ #_ #_ #_ #j #H destruct
55 | #L #V #T #U #W #l #_ #_ #_ #_ #j #H destruct
56 | #L #T #U #W #l1 #l2 #_ #_ #_ #_ #j #H destruct
57 | #L #T #U1 #U2 #V2 #l #_ #HU12 #_ #IHTU1 #_ #j #H destruct
58   elim (IHTU1 ??) -IHTU1 [4: // |2: skip ] * #K #V #W #U0 #HLK #HVW #HWU0 [2: #H ] #HU01
59   lapply (cpcs_trans … HU01 … HU12) -U1 /3 width=8/
60 ]
61 qed.
62
63 lemma snta_inv_lref1: ∀h,L,U,i,l. ⦃h, L⦄ ⊢ #i :[l] U →
64                      (∃∃K,V,W,U0. ⇩[0, i] L ≡ K. ⓓV & ⦃h, K⦄ ⊢ V :[l] W &
65                                   ⇧[0, i + 1] W ≡ U0 & L ⊢ U0 ⬌* U
66                      ) ∨
67                      (∃∃K,W,V,U0. ⇩[0, i] L ≡ K. ⓛW & ⦃h, K⦄ ⊢ W :[l-1] V &
68                                   ⇧[0, i + 1] W ≡ U0 & l > 0 & L ⊢ U0 ⬌* U
69                      ).
70 /2 width=3/ qed-.
71
72 fact snta_inv_bind1_aux: ∀h,L,T,U,l. ⦃h, L⦄ ⊢ T :[l] U → ∀J,X,Y. T = ⓑ{J}Y.X →
73                          ∃∃Z1,Z2,l0. ⦃h, L⦄ ⊢ Y :[l0] Z1 &
74                                   ⦃h, L.ⓑ{J}Y⦄ ⊢ X :[l] Z2 &
75                                   L ⊢ ⓑ{J}Y.Z2 ⬌* U.
76 #h #L #T #U #l #H elim H -L -T -U -l
77 [ #L #k #J #X #Y #H destruct
78 | #L #K #V #W #U #i #l #_ #_ #_ #_ #J #X #Y #H destruct
79 | #L #K #W #V #U #i #l #_ #_ #_ #_ #J #X #Y #H destruct
80 | #I #L #V #W #T #U #l1 #l2 #HVW #HTU #_ #_ #J #X #Y #H destruct /2 width=3/
81 | #L #V #W1 #W2 #T #U #l1 #l2 #_ #_ #_ #_ #J #X #Y #H destruct
82 | #L #V #T #U #W #l #_ #_ #_ #_ #J #X #Y #H destruct
83 | #L #T #U #W #l1 #l2 #_ #_ #_ #_ #J #X #Y #H destruct
84 | #L #T #U1 #U2 #V2 #l #_ #HU12 #_ #IHTU1 #_ #J #X #Y #H destruct
85   elim (IHTU1 ????) -IHTU1 [5: // |2,3,4: skip ] #Z1 #Z2 #l0 #HZ1 #HZ2 #HU1
86   lapply (cpcs_trans … HU1 … HU12) -U1 /2 width=3/
87 ]
88 qed.
89
90 lemma snta_inv_bind1: ∀h,J,L,Y,X,U,l. ⦃h, L⦄ ⊢ ⓑ{J}Y.X :[l] U →
91                       ∃∃Z1,Z2,l0. ⦃h, L⦄ ⊢ Y :[l0] Z1 & ⦃h, L.ⓑ{J}Y⦄ ⊢ X :[l] Z2 &
92                                   L ⊢ ⓑ{J}Y.Z2 ⬌* U.
93 /2 width=3/ qed-.
94
95 fact snta_inv_cast1_aux: ∀h,L,T,U,l. ⦃h, L⦄ ⊢ T :[l] U → ∀X,Y. T = ⓝY.X →
96                       ⦃h, L⦄ ⊢ X :[l] Y ∧ L ⊢ Y ⬌* U.
97 #h #L #T #U #l #H elim H -L -T -U -l
98 [ #L #k #X #Y #H destruct
99 | #L #K #V #W #U #i #l #_ #_ #_ #_ #X #Y #H destruct
100 | #L #K #W #V #U #i #l #_ #_ #_ #_ #X #Y #H destruct
101 | #I #L #V #W #T #U #l1 #l2 #_ #_ #_ #_ #X #Y #H destruct
102 | #L #V #W1 #W2 #T #U #l1 #l2 #_ #_ #_ #_ #X #Y #H destruct
103 | #L #V #T #U #W #l #_ #_ #_ #_ #X #Y #H destruct
104 | #L #T #U #W #l1 #l2 #HTU #_ #_ #_ #X #Y #H destruct /2 width=1/
105 | #L #T #U1 #U2 #V2 #l #_ #HU12 #_ #IHTU1 #_ #X #Y #H destruct
106   elim (IHTU1 ???) -IHTU1 [4: // |2,3: skip ] #HXY #HU1
107   lapply (cpcs_trans … HU1 … HU12) -U1 /2 width=1/
108 ]
109 qed.
110
111 lemma snta_inv_cast1: ∀h,L,X,Y,U,l. ⦃h, L⦄ ⊢ ⓝY.X :[l] U →
112                       ⦃h, L⦄ ⊢ X :[l] Y ∧ L ⊢ Y ⬌* U.
113 /2 width=3/ qed-.
114
115 (* Properties on relocation *************************************************)
116
117 lemma snta_lift: ∀h,L1,T1,U1,l. ⦃h, L1⦄ ⊢ T1 :[l] U1 →
118                  ∀L2,d,e. ⇩[d, e] L2 ≡ L1 →
119                  ∀T2. ⇧[d, e] T1 ≡ T2 → ∀U2. ⇧[d, e] U1 ≡ U2 →
120                  ⦃h, L2⦄ ⊢ T2 :[l] U2.
121 #h #L1 #T1 #U1 #l #H elim H -L1 -T1 -U1 -l
122 [ #L1 #k #L2 #d #e #HL21 #X1 #H1 #X2 #H2
123   >(lift_inv_sort1 … H1) -X1
124   >(lift_inv_sort1 … H2) -X2 //
125 | #L1 #K1 #V1 #W1 #W #i #l #HLK1 #_ #HW1 #IHVW1 #L2 #d #e #HL21 #X #H #U2 #HWU2
126   elim (lift_inv_lref1 … H) * #Hid #H destruct
127   [ elim (lift_trans_ge … HW1 … HWU2 ?) -W // #W2 #HW12 #HWU2
128     elim (ldrop_trans_le … HL21 … HLK1 ?) -L1 /2 width=2/ #X #HLK2 #H
129     elim (ldrop_inv_skip2 … H ?) -H /2 width=1/ -Hid #K2 #V2 #HK21 #HV12 #H destruct
130     /3 width=8/
131   | lapply (lift_trans_be … HW1 … HWU2 ? ?) -W // /2 width=1/ #HW1U2
132     lapply (ldrop_trans_ge … HL21 … HLK1 ?) -L1 // -Hid /3 width=8/
133   ]
134 | #L1 #K1 #W1 #V1 #W #i #l #HLK1 #_ #HW1 #IHWV1 #L2 #d #e #HL21 #X #H #U2 #HWU2
135   elim (lift_inv_lref1 … H) * #Hid #H destruct
136   [ elim (lift_trans_ge … HW1 … HWU2 ?) -W // <minus_plus #W #HW1 #HWU2
137     elim (ldrop_trans_le … HL21 … HLK1 ?) -L1 /2 width=2/ #X #HLK2 #H
138     elim (ldrop_inv_skip2 … H ?) -H /2 width=1/ -Hid #K2 #W2 #HK21 #HW12 #H destruct
139     lapply (lift_mono … HW1 … HW12) -HW1 #H destruct
140     elim (lift_total V1 (d-i-1) e) /3 width=8/
141   | lapply (lift_trans_be … HW1 … HWU2 ? ?) -W // /2 width=1/ #HW1U2
142     lapply (ldrop_trans_ge … HL21 … HLK1 ?) -L1 // -Hid /3 width=8/
143   ]
144 | #I #L1 #V1 #W1 #T1 #U1 #l1 #l2 #_ #_ #IHVW1 #IHTU1 #L2 #d #e #HL21 #X1 #H1 #X2 #H2
145   elim (lift_inv_bind1 … H1) -H1 #V2 #T2 #HV12 #HT12 #H destruct
146   elim (lift_inv_bind1 … H2) -H2 #X #U2 #H1 #HU12 #H2 destruct
147   lapply (lift_mono … H1 … HV12) -H1 #H destruct
148   elim (lift_total W1 d e) /4 width=6/
149 | #L1 #V1 #W11 #W12 #T1 #U1 #l1 #l2 #_ #_ #IHVW1 #IHTU1 #L2 #d #e #HL21 #X1 #H1 #X2 #H2
150   elim (lift_inv_flat1 … H1) -H1 #V2 #X #HV12 #H1 #H destruct
151   elim (lift_inv_bind1 … H1) -H1 #W21 #T2 #HW121 #HT12 #H destruct
152   elim (lift_inv_flat1 … H2) -H2 #Y2 #X #HY #H2 #H destruct
153   elim (lift_inv_bind1 … H2) -H2 #W22 #U2 #HW122 #HU12 #H destruct
154   lapply (lift_mono … HY … HV12) -HY #H destruct /4 width=6/
155 | #L1 #V1 #T1 #U1 #W1 #l #_ #_ #IHTU1 #IHUW1 #L2 #d #e #HL21 #X1 #H1 #X2 #H2
156   elim (lift_inv_flat1 … H1) -H1 #V2 #T2 #HV12 #HT12 #H destruct
157   elim (lift_inv_flat1 … H2) -H2 #X #U2 #H1 #HU12 #H2 destruct
158   lapply (lift_mono … H1 … HV12) -H1 #H destruct
159   elim (lift_total W1 d e) #W2 #HW12 /4 width=6/
160 | #L1 #T1 #U1 #W1 #l1 #l2 #_ #_ #IHTU1 #IHUW1 #L2 #d #e #HL21 #X #H #U2 #HU12
161   elim (lift_inv_flat1 … H) -H #X2 #T2 #HUX2 #HT12 #H destruct
162   lapply (lift_mono … HUX2 … HU12) -HUX2 #H destruct
163   elim (lift_total W1 d e) /3 width=6/
164 | #L1 #T1 #U11 #U12 #V12 #l #_ #HU112 #_ #IHTU11 #IHUV12 #L2 #d #e #HL21 #U1 #HTU1 #U2 #HU12
165   elim (lift_total U11 d e) #U #HU11
166   elim (lift_total V12 d e) #V22 #HV122
167   lapply (cpcs_lift … HL21 … HU11 … HU12 HU112) -HU112 /3 width=6/
168 ]
169 qed.
170
171 (* Advanced forvard lemmas **************************************************)
172
173 fact snta_fwd_pure1_aux: ∀h,L,T,U,l. ⦃h, L⦄ ⊢ T :[l] U → ∀X,Y. T = ⓐY.X →
174                          ∃∃V,W,l0. ⦃h, L⦄ ⊢ Y :[l0+1] W & ⦃h, L⦄ ⊢ X :[l] V &
175                                    L ⊢ ⓐY.V ⬌* U.
176 #h #L #T #U #l #H elim H -L -T -U -l
177 [ #L #k #X #Y #H destruct
178 | #L #K #V #W #U #i #l #_ #_ #_ #_ #X #Y #H destruct
179 | #L #K #W #V #U #i #l #_ #_ #_ #_ #X #Y #H destruct
180 | #I #L #V #W #T #U #l1 #l2 #_ #_ #_ #_ #X #Y #H destruct
181 | #L #V #W1 #W2 #T #U #l1 #l2 #HVW2 #HTU #_ #_ #X #Y #H destruct /2 width=3/
182 | #L #V #T #U #W #l #HTU #_ #_ #IHU #X #Y #H destruct
183   elim (IHU U Y ?) -IHU // /3 width=3/
184 | #L #T #U #W #l1 #l2 #_ #_ #_ #_ #X #Y #H destruct
185 | #L #T #U1 #U2 #V2 #l #_ #HU12 #_ #IHTU1 #_ #X #Y #H destruct
186   elim (IHTU1 ???) -IHTU1 [4: // |2,3: skip ] #V #W #l0 #HYW #HXV #HU1
187   lapply (cpcs_trans … HU1 … HU12) -U1 /2 width=3/
188 ]
189 qed.
190
191 lemma snta_fwd_pure1: ∀h,L,X,Y,U,l. ⦃h, L⦄ ⊢ ⓐY.X :[l] U →
192                       ∃∃V,W,l0. ⦃h, L⦄ ⊢ Y :[l0+1] W & ⦃h, L⦄ ⊢ X :[l] V &
193                                 L ⊢ ⓐY.V ⬌* U.
194 /2 width=3/ qed-.
195
196 lemma snta_fwd_correct: ∀h,L,T,U,l. ⦃h, L⦄ ⊢ T :[l] U →
197                         ∃T0. ⦃h, L⦄ ⊢ U :[l-1] T0.
198 #h #L #T #U #l #H elim H -L -T -U -l
199 [ /2 width=2/
200 | #L #K #V #W #W0 #i #l #HLK #_ #HW0 * #V0 #HWV0
201   lapply (ldrop_fwd_ldrop2 … HLK) -HLK #HLK
202   elim (lift_total V0 0 (i+1)) /3 width=10/
203 | #L #K #W #V #V0 #i #l #HLK #HWV #HWV0 #_
204   lapply (ldrop_fwd_ldrop2 … HLK) -HLK #HLK
205   elim (lift_total V 0 (i+1)) /3 width=10/
206 | #I #L #V #W #T #U #l1 #l2 #HVW #_ #_ * /3 width=3/
207 | #L #V #W1 #W2 #T #U #l1 #l2 #HVW2 #_ #_ * #X #H
208   elim (snta_inv_bind1 … H) -H /4 width=5/   
209 | /3 width=2/
210 | /2 width=2/
211 | /2 width=2/
212 ]
213 qed-.
214
215 (* Advanced properties ******************************************************)
216
217 lemma snta_cast_short: ∀h,L,T,U,l. ⦃h, L⦄ ⊢ T :[l] U → ⦃h, L⦄ ⊢ ⓝU.T :[l] U.
218 #h #L #T #U #l #HTU
219 elim (snta_fwd_correct … HTU) /2 width=3/
220 qed.
221
222 lemma snta_typecheck: ∀h,L,T,U,l. ⦃h, L⦄ ⊢ T :[l] U →
223                       ∃T0. ⦃h, L⦄ ⊢ ⓝU.T :[l] T0.
224 /3 width=2/ qed.
225
226 lemma snta_cast_old: ∀h,L,W,T,U,l.
227                     ⦃h, L⦄ ⊢ T :[l] U → ⦃h, L⦄ ⊢ U :[l-1] W → ⦃h, L⦄ ⊢ ⓝU.T :[l] ⓝW.U.
228 #h #L #W #T #U #l #HTU #HUW
229 @(snta_conv … U) /2 width=2/ /3 width=1/ (**) (* /4 width=3/ is a bit slow *)
230 qed.
231
232 lemma snta_appl_old: ∀h,L,V,W,T,U,l1,l2.
233                      ⦃h, L⦄ ⊢ V :[l1+1] W → ⦃h, L⦄ ⊢ T :[l2+1] ⓛW.U →
234                      ⦃h, L⦄ ⊢ ⓐV.T :[l2+1] ⓐV.ⓛW.U.
235 #h #L #V #W #T #U #l1 #l2 #HVW #HTU
236 elim (snta_fwd_correct … HTU) #X #H
237 elim (snta_inv_bind1 … H) -H /4 width=5/
238 qed.