matita/matita/contribs/lambdadelta/basic_2/i_dynamic/ntas_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/dynamic/nta_preserve.ma".
  16 include "basic_2/i_dynamic/ntas_preserve.ma".
  17
  18 (* ITERATED NATIVE TYPE ASSIGNMENT FOR TERMS ********************************)
  19
  20 (* Properties with native type assignment for terms *************************)
  21
  22 lemma nta_ntas (h) (a) (G) (L):
  23       ∀T,U. ⦃G,L⦄ ⊢ T :[h,a] U → ⦃G,L⦄ ⊢ T :*[h,a,1] U.
  24 #h #a #G #L #T #U #H
  25 elim (cnv_inv_cast … H) -H /2 width=3 by ntas_intro/
  26 qed-.
  27
  28 (* Inversion lemmas with native type assignment for terms *******************)
  29
  30 lemma ntas_inv_nta (h) (a) (G) (L):
  31       ∀T,U. ⦃G,L⦄ ⊢ T :*[h,a,1] U → ⦃G,L⦄ ⊢ T :[h,a] U.
  32 #h #a #G #L #T #U
  33 * /2 width=3 by cnv_cast/
  34 qed-.
  35
  36 (* Note: this follows from ntas_inv_appl_sn *)
  37 lemma nta_inv_appl_sn_ntas (h) (a) (G) (L) (V) (T):
  38       ∀X. ⦃G,L⦄ ⊢ ⓐV.T :[h,a] X →
  39       ∨∨ ∃∃p,W,U,U0. ad a 0 & ⦃G,L⦄ ⊢ V :[h,a] W & ⦃G,L⦄ ⊢ T :*[h,a,0] ⓛ{p}W.U0 & ⦃G,L.ⓛW⦄ ⊢ U0 :[h,a] U & ⦃G,L⦄ ⊢ ⓐV.ⓛ{p}W.U ⬌*[h] X & ⦃G,L⦄ ⊢ X ![h,a]
  40        | ∃∃n,p,W,U,U0. ad a (↑n) & ⦃G,L⦄ ⊢ V :[h,a] W & ⦃G,L⦄ ⊢ T :[h,a] U & ⦃G,L⦄ ⊢ U :*[h,a,n] ⓛ{p}W.U0 & ⦃G,L⦄ ⊢ ⓐV.U ⬌*[h] X & ⦃G,L⦄ ⊢ X ![h,a].
  41 #h #a #G #L #V #T #X #H
  42 (*
  43 lapply (nta_ntas … H) -H #H
  44 elim (ntas_inv_appl_sn … H) -H * #n #p #W #U #U0 #Hn #Ha #HVW #HTU #HU #HUX #HX
  45 [ elim (eq_or_gt n) #H destruct
  46   [ <minus_n_O in HU; #HU -Hn
  47     /4 width=8 by ntas_inv_nta, ex6_4_intro, or_introl/
  48   | lapply (le_to_le_to_eq … Hn H) -Hn -H #H destruct
  49     <minus_n_n in HU; #HU
  50     @or_intror
  51     @(ex6_5_intro … Ha … HUX HX) -Ha -X
  52     [2,4: /2 width=2 by ntas_inv_nta/
  53     |6: @ntas_refl
  54 *)
  55 elim (cnv_inv_cast … H) -H #X0 #HX #HVT #HX0 #HTX0
  56 elim (cnv_inv_appl … HVT) #n #p #W #U0 #Ha #HV #HT #HVW #HTU0
  57 elim (eq_or_gt n) #Hn destruct
  58 [ elim (cnv_fwd_cpms_abst_dx_le … HT … HTU0 1) [| // ] <minus_n_O #U #H #HU0
  59   lapply (cpms_appl_dx … V V … H) [ // ] -H #H
  60   elim (cnv_cpms_conf … HVT … HTX0 … H) -HVT -HTX0 -H <minus_n_n #X1 #HX01 #HUX1
  61   lapply (cpms_trans … HX0 … HX01) -X0 #HX1
  62   lapply (cprs_div … HUX1 … HX1) -X1 #HUX
  63   lapply (cnv_cpms_trans … HT … HTU0) #H
  64   elim (cnv_inv_bind … H) -H #_ #HU0
  65   /4 width=8 by cnv_cpms_ntas, cnv_cpms_nta, ex6_4_intro, or_introl/
  66 | >(plus_minus_m_m_commutative … Hn) in HTU0; #H
  67   elim (cpms_inv_plus … H) -H #U #HTU #HU0
  68   lapply (cpms_appl_dx … V V … HTU) [ // ] #H
  69   elim (cnv_cpms_conf … HVT … HTX0 … H) -HVT -HTX0 -H <minus_n_n #X1 #HX01 #HUX1
  70   lapply (cpms_trans … HX0 … HX01) -X0 #HX1
  71   lapply (cprs_div … HUX1 … HX1) -X1 #HUX
  72   <(S_pred … Hn) in Ha; -Hn #Ha
  73   /5 width=10 by cnv_cpms_ntas, cnv_cpms_nta, cnv_cpms_trans, ex6_5_intro, or_intror/
  74 ]
  75 qed-.
  76
  77 (*
  78
  79 definition ntas: sh → lenv → relation term ≝
  80                  λh,L. star … (nta h L).
  81
  82 (* Basic eliminators ********************************************************)
  83
  84 axiom ntas_ind_dx: ∀h,L,T2. ∀R:predicate term. R T2 →
  85                    (∀T1,T. ⦃h,L⦄ ⊢ T1 : T → ⦃h,L⦄ ⊢ T :* T2 → R T → R T1) →
  86                    ∀T1. ⦃h,L⦄ ⊢ T1 :* T2 → R T1.
  87 (*
  88 #h #L #T2 #R #HT2 #IHT2 #T1 #HT12
  89 @(star_ind_dx … HT2 IHT2 … HT12) //
  90 qed-.
  91 *)
  92 (* Basic properties *********************************************************)
  93
  94 lemma ntas_strap1: ∀h,L,T1,T,T2.
  95                    ⦃h,L⦄ ⊢ T1 :* T → ⦃h,L⦄  ⊢ T : T2 → ⦃h,L⦄  ⊢ T1 :* T2.
  96 /2 width=3/ qed.
  97
  98 lemma ntas_strap2: ∀h,L,T1,T,T2.
  99                    ⦃h,L⦄  ⊢ T1 : T → ⦃h,L⦄ ⊢ T :* T2 → ⦃h,L⦄ ⊢ T1 :* T2.
 100 /2 width=3/ qed.
 101 *)