matita/matita/contribs/lambdadelta/basic_2/etc_2A1/nta/nta_lift.etc

   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_alt.ma".
  16
  17 (* NATIVE TYPE ASSIGNMENT ON TERMS ******************************************)
  18
  19 (* Advanced inversion lemmas ************************************************)
  20
  21 fact nta_inv_sort1_aux: ∀h,L,T,U. ⦃h, L⦄ ⊢ T : U → ∀k0. T = ⋆k0 →
  22                         L ⊢ ⋆(next h k0) ⬌* U.
  23 #h #L #T #U #H elim H -L -T -U
  24 [ #L #k #k0 #H destruct //
  25 | #L #K #V #W #U #i #_ #_ #_ #_ #k0 #H destruct
  26 | #L #K #W #V #U #i #_ #_ #_ #_ #k0 #H destruct
  27 | #I #L #V #W #T #U #_ #_ #_ #_ #k0 #H destruct
  28 | #L #V #W #T #U #_ #_ #_ #_ #k0 #H destruct
  29 | #L #V #W #T #U #_ #_ #_ #_ #k0 #H destruct
  30 | #L #T #U #_ #_ #k0 #H destruct
  31 | #L #T #U1 #U2 #V2 #_ #HU12 #_ #IHTU1 #_ #k0 #H destruct
  32   lapply (IHTU1 ??) -IHTU1 [ // | skip ] #Hk0
  33   lapply (cpcs_trans … Hk0 … HU12) -U1 //
  34 ]
  35 qed.
  36
  37 (* Basic_1: was: ty3_gen_sort *)
  38 lemma nta_inv_sort1: ∀h,L,U,k. ⦃h, L⦄ ⊢ ⋆k : U → L ⊢ ⋆(next h k) ⬌* U.
  39 /2 width=3/ qed-.
  40
  41 fact nta_inv_lref1_aux: ∀h,L,T,U. ⦃h, L⦄ ⊢ T : U → ∀j. T = #j →
  42                         (∃∃K,V,W,U0. ⇩[0, j] L ≡ K. ⓓV & ⦃h, K⦄ ⊢ V : W &
  43                                      ⇧[0, j + 1] W ≡ U0 & L ⊢ U0 ⬌* U
  44                         ) ∨
  45                         (∃∃K,W,V,U0. ⇩[0, j] L ≡ K. ⓛW & ⦃h, K⦄ ⊢ W : V &
  46                                      ⇧[0, j + 1] W ≡ U0 & L ⊢ U0 ⬌* U
  47                         ).
  48 #h #L #T #U #H elim H -L -T -U
  49 [ #L #k #j #H destruct
  50 | #L #K #V #W #U #i #HLK #HVW #HWU #_ #j #H destruct /3 width=8/
  51 | #L #K #W #V #U #i #HLK #HWV #HWU #_ #j #H destruct /3 width=8/
  52 | #I #L #V #W #T #U #_ #_ #_ #_ #j #H destruct
  53 | #L #V #W #T #U #_ #_ #_ #_ #j #H destruct
  54 | #L #V #W #T #U #_ #_ #_ #_ #j #H destruct
  55 | #L #T #U #_ #_ #j #H destruct
  56 | #L #T #U1 #U2 #V2 #_ #HU12 #_ #IHTU1 #_ #j #H destruct
  57   elim (IHTU1 ??) -IHTU1 [4: // |2: skip ] * #K #V #W #U0 #HLK #HVW #HWU0 #HU01
  58   lapply (cpcs_trans … HU01 … HU12) -U1 /3 width=8/
  59 ]
  60 qed.
  61
  62 (* Basic_1: was ty3_gen_lref *)
  63 lemma nta_inv_lref1: ∀h,L,U,i. ⦃h, L⦄ ⊢ #i : U →
  64                      (∃∃K,V,W,U0. ⇩[0, i] L ≡ K. ⓓV & ⦃h, K⦄ ⊢ V : W &
  65                                   ⇧[0, i + 1] W ≡ U0 & L ⊢ U0 ⬌* U
  66                      ) ∨
  67                      (∃∃K,W,V,U0. ⇩[0, i] L ≡ K. ⓛW & ⦃h, K⦄ ⊢ W : V &
  68                                   ⇧[0, i + 1] W ≡ U0 & L ⊢ U0 ⬌* U
  69                      ).
  70 /2 width=3/ qed-.
  71
  72 (* Basic_1: was: ty3_gen_bind *)
  73 lemma nta_inv_bind1: ∀h,I,L,Y,X,U. ⦃h, L⦄ ⊢ ⓑ{I}Y.X : U →
  74                      ∃∃Z1,Z2. ⦃h, L⦄ ⊢ Y : Z1 & ⦃h, L.ⓑ{I}Y⦄ ⊢ X : Z2 &
  75                               L ⊢ ⓑ{I}Y.Z2 ⬌* U.
  76 #h #I #L #Y #X #U #H
  77 elim (ntaa_inv_bind1 … (nta_ntaa … H)) -H /3 width=3 by ntaa_nta, ex3_2_intro/
  78 qed-.
  79
  80 fact nta_inv_cast1_aux: ∀h,L,T,U. ⦃h, L⦄ ⊢ T : U → ∀X,Y. T = ⓝY.X →
  81                      ⦃h, L⦄ ⊢ X : Y ∧ L ⊢ Y ⬌* U.
  82 #h #L #T #U #H elim H -L -T -U
  83 [ #L #k #X #Y #H destruct
  84 | #L #K #V #W #U #i #_ #_ #_ #_ #X #Y #H destruct
  85 | #L #K #W #V #U #i #_ #_ #_ #_ #X #Y #H destruct
  86 | #I #L #V #W #T #U #_ #_ #_ #_ #X #Y #H destruct
  87 | #L #V #W #T #U #_ #_ #_ #_ #X #Y #H destruct
  88 | #L #V #W #T #U #_ #_ #_ #_ #X #Y #H destruct
  89 | #L #T #U #HTU #_ #X #Y #H destruct /2 width=1/
  90 | #L #T #U1 #U2 #V2 #_ #HU12 #_ #IHTU1 #_ #X #Y #H destruct
  91   elim (IHTU1 ???) -IHTU1 [4: // |2,3: skip ] #HXY #HU1
  92   lapply (cpcs_trans … HU1 … HU12) -U1 /2 width=1/
  93 ]
  94 qed.
  95
  96 (* Basic_1: was: ty3_gen_cast *)
  97 lemma nta_inv_cast1: ∀h,L,X,Y,U. ⦃h, L⦄ ⊢ ⓝY.X : U →  ⦃h, L⦄ ⊢ X : Y ∧ L ⊢ Y ⬌* U.
  98 /2 width=3/ qed-.
  99
 100 (* Advanced forvard lemmas **************************************************)
 101
 102 fact nta_fwd_pure1_aux: ∀h,L,T,U. ⦃h, L⦄ ⊢ T : U → ∀X,Y. T = ⓐY.X →
 103                         ∃∃V,W. ⦃h, L⦄ ⊢ Y : W & ⦃h, L⦄ ⊢ X : V & L ⊢ ⓐY.V ⬌* U.
 104 #h #L #T #U #H elim H -L -T -U
 105 [ #L #k #X #Y #H destruct
 106 | #L #K #V #W #U #i #_ #_ #_ #_ #X #Y #H destruct
 107 | #L #K #W #V #U #i #_ #_ #_ #_ #X #Y #H destruct
 108 | #I #L #V #W #T #U #_ #_ #_ #_ #X #Y #H destruct
 109 | #L #V #W #T #U #HVW #HTU #_ #_ #X #Y #H destruct /2 width=3/
 110 | #L #V #W #T #U #HTU #_ #_ #IHUW #X #Y #H destruct
 111   elim (IHUW U Y ?) -IHUW // /2 width=3/
 112 | #L #T #U #_ #_ #X #Y #H destruct
 113 | #L #T #U1 #U2 #V2 #_ #HU12 #_ #IHTU1 #_ #X #Y #H destruct
 114   elim (IHTU1 ???) -IHTU1 [4: // |2,3: skip ] #V #W #HYW #HXV #HU1
 115   lapply (cpcs_trans … HU1 … HU12) -U1 /2 width=3/
 116 ]
 117 qed.
 118
 119 lemma nta_fwd_pure1: ∀h,L,X,Y,U. ⦃h, L⦄ ⊢ ⓐY.X : U →
 120                      ∃∃V,W. ⦃h, L⦄ ⊢ Y : W & ⦃h, L⦄ ⊢ X : V & L ⊢ ⓐY.V ⬌* U.
 121 /2 width=3/ qed-.
 122
 123 (* Basic_1: was: ty3_correct *)
 124 lemma nta_fwd_correct: ∀h,L,T,U. ⦃h, L⦄ ⊢ T : U → ∃T0. ⦃h, L⦄ ⊢ U : T0.
 125 #h #L #T #U #H
 126 elim (ntaa_fwd_correct … (nta_ntaa … H)) -H /3 width=2 by ntaa_nta, ex_intro/
 127 qed-.
 128
 129 (* Advanced properties ******************************************************)
 130
 131 (* Basic_1: was: ty3_appl *)
 132 lemma nta_appl_old: ∀h,L,V,W,T,U. ⦃h, L⦄ ⊢ V : W → ⦃h, L⦄ ⊢ T : ⓛW.U →
 133                     ⦃h, L⦄ ⊢ ⓐV.T : ⓐV.ⓛW.U.
 134 #h #L #V #W #T #U #HVW #HTU
 135 elim (nta_fwd_correct … HTU) #X #H
 136 elim (nta_inv_bind1 … H) -H /4 width=2/
 137 qed.
 138
 139 (* Properties on relocation *************************************************)
 140
 141 (* Basic_1: was: ty3_lift *)
 142 lemma nta_lift: ∀h,L1,T1,U1. ⦃h, L1⦄ ⊢ T1 : U1 → ∀L2,d,e. ⇩[d, e] L2 ≡ L1 →
 143                 ∀T2. ⇧[d, e] T1 ≡ T2 → ∀U2. ⇧[d, e] U1 ≡ U2 → ⦃h, L2⦄ ⊢ T2 : U2.
 144 /4 width=9 by ntaa_nta, nta_ntaa, ntaa_lift/ qed.