matita/matita/contribs/lambdadelta/basic_2/i_dynamic/ntas_preserve.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 "ground_2/xoa/ex_7_5.ma".
  16 include "basic_2/rt_equivalence/cpcs_cprs.ma".
  17 include "basic_2/dynamic/cnv_preserve.ma".
  18 include "basic_2/i_dynamic/ntas.ma".
  19
  20 (* ITERATED NATIVE TYPE ASSIGNMENT FOR TERMS ********************************)
  21
  22 (* Properties based on preservation *****************************************)
  23
  24 lemma cnv_cpms_ntas (h) (a) (G) (L):
  25       ∀T. ❪G,L❫ ⊢ T ![h,a] → ∀n,U.❪G,L❫ ⊢ T ➡*[n,h] U → ❪G,L❫ ⊢ T :*[h,a,n] U.
  26 /3 width=4 by ntas_intro, cnv_cpms_trans/ qed.
  27
  28 (* Inversion lemmas based on preservation ***********************************)
  29
  30 lemma ntas_inv_plus (h) (a) (n1) (n2) (G) (L):
  31       ∀T1,T2. ❪G,L❫ ⊢ T1 :*[h,a,n1+n2] T2 →
  32       ∃∃T0. ❪G,L❫ ⊢ T1 :*[h,a,n1] T0 & ❪G,L❫ ⊢ T0 :*[h,a,n2] T2.
  33 #h #a #n1 #n2 #G #L #T1 #T2 * #X0 #HT2 #HT1 #H20 #H10
  34 elim (cpms_inv_plus … H10) -H10 #T0 #H10 #H00
  35 lapply (cnv_cpms_trans … HT1 … H10) #HT0
  36 /3 width=6 by cnv_cpms_ntas, ntas_intro, ex2_intro/
  37 qed-.
  38
  39 lemma ntas_inv_appl_sn (h) (a) (m) (G) (L) (V) (T):
  40       ∀X. ❪G,L❫ ⊢ ⓐV.T :*[h,a,m] X →
  41       ∨∨ ∃∃n,p,W,U,U0. n ≤ m & ad a n & ❪G,L❫ ⊢ V :*[h,a,1] W & ❪G,L❫ ⊢ T :*[h,a,n] ⓛ[p]W.U0 & ❪G,L.ⓛW❫ ⊢ U0 :*[h,a,m-n] U & ❪G,L❫ ⊢ ⓐV.ⓛ[p]W.U ⬌*[h] X & ❪G,L❫ ⊢ X ![h,a]
  42        | ∃∃n,p,W,U,U0. m ≤ n & ad a n & ❪G,L❫ ⊢ V :*[h,a,1] W & ❪G,L❫ ⊢ T :*[h,a,m] U & ❪G,L❫ ⊢ U :*[h,a,n-m] ⓛ[p]W.U0 & ❪G,L❫ ⊢ ⓐV.U ⬌*[h] X & ❪G,L❫ ⊢ X ![h,a].
  43 #h #a #m #G #L #V #T #X
  44 * #X0 #HX #HVT #HX0 #HTX0
  45 elim (cnv_inv_appl … HVT) #n #p #W #U0 #Ha #HV #HT #HVW #HTU0
  46 elim (le_or_ge n m) #Hnm
  47 [ elim (cnv_fwd_cpms_abst_dx_le … HT … HTU0 … Hnm) #U #H #HU0
  48   lapply (cpms_appl_dx … V V … H) [ // ] -H #H
  49   elim (cnv_cpms_conf … HVT … HTX0 … H) -HVT -HTX0 -H <minus_n_n #X1 #HX01 #HUX1
  50   lapply (cpms_trans … HX0 … HX01) -X0 #HX1
  51   lapply (cprs_div … HUX1 … HX1) -X1 #HUX
  52   lapply (cnv_cpms_trans … HT … HTU0) #H
  53   elim (cnv_inv_bind … H) -H #_ #HU0
  54   /4 width=11 by cnv_cpms_ntas, ex7_5_intro, or_introl/
  55 | >(plus_minus_m_m_commutative … Hnm) in HTU0; #H
  56   elim (cpms_inv_plus … H) -H #U #HTU #HU0
  57   lapply (cpms_appl_dx … V V … HTU) [ // ] #H
  58   elim (cnv_cpms_conf … HVT … HTX0 … H) -HVT -HTX0 -H <minus_n_n #X1 #HX01 #HUX1
  59   lapply (cpms_trans … HX0 … HX01) -X0 #HX1
  60   lapply (cprs_div … HUX1 … HX1) -X1 #HUX
  61   /5 width=11 by cnv_cpms_ntas, cnv_cpms_trans, ex7_5_intro, or_intror/
  62 ]
  63 qed-.