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_alt.ma".
17 (* NATIVE TYPE ASSIGNMENT ON TERMS ******************************************)
19 (* Advanced inversion lemmas ************************************************)
21 fact nta_inv_lref1_aux: ∀h,L,T,U. ⦃h, L⦄ ⊢ T : U → ∀j. T = #j →
22 (∃∃K,V,W,U0. ⇩[0, j] L ≡ K. ⓓV & ⦃h, K⦄ ⊢ V : W &
23 ⇧[0, j + 1] W ≡ U0 & L ⊢ U0 ⬌* U
25 (∃∃K,W,V,U0. ⇩[0, j] L ≡ K. ⓛW & ⦃h, K⦄ ⊢ W : V &
26 ⇧[0, j + 1] W ≡ U0 & L ⊢ U0 ⬌* U
28 #h #L #T #U #H elim H -L -T -U
29 [ #L #k #j #H destruct
30 | #L #K #V #W #U #i #HLK #HVW #HWU #_ #j #H destruct /3 width=8/
31 | #L #K #W #V #U #i #HLK #HWV #HWU #_ #j #H destruct /3 width=8/
32 | #I #L #V #W #T #U #_ #_ #_ #_ #j #H destruct
33 | #L #V #W #T #U #_ #_ #_ #_ #j #H destruct
34 | #L #V #W #T #U #_ #_ #_ #_ #j #H destruct
35 | #L #T #U #_ #_ #j #H destruct
36 | #L #T #U1 #U2 #V2 #_ #HU12 #_ #IHTU1 #_ #j #H destruct
37 elim (IHTU1 ??) -IHTU1 [4: // |2: skip ] * #K #V #W #U0 #HLK #HVW #HWU0 #HU01
38 lapply (cpcs_trans … HU01 … HU12) -U1 /3 width=8/
42 (* Basic_1: was ty3_gen_lref *)
43 lemma nta_inv_lref1: ∀h,L,U,i. ⦃h, L⦄ ⊢ #i : U →
44 (∃∃K,V,W,U0. ⇩[0, i] L ≡ K. ⓓV & ⦃h, K⦄ ⊢ V : W &
45 ⇧[0, i + 1] W ≡ U0 & L ⊢ U0 ⬌* U
47 (∃∃K,W,V,U0. ⇩[0, i] L ≡ K. ⓛW & ⦃h, K⦄ ⊢ W : V &
48 ⇧[0, i + 1] W ≡ U0 & L ⊢ U0 ⬌* U
52 (* Advanced forvard lemmas **************************************************)
54 fact nta_fwd_pure1_aux: ∀h,L,T,U. ⦃h, L⦄ ⊢ T : U → ∀X,Y. T = ⓐY.X →
55 ∃∃V,W. ⦃h, L⦄ ⊢ Y : W & ⦃h, L⦄ ⊢ X : V & L ⊢ ⓐY.V ⬌* U.
56 #h #L #T #U #H elim H -L -T -U
57 [ #L #k #X #Y #H destruct
58 | #L #K #V #W #U #i #_ #_ #_ #_ #X #Y #H destruct
59 | #L #K #W #V #U #i #_ #_ #_ #_ #X #Y #H destruct
60 | #I #L #V #W #T #U #_ #_ #_ #_ #X #Y #H destruct
61 | #L #V #W #T #U #HVW #HTU #_ #_ #X #Y #H destruct /2 width=3/
62 | #L #V #W #T #U #HTU #_ #_ #IHUW #X #Y #H destruct
63 elim (IHUW U Y ?) -IHUW // /2 width=3/
64 | #L #T #U #_ #_ #X #Y #H destruct
65 | #L #T #U1 #U2 #V2 #_ #HU12 #_ #IHTU1 #_ #X #Y #H destruct
66 elim (IHTU1 ???) -IHTU1 [4: // |2,3: skip ] #V #W #HYW #HXV #HU1
67 lapply (cpcs_trans … HU1 … HU12) -U1 /2 width=3/
71 lemma nta_fwd_pure1: ∀h,L,X,Y,U. ⦃h, L⦄ ⊢ ⓐY.X : U →
72 ∃∃V,W. ⦃h, L⦄ ⊢ Y : W & ⦃h, L⦄ ⊢ X : V & L ⊢ ⓐY.V ⬌* U.
75 (* Properties on relocation *************************************************)
77 (* Basic_1: was: ty3_lift *)
78 (* Basic_2A1: was: ntaa_lift *)
79 lemma nta_lift: ∀h,L1,T1,U1. ⦃h, L1⦄ ⊢ T1 : U1 → ∀L2,d,e. ⇩[d, e] L2 ≡ L1 →
80 ∀T2. ⇧[d, e] T1 ≡ T2 → ∀U2. ⇧[d, e] U1 ≡ U2 → ⦃h, L2⦄ ⊢ T2 : U2.
81 /4 width=9 by ntaa_nta, nta_ntaa, ntaa_lift/ qed.