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/cnv_drops.ma".
16 include "basic_2/dynamic/nta.ma".
18 (* NATIVE TYPE ASSIGNMENT FOR TERMS *****************************************)
20 (* Advanced properties ******************************************************)
22 lemma nta_ldef (h) (a) (G) (K):
23 ∀V,W. ❨G,K❩ ⊢ V :[h,a] W →
24 ∀U. ⇧[1] W ≘ U → ❨G,K.ⓓV❩ ⊢ #0 :[h,a] U.
25 #h #a #G #K #V #W #H #U #HWU
26 elim (cnv_inv_cast … H) -H #X #HW #HV #HWX #HVX
27 lapply (cnv_lifts … HW (Ⓣ) … (K.ⓓV) … HWU) -HW
28 [ /3 width=3 by drops_refl, drops_drop/ ] #HU
29 elim (cpms_lifts_sn … HWX … (Ⓣ) … (K.ⓓV) … HWU) -W
30 [| /3 width=3 by drops_refl, drops_drop/ ] #XW #HXW #HUXW
31 /3 width=5 by cnv_zero, cnv_cast, cpms_delta/
34 lemma nta_ldec_cnv (h) (a) (G) (K):
35 ∀W. ❨G,K❩ ⊢ W ![h,a] →
36 ∀U. ⇧[1] W ≘ U → ❨G,K.ⓛW❩ ⊢ #0 :[h,a] U.
37 #h #a #G #K #W #HW #U #HWU
38 lapply (cnv_lifts … HW (Ⓣ) … (K.ⓛW) … HWU)
39 /3 width=5 by cnv_zero, cnv_cast, cpms_ell, drops_refl, drops_drop/
42 lemma nta_lref (h) (a) (I) (G) (K):
43 ∀T,i. ❨G,K❩ ⊢ #i :[h,a] T →
44 ∀U. ⇧[1] T ≘ U → ❨G,K.ⓘ[I]❩ ⊢ #(↑i) :[h,a] U.
45 #h #a #I #G #K #T #i #H #U #HTU
46 elim (cnv_inv_cast … H) -H #X #HT #Hi #HTX #H2
47 lapply (cnv_lifts … HT (Ⓣ) … (K.ⓘ[I]) … HTU) -HT
48 [ /3 width=3 by drops_refl, drops_drop/ ] #HU
49 lapply (cnv_lifts … Hi (Ⓣ) (𝐔❨1❩) (K.ⓘ[I]) ???) -Hi
50 [4:|*: /3 width=3 by drops_refl, drops_drop/ ] #Hi
51 elim (cpms_lifts_sn … HTX … (Ⓣ) … (K.ⓘ[I]) … HTU) -T
52 [| /3 width=3 by drops_refl, drops_drop/ ] #XU #HXU #HUXU
53 /3 width=5 by cnv_cast, cpms_lref/
56 (* Properties with generic slicing for local environments *******************)
58 lemma nta_lifts_sn (h) (a) (G): d_liftable2_sn … lifts (nta a h G).
59 #h #a #G #K #T1 #T2 #H #b #f #L #HLK #U1 #HTU1
60 elim (cnv_inv_cast … H) -H #X #HT2 #HT1 #HT2X #HT1X
61 elim (lifts_total T2 f) #U2 #HTU2
62 lapply (cnv_lifts … HT2 … HLK … HTU2) -HT2 #HU2
63 lapply (cnv_lifts … HT1 … HLK … HTU1) -HT1 #HU1
64 elim (cpms_lifts_sn … HT2X … HLK … HTU2) -HT2X #X2 #HX2 #HUX2
65 elim (cpms_lifts_sn … HT1X … HLK … HTU1) -T1 #X1 #HX1 #HUX1
66 lapply (lifts_mono … HX2 … HX1) -K -X #H destruct
67 /3 width=6 by cnv_cast, ex2_intro/
70 (* Basic_1: was: ty3_lift *)
71 (* Basic_2A1: was: nta_lift ntaa_lift *)
72 lemma nta_lifts_bi (h) (a) (G): d_liftable2_bi … lifts (nta a h G).
73 /3 width=12 by nta_lifts_sn, d_liftable2_sn_bi, lifts_mono/ qed-.
75 (* Basic_1: was by definition: ty3_abbr *)
76 (* Basic_2A1: was by definition: nta_ldef ntaa_ldef *)
77 lemma nta_ldef_drops (h) (a) (G) (K) (L) (i):
78 ∀V,W. ❨G,K❩ ⊢ V :[h,a] W →
79 ∀U. ⇧[↑i] W ≘ U → ⇩[i] L ≘ K.ⓓV → ❨G,L❩ ⊢ #i :[h,a] U.
80 #h #a #G #K #L #i #V #W #HVW #U #HWU #HLK
81 elim (lifts_split_trans … HWU (𝐔❨1❩) (𝐔❨i❩)) [| // ] #X #HWX #HXU
82 /3 width=9 by nta_lifts_bi, nta_ldef/
85 lemma nta_ldec_drops_cnv (h) (a) (G) (K) (L) (i):
86 ∀W. ❨G,K❩ ⊢ W ![h,a] →
87 ∀U. ⇧[↑i] W ≘ U → ⇩[i] L ≘ K.ⓛW → ❨G,L❩ ⊢ #i :[h,a] U.
88 #h #a #G #K #L #i #W #HW #U #HWU #HLK
89 elim (lifts_split_trans … HWU (𝐔❨1❩) (𝐔❨i❩)) [| // ] #X #HWX #HXU
90 /3 width=9 by nta_lifts_bi, nta_ldec_cnv/