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 include "basic_2/dynamic/nta_ltpss.ma".
  16 include "basic_2/dynamic/nta_thin.ma".
  17 include "basic_2/dynamic/lsubn_nta.ma".
  18
  19 lemma cpr_beta: ∀L,V1,V2,W,T1,T2.
  20                 V1 ➡ V2 → L.ⓛW ⊢ T1 ➡ T2 → L ⊢ ⓐV1.ⓛW.T1 ➡ ⓓV2.T2.
  21 #L #V1 #V2 #W #T1 #T2 #HV12 * #T #HT1 #HT2
  22 lapply (tpss_inv_S2 … HT2 L W ?) -HT2 // #HT2
  23 lapply (tpss_lsubs_trans … HT2 (L.ⓓV2) ?) -HT2 /2 width=1/ #HT2
  24 @(ex2_1_intro … (ⓓV2.T)) /2 width=1/ (**) (* explicit constructor, /3/ is too skow *)
  25 qed.
  26
  27 lemma cpr_beta2: ∀L,V1,V2,W,T1,T2.
  28                  L ⊢ V1 ➡ V2 → L.ⓛW ⊢ T1 ➡ T2 → L ⊢ ⓐV1.ⓛW.T1 ➡ ⓓV2.T2.
  29 #L #V1 #V2 #W #T1 #T2 * #V #HV1 #HV2 * #T #HT1 #HT2
  30 lapply (tpss_inv_S2 … HT2 L W ?) -HT2 // #HT2
  31 lapply (tpss_lsubs_trans … HT2 (L.ⓓV2) ?) -HT2 /2 width=1/ #HT2
  32 @(ex2_1_intro … (ⓓV.T)) /2 width=1/ (**) (* explicit constructor, /3/ is too skow *)
  33 qed.
  34
  35 (* NATIVE TYPE ASSIGNMENT ON TERMS ******************************************)
  36
  37 (* Properties on context-free parallel reduction for local environments ******)
  38
  39 lemma nta_ltpr_tpr_conf: ∀h,L1,T1,U. ⦃h, L1⦄ ⊢ T1 : U → ∀L2. L1 ➡ L2 →
  40                          ∀T2. T1 ➡ T2 → ⦃h, L2⦄ ⊢ T2 : U.
  41 #h #L1 #T1 #U #H @(nta_ind_alt … H) -L1 -T1 -U
  42 [ #L1 #k #L2 #_ #T2 #H
  43   >(tpr_inv_atom1 … H) -H //
  44 | #L1 #K1 #V1 #W #U #i #HLK1 #_ #HWU #IHV1 #L2 #HL12 #T2 #H
  45   >(tpr_inv_atom1 … H) -T2
  46   elim (ltpr_ldrop_conf … HLK1 … HL12) -HLK1 -HL12 #X #HLK2 #H
  47   elim (ltpr_inv_pair1 … H) -H #K2 #V2 #HK12 #HV12 #H destruct /3 width=6/
  48 | #L1 #K1 #W1 #V1 #U1 #i #HLK1 #HWV1 #HWU1 #IHWV1 #L2 #HL12 #T2 #H
  49   >(tpr_inv_atom1 … H) -T2
  50   elim (ltpr_ldrop_conf … HLK1 … HL12) -HLK1 -HL12 #X #HLK2 #H
  51   elim (ltpr_inv_pair1 … H) -H #K2 #W2 #HK12 #HW12 #H destruct
  52   lapply (ldrop_fwd_ldrop2 … HLK2) #HLK
  53   elim (lift_total V1 0 (i+1)) #W #HW
  54   lapply (nta_lift h … HLK … HWU1 … HW) /2 width=1/ -HLK -HW
  55   elim (lift_total W2 0 (i+1)) #U2 #HWU2
  56   lapply (tpr_lift … HW12 … HWU1 … HWU2) -HWU1 #HU12
  57   @(nta_conv … U2) /2 width=1/ /3 width=6/ (**) (* explicit constructor, /3 width=6/ is too slow *)
  58 | #I #L1 #V1 #W1 #T1 #U1 #_ #_ #IHVW1 #IHTU1 #L2 #HL12 #X #H
  59   elim (tpr_inv_bind1 … H) -H *
  60   [ #V2 #T0 #T2 #HV12 #HT10 #HT02 #H destruct
  61     lapply (IHVW1 … HL12 … HV12) #HV2W1
  62     lapply (IHVW1 L2 … V1 ?) // -IHVW1 #HWV1
  63     lapply (IHTU1 (L2.ⓑ{I}V2) … HT10) -HT10 /2 width=1/ #HT0U1
  64     lapply (IHTU1 (L2.ⓑ{I}V1) ? T1 ?) -IHTU1 // /2 width=1/ -HL12 #H
  65     lapply (tps_lsubs_trans … HT02 (L2.ⓑ{I}V2) ?) -HT02 /2 width=1/ #HT02
  66     lapply (nta_tps_conf … HT0U1 … HT02) -T0 #HT2U1
  67     elim (nta_fwd_correct … H) -H #U2 #HU12
  68     @(nta_conv … (ⓑ{I}V2.U1)) /2 width=2/ /3 width=1/ (**) (* explicit constructor, /4 width=6/ is too slow *)
  69   | #T #HT1 #HTX #H destruct
  70     lapply (IHVW1 … HL12 V1 ?) -IHVW1 // #HVW1
  71     elim (lift_total X 0 1) #Y #HXY
  72     lapply (tpr_lift … HTX … HT1 … HXY) -T #H
  73     lapply (IHTU1 (L2.ⓓV1) … H) -T1 /2 width=1/ -L1 #H
  74     elim (nta_fwd_correct … H) #T1 #HUT1
  75     elim (nta_thin_conf … H L2 0 (0+1) ? ?) -H /2 width=1/ /3 width=1/ #T #U #HTU #H
  76     normalize in ⊢ (??%??? → ?); #HU1
  77     lapply (delift_inv_lift1_eq … H L2 … HXY) -Y /2 width=1/ #H destruct
  78     @(nta_conv … U) // /2 width=2/
  79   ]
  80 | #L1 #V1 #W1 #T1 #U1 #_ #_ #IHVW1 #IHTU1 #L2 #HL12 #X #H
  81   elim (tpr_inv_appl1 … H) -H *
  82   [ #V2 #Y #HV12 #HY #H destruct
  83     elim (tpr_inv_abst1 … HY) -HY #W2 #T2 #HW12 #HT12 #H destruct
  84     lapply (IHTU1 L2 ? (ⓛW1.T1) ?) // #H
  85     elim (nta_fwd_correct … H) -H #X #H
  86     elim (nta_inv_bind1 … H) -H #W #U #HW #HU #_
  87     @(nta_conv … (ⓐV2.ⓛW1.U1)) /4 width=2/ (**) (* explicit constructor, /5 width=5/ is too slow *)
  88   | #V2 #W2 #T0 #T2 #HV12 #HT02 #H1 #H2 destruct
  89     lapply (IHVW1 … HL12 … HV12) #HVW2
  90     lapply (IHVW1 … HL12 V1 ?) -IHVW1 // #HV1W2
  91     lapply (IHTU1 … HL12 (ⓛW2.T2) ?) -IHTU1 -HL12 /2 width=1/ -HT02 #H1
  92     elim (nta_fwd_correct … H1) #T #H2
  93     elim (nta_inv_bind1 … H1) -H1 #W #U2 #HW2 #HTU2 #H
  94     elim (cpcs_inv_abst … H Abst W2) -H #_ #HU21
  95     elim (nta_inv_bind1 … H2) -H2 #W0 #U0 #_ #H #_ -T -W0
  96     lapply (lsubn_nta_trans … HTU2 (L2.ⓓV2) ?) -HTU2 /2 width=1/ #HTU2
  97     @(nta_conv … (ⓓV2.U2))
  98     [2: /2 width=2/
  99     |3: -h -L1 -T0 -T2 -W -U0
 100     |4: /3 width=2/
 101     ]
 102   | #V0 #V2 #W0 #W2 #T0 #T2 #_ #_ #_ #_ #H destruct
 103   ]
 104
 105
 106
 107
 108
 109 | #L1 #V1 #W1 #T1 #U1 #_ #_ #IHTU1 #IHUW1 #L2 #d #e #HL12 #X #H
 110   elim (tpss_inv_flat1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct
 111   lapply (cpr_tpss … HV12) #HV
 112   elim (nta_fwd_correct h L2 (ⓐV1.T1) (ⓐV1.U1) ?) [2: /3 width=4/ ] #U #HU
 113   @(nta_conv … (ⓐV2.U1)) // /3 width=1/ /4 width=5/ (**) (* explicit constructor, /5 width=5/ is too slow *)
 114 | #L1 #T1 #U1 #W1 #_ #_ #IHTU1 #IHUW1 #L2 #d #e #HL12 #X #H
 115   elim (tpss_inv_flat1 … H) -H #U2 #T2 #HU12 #HT12 #H destruct
 116   lapply (cpr_tpss … HU12) /4 width=4/
 117 | #L1 #T1 #U11 #U12 #U #_ #HU112 #_ #IHTU11 #IHU12 #L2 #d #e #HL12 #T2 #HT12
 118   @(nta_conv … U11) /2 width=5/ (**) (* explicot constructor, /3 width=7/ is too slow *)
 119 ]
 120 qed.
 121
 122
 123
 124
 125
 126
 127
 128
 129
 130
 131
 132
 133
 134
 135
 136
 137
 138
 139
 140 fact nta_ltpr_tpr_conf_aux: ∀h,L,T,L1,T1,U. ⦃h, L1⦄ ⊢ T1 : U → L = L1 → T = T1 →
 141                             ∀L2. L1 ➡ L2 → ∀T2. T1 ➡ T2 → ⦃h, L2⦄ ⊢ T2 : U.
 142
 143
 144 | #L1 #V1 #T1 #B #A #HV1 #HT1 #H1 #H2 #L2 #HL12 #X #H destruct
 145   elim (tpr_inv_appl1 … H) -H *
 146   [ #V2 #T2 #HV12 #HT12 #H destruct
 147     lapply (IH … HV1 … HL12 … HV12) -HV1 -HV12 /width=5/ #HB
 148     lapply (IH … HT1 … HL12 … HT12) -IH -HT1 -HL12 -HT12 /width=5/ /2 width=3/
 149   | #V2 #W2 #T0 #T2 #HV12 #HT02 #H1 #H2 destruct
 150     elim (nta_inv_abst … HT1) -HT1 #B0 #A0 #HB0 #HA0 #H destruct
 151     lapply (IH … HV1 … HL12 … HV12) -HV1 -HV12 /width=5/ #HB
 152     lapply (IH … HB0  … HL12 W2 ?) -HB0 /width=5/ #HB0
 153     lapply (IH … HA0 … (L2.ⓛW2) … HT02) -IH -HA0 -HT02 /width=5/ -T0 /2 width=1/ -L1 -V1 /4 width=7/
 154   | #V0 #V2 #W0 #W2 #T0 #T2 #HV10 #HW02 #HT02 #HV02 #H1 #H2 destruct
 155     elim (nta_inv_abbr … HT1) -HT1 #B0 #HW0 #HT0
 156     lapply (IH … HW0  … HL12 … HW02) -HW0 /width=5/ #HW2
 157     lapply (IH … HV1 … HL12 … HV10) -HV1 -HV10 /width=5/ #HV0
 158     lapply (IH … HT0 … (L2.ⓓW2) … HT02) -IH -HT0 -HT02 /width=5/ -V1 -T0 /2 width=1/ -L1 -W0 #HT2
 159     @(nta_abbr … HW2) -HW2
 160     @(nta_appl … HT2) -HT2 /3 width=7/ (**) (* explict constructors, /5 width=7/ is too slow *)
 161   ]
 162 | #L1 #V1 #T1 #A #HV1 #HT1 #H1 #H2 #L2 #HL12 #X #H destruct
 163   elim (tpr_inv_cast1 … H) -H
 164   [ * #V2 #T2 #HV12 #HT12 #H destruct
 165     lapply (IH … HV1 … HL12 … HV12) -HV1 -HV12 /width=5/ #HV2
 166     lapply (IH … HT1 … HL12 … HT12) -IH -HT1 -HL12 -HT12 /width=5/ -L1 -V1 -T1 /2 width=1/
 167   | -HV1 #HT1X
 168      lapply (IH … HT1 … HL12 … HT1X) -IH -HT1 -HL12 -HT1X /width=5/
 169   ]
 170 ]
 171 qed.
 172
 173 /2 width=9/ qed.
 174
 175 lemma nta_ltpr_conf: ∀L1,T,A. L1 ⊢ T : A → ∀L2. L1 ➡ L2 → L2 ⊢ T : A.
 176 /2 width=5/ qed.
 177
 178 lemma nta_tpr_conf: ∀L,T1,A. L ⊢ T1 : A → ∀T2. T1 ➡ T2 → L ⊢ T2 : A.
 179 /2 width=5/ qed.