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/notation/relations/colon_6.ma".
16 include "basic_2/notation/relations/colon_5.ma".
17 include "basic_2/notation/relations/colonstar_5.ma".
18 include "basic_2/dynamic/cnv.ma".
20 (* NATIVE TYPE ASSIGNMENT FOR TERMS *****************************************)
22 definition nta (a) (h): relation4 genv lenv term term ≝
23 λG,L,T,U. ⦃G,L⦄ ⊢ ⓝU.T ![a,h].
25 interpretation "native type assignment (term)"
26 'Colon a h G L T U = (nta a h G L T U).
28 interpretation "restricted native type assignment (term)"
29 'Colon h G L T U = (nta (ac_eq (S O)) h G L T U).
31 interpretation "extended native type assignment (term)"
32 'ColonStar h G L T U = (nta ac_top h G L T U).
34 (* Basic properties *********************************************************)
36 (* Basic_1: was by definition: ty3_sort *)
37 (* Basic_2A1: was by definition: nta_sort ntaa_sort *)
38 lemma nta_sort (a) (h) (G) (L) (s): ⦃G,L⦄ ⊢ ⋆s :[a,h] ⋆(⫯[h]s).
39 #a #h #G #L #s /2 width=3 by cnv_sort, cnv_cast, cpms_sort/
42 lemma nta_bind_cnv (a) (h) (G) (K):
43 ∀V. ⦃G,K⦄ ⊢ V ![a,h] →
44 ∀I,T,U. ⦃G,K.ⓑ{I}V⦄ ⊢ T :[a,h] U →
45 ∀p. ⦃G,K⦄ ⊢ ⓑ{p,I}V.T :[a,h] ⓑ{p,I}V.U.
46 #a #h #G #K #V #HV #I #T #U #H #p
47 elim (cnv_inv_cast … H) -H #X #HU #HT #HUX #HTX
48 /3 width=5 by cnv_bind, cnv_cast, cpms_bind_dx/
51 (* Basic_2A1: was by definition: nta_cast *)
52 lemma nta_cast (a) (h) (G) (L):
53 ∀T,U. ⦃G,L⦄ ⊢ T :[a,h] U → ⦃G,L⦄ ⊢ ⓝU.T :[a,h] U.
55 elim (cnv_inv_cast … H) #X #HU #HT #HUX #HTX
56 /3 width=3 by cnv_cast, cpms_eps/
59 (* Basic_1: was by definition: ty3_cast *)
60 lemma nta_cast_old (a) (h) (G) (L):
61 ∀T0,T1. ⦃G,L⦄ ⊢ T0 :[a,h] T1 →
62 ∀T2. ⦃G,L⦄ ⊢ T1 :[a,h] T2 → ⦃G,L⦄ ⊢ ⓝT1.T0 :[a,h] ⓝT2.T1.
63 #a #h #G #L #T0 #T1 #H1 #T2 #H2
64 elim (cnv_inv_cast … H1) #X1 #_ #_ #HTX1 #HTX01
65 elim (cnv_inv_cast … H2) #X2 #_ #_ #HTX2 #HTX12
66 /3 width=3 by cnv_cast, cpms_eps/
69 (* Basic inversion lemmas ***************************************************)
71 lemma nta_inv_gref_sn (a) (h) (G) (L):
72 ∀X2,l. ⦃G,L⦄ ⊢ §l :[a,h] X2 → ⊥.
74 elim (cnv_inv_cast … H) -H #X #_ #H #_ #_
75 elim (cnv_inv_gref … H)
78 (* Basic_forward lemmas *****************************************************)
80 lemma nta_fwd_cnv_sn (a) (h) (G) (L):
81 ∀T,U. ⦃G,L⦄ ⊢ T :[a,h] U → ⦃G,L⦄ ⊢ T ![a,h].
83 elim (cnv_inv_cast … H) -H #X #_ #HT #_ #_ //
86 (* Note: this is nta_fwd_correct_cnv *)
87 lemma nta_fwd_cnv_dx (a) (h) (G) (L):
88 ∀T,U. ⦃G,L⦄ ⊢ T :[a,h] U → ⦃G,L⦄ ⊢ U ![a,h].
90 elim (cnv_inv_cast … H) -H #X #HU #_ #_ #_ //
93 (* Basic_1: removed theorems 4:
94 ty3_getl_subst0 ty3_fsubst0 ty3_csubst0 ty3_subst0
96 (* Basic_2A1: removed theorems 2: