matita/matita/contribs/lambda_delta/basic_2/native/nta_lift.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/equivalence/cpcs_cpcs.ma".
  16 include "basic_2/native/nta.ma".
  17
  18 (* NATIVE TYPE ASSIGNMENT ON TERMS ******************************************)
  19
  20 (* Advanced inversion lemmas ************************************************)
  21
  22 fact nta_inv_sort_aux: ∀h,L,T,U. ⦃h, L⦄ ⊢ T : U → ∀k0. T = ⋆k0 →
  23                        L ⊢ ⋆(next h k0) ⬌* U.
  24 #h #L #T #U #H elim H -L -T -U
  25 [ #L #k #k0 #H destruct //
  26 | #L #K #V #W #U #i #_ #_ #_ #_ #k0 #H destruct
  27 | #L #K #W #V #U #i #_ #_ #_ #_ #k0 #H destruct
  28 | #I #L #V #W #T #U #_ #_ #_ #_ #k0 #H destruct
  29 | #L #V #W #U #T1 #T2 #_ #_ #_ #_ #_ #_ #k0 #H destruct
  30 | #L #V #W #T #U #_ #_ #_ #_ #k0 #H destruct
  31 | #L #T #U #_ #_ #k0 #H destruct
  32 | #L #T #U1 #U2 #V2 #_ #HU12 #_ #IHTU1 #_ #k0 #H destruct
  33   lapply (IHTU1 ??) -IHTU1 [ // | skip ] #Hk0
  34   lapply (cpcs_trans … Hk0 … HU12) -U1 //
  35 ]
  36 qed.
  37
  38 (* Basic_1: was: ty3_gen_sort *)
  39 lemma nta_inv_sort: ∀h,L,U,k. ⦃h, L⦄ ⊢ ⋆k : U → L ⊢ ⋆(next h k) ⬌* U.
  40 /2 width=3/ qed-.
  41
  42 fact nta_inv_lref_aux: ∀h,L,T,U. ⦃h, L⦄ ⊢ T : U → ∀j. T = #j →
  43                        (∃∃K,V,W,U0. ⇩[0, j] L ≡ K. ⓓV & ⦃h, K⦄ ⊢ V : W &
  44                                     ⇧[0, j + 1] W ≡ U0 & L ⊢ U0 ⬌* U
  45                        ) ∨
  46                        (∃∃K,W,V,U0. ⇩[0, j] L ≡ K. ⓛW & ⦃h, K⦄ ⊢ W : V &
  47                                     ⇧[0, j + 1] W ≡ U0 & L ⊢ U0 ⬌* U
  48                        ).
  49 #h #L #T #U #H elim H -L -T -U
  50 [ #L #k #j #H destruct
  51 | #L #K #V #W #U #i #HLK #HVW #HWU #_ #j #H destruct /3 width=8/
  52 | #L #K #W #V #U #i #HLK #HWV #HWU #_ #j #H destruct /3 width=8/
  53 | #I #L #V #W #T #U #_ #_ #_ #_ #j #H destruct
  54 | #L #V #W #U #T1 #T2 #_ #_ #_ #_ #_ #_ #j #H destruct
  55 | #L #V #W #T #U #_ #_ #_ #_ #j #H destruct
  56 | #L #T #U #_ #_ #j #H destruct
  57 | #L #T #U1 #U2 #V2 #_ #HU12 #_ #IHTU1 #_ #j #H destruct
  58   elim (IHTU1 ??) -IHTU1 [4: // |2: skip ] * #K #V #W #U0 #HLK #HVW #HWU0 #HU01
  59   lapply (cpcs_trans … HU01 … HU12) -U1 /3 width=8/
  60 ]
  61 qed.
  62
  63 (* Basic_1: was ty3_gen_lref *)
  64 lemma nta_inv_lref: ∀h,L,U,i. ⦃h, L⦄ ⊢ #i : U →
  65                     (∃∃K,V,W,U0. ⇩[0, i] L ≡ K. ⓓV & ⦃h, K⦄ ⊢ V : W &
  66                                  ⇧[0, i + 1] W ≡ U0 & L ⊢ U0 ⬌* U
  67                     ) ∨
  68                     (∃∃K,W,V,U0. ⇩[0, i] L ≡ K. ⓛW & ⦃h, K⦄ ⊢ W : V &
  69                                  ⇧[0, i + 1] W ≡ U0 & L ⊢ U0 ⬌* U
  70                     ).
  71 /2 width=3/ qed-.
  72
  73 fact nta_inv_bind_aux: ∀h,L,T,U. ⦃h, L⦄ ⊢ T : U → ∀J,X,Y. T = ⓑ{J}Y.X →
  74                        ∃∃Z1,Z2. ⦃h, L⦄ ⊢ Y : Z1 & ⦃h, L.ⓑ{J}Y⦄ ⊢ X : Z2 &
  75                                 L ⊢ ⓑ{J}Y.Z2 ⬌* U.
  76 #h #L #T #U #H elim H -L -T -U
  77 [ #L #k #J #X #Y #H destruct
  78 | #L #K #V #W #U #i #_ #_ #_ #_ #J #X #Y #H destruct
  79 | #L #K #W #V #U #i #_ #_ #_ #_ #J #X #Y #H destruct
  80 | #I #L #V #W #T #U #HVW #HTU #_ #_ #J #X #Y #H destruct /2 width=3/
  81 | #L #V #W #U #T1 #T2 #_ #_ #_ #_ #_ #_ #J #X #Y #H destruct
  82 | #L #V #W #T #U #_ #_ #_ #_ #J #X #Y #H destruct
  83 | #L #T #U #_ #_ #J #X #Y #H destruct
  84 | #L #T #U1 #U2 #V2 #_ #HU12 #_ #IHTU1 #_ #J #X #Y #H destruct
  85   elim (IHTU1 ????) -IHTU1 [5: // |2,3,4: skip ] #Z1 #Z2 #HZ1 #HZ2 #HU1
  86   lapply (cpcs_trans … HU1 … HU12) -U1 /2 width=3/
  87 ]
  88 qed.
  89
  90 (* Basic_1: was: ty3_gen_bind *)
  91 lemma nta_inv_bind: ∀h,J,L,Y,X,U. ⦃h, L⦄ ⊢ ⓑ{J}Y.X : U →
  92                     ∃∃Z1,Z2. ⦃h, L⦄ ⊢ Y : Z1 & ⦃h, L.ⓑ{J}Y⦄ ⊢ X : Z2 &
  93                              L ⊢ ⓑ{J}Y.Z2 ⬌* U.
  94 /2 width=3/ qed-.
  95
  96 fact nta_inv_cast_aux: ∀h,L,T,U. ⦃h, L⦄ ⊢ T : U → ∀X,Y. T = ⓣY.X →
  97                     ⦃h, L⦄ ⊢ X : Y ∧ L ⊢ Y ⬌* U.
  98 #h #L #T #U #H elim H -L -T -U
  99 [ #L #k #X #Y #H destruct
 100 | #L #K #V #W #U #i #_ #_ #_ #_ #X #Y #H destruct
 101 | #L #K #W #V #U #i #_ #_ #_ #_ #X #Y #H destruct
 102 | #I #L #V #W #T #U #_ #_ #_ #_ #X #Y #H destruct
 103 | #L #V #W #U #T1 #T2 #_ #_ #_ #_ #_ #_ #X #Y #H destruct
 104 | #L #V #W #T #U #_ #_ #_ #_ #X #Y #H destruct
 105 | #L #T #U #HTU #_ #X #Y #H destruct /2 width=1/
 106 | #L #T #U1 #U2 #V2 #_ #HU12 #_ #IHTU1 #_ #X #Y #H destruct
 107   elim (IHTU1 ???) -IHTU1 [4: // |2,3: skip ] #HXY #HU1
 108   lapply (cpcs_trans … HU1 … HU12) -U1 /2 width=1/
 109 ]
 110 qed.
 111
 112 (* Basic_1: was: ty3_gen_cast *)
 113 lemma nta_inv_cast: ∀h,L,X,Y,U. ⦃h, L⦄ ⊢ ⓣY.X : U →  ⦃h, L⦄ ⊢ X : Y ∧ L ⊢ Y ⬌* U.
 114 /2 width=3/ qed-.
 115
 116 (* Properties on relocation *************************************************)
 117
 118 (* Basic_1: was: ty3_lift *)
 119 lemma nta_lift: ∀h,L1,T1,U1. ⦃h, L1⦄ ⊢ T1 : U1 → ∀L2,d,e. ⇩[d, e] L2 ≡ L1 →
 120                 ∀T2. ⇧[d, e] T1 ≡ T2 → ∀U2. ⇧[d, e] U1 ≡ U2 → ⦃h, L2⦄ ⊢ T2 : U2.
 121 #h #L1 #T1 #U1 #H elim H -L1 -T1 -U1
 122 [ #L1 #k #L2 #d #e #HL21 #X1 #H1 #X2 #H2
 123   >(lift_inv_sort1 … H1) -X1
 124   >(lift_inv_sort1 … H2) -X2 //
 125 | #L1 #K1 #V1 #W1 #W #i #HLK1 #_ #HW1 #IHVW1 #L2 #d #e #HL21 #X #H #U2 #HWU2
 126   elim (lift_inv_lref1 … H) * #Hid #H destruct
 127   [ elim (lift_trans_ge … HW1 … HWU2 ?) -W // #W2 #HW12 #HWU2
 128     elim (ldrop_trans_le … HL21 … HLK1 ?) -L1 /2 width=2/ #X #HLK2 #H
 129     elim (ldrop_inv_skip2 … H ?) -H /2 width=1/ -Hid #K2 #V2 #HK21 #HV12 #H destruct
 130     /3 width=8/
 131   | lapply (lift_trans_be … HW1 … HWU2 ? ?) -W // /2 width=1/ #HW1U2
 132     lapply (ldrop_trans_ge … HL21 … HLK1 ?) -L1 // -Hid /3 width=8/
 133   ]
 134 | #L1 #K1 #W1 #V1 #W #i #HLK1 #_ #HW1 #IHWV1 #L2 #d #e #HL21 #X #H #U2 #HWU2
 135   elim (lift_inv_lref1 … H) * #Hid #H destruct
 136   [ elim (lift_trans_ge … HW1 … HWU2 ?) -W // <minus_plus #W #HW1 #HWU2
 137     elim (ldrop_trans_le … HL21 … HLK1 ?) -L1 /2 width=2/ #X #HLK2 #H
 138     elim (ldrop_inv_skip2 … H ?) -H /2 width=1/ -Hid #K2 #W2 #HK21 #HW12 #H destruct
 139     lapply (lift_mono … HW1 … HW12) -HW1 #H destruct
 140     elim (lift_total V1 (d-i-1) e) /3 width=8/
 141   | lapply (lift_trans_be … HW1 … HWU2 ? ?) -W // /2 width=1/ #HW1U2
 142     lapply (ldrop_trans_ge … HL21 … HLK1 ?) -L1 // -Hid /3 width=8/
 143   ]
 144 | #I #L1 #V1 #W1 #T1 #U1 #_ #_ #IHVW1 #IHTU1 #L2 #d #e #HL21 #X1 #H1 #X2 #H2
 145   elim (lift_inv_bind1 … H1) -H1 #V2 #T2 #HV12 #HT12 #H destruct
 146   elim (lift_inv_bind1 … H2) -H2 #X #U2 #H1 #HU12 #H2 destruct
 147   lapply (lift_mono … H1 … HV12) -H1 #H destruct
 148   elim (lift_total W1 d e) /4 width=6/
 149 | #L1 #V1 #W1 #U1 #T11 #T12 #_ #_ #_ #IHVW1 #IHWU1 #IHT112 #L2 #d #e #HL21 #X1 #H1 #X2 #H2
 150   elim (lift_inv_flat1 … H1) -H1 #V2 #X #HV12 #H1 #H destruct
 151   elim (lift_inv_bind1 … H1) -H1 #W2 #T12 #HW12 #HT112 #H destruct
 152   elim (lift_inv_flat1 … H2) -H2 #X0 #X #H0 #H2 #H destruct
 153   elim (lift_inv_bind1 … H2) -H2 #Y0 #T22 #H2 #HT122 #H destruct
 154   lapply (lift_mono … H0 … HV12) -H0 #H destruct
 155   lapply (lift_mono … H2 … HW12) -H2 #H destruct
 156   elim (lift_total U1 d e) #U2 #HU12
 157   @nta_appl [2,3: /2 width=5/ | skip | /3 width=5/ ] (**) (* explicit constructor, /4 width=6/ is too slow *)
 158 | #L1 #V1 #W1 #T1 #U1 #_ #_ #IHTU1 #IHUW1 #L2 #d #e #HL21 #X1 #H1 #X2 #H2
 159   elim (lift_inv_flat1 … H1) -H1 #V2 #T2 #HV12 #HT12 #H destruct
 160   elim (lift_inv_flat1 … H2) -H2 #X #U2 #H1 #HU12 #H2 destruct
 161   lapply (lift_mono … H1 … HV12) -H1 #H destruct
 162   elim (lift_total W1 d e) /4 width=6/
 163 | #L1 #T1 #U1 #_ #IHTU1 #L2 #d #e #HL21 #X #H #U2 #HU12
 164   elim (lift_inv_flat1 … H) -H #X2 #T2 #HUX2 #HT12 #H destruct
 165   lapply (lift_mono … HUX2 … HU12) -HUX2 #H destruct /3 width=5/
 166 | #L1 #T1 #U11 #U12 #V12 #_ #HU112 #_ #IHTU11 #IHUV12 #L2 #d #e #HL21 #U1 #HTU1 #U2 #HU12
 167   elim (lift_total U11 d e) #U #HU11
 168   elim (lift_total V12 d e) #V22 #HV122
 169   lapply (cpcs_lift … HL21 … HU11 … HU12 HU112) -HU112 /3 width=6/
 170 ]
 171 qed.
 172
 173 (* Advanced forvard lemmas **************************************************)
 174
 175 (* Basic_1: was: ty3_correct *)
 176 lemma nta_fwd_correct: ∀h,L,T,U. ⦃h, L⦄ ⊢ T : U → ∃T0. ⦃h, L⦄ ⊢ U : T0.
 177 #h #L #T #U #H elim H -L -T -U
 178 [ /2 width=2/
 179 | #L #K #V #W #W0 #i #HLK #_ #HW0 * #V0 #HWV0
 180   lapply (ldrop_fwd_ldrop2 … HLK) -HLK #HLK
 181   elim (lift_total V0 0 (i+1)) /3 width=10/
 182 | #L #K #W #V #V0 #i #HLK #HWV #HWV0 #_
 183   lapply (ldrop_fwd_ldrop2 … HLK) -HLK #HLK
 184   elim (lift_total V 0 (i+1)) /3 width=10/
 185 | #I #L #V #W #T #U #HVW #_ #_ * /3 width=2/
 186 | #L #V #W #U #T1 #T2 #HVW #HWU #_ #_ #_ * /3 width=2/
 187 | #L #V #W #T #U #_ #HUW * #T0 #HUT0 /3 width=2/
 188 | #L #T #U #_ * /2 width=2/
 189 | /2 width=2/
 190 ]
 191 qed-.
 192
 193 (* Advanced properties ******************************************************)
 194
 195 (* Basic_1: was: ty3_appl *)
 196 lemma nta_appl_old: ∀h,L,V,W,T,U. ⦃h, L⦄ ⊢ V : W → ⦃h, L⦄ ⊢ T : ⓛW.U →
 197                     ⦃h, L⦄ ⊢ ⓐV.T : ⓐV.ⓛW.U.
 198 #h #L #V #W #T #U #HVW #HTU
 199 elim (nta_fwd_correct … HTU) #X #H
 200 elim (nta_inv_bind … H) -H #V0 #T0 #HWV0 #HUT0 #_ -X /3 width=2/
 201 qed.