matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_drops.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/cnv_drops.ma".
  16 include "basic_2/dynamic/nta.ma".
  17
  18 (* NATIVE TYPE ASSIGNMENT FOR TERMS *****************************************)
  19
  20 (* Advanced properties ******************************************************)
  21
  22 lemma nta_ldef (a) (h) (G) (K):
  23       ∀V,W. ⦃G,K⦄ ⊢ V :[a,h] W →
  24       ∀U. ⬆*[1] W ≘ U → ⦃G,K.ⓓV⦄ ⊢ #0 :[a,h] U.
  25 #a #h #G #K #V #W #H #U #HWU
  26 elim (cnv_inv_cast … H) -H #X #HW #HV #HWX #HVX
  27 lapply (cnv_lifts … HW (Ⓣ) … (K.ⓓV) … HWU) -HW
  28 [ /3 width=3 by drops_refl, drops_drop/ ] #HU
  29 elim (cpms_lifts_sn … HWX … (Ⓣ) … (K.ⓓV) … HWU) -W
  30 [| /3 width=3 by drops_refl, drops_drop/ ] #XW #HXW #HUXW
  31 /3 width=5 by cnv_zero, cnv_cast, cpms_delta/
  32 qed.
  33
  34 lemma nta_ldec_cnv (a) (h) (G) (K):
  35       ∀W. ⦃G,K⦄ ⊢ W ![a,h] →
  36       ∀U. ⬆*[1] W ≘ U → ⦃G,K.ⓛW⦄ ⊢ #0 :[a,h] U.
  37 #a #h #G #K #W #HW #U #HWU
  38 lapply (cnv_lifts … HW (Ⓣ) … (K.ⓛW) … HWU)
  39 /3 width=5 by cnv_zero, cnv_cast, cpms_ell, drops_refl, drops_drop/
  40 qed.
  41
  42 lemma nta_lref (a) (h) (I) (G) (K):
  43       ∀T,i. ⦃G,K⦄ ⊢ #i :[a,h] T →
  44       ∀U. ⬆*[1] T ≘ U → ⦃G,K.ⓘ{I}⦄ ⊢ #(↑i) :[a,h] U.
  45 #a #h #I #G #K #T #i #H #U #HTU
  46 elim (cnv_inv_cast … H) -H #X #HT #Hi #HTX #H2
  47 lapply (cnv_lifts … HT (Ⓣ) … (K.ⓘ{I}) … HTU) -HT
  48 [ /3 width=3 by drops_refl, drops_drop/ ] #HU
  49 lapply (cnv_lifts … Hi (Ⓣ) (𝐔❴1❵) (K.ⓘ{I}) ???) -Hi
  50 [4:|*: /3 width=3 by drops_refl, drops_drop/ ] #Hi
  51 elim (cpms_lifts_sn … HTX … (Ⓣ) … (K.ⓘ{I}) … HTU) -T
  52 [| /3 width=3 by drops_refl, drops_drop/ ] #XU #HXU #HUXU
  53 /3 width=5 by cnv_cast, cpms_lref/
  54 qed.
  55
  56 (* Properties with generic slicing for local environments *******************)
  57
  58 lemma nta_lifts_sn (a) (h) (G): d_liftable2_sn … lifts (nta a h G).
  59 #a #h #G #K #T1 #T2 #H #b #f #L #HLK #U1 #HTU1
  60 elim (cnv_inv_cast … H) -H #X #HT2 #HT1 #HT2X #HT1X
  61 elim (lifts_total T2 f) #U2 #HTU2
  62 lapply (cnv_lifts … HT2 … HLK … HTU2) -HT2 #HU2
  63 lapply (cnv_lifts … HT1 … HLK … HTU1) -HT1 #HU1
  64 elim (cpms_lifts_sn … HT2X … HLK … HTU2) -HT2X #X2 #HX2 #HUX2
  65 elim (cpms_lifts_sn … HT1X … HLK … HTU1) -T1 #X1 #HX1 #HUX1
  66 lapply (lifts_mono … HX2 … HX1) -K -X #H destruct
  67 /3 width=6 by cnv_cast, ex2_intro/
  68 qed-.
  69
  70 (* Basic_1: was: ty3_lift *)
  71 (* Basic_2A1: was: nta_lift ntaa_lift *)
  72 lemma nta_lifts_bi (a) (h) (G): d_liftable2_bi … lifts (nta a h G).
  73 /3 width=12 by nta_lifts_sn, d_liftable2_sn_bi, lifts_mono/ qed-.
  74
  75 (* Basic_1: was by definition: ty3_abbr *)
  76 (* Basic_2A1: was by definition: nta_ldef ntaa_ldef *)
  77 lemma nta_ldef_drops (a) (h) (G) (K) (L) (i):
  78       ∀V,W. ⦃G,K⦄ ⊢ V :[a,h] W →
  79       ∀U. ⬆*[↑i] W ≘ U → ⬇*[i] L ≘ K.ⓓV → ⦃G,L⦄ ⊢ #i :[a,h] U.
  80 #a #h #G #K #L #i #V #W #HVW #U #HWU #HLK
  81 elim (lifts_split_trans … HWU (𝐔❴1❵) (𝐔❴i❵)) [| // ] #X #HWX #HXU
  82 /3 width=9 by nta_lifts_bi, nta_ldef/
  83 qed.
  84
  85 lemma nta_ldec_drops_cnv (a) (h) (G) (K) (L) (i):
  86       ∀W. ⦃G,K⦄ ⊢ W ![a,h] →
  87       ∀U. ⬆*[↑i] W ≘ U → ⬇*[i] L ≘ K.ⓛW → ⦃G,L⦄ ⊢ #i :[a,h] U.
  88 #a #h #G #K #L #i #W #HW #U #HWU #HLK
  89 elim (lifts_split_trans … HWU (𝐔❴1❵) (𝐔❴i❵)) [| // ] #X #HWX #HXU
  90 /3 width=9 by nta_lifts_bi, nta_ldec_cnv/
  91 qed.