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 (* Advanced properties of native validity for terms *************************)
  21
  22 lemma cnv_appl_ntas_ge (h) (a) (G) (L):
  23       ∀m,n. m ≤ n → ad a n → ∀V,W. ⦃G,L⦄ ⊢ V :[h,a] W →
  24       ∀p,T,U. ⦃G,L⦄ ⊢ T :*[h,a,m] ⓛ{p}W.U → ⦃G,L⦄ ⊢ ⓐV.T ![h,a].
  25 #h #a #G #L #m #n #Hmn #Hn #V #W #HVW #p #T #U #HTU
  26 elim (cnv_inv_cast … HVW) -HVW #W0 #HW #HV #HW0 #HVW0
  27 elim HTU -HTU #U0 #H #HT #HU0 #HTU0
  28 elim (cnv_cpms_conf … H … HU0 0 (ⓛ{p}W0.U)) -H -HU0
  29 [| /2 width=1 by cpms_bind/ ] -HW0 <minus_n_O #X0 #HUX0 #H
  30 elim (cpms_inv_abst_sn … H) -H #W1 #U1 #HW01 #_ #H destruct
  31 /3 width=13 by cnv_appl_ge, cpms_cprs_trans/
  32 qed-.
  33
  34 (* Advanced inversion lemmas of native validity for terms *******************)
  35
  36 lemma cnv_inv_appl_ntas (h) (a) (G) (L):
  37       ∀V,T. ⦃G,L⦄ ⊢ ⓐV.T ![h,a] →
  38       ∃∃n,p,W,T,U. ad a n & ⦃G,L⦄ ⊢ V :[h,a] W & ⦃G,L⦄ ⊢ T :*[h,a,n] ⓛ{p}W.U.
  39 #h #a #G #L #V #T #H
  40 elim (cnv_inv_appl … H) -H #n #p #W #U #Hn #HV #HT #HVW #HTU
  41 /3 width=9 by cnv_cpms_nta, cnv_cpms_ntas, ex3_5_intro/
  42 qed-.
  43
  44 (* Properties with native type assignment for terms *************************)
  45
  46 lemma nta_ntas (h) (a) (G) (L):
  47       ∀T,U. ⦃G,L⦄ ⊢ T :[h,a] U → ⦃G,L⦄ ⊢ T :*[h,a,1] U.
  48 #h #a #G #L #T #U #H
  49 elim (cnv_inv_cast … H) -H /2 width=3 by ntas_intro/
  50 qed-.
  51
  52 lemma ntas_step_sn (h) (a) (G) (L):
  53       ∀T1,T. ⦃G,L⦄ ⊢ T1 :[h,a] T →
  54       ∀n,T2. ⦃G,L⦄ ⊢ T :*[h,a,n] T2 → ⦃G,L⦄ ⊢ T1 :*[h,a,↑n] T2.
  55 #h #a #G #L #T1 #T #H #n #T2 * #X2 #HT2 #HT #H1TX2 #H2TX2
  56 elim (cnv_inv_cast … H) -H #X1 #_ #HT1 #H1TX1 #H2TX1
  57 elim (cnv_cpms_conf … HT … H1TX1 … H2TX2) -T <minus_n_O <minus_O_n <plus_SO_sn #X #HX1 #HX2
  58 /3 width=5 by ntas_intro, cprs_trans, cpms_trans/
  59 qed-.
  60
  61 lemma ntas_step_dx (h) (a) (G) (L):
  62       ∀n,T1,T. ⦃G,L⦄ ⊢ T1 :*[h,a,n] T →
  63       ∀T2. ⦃G,L⦄ ⊢ T :[h,a] T2 → ⦃G,L⦄ ⊢ T1 :*[h,a,↑n] T2.
  64 #h #a #G #L #n #T1 #T * #X1 #HT #HT1 #H1TX1 #H2TX1 #T2 #H
  65 elim (cnv_inv_cast … H) -H #X2 #HT2 #_ #H1TX2 #H2TX2
  66 elim (cnv_cpms_conf … HT … H1TX1 … H2TX2) -T <minus_n_O <minus_O_n <plus_SO_dx #X #HX1 #HX2
  67 /3 width=5 by ntas_intro, cprs_trans, cpms_trans/
  68 qed-.
  69
  70 lemma nta_appl_ntas_zero (h) (a) (G) (L): ad a 0 →
  71       ∀V,W. ⦃G,L⦄ ⊢ V :[h,a] W → ∀p,T,U0. ⦃G,L⦄ ⊢ T :*[h,a,0] ⓛ{p}W.U0 →
  72       ∀U. ⦃G,L.ⓛW⦄ ⊢ U0 :[h,a] U → ⦃G,L⦄ ⊢ ⓐV.T :[h,a] ⓐV.ⓛ{p}W.U.
  73 #h #a #G #L #Ha #V #W #HVW #p #T #U0 #HTU0 #U #HU0
  74 lapply (nta_fwd_cnv_dx … HVW) #HW
  75 lapply (nta_bind_cnv … HW … HU0 p) -HW -HU0 #HU0
  76 elim (ntas_step_dx … HTU0 … HU0) -HU0 #X #HU #_ #HUX #HTX
  77 /4 width=9 by cnv_appl_ntas_ge, ntas_refl, cnv_cast, cpms_appl_dx/
  78 qed.
  79
  80 lemma nta_appl_ntas_pos (h) (a) (n) (G) (L): ad a (↑n) →
  81       ∀V,W. ⦃G,L⦄ ⊢ V :[h,a] W → ∀T,U. ⦃G,L⦄ ⊢ T :[h,a] U →
  82       ∀p,U0. ⦃G,L⦄ ⊢ U :*[h,a,n] ⓛ{p}W.U0 → ⦃G,L⦄ ⊢ ⓐV.T :[h,a] ⓐV.U.
  83 #h #a #n #G #L #Ha #V #W #HVW #T #U #HTU #p #U0 #HU0
  84 elim (cnv_inv_cast … HTU) #X #_ #_ #HUX #HTX
  85 /4 width=11 by ntas_step_sn, cnv_appl_ntas_ge, cnv_cast, cpms_appl_dx/
  86 qed-.
  87
  88 (* Inversion lemmas with native type assignment for terms *******************)
  89
  90 lemma ntas_inv_nta (h) (a) (G) (L):
  91       ∀T,U. ⦃G,L⦄ ⊢ T :*[h,a,1] U → ⦃G,L⦄ ⊢ T :[h,a] U.
  92 #h #a #G #L #T #U
  93 * /2 width=3 by cnv_cast/
  94 qed-.
  95
  96 (* Note: this follows from ntas_inv_appl_sn *)
  97 lemma nta_inv_appl_sn_ntas (h) (a) (G) (L) (V) (T):
  98       ∀X. ⦃G,L⦄ ⊢ ⓐV.T :[h,a] X →
  99       ∨∨ ∃∃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]
 100        | ∃∃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].
 101 #h #a #G #L #V #T #X #H
 102 (*
 103 lapply (nta_ntas … H) -H #H
 104 elim (ntas_inv_appl_sn … H) -H * #n #p #W #U #U0 #Hn #Ha #HVW #HTU #HU #HUX #HX
 105 [ elim (eq_or_gt n) #H destruct
 106   [ <minus_n_O in HU; #HU -Hn
 107     /4 width=8 by ntas_inv_nta, ex6_4_intro, or_introl/
 108   | lapply (le_to_le_to_eq … Hn H) -Hn -H #H destruct
 109     <minus_n_n in HU; #HU
 110     @or_intror
 111     @(ex6_5_intro … Ha … HUX HX) -Ha -X
 112     [2,4: /2 width=2 by ntas_inv_nta/
 113     |6: @ntas_refl
 114 *)
 115 elim (cnv_inv_cast … H) -H #X0 #HX #HVT #HX0 #HTX0
 116 elim (cnv_inv_appl … HVT) #n #p #W #U0 #Ha #HV #HT #HVW #HTU0
 117 elim (eq_or_gt n) #Hn destruct
 118 [ elim (cnv_fwd_cpms_abst_dx_le … HT … HTU0 1) [| // ] <minus_n_O #U #H #HU0
 119   lapply (cpms_appl_dx … V V … H) [ // ] -H #H
 120   elim (cnv_cpms_conf … HVT … HTX0 … H) -HVT -HTX0 -H <minus_n_n #X1 #HX01 #HUX1
 121   lapply (cpms_trans … HX0 … HX01) -X0 #HX1
 122   lapply (cprs_div … HUX1 … HX1) -X1 #HUX
 123   lapply (cnv_cpms_trans … HT … HTU0) #H
 124   elim (cnv_inv_bind … H) -H #_ #HU0
 125   /4 width=8 by cnv_cpms_ntas, cnv_cpms_nta, ex6_4_intro, or_introl/
 126 | >(plus_minus_m_m_commutative … Hn) in HTU0; #H
 127   elim (cpms_inv_plus … H) -H #U #HTU #HU0
 128   lapply (cpms_appl_dx … V V … HTU) [ // ] #H
 129   elim (cnv_cpms_conf … HVT … HTX0 … H) -HVT -HTX0 -H <minus_n_n #X1 #HX01 #HUX1
 130   lapply (cpms_trans … HX0 … HX01) -X0 #HX1
 131   lapply (cprs_div … HUX1 … HX1) -X1 #HUX
 132   <(S_pred … Hn) in Ha; -Hn #Ha
 133   /5 width=10 by cnv_cpms_ntas, cnv_cpms_nta, cnv_cpms_trans, ex6_5_intro, or_intror/
 134 ]
 135 qed-.