matita/matita/contribs/lambda_delta/basic_2/dynamic/nta_ltpr.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 (* FRAGMENT 0
  16 include "basic_2/unfold/delift_lift.ma".
  17
  18
  19 include "basic_2/equivalence/cpcs_cpcs.ma".
  20 include "basic_2/unfold/delift_delift.ma".
  21
  22
  23
  24 axiom pippo1: ∀T1,V. ∃∃T2. ⓓV.T1 ➡ T2 & ⋆.ⓓV ⊢ T1 ▼*[0, 1] ≡ T2.
  25 (*
  26 #T1 #V elim (pippo0 (⋆.ⓓV) 0 1 ? T1)
  27 [ #T2 #HT12 @(ex2_1_intro … HT12)
  28   @tpr
  29 *)
  30
  31 axiom pippo: ∀L,V,T1. ∃∃T2. L ⊢ ⓓV.T1 ➡ T2 & L.ⓓV ⊢ T1 ▼*[0, 1] ≡ T2.
  32
  33 axiom cprs_inv_appl1_cpcs: ∀L,V1,T1,U2. L ⊢ ⓐV1. T1 ➡* U2 → (
  34                            ∃∃V2,T2.  L ⊢ V1 ➡* V2 & L ⊢ T1 ➡* T2 &
  35                                      L ⊢ U2 ➡* ⓐV2. T2
  36                            ) ∨
  37                            ∃∃V2,W,T. L ⊢ V1 ➡* V2 &
  38                                      L ⊢ T1 ➡* ⓛW. T & L ⊢ ⓓV2. T ⬌* U2.
  39 #L #V1 #T1 #U2 #H @(cprs_ind … H) -U2 /3 width=5/
  40 #U #U2 #_ #HU2 * *
  41 [ #V0 #T0 #HV10 #HT10 #HUT0
  42   elim (cprs_strip … HUT0 … HU2) -U #U #H #HU2
  43   elim (cpr_inv_appl1 … H) -H *
  44   [ #V2 #T2 #HV02 #HT02 #H destruct /4 width=5/
  45   | #V2 #W2 #T #T2 #HV02 #HT2 #H1 #H2 destruct
  46     lapply (cprs_strap1 … HV10 HV02) -V0 #HV12
  47     lapply (cprs_div ? (ⓓV2.T) ? ? ? HU2) -HU2 /2 width=1/ /3 width=6/
  48   | #V #V2 #W0 #W2 #T #T2 #HV0 #HW02 #HT2 #HV2 #H1 #H2 destruct
  49     lapply (cprs_strap1 … HV10 HV0) -V0 #HV1
  50     lapply (cprs_trans … HT10 (ⓓW2.T2) ?) -HT10 /2 width=1/ -W0 -T #HT1
  51     elim (pippo L W2 T2) #T3 #H1T3 #H2T3
  52     elim (pippo L W2 (ⓐV2.T2)) #X #H1X #H
  53     elim (delift_inv_flat1 … H) -H #V3 #Y #HV23 #HY #H destruct
  54
  55
  56     @or_introl @(ex3_2_intro … HV1 HT1) -HV1 -HT1
  57
  58   ]
  59 | /4 width=8/
  60 ]
  61 qed-.
  62
  63
  64 include "basic_2/computation/cprs_lcprs.ma".
  65 include "basic_2/dynamic/nta.ma".
  66
  67 axiom cprs_inv_appl_abst: ∀L,V,T,W,U. L ⊢ ⓐV.T ➡* ⓛW.U →
  68                           ∃∃V0,W0,T0,W1,U1. ⇧[O, 1] W ≡ W1 &
  69                                             ⇧[O + 1, 1] U ≡ U1 &
  70                                             L ⊢ V ➡* V0 & L ⊢ T ➡* ⓛW0.T0 &
  71                                             L.ⓓV0 ⊢ T0 ➡* ⓛW1.U1.
  72 #L #V #T #W #U #H
  73 elim (cprs_inv_appl1 … H) -H *
  74 [ #V0 #T0 #_ #_ #H destruct
  75 | #V0 #W0 #T0 #HV0 #HT0 #H
  76   elim (cprs_inv_abbr1 … H) -H *
  77   [ #V1 #T1 #_ #_ #H destruct
  78   | #X #H #HT01
  79     elim (lift_inv_bind1 … H) -H #W1 #U1 #HW1 #HU1 #H destruct /2 width=10/
  80   ]
  81 | #V0 #V1 #V2 #T0 #HV0 #HV01 #HT0 #H
  82   elim (cprs_inv_abbr1 … H) -H *
  83   [ #V3 #T3 #_ #_ #H destruct
  84   | #X #H #HT3
  85     elim (lift_inv_bind1 … H) -H #W3 #U3 #HW3 #HU3 #H destruct /2 width=10/
  86
  87 axiom pippo: ∀h,L,T,U. ⦃h, L⦄ ⊢ T : U → ∀X,Y. L ⊢ T ➡* ⓛX.Y →
  88              ∃Z. L ⊢ U ➡* ⓛX.Z.
  89 #h #L #T #U #H elim H -L -T -U
  90 [
  91 |
  92 |
  93 |
  94 |
  95 | #L #V #W #T #U #HTU #HUW #IHTU #IHUW #X #Y #HTY
  96   elim (cprs_inv_appl1 … HTY) -HTY *
  97   [ #V0 #T0 #_ #_ #H destruct
  98   | #V0 #W0 #T0 #HV0 #HT0 #HTY
  99     elim (IHTU … HT0) -IHTU -HT0 #Z #HUZ
 100     elim (cprs_inv_abbr1 … HTY) -HTY *
 101     [ #V1 #T1 #_ #_ #H destruct #X0
 102
 103
 104 include "basic_2/dynamic/nta_ltpss.ma".
 105 include "basic_2/dynamic/nta_thin.ma".
 106 include "basic_2/dynamic/lsubn_nta.ma".
 107
 108 include "basic_2/hod/ntas_lift.ma".
 109
 110
 111   elim (nta_inv_pure1 … HUW) -HUW #V0 #U0 #U1 #HV0 #HU0 #HU0W #HU01
 112   @(ex2_2_intro … HYW)
 113   [2:
 114
 115
 116 axiom pippo_aux: ∀h,L,Z,U. ⦃h, L⦄ ⊢ Z : U → ∀Y,X. Z = ⓐY.X →
 117                  ∀W,T. L ⊢ X ➡* ⓛW.T → ⦃h, L⦄ ⊢ Y : W.
 118 #h #L #Z #U #H elim H -L -Z -U
 119 [
 120 |
 121 |
 122 |
 123 |
 124 | #L #V #W #T #U #HTU #_ #_ #IHUW #Y #X #H #W0 #T0 #HX destruct
 125   lapply (IHUW Y U ? ?) -IHUW -W // #T
 126   @(ex2_2_intro … HYW)
 127   [2:
 128
 129 axiom pippo: ∀h,L,V,X,U. ⦃h, L⦄ ⊢ ⓐV.X : U →
 130              ∃∃W,T. L ⊢ X ➡* ⓛW.T & ⦃h, L⦄ ⊢ V : W.
 131 #h #L #V #X #Y #H
 132
 133 *)
 134 (* NATIVE TYPE ASSIGNMENT ON TERMS ******************************************)
 135
 136 (* Properties on context-free parallel reduction for local environments ******)
 137 (*
 138 axiom nta_ltpr_cprs_conf: ∀h,L1,T1,U. ⦃h, L1⦄ ⊢ T1 : U → ∀L2. L1 ➡ L2 →
 139                           ∀T2. L2 ⊢ T1 ➡* T2 → ⦃h, L2⦄ ⊢ T2 : U.
 140 #h #L1 #T1 #U #H @(nta_ind_alt … H) -L1 -T1 -U
 141 [ #L1 #k #L2 #_ #T2 #H
 142   >(cprs_inv_sort1 … H) -H //
 143 |
 144 |
 145 |
 146 |
 147 | #L1 #V1 #W1 #T1 #U1 #_ #_ #IHTU1 #IHUW1 #L2 #HL12 #T2 #H
 148   elim (cprs_inv_appl1 … H) -H *
 149   [ #V2 #T0 #HV12 #HT10 #H destruct
 150     elim (nta_fwd_correct h L2 (ⓐV1.T1) (ⓐV1.U1) ?) [2: /3 width=2/ ] #U
 151     @(nta_conv … (ⓐV2.U1)) (* /2 width=1/*) [ /4 width=2/] (**) (* explicit constructor, /5 width=5/ is too slow *)
 152   | #V2 #W2 #T0 #HV12 #HT10 #HT02
 153     lapply (IHTU1 … HL12 (ⓛW2.T0) ?) -IHTU1 /2 width=1/ -HT10 #H
 154     elim (nta_inv_bind1 … H) -H #W #U0 #HW2 #HTU0 #HU01
 155     elim (cpcs_inv_abst1 … HU01) -HU01 #W #U #HU1 #HU0
 156     lapply (IHUW1 … HL12 (ⓐV2.ⓛW.U) ?) -IHUW1 -HL12 /2 width=1/ -HV12 #H
 157
 158
 159
 160     elim (nta_fwd_pure1 … H) -H #W0 #U2 #HVU2 #H #HW01
 161     elim (nta_inv_bind1 … H) -H #W3 #U3 #HW3 #HU3 #H
 162     elim (cpcs_inv_abst1 … H) -H #W4 #U4
 163 *)
 164 (*
 165 axiom nta_ltpr_tpr_conf: ∀h,L1,T1,U. ⦃h, L1⦄ ⊢ T1 : U → ∀L2. L1 ➡ L2 →
 166                          ∀T2. T1 ➡ T2 → ⦃h, L2⦄ ⊢ T2 : U.
 167 #h #L1 #T1 #U #H @(nta_ind_alt … H) -L1 -T1 -U
 168 [ #L1 #k #L2 #_ #T2 #H
 169   >(tpr_inv_atom1 … H) -H //
 170 | #L1 #K1 #V1 #W #U #i #HLK1 #_ #HWU #IHV1 #L2 #HL12 #T2 #H
 171   >(tpr_inv_atom1 … H) -T2
 172   elim (ltpr_ldrop_conf … HLK1 … HL12) -HLK1 -HL12 #X #HLK2 #H
 173   elim (ltpr_inv_pair1 … H) -H #K2 #V2 #HK12 #HV12 #H destruct /3 width=6/
 174 | #L1 #K1 #W1 #V1 #U1 #i #HLK1 #HWV1 #HWU1 #IHWV1 #L2 #HL12 #T2 #H
 175   >(tpr_inv_atom1 … H) -T2
 176   elim (ltpr_ldrop_conf … HLK1 … HL12) -HLK1 -HL12 #X #HLK2 #H
 177   elim (ltpr_inv_pair1 … H) -H #K2 #W2 #HK12 #HW12 #H destruct
 178   lapply (ldrop_fwd_ldrop2 … HLK2) #HLK
 179   elim (lift_total V1 0 (i+1)) #W #HW
 180   lapply (nta_lift h … HLK … HWU1 … HW) /2 width=1/ -HLK -HW
 181   elim (lift_total W2 0 (i+1)) #U2 #HWU2
 182   lapply (tpr_lift … HW12 … HWU1 … HWU2) -HWU1 #HU12
 183   @(nta_conv … U2) /2 width=1/ /3 width=6/ (**) (* explicit constructor, /3 width=6/ is too slow *)
 184 | #I #L1 #V1 #W1 #T1 #U1 #_ #_ #IHVW1 #IHTU1 #L2 #HL12 #X #H
 185   elim (tpr_inv_bind1 … H) -H *
 186   [ #V2 #T0 #T2 #HV12 #HT10 #HT02 #H destruct
 187     lapply (IHVW1 … HL12 … HV12) #HV2W1
 188     lapply (IHVW1 L2 … V1 ?) // -IHVW1 #HWV1
 189     lapply (IHTU1 (L2.ⓑ{I}V2) … HT10) -HT10 /2 width=1/ #HT0U1
 190     lapply (IHTU1 (L2.ⓑ{I}V1) ? T1 ?) -IHTU1 // /2 width=1/ -HL12 #H
 191     lapply (tps_lsubs_trans … HT02 (L2.ⓑ{I}V2) ?) -HT02 /2 width=1/ #HT02
 192     lapply (nta_tps_conf … HT0U1 … HT02) -T0 #HT2U1
 193     elim (nta_fwd_correct … H) -H #U2 #HU12
 194     @(nta_conv … (ⓑ{I}V2.U1)) /2 width=2/ /3 width=1/ (**) (* explicit constructor, /4 width=6/ is too slow *)
 195   | #T #HT1 #HTX #H destruct
 196     lapply (IHVW1 … HL12 V1 ?) -IHVW1 // #HVW1
 197     elim (lift_total X 0 1) #Y #HXY
 198     lapply (tpr_lift … HTX … HT1 … HXY) -T #H
 199     lapply (IHTU1 (L2.ⓓV1) … H) -T1 /2 width=1/ -L1 #H
 200     elim (nta_fwd_correct … H) #T1 #HUT1
 201     elim (nta_thin_conf … H L2 0 (0+1) ? ?) -H /2 width=1/ /3 width=1/ #T #U #HTU #H
 202     normalize in ⊢ (??%??? → ?); #HU1
 203     lapply (delift_inv_lift1_eq … H L2 … HXY) -Y /2 width=1/ #H destruct
 204     @(nta_conv … U) // /2 width=2/
 205   ]
 206 | #L1 #V1 #W1 #T1 #U1 #_ #_ #IHVW1 #IHTU1 #L2 #HL12 #X #H
 207   elim (tpr_inv_appl1 … H) -H *
 208   [ #V2 #Y #HV12 #HY #H destruct
 209     elim (tpr_inv_abst1 … HY) -HY #W2 #T2 #HW12 #HT12 #H destruct
 210     lapply (IHTU1 L2 ? (ⓛW1.T1) ?) // #H
 211     elim (nta_fwd_correct … H) -H #X #H
 212     elim (nta_inv_bind1 … H) -H #W #U #HW #HU #_
 213     @(nta_conv … (ⓐV2.ⓛW1.U1)) /4 width=2/ (**) (* explicit constructor, /5 width=5/ is too slow *)
 214   | #V2 #W2 #T0 #T2 #HV12 #HT02 #H1 #H2 destruct
 215     lapply (IHVW1 … HL12 … HV12) #HVW2
 216     lapply (IHVW1 … HL12 V1 ?) -IHVW1 // #HV1W2
 217     lapply (IHTU1 … HL12 (ⓛW2.T2) ?) -IHTU1 -HL12 /2 width=1/ -HT02 #H1
 218     elim (nta_fwd_correct … H1) #T #H2
 219     elim (nta_inv_bind1 … H1) -H1 #W #U2 #HW2 #HTU2 #H
 220     elim (cpcs_inv_abst … H Abst W2) -H #_ #HU21
 221     elim (nta_inv_bind1 … H2) -H2 #W0 #U0 #_ #H #_ -T -W0
 222     lapply (lsubn_nta_trans … HTU2 (L2.ⓓV2) ?) -HTU2 /2 width=1/ #HTU2
 223     @(nta_conv … (ⓓV2.U2)) /2 width=2/ /3 width=2/ (**) (* explicit constructor, /4 width=5/ is too slow *)
 224   | #V0 #V2 #W0 #W2 #T0 #T2 #_ #_ #_ #_ #H destruct
 225   ]
 226 | #L1 #V1 #W1 #T1 #U1 #_ #_ #IHTU1 #IHUW1 #L2 #HL12 #X #H
 227   elim (tpr_inv_appl1 … H) -H *
 228   [ #V2 #T2 #HV12 #HT12 #H destruct
 229     elim (nta_fwd_correct h L2 (ⓐV1.T1) (ⓐV1.U1) ?) [2: /3 width=2/ ] #U
 230     @(nta_conv … (ⓐV2.U1)) /2 width=1/ /4 width=2/ (**) (* explicit constructor, /5 width=5/ is too slow *)
 231   | #V2 #W2 #T0 #T2 #HV12 #HT02 #H1 #H2 destruct
 232     lapply (IHTU1 … HL12 (ⓛW2.T2) ?) -IHTU1 /2 width=1/ -T0 #H
 233     elim (nta_inv_bind1 … H) -H #W #U2 #HW2 #HTU2 #HU21
 234     lapply (IHUW1 … HL12 (ⓐV2.U1) ?) -IHUW1 -HL12 /2 width=1/ #H
 235     elim (nta_inv_pure1 … H) -H #V0 #U0 #U #HV20 #HU10 #HU0W1 #HU0
 236     @(nta_conv … (ⓓV2.U2))
 237     [2: @nta_bind //
 238         @(lsubn_nta_trans … HTU2) @lsubn_abbr //
 239 (*
 240     lapply (IH … HV1 … HL12 … HV12) -HV1 -HV12 /width=5/ #HB
 241     lapply (IH … HB0  … HL12 W2 ?) -HB0 /width=5/ #HB0
 242     lapply (IH … HA0 … (L2.ⓛW2) … HT02) -IH -HA0 -HT02 /width=5/ -T0 /2 width=1/ -L1 -V1 /4 width=7/
 243 *)
 244 *)
 245 (*
 246 axiom pippo: ⦃h, L⦄ ⊢ ⓐV.X : Y →
 247              ∃∃W,T. L ⊢ X ➡* ⓛW.T & ⦃h, L⦄ ⊢ ⓐV : W.
 248
 249 *)
 250 (* SEGMENT 2
 251 | #L1 #T1 #U1 #W1 #_ #_ #IHTU1 #IHUW1 #L2 #d #e #HL12 #X #H
 252   elim (tpss_inv_flat1 … H) -H #U2 #T2 #HU12 #HT12 #H destruct
 253   lapply (cpr_tpss … HU12) /4 width=4/
 254 | #L1 #T1 #U11 #U12 #U #_ #HU112 #_ #IHTU11 #IHU12 #L2 #d #e #HL12 #T2 #HT12
 255   @(nta_conv … U11) /2 width=5/ (**) (* explicot constructor, /3 width=7/ is too slow *)
 256 ]
 257 qed.
 258 *)
 259
 260 (* SEGMENT 3
 261 fact nta_ltpr_tpr_conf_aux: ∀h,L,T,L1,T1,U. ⦃h, L1⦄ ⊢ T1 : U → L = L1 → T = T1 →
 262                             ∀L2. L1 ➡ L2 → ∀T2. T1 ➡ T2 → ⦃h, L2⦄ ⊢ T2 : U.
 263
 264
 265   | #V0 #V2 #W0 #W2 #T0 #T2 #HV10 #HW02 #HT02 #HV02 #H1 #H2 destruct
 266     elim (nta_inv_abbr … HT1) -HT1 #B0 #HW0 #HT0
 267     lapply (IH … HW0  … HL12 … HW02) -HW0 /width=5/ #HW2
 268     lapply (IH … HV1 … HL12 … HV10) -HV1 -HV10 /width=5/ #HV0
 269     lapply (IH … HT0 … (L2.ⓓW2) … HT02) -IH -HT0 -HT02 /width=5/ -V1 -T0 /2 width=1/ -L1 -W0 #HT2
 270     @(nta_abbr … HW2) -HW2
 271     @(nta_appl … HT2) -HT2 /3 width=7/ (**) (* explict constructors, /5 width=7/ is too slow *)
 272   ]
 273 | #L1 #V1 #T1 #A #HV1 #HT1 #H1 #H2 #L2 #HL12 #X #H destruct
 274   elim (tpr_inv_cast1 … H) -H
 275   [ * #V2 #T2 #HV12 #HT12 #H destruct
 276     lapply (IH … HV1 … HL12 … HV12) -HV1 -HV12 /width=5/ #HV2
 277     lapply (IH … HT1 … HL12 … HT12) -IH -HT1 -HL12 -HT12 /width=5/ -L1 -V1 -T1 /2 width=1/
 278   | -HV1 #HT1X
 279      lapply (IH … HT1 … HL12 … HT1X) -IH -HT1 -HL12 -HT1X /width=5/
 280   ]
 281 ]
 282 qed.
 283
 284 /2 width=9/ qed.
 285
 286 axiom nta_ltpr_conf: ∀L1,T,A. L1 ⊢ T : A → ∀L2. L1 ➡ L2 → L2 ⊢ T : A.
 287 /2 width=5/ qed.
 288
 289 axiom nta_tpr_conf: ∀L,T1,A. L ⊢ T1 : A → ∀T2. T1 ➡ T2 → L ⊢ T2 : A.
 290 /2 width=5/ qed.
 291 *)