matita/matita/contribs/lambdadelta/basic_2/i_dynamic/ntas_etc.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_lift.ma".
  16 include "basic_2/hod/ntas.ma".
  17
  18 (* HIGHER ORDER NATIVE TYPE ASSIGNMENT ON TERMS *****************************)
  19
  20 (* Advanced properties on native type assignment for terms ******************)
  21
  22 lemma nta_pure_ntas: ∀h,L,U,W,Y. ⦃h,L⦄ ⊢ U :* ⓛW.Y → ∀T. ⦃h,L⦄ ⊢ T : U →
  23                      ∀V. ⦃h,L⦄ ⊢ V : W →  ⦃h,L⦄ ⊢ ⓐV.T : ⓐV.U.
  24 #h #L #U #W #Y #H @(ntas_ind_dx … H) -U /2 width=1/ /3 width=2/
  25 qed.
  26
  27 axiom pippo: ∀h,L,T,W,Y. ⦃h,L⦄ ⊢ T :* ⓛW.Y → ∀U. ⦃h,L⦄ ⊢ T : U →
  28              ∃Z. ⦃h,L⦄ ⊢ U :* ⓛW.Z.
  29 (* REQUIRES SUBJECT CONVERSION
  30 #h #L #T #W #Y #H @(ntas_ind_dx … H) -T
  31 [ #U #HYU
  32   elim (nta_fwd_correct … HYU) #U0 #HU0
  33   elim (nta_inv_bind1 … HYU) #W0 #Y0 #HW0 #HY0 #HY0U
  34 *)
  35
  36 (* Advanced inversion lemmas on native type assignment for terms ************)
  37
  38 fact nta_inv_pure1_aux: ∀h,L,Z,U. ⦃h,L⦄ ⊢ Z : U → ∀X,Y. Z = ⓐY.X →
  39                         ∃∃W,V,T. ⦃h,L⦄ ⊢ Y : W & ⦃h,L⦄ ⊢ X : V &
  40                                  L ⊢ ⓐY.V ⬌* U & ⦃h,L⦄ ⊢ V :* ⓛW.T.
  41 #h #L #Z #U #H elim H -L -Z -U
  42 [ #L #k #X #Y #H destruct
  43 | #L #K #V #W #U #i #_ #_ #_ #_ #X #Y #H destruct
  44 | #L #K #W #V #U #i #_ #_ #_ #_ #X #Y #H destruct
  45 | #I #L #V #W #T #U #_ #_ #_ #_ #X #Y #H destruct
  46 | #L #V #W #Z #U #HVW #HZU #_ #_ #X #Y #H destruct /2 width=7/
  47 | #L #V #W #Z #U #HZU #_ #_ #IHUW #X #Y #H destruct
  48   elim (IHUW U Y ?) -IHUW // /3 width=9/
  49 | #L #Z #U #_ #_ #X #Y #H destruct
  50 | #L #Z #U1 #U2 #V2 #_ #HU12 #_ #IHTU1 #_ #X #Y #H destruct
  51   elim (IHTU1 ???) -IHTU1 [4: // |2,3: skip ] #W #V #T #HYW #HXV #HU1 #HVT
  52   lapply (cpcs_trans … HU1 … HU12) -U1 /2 width=7/
  53 ]
  54 qed.
  55
  56 (* Basic_1: was only: ty3_gen_appl *)
  57 lemma nta_inv_pure1: ∀h,L,Y,X,U. ⦃h,L⦄ ⊢ ⓐY.X : U →
  58                      ∃∃W,V,T. ⦃h,L⦄ ⊢ Y : W & ⦃h,L⦄ ⊢ X : V &
  59                               L ⊢ ⓐY.V ⬌* U & ⦃h,L⦄ ⊢ V :* ⓛW.T.
  60 /2 width=3/ qed-.
  61
  62 axiom nta_inv_appl1: ∀h,L,Z,Y,X,U. ⦃h,L⦄ ⊢ ⓐZ.ⓛY.X : U →
  63                      ∃∃W. ⦃h,L⦄ ⊢ Z : Y & ⦃h,L⦄ ⊢ ⓛY.X : ⓛY.W &
  64                      L ⊢ ⓐZ.ⓛY.W ⬌* U.
  65 (* REQUIRES SUBJECT REDUCTION
  66 #h #L #Z #Y #X #U #H
  67 elim (nta_inv_pure1 … H) -H #W #V #T #HZW #HXV #HVU #HVT
  68 elim (nta_inv_bind1 … HXV) -HXV #Y0 #X0 #HY0 #HX0 #HX0V
  69 lapply (cpcs_trans … (ⓐZ.ⓛY.X0) … HVU) -HVU /2 width=1/ -HX0V #HX0U
  70 @(ex3_1_intro … HX0U) /2 width=2/
  71 *)
  72 *)