]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/lambda_delta/basic_2/dynamic/nta_ltpr.ma
c461e9f7e736f5306a1cc2b9e46ce20612f11aff
[helm.git] / matita / matita / contribs / lambda_delta / basic_2 / dynamic / nta_ltpr.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 "basic_2/equivalence/cpcs_delift.ma".
16 include "basic_2/dynamic/nta.ma".
17 (*
18 lemma pippo: ∀h,L,T,U. ⦃h, L⦄ ⊢ T : U → ∀X,Y. L ⊢ T ➡* ⓛX.Y →
19              ∃Z. L ⊢ U ➡* ⓛX.Z.
20 #h #L #T #U #H elim H -L -T -U
21 [
22 |
23 |
24 |
25 | #L #V #W #T #U #_ #_ #IHVW #IHTU #X #Y #H  
26 | #L #V #W #T #U #_ #HUW #IHTU #IHUW #X #Y #HTY
27   elim (cprs_inv_appl_abst … HTY) -HTY #W1 #T1 #W2 #T2 #HT1 #HT12 #HYT2
28   elim (IHTU … HT1) -IHTU -HT1 #U1 #HU1 
29  
30   
31   
32    *
33   [ #V0 #T0 #_ #_ #H destruct
34   | #V0 #W0 #T0 #HV0 #HT0 #HTY
35     elim (IHTU … HT0) -IHTU -HT0 #Z #HUZ
36     elim (cprs_inv_abbr1 … HTY) -HTY *
37     [ #V1 #T1 #_ #_ #H destruct #X0  
38
39 *)
40
41 (*
42
43 include "basic_2/computation/cprs_lcprs.ma".
44
45
46
47
48 include "basic_2/dynamic/nta_ltpss.ma".
49 include "basic_2/dynamic/nta_thin.ma".
50 include "basic_2/dynamic/lsubn_nta.ma".
51
52 include "basic_2/hod/ntas_lift.ma".
53
54   
55   elim (nta_inv_pure1 … HUW) -HUW #V0 #U0 #U1 #HV0 #HU0 #HU0W #HU01
56   @(ex2_2_intro … HYW)
57   [2: 
58
59
60 axiom pippo_aux: ∀h,L,Z,U. ⦃h, L⦄ ⊢ Z : U → ∀Y,X. Z = ⓐY.X →
61                  ∀W,T. L ⊢ X ➡* ⓛW.T → ⦃h, L⦄ ⊢ Y : W.
62 #h #L #Z #U #H elim H -L -Z -U
63 [
64 |
65 |
66 |
67 |
68 | #L #V #W #T #U #HTU #_ #_ #IHUW #Y #X #H #W0 #T0 #HX destruct 
69   lapply (IHUW Y U ? ?) -IHUW -W // #T 
70   @(ex2_2_intro … HYW)
71   [2: 
72
73 axiom pippo: ∀h,L,V,X,U. ⦃h, L⦄ ⊢ ⓐV.X : U →
74              ∃∃W,T. L ⊢ X ➡* ⓛW.T & ⦃h, L⦄ ⊢ V : W.
75 #h #L #V #X #Y #H 
76
77 *)
78 (* NATIVE TYPE ASSIGNMENT ON TERMS ******************************************)
79
80 (* Properties on context-free parallel reduction for local environments ******)
81 (*
82 axiom nta_ltpr_cprs_conf: ∀h,L1,T1,U. ⦃h, L1⦄ ⊢ T1 : U → ∀L2. L1 ➡ L2 →
83                           ∀T2. L2 ⊢ T1 ➡* T2 → ⦃h, L2⦄ ⊢ T2 : U.
84 #h #L1 #T1 #U #H @(nta_ind_alt … H) -L1 -T1 -U
85 [ #L1 #k #L2 #_ #T2 #H
86   >(cprs_inv_sort1 … H) -H //
87 |
88 |
89 |
90 |
91 | #L1 #V1 #W1 #T1 #U1 #_ #_ #IHTU1 #IHUW1 #L2 #HL12 #T2 #H
92   elim (cprs_inv_appl1 … H) -H *
93   [ #V2 #T0 #HV12 #HT10 #H destruct
94     elim (nta_fwd_correct h L2 (ⓐV1.T1) (ⓐV1.U1) ?) [2: /3 width=2/ ] #U
95     @(nta_conv … (ⓐV2.U1)) (* /2 width=1/*) [ /4 width=2/] (**) (* explicit constructor, /5 width=5/ is too slow *)
96   | #V2 #W2 #T0 #HV12 #HT10 #HT02
97     lapply (IHTU1 … HL12 (ⓛW2.T0) ?) -IHTU1 /2 width=1/ -HT10 #H
98     elim (nta_inv_bind1 … H) -H #W #U0 #HW2 #HTU0 #HU01
99     elim (cpcs_inv_abst1 … HU01) -HU01 #W #U #HU1 #HU0
100     lapply (IHUW1 … HL12 (ⓐV2.ⓛW.U) ?) -IHUW1 -HL12 /2 width=1/ -HV12 #H
101     
102     
103     
104     elim (nta_fwd_pure1 … H) -H #W0 #U2 #HVU2 #H #HW01
105     elim (nta_inv_bind1 … H) -H #W3 #U3 #HW3 #HU3 #H
106     elim (cpcs_inv_abst1 … H) -H #W4 #U4  
107 *)      
108 (*
109 axiom nta_ltpr_tpr_conf: ∀h,L1,T1,U. ⦃h, L1⦄ ⊢ T1 : U → ∀L2. L1 ➡ L2 →
110                          ∀T2. T1 ➡ T2 → ⦃h, L2⦄ ⊢ T2 : U.
111 #h #L1 #T1 #U #H @(nta_ind_alt … H) -L1 -T1 -U
112 [ #L1 #k #L2 #_ #T2 #H
113   >(tpr_inv_atom1 … H) -H //
114 | #L1 #K1 #V1 #W #U #i #HLK1 #_ #HWU #IHV1 #L2 #HL12 #T2 #H
115   >(tpr_inv_atom1 … H) -T2
116   elim (ltpr_ldrop_conf … HLK1 … HL12) -HLK1 -HL12 #X #HLK2 #H
117   elim (ltpr_inv_pair1 … H) -H #K2 #V2 #HK12 #HV12 #H destruct /3 width=6/
118 | #L1 #K1 #W1 #V1 #U1 #i #HLK1 #HWV1 #HWU1 #IHWV1 #L2 #HL12 #T2 #H
119   >(tpr_inv_atom1 … H) -T2
120   elim (ltpr_ldrop_conf … HLK1 … HL12) -HLK1 -HL12 #X #HLK2 #H
121   elim (ltpr_inv_pair1 … H) -H #K2 #W2 #HK12 #HW12 #H destruct
122   lapply (ldrop_fwd_ldrop2 … HLK2) #HLK
123   elim (lift_total V1 0 (i+1)) #W #HW
124   lapply (nta_lift h … HLK … HWU1 … HW) /2 width=1/ -HLK -HW
125   elim (lift_total W2 0 (i+1)) #U2 #HWU2
126   lapply (tpr_lift … HW12 … HWU1 … HWU2) -HWU1 #HU12
127   @(nta_conv … U2) /2 width=1/ /3 width=6/ (**) (* explicit constructor, /3 width=6/ is too slow *)
128 | #I #L1 #V1 #W1 #T1 #U1 #_ #_ #IHVW1 #IHTU1 #L2 #HL12 #X #H
129   elim (tpr_inv_bind1 … H) -H *
130   [ #V2 #T0 #T2 #HV12 #HT10 #HT02 #H destruct
131     lapply (IHVW1 … HL12 … HV12) #HV2W1
132     lapply (IHVW1 L2 … V1 ?) // -IHVW1 #HWV1
133     lapply (IHTU1 (L2.ⓑ{I}V2) … HT10) -HT10 /2 width=1/ #HT0U1
134     lapply (IHTU1 (L2.ⓑ{I}V1) ? T1 ?) -IHTU1 // /2 width=1/ -HL12 #H
135     lapply (tps_lsubs_trans … HT02 (L2.ⓑ{I}V2) ?) -HT02 /2 width=1/ #HT02
136     lapply (nta_tps_conf … HT0U1 … HT02) -T0 #HT2U1
137     elim (nta_fwd_correct … H) -H #U2 #HU12
138     @(nta_conv … (ⓑ{I}V2.U1)) /2 width=2/ /3 width=1/ (**) (* explicit constructor, /4 width=6/ is too slow *)
139   | #T #HT1 #HTX #H destruct
140     lapply (IHVW1 … HL12 V1 ?) -IHVW1 // #HVW1
141     elim (lift_total X 0 1) #Y #HXY
142     lapply (tpr_lift … HTX … HT1 … HXY) -T #H
143     lapply (IHTU1 (L2.ⓓV1) … H) -T1 /2 width=1/ -L1 #H
144     elim (nta_fwd_correct … H) #T1 #HUT1
145     elim (nta_thin_conf … H L2 0 (0+1) ? ?) -H /2 width=1/ /3 width=1/ #T #U #HTU #H
146     normalize in ⊢ (??%??? → ?); #HU1
147     lapply (delift_inv_lift1_eq … H L2 … HXY) -Y /2 width=1/ #H destruct
148     @(nta_conv … U) // /2 width=2/
149   ]
150 | #L1 #V1 #W1 #T1 #U1 #_ #_ #IHVW1 #IHTU1 #L2 #HL12 #X #H
151   elim (tpr_inv_appl1 … H) -H *
152   [ #V2 #Y #HV12 #HY #H destruct
153     elim (tpr_inv_abst1 … HY) -HY #W2 #T2 #HW12 #HT12 #H destruct
154     lapply (IHTU1 L2 ? (ⓛW1.T1) ?) // #H
155     elim (nta_fwd_correct … H) -H #X #H
156     elim (nta_inv_bind1 … H) -H #W #U #HW #HU #_
157     @(nta_conv … (ⓐV2.ⓛW1.U1)) /4 width=2/ (**) (* explicit constructor, /5 width=5/ is too slow *)
158   | #V2 #W2 #T0 #T2 #HV12 #HT02 #H1 #H2 destruct
159     lapply (IHVW1 … HL12 … HV12) #HVW2
160     lapply (IHVW1 … HL12 V1 ?) -IHVW1 // #HV1W2
161     lapply (IHTU1 … HL12 (ⓛW2.T2) ?) -IHTU1 -HL12 /2 width=1/ -HT02 #H1
162     elim (nta_fwd_correct … H1) #T #H2
163     elim (nta_inv_bind1 … H1) -H1 #W #U2 #HW2 #HTU2 #H
164     elim (cpcs_inv_abst … H Abst W2) -H #_ #HU21
165     elim (nta_inv_bind1 … H2) -H2 #W0 #U0 #_ #H #_ -T -W0
166     lapply (lsubn_nta_trans … HTU2 (L2.ⓓV2) ?) -HTU2 /2 width=1/ #HTU2
167     @(nta_conv … (ⓓV2.U2)) /2 width=2/ /3 width=2/ (**) (* explicit constructor, /4 width=5/ is too slow *)
168   | #V0 #V2 #W0 #W2 #T0 #T2 #_ #_ #_ #_ #H destruct
169   ]
170 | #L1 #V1 #W1 #T1 #U1 #_ #_ #IHTU1 #IHUW1 #L2 #HL12 #X #H
171   elim (tpr_inv_appl1 … H) -H *
172   [ #V2 #T2 #HV12 #HT12 #H destruct
173     elim (nta_fwd_correct h L2 (ⓐV1.T1) (ⓐV1.U1) ?) [2: /3 width=2/ ] #U
174     @(nta_conv … (ⓐV2.U1)) /2 width=1/ /4 width=2/ (**) (* explicit constructor, /5 width=5/ is too slow *)
175   | #V2 #W2 #T0 #T2 #HV12 #HT02 #H1 #H2 destruct
176     lapply (IHTU1 … HL12 (ⓛW2.T2) ?) -IHTU1 /2 width=1/ -T0 #H
177     elim (nta_inv_bind1 … H) -H #W #U2 #HW2 #HTU2 #HU21
178     lapply (IHUW1 … HL12 (ⓐV2.U1) ?) -IHUW1 -HL12 /2 width=1/ #H
179     elim (nta_inv_pure1 … H) -H #V0 #U0 #U #HV20 #HU10 #HU0W1 #HU0
180     @(nta_conv … (ⓓV2.U2))
181     [2: @nta_bind //
182         @(lsubn_nta_trans … HTU2) @lsubn_abbr //
183 (*
184     lapply (IH … HV1 … HL12 … HV12) -HV1 -HV12 /width=5/ #HB
185     lapply (IH … HB0  … HL12 W2 ?) -HB0 /width=5/ #HB0
186     lapply (IH … HA0 … (L2.ⓛW2) … HT02) -IH -HA0 -HT02 /width=5/ -T0 /2 width=1/ -L1 -V1 /4 width=7/
187 *)
188 *)
189 (*
190 axiom pippo: ⦃h, L⦄ ⊢ ⓐV.X : Y →
191              ∃∃W,T. L ⊢ X ➡* ⓛW.T & ⦃h, L⦄ ⊢ ⓐV : W.
192
193 *)
194 (* SEGMENT 2
195 | #L1 #T1 #U1 #W1 #_ #_ #IHTU1 #IHUW1 #L2 #d #e #HL12 #X #H
196   elim (tpss_inv_flat1 … H) -H #U2 #T2 #HU12 #HT12 #H destruct
197   lapply (cpr_tpss … HU12) /4 width=4/
198 | #L1 #T1 #U11 #U12 #U #_ #HU112 #_ #IHTU11 #IHU12 #L2 #d #e #HL12 #T2 #HT12
199   @(nta_conv … U11) /2 width=5/ (**) (* explicot constructor, /3 width=7/ is too slow *)
200 ]
201 qed.
202 *)
203
204 (* SEGMENT 3
205 fact nta_ltpr_tpr_conf_aux: ∀h,L,T,L1,T1,U. ⦃h, L1⦄ ⊢ T1 : U → L = L1 → T = T1 →
206                             ∀L2. L1 ➡ L2 → ∀T2. T1 ➡ T2 → ⦃h, L2⦄ ⊢ T2 : U.
207   
208   
209   | #V0 #V2 #W0 #W2 #T0 #T2 #HV10 #HW02 #HT02 #HV02 #H1 #H2 destruct
210     elim (nta_inv_abbr … HT1) -HT1 #B0 #HW0 #HT0
211     lapply (IH … HW0  … HL12 … HW02) -HW0 /width=5/ #HW2
212     lapply (IH … HV1 … HL12 … HV10) -HV1 -HV10 /width=5/ #HV0
213     lapply (IH … HT0 … (L2.ⓓW2) … HT02) -IH -HT0 -HT02 /width=5/ -V1 -T0 /2 width=1/ -L1 -W0 #HT2
214     @(nta_abbr … HW2) -HW2
215     @(nta_appl … HT2) -HT2 /3 width=7/ (**) (* explict constructors, /5 width=7/ is too slow *)
216   ]
217 | #L1 #V1 #T1 #A #HV1 #HT1 #H1 #H2 #L2 #HL12 #X #H destruct
218   elim (tpr_inv_cast1 … H) -H
219   [ * #V2 #T2 #HV12 #HT12 #H destruct
220     lapply (IH … HV1 … HL12 … HV12) -HV1 -HV12 /width=5/ #HV2
221     lapply (IH … HT1 … HL12 … HT12) -IH -HT1 -HL12 -HT12 /width=5/ -L1 -V1 -T1 /2 width=1/
222   | -HV1 #HT1X
223      lapply (IH … HT1 … HL12 … HT1X) -IH -HT1 -HL12 -HT1X /width=5/
224   ]
225 ]
226 qed.
227
228 /2 width=9/ qed.
229
230 axiom nta_ltpr_conf: ∀L1,T,A. L1 ⊢ T : A → ∀L2. L1 ➡ L2 → L2 ⊢ T : A.
231 /2 width=5/ qed.
232
233 axiom nta_tpr_conf: ∀L,T1,A. L ⊢ T1 : A → ∀T2. T1 ➡ T2 → L ⊢ T2 : A.
234 /2 width=5/ qed.
235 *)