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/notation/relations/colon_5.ma".
  17 include "basic_2/notation/relations/colonstar_5.ma".
  18 include "basic_2/dynamic/cnv.ma".
  19
  20 (* NATIVE TYPE ASSIGNMENT FOR TERMS *****************************************)
  21
  22 definition nta (a) (h): relation4 genv lenv term term ≝
  23                         λG,L,T,U. ⦃G,L⦄ ⊢ ⓝU.T ![a,h].
  24
  25 interpretation "native type assignment (term)"
  26    'Colon a h G L T U = (nta a h G L T U).
  27
  28 interpretation "restricted native type assignment (term)"
  29    'Colon h G L T U = (nta (yinj (S (S O))) h G L T U).
  30
  31 interpretation "extended native type assignment (term)"
  32    'ColonStar h G L T U = (nta Y h G L T U).
  33
  34 (* Basic properties *********************************************************)
  35
  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] ⋆(next h s).
  39 #a #h #G #L #s /2 width=3 by cnv_sort, cnv_cast, cpms_sort/
  40 qed.
  41
  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/
  49 qed.
  50
  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.
  54 #a #h #G #L #T #U #H
  55 elim (cnv_inv_cast … H) #X #HU #HT #HUX #HTX
  56 /3 width=3 by cnv_cast, cpms_eps/
  57 qed.
  58
  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/
  67 qed.
  68
  69 (* Basic inversion lemmas ***************************************************)
  70
  71 lemma nta_inv_gref_sn (a) (h) (G) (L):
  72       ∀X2,l. ⦃G,L⦄ ⊢ §l :[a,h] X2 → ⊥.
  73 #a #h #G #L #X2 #l #H
  74 elim (cnv_inv_cast … H) -H #X #_ #H #_ #_
  75 elim (cnv_inv_gref … H)
  76 qed-.
  77
  78 (* Basic_forward lemmas *****************************************************)
  79
  80 lemma nta_fwd_cnv_sn (a) (h) (G) (L):
  81                      ∀T,U. ⦃G,L⦄ ⊢ T :[a,h] U → ⦃G,L⦄ ⊢ T ![a,h].
  82 #a #h #G #L #T #U #H
  83 elim (cnv_inv_cast … H) -H #X #_ #HT #_ #_ //
  84 qed-.
  85
  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].
  89 #a #h #G #L #T #U #H
  90 elim (cnv_inv_cast … H) -H #X #HU #_ #_ #_ //
  91 qed-.
  92
  93 (* Basic_1: removed theorems 4:
  94             ty3_getl_subst0 ty3_fsubst0 ty3_csubst0 ty3_subst0
  95 *)
  96 (* Basic_2A1: removed theorems 2:
  97    ntaa_nta nta_ntaa
  98 *)