matita/matita/contribs/lambdadelta/basic_2/i_dynamic/ntas.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/colonstar_7.ma".
  16 include "basic_2/dynamic/cnv.ma".
  17
  18 (* ITERATED NATIVE TYPE ASSIGNMENT FOR TERMS ********************************)
  19
  20 definition ntas (h) (a) (n) (G) (L): relation term ≝ λT,U.
  21            ∃∃U0. ❨G,L❩ ⊢ U ![h,a] & ❨G,L❩ ⊢ T ![h,a] & ❨G,L❩ ⊢ U ➡*[h,0] U0 & ❨G,L❩ ⊢ T ➡*[h,n] U0.
  22
  23 interpretation "iterated native type assignment (term)"
  24    'ColonStar h a n G L T U = (ntas h a n G L T U).
  25
  26 (* Basic properties *********************************************************)
  27
  28 lemma ntas_intro (h) (a) (n) (G) (L):
  29       ∀U. ❨G,L❩ ⊢ U ![h,a] → ∀T. ❨G,L❩ ⊢ T ![h,a] →
  30       ∀U0. ❨G,L❩ ⊢ U ➡*[h,0] U0 → ❨G,L❩ ⊢ T ➡*[h,n] U0 → ❨G,L❩ ⊢ T :*[h,a,n] U.
  31 /2 width=3 by ex4_intro/ qed.
  32
  33 lemma ntas_refl (h) (a) (G) (L):
  34       ∀T. ❨G,L❩ ⊢ T ![h,a] → ❨G,L❩ ⊢ T :*[h,a,0] T.
  35 /2 width=3 by ntas_intro/ qed.
  36
  37 lemma ntas_sort (h) (a) (n) (G) (L):
  38       ∀s. ❨G,L❩ ⊢ ⋆s :*[h,a,n] ⋆((next h)^n s).
  39 #h #a #n #G #L #s
  40 /2 width=3 by ntas_intro, cnv_sort, cpms_sort/
  41 qed.
  42
  43 lemma ntas_bind_cnv (h) (a) (n) (G) (K):
  44       ∀V. ❨G,K❩ ⊢ V ![h,a] →
  45       ∀I,T,U. ❨G,K.ⓑ[I]V❩ ⊢ T :*[h,a,n] U →
  46       ∀p. ❨G,K❩ ⊢ ⓑ[p,I]V.T :*[h,a,n] ⓑ[p,I]V.U.
  47 #h #a #n #G #K #V #HV #I #T #U
  48 * #X #HU #HT #HUX #HTX #p
  49 /3 width=5 by ntas_intro, cnv_bind, cpms_bind_dx/
  50 qed.
  51
  52 (* Basic_forward lemmas *****************************************************)
  53
  54 lemma ntas_fwd_cnv_sn (h) (a) (n) (G) (L):
  55       ∀T,U. ❨G,L❩ ⊢ T :*[h,a,n] U → ❨G,L❩ ⊢ T ![h,a].
  56 #h #a #n #G #L #T #U
  57 * #X #_ #HT #_ #_ //
  58 qed-.
  59
  60 (* Note: this is ntas_fwd_correct_cnv *)
  61 lemma ntas_fwd_cnv_dx (h) (a) (n) (G) (L):
  62       ∀T,U. ❨G,L❩ ⊢ T :*[h,a,n] U → ❨G,L❩ ⊢ U ![h,a].
  63 #h #a #n #G #L #T #U
  64 * #X #HU #_ #_ #_ //
  65 qed-.