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 "basic_2/dynamic/nta_preserve.ma".
16 include "basic_2/i_dynamic/ntas_preserve.ma".
18 (* ITERATED NATIVE TYPE ASSIGNMENT FOR TERMS ********************************)
20 (* Advanced properties of native validity for terms *************************)
22 lemma cnv_appl_ntas_ge (h) (a) (G) (L):
23 ∀m,n. m ≤ n → ad a n → ∀V,W. ❨G,L❩ ⊢ V :[h,a] W →
24 ∀p,T,U. ❨G,L❩ ⊢ T :*[h,a,m] ⓛ[p]W.U → ❨G,L❩ ⊢ ⓐV.T ![h,a].
25 #h #a #G #L #m #n #Hmn #Hn #V #W #HVW #p #T #U #HTU
26 elim (cnv_inv_cast … HVW) -HVW #W0 #HW #HV #HW0 #HVW0
27 elim HTU -HTU #U0 #H #HT #HU0 #HTU0
28 elim (cnv_cpms_conf … H … HU0 0 (ⓛ[p]W0.U)) -H -HU0
29 [| /2 width=1 by cpms_bind/ ] -HW0 <minus_n_O #X0 #HUX0 #H
30 elim (cpms_inv_abst_sn … H) -H #W1 #U1 #HW01 #_ #H destruct
31 /3 width=13 by cnv_appl_ge, cpms_cprs_trans/
34 (* Advanced inversion lemmas of native validity for terms *******************)
36 lemma cnv_inv_appl_ntas (h) (a) (G) (L):
37 ∀V,T. ❨G,L❩ ⊢ ⓐV.T ![h,a] →
38 ∃∃n,p,W,T,U. ad a n & ❨G,L❩ ⊢ V :[h,a] W & ❨G,L❩ ⊢ T :*[h,a,n] ⓛ[p]W.U.
40 elim (cnv_inv_appl … H) -H #n #p #W #U #Hn #HV #HT #HVW #HTU
41 /3 width=9 by cnv_cpms_nta, cnv_cpms_ntas, ex3_5_intro/
44 (* Properties with native type assignment for terms *************************)
46 lemma nta_ntas (h) (a) (G) (L):
47 ∀T,U. ❨G,L❩ ⊢ T :[h,a] U → ❨G,L❩ ⊢ T :*[h,a,1] U.
49 elim (cnv_inv_cast … H) -H /2 width=3 by ntas_intro/
52 lemma ntas_step_sn (h) (a) (G) (L):
53 ∀T1,T. ❨G,L❩ ⊢ T1 :[h,a] T →
54 ∀n,T2. ❨G,L❩ ⊢ T :*[h,a,n] T2 → ❨G,L❩ ⊢ T1 :*[h,a,↑n] T2.
55 #h #a #G #L #T1 #T #H #n #T2 * #X2 #HT2 #HT #H1TX2 #H2TX2
56 elim (cnv_inv_cast … H) -H #X1 #_ #HT1 #H1TX1 #H2TX1
57 elim (cnv_cpms_conf … HT … H1TX1 … H2TX2) -T <minus_n_O <minus_O_n <plus_SO_sn #X #HX1 #HX2
58 /3 width=5 by ntas_intro, cprs_trans, cpms_trans/
61 lemma ntas_step_dx (h) (a) (G) (L):
62 ∀n,T1,T. ❨G,L❩ ⊢ T1 :*[h,a,n] T →
63 ∀T2. ❨G,L❩ ⊢ T :[h,a] T2 → ❨G,L❩ ⊢ T1 :*[h,a,↑n] T2.
64 #h #a #G #L #n #T1 #T * #X1 #HT #HT1 #H1TX1 #H2TX1 #T2 #H
65 elim (cnv_inv_cast … H) -H #X2 #HT2 #_ #H1TX2 #H2TX2
66 elim (cnv_cpms_conf … HT … H1TX1 … H2TX2) -T <minus_n_O <minus_O_n <plus_SO_dx #X #HX1 #HX2
67 /3 width=5 by ntas_intro, cprs_trans, cpms_trans/
70 lemma nta_appl_ntas_zero (h) (a) (G) (L): ad a 0 →
71 ∀V,W. ❨G,L❩ ⊢ V :[h,a] W → ∀p,T,U0. ❨G,L❩ ⊢ T :*[h,a,0] ⓛ[p]W.U0 →
72 ∀U. ❨G,L.ⓛW❩ ⊢ U0 :[h,a] U → ❨G,L❩ ⊢ ⓐV.T :[h,a] ⓐV.ⓛ[p]W.U.
73 #h #a #G #L #Ha #V #W #HVW #p #T #U0 #HTU0 #U #HU0
74 lapply (nta_fwd_cnv_dx … HVW) #HW
75 lapply (nta_bind_cnv … HW … HU0 p) -HW -HU0 #HU0
76 elim (ntas_step_dx … HTU0 … HU0) -HU0 #X #HU #_ #HUX #HTX
77 /4 width=9 by cnv_appl_ntas_ge, ntas_refl, cnv_cast, cpms_appl_dx/
80 lemma nta_appl_ntas_pos (h) (a) (n) (G) (L): ad a (↑n) →
81 ∀V,W. ❨G,L❩ ⊢ V :[h,a] W → ∀T,U. ❨G,L❩ ⊢ T :[h,a] U →
82 ∀p,U0. ❨G,L❩ ⊢ U :*[h,a,n] ⓛ[p]W.U0 → ❨G,L❩ ⊢ ⓐV.T :[h,a] ⓐV.U.
83 #h #a #n #G #L #Ha #V #W #HVW #T #U #HTU #p #U0 #HU0
84 elim (cnv_inv_cast … HTU) #X #_ #_ #HUX #HTX
85 /4 width=11 by ntas_step_sn, cnv_appl_ntas_ge, cnv_cast, cpms_appl_dx/
88 (* Inversion lemmas with native type assignment for terms *******************)
90 lemma ntas_inv_nta (h) (a) (G) (L):
91 ∀T,U. ❨G,L❩ ⊢ T :*[h,a,1] U → ❨G,L❩ ⊢ T :[h,a] U.
93 * /2 width=3 by cnv_cast/
96 (* Note: this follows from ntas_inv_appl_sn *)
97 lemma nta_inv_appl_sn_ntas (h) (a) (G) (L) (V) (T):
98 ∀X. ❨G,L❩ ⊢ ⓐV.T :[h,a] X →
99 ∨∨ ∃∃p,W,U,U0. ad a 0 & ❨G,L❩ ⊢ V :[h,a] W & ❨G,L❩ ⊢ T :*[h,a,0] ⓛ[p]W.U0 & ❨G,L.ⓛW❩ ⊢ U0 :[h,a] U & ❨G,L❩ ⊢ ⓐV.ⓛ[p]W.U ⬌*[h] X & ❨G,L❩ ⊢ X ![h,a]
100 | ∃∃n,p,W,U,U0. ad a (↑n) & ❨G,L❩ ⊢ V :[h,a] W & ❨G,L❩ ⊢ T :[h,a] U & ❨G,L❩ ⊢ U :*[h,a,n] ⓛ[p]W.U0 & ❨G,L❩ ⊢ ⓐV.U ⬌*[h] X & ❨G,L❩ ⊢ X ![h,a].
101 #h #a #G #L #V #T #X #H
102 (* Note: insert here: alternate proof in ntas_nta.etc *)
103 elim (cnv_inv_cast … H) -H #X0 #HX #HVT #HX0 #HTX0
104 elim (cnv_inv_appl … HVT) #n #p #W #U0 #Ha #HV #HT #HVW #HTU0
105 elim (eq_or_gt n) #Hn destruct
106 [ elim (cnv_fwd_cpms_abst_dx_le … HT … HTU0 1) [| // ] <minus_n_O #U #H #HU0
107 lapply (cpms_appl_dx … V V … H) [ // ] -H #H
108 elim (cnv_cpms_conf … HVT … HTX0 … H) -HVT -HTX0 -H <minus_n_n #X1 #HX01 #HUX1
109 lapply (cpms_trans … HX0 … HX01) -X0 #HX1
110 lapply (cprs_div … HUX1 … HX1) -X1 #HUX
111 lapply (cnv_cpms_trans … HT … HTU0) #H
112 elim (cnv_inv_bind … H) -H #_ #HU0
113 /4 width=8 by cnv_cpms_ntas, cnv_cpms_nta, ex6_4_intro, or_introl/
114 | >(plus_minus_m_m_commutative … Hn) in HTU0; #H
115 elim (cpms_inv_plus … H) -H #U #HTU #HU0
116 lapply (cpms_appl_dx … V V … HTU) [ // ] #H
117 elim (cnv_cpms_conf … HVT … HTX0 … H) -HVT -HTX0 -H <minus_n_n #X1 #HX01 #HUX1
118 lapply (cpms_trans … HX0 … HX01) -X0 #HX1
119 lapply (cprs_div … HUX1 … HX1) -X1 #HUX
120 <(S_pred … Hn) in Ha; -Hn #Ha
121 /5 width=10 by cnv_cpms_ntas, cnv_cpms_nta, cnv_cpms_trans, ex6_5_intro, or_intror/