matita/matita/contribs/lambdadelta/basic_2/dynamic/nta.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/notation/relations/colon_6.ma".
  16 include "basic_2/dynamic/cnv.ma".
  17
  18 (* NATIVE TYPE ASSIGNMENT FOR TERMS *****************************************)
  19
  20 definition nta (h) (a): relation4 genv lenv term term ≝
  21            λG,L,T,U. ❨G,L❩ ⊢ ⓝU.T ![h,a].
  22
  23 interpretation "native type assignment (term)"
  24   'Colon h a G L T U = (nta h a G L T U).
  25
  26 (* Basic properties *********************************************************)
  27
  28 (* Basic_1: was by definition: ty3_sort *)
  29 (* Basic_2A1: was by definition: nta_sort ntaa_sort *)
  30 lemma nta_sort (h) (a) (G) (L): ∀s. ❨G,L❩ ⊢ ⋆s :[h,a] ⋆(⫯[h]s).
  31 #h #a #G #L #s /2 width=3 by cnv_sort, cnv_cast, cpms_sort/
  32 qed.
  33
  34 lemma nta_bind_cnv (h) (a) (G) (K):
  35       ∀V. ❨G,K❩ ⊢ V ![h,a] →
  36       ∀I,T,U. ❨G,K.ⓑ[I]V❩ ⊢ T :[h,a] U →
  37       ∀p. ❨G,K❩ ⊢ ⓑ[p,I]V.T :[h,a] ⓑ[p,I]V.U.
  38 #h #a #G #K #V #HV #I #T #U #H #p
  39 elim (cnv_inv_cast … H) -H #X #HU #HT #HUX #HTX
  40 /3 width=5 by cnv_bind, cnv_cast, cpms_bind_dx/
  41 qed.
  42
  43 (* Basic_2A1: was by definition: nta_cast *)
  44 lemma nta_cast (h) (a) (G) (L):
  45       ∀T,U. ❨G,L❩ ⊢ T :[h,a] U → ❨G,L❩ ⊢ ⓝU.T :[h,a] U.
  46 #h #a #G #L #T #U #H
  47 elim (cnv_inv_cast … H) #X #HU #HT #HUX #HTX
  48 /3 width=3 by cnv_cast, cpms_eps/
  49 qed.
  50
  51 (* Basic_1: was by definition: ty3_cast *)
  52 lemma nta_cast_old (h) (a) (G) (L):
  53       ∀T0,T1. ❨G,L❩ ⊢ T0 :[h,a] T1 →
  54       ∀T2. ❨G,L❩ ⊢ T1 :[h,a] T2 → ❨G,L❩ ⊢ ⓝT1.T0 :[h,a] ⓝT2.T1.
  55 #h #a #G #L #T0 #T1 #H1 #T2 #H2
  56 elim (cnv_inv_cast … H1) #X1 #_ #_ #HTX1 #HTX01
  57 elim (cnv_inv_cast … H2) #X2 #_ #_ #HTX2 #HTX12
  58 /3 width=3 by cnv_cast, cpms_eps/
  59 qed.
  60
  61 (* Basic inversion lemmas ***************************************************)
  62
  63 lemma nta_inv_gref_sn (h) (a) (G) (L):
  64       ∀X2,l. ❨G,L❩ ⊢ §l :[h,a] X2 → ⊥.
  65 #h #a #G #L #X2 #l #H
  66 elim (cnv_inv_cast … H) -H #X #_ #H #_ #_
  67 elim (cnv_inv_gref … H)
  68 qed-.
  69
  70 (* Basic_forward lemmas *****************************************************)
  71
  72 lemma nta_fwd_cnv_sn (h) (a) (G) (L):
  73       ∀T,U. ❨G,L❩ ⊢ T :[h,a] U → ❨G,L❩ ⊢ T ![h,a].
  74 #h #a #G #L #T #U #H
  75 elim (cnv_inv_cast … H) -H #X #_ #HT #_ #_ //
  76 qed-.
  77
  78 (* Note: this is nta_fwd_correct_cnv *)
  79 lemma nta_fwd_cnv_dx (h) (a) (G) (L):
  80       ∀T,U. ❨G,L❩ ⊢ T :[h,a] U → ❨G,L❩ ⊢ U ![h,a].
  81 #h #a #G #L #T #U #H
  82 elim (cnv_inv_cast … H) -H #X #HU #_ #_ #_ //
  83 qed-.
  84
  85 (* Basic_1: removed theorems 4:
  86             ty3_getl_subst0 ty3_fsubst0 ty3_csubst0 ty3_subst0
  87 *)
  88 (* Basic_2A1: removed theorems 2:
  89    ntaa_nta nta_ntaa
  90 *)