matita/matita/contribs/lambdadelta/basic_2/etc/snta/snta_ltpr.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/snta_ltpss.ma".
  16 include "basic_2/dynamic/snta_thin.ma".
  17 include "basic_2/dynamic/lsubsn_snta.ma".
  18
  19 (* STRATIFIED NATIVE TYPE ASSIGNMENT ON TERMS *******************************)
  20 (*
  21 lemma snta_fwd_abst: ∀h,L,W1,W2,T,U,l2. ⦃h, L⦄ ⊢ ⓛW1.T :[l2] ⓛW2.U →
  22                      ∃∃V1,V2,l1. ⦃h, L⦄ ⊢ W1 :[l1] V1 & ⦃h, L⦄ ⊢ W2 :[l1] V2 &
  23                                  L ⊢ W1 ⬌* W2.
  24 #h #L #W1 #W2 #T #U #l2 #HTU
  25 elim (snta_fwd_correct … HTU) #X #H
  26 elim (snta_inv_bind1 … H) -H #W #T0 #l #HW2 #_ #_ -X
  27 elim (snta_inv_bind1 … HTU) -HTU #V1 #U0 #l0 #HWV1 #_ #H
  28 elim (cpcs_inv_abst … H Abst W1) -H
  29 #HW12 #_ -U0
  30 @(ex3_3_intro … HWV1 … HW12)
  31 [3: @(snta_conv … HTU0 HU0)
  32
  33  /3 width=3/
  34
  35 *)
  36 (*
  37 #h #L #V #T #U #l2 #HTU
  38 elim (snta_fwd_correct … HTU) #X #H
  39 elim (snta_inv_bind1 … H) -H #W #T0 #l1 #HVW #HUT0 #_ -X
  40 elim (snta_inv_bind1 … HTU) -HTU #W0 #U0 #l0 #_ #HTU0 #H -l0
  41 elim (cpcs_inv_abst … H Abst V) -H /3 width=3/
  42 qed-.
  43 *)
  44 (*
  45 lemma snta_fwd_appl1_sound_aux: ∀h,l0. (∀L1,L2,T1,T2,U,l.
  46                                         l < l0 → ⦃h, L1⦄ ⊢ T1 :[l] U →
  47                                         L1 ➡ L2 → L2 ⊢ T1 ➡* T2 → ⦃h, L2⦄ ⊢ T2 :[l] U
  48                                        ) →
  49                                 ∀L,T,U,l2. ⦃h, L⦄ ⊢ T :[l2] U →
  50                                 ∀Z,Y,X1. T = ⓐZ.ⓛY.X1 → l0 = l2 →
  51                                 ∃l1. ⦃h, L⦄ ⊢ Z :[l1+1] Y.
  52 #h #l0 #IH #L #T #U #l2 #H elim H -L -T -U -l2
  53 [
  54 |
  55 |
  56 |
  57 | #L #V #W1 #W2 #T #U #l1 #l2 #HVW2 #HTU #_ #_ #Z #Y #X1 #H1 #H2 destruct -IH
  58   elim (snta_fwd_abst … HTU) -X1 -U -l2 #Y0 #W0 #l0 #HY0 #H1 #HYW2
  59   elim (snta_fwd_correct … HVW2) #W #H2
  60   elim (snta_mono … H1 … H2) -H1 -H2 #H #_ destruct -W0 -W /4 width=6/
  61 | #L #V #T #U #W #l #HTU #HUW #Z #Y #X1 #X2 #H1 #H2 #H3 destruct
  62   elim (snta_inv_abst_sn … HTU) -HTU #Y0 #l0 #HY0 #HX12
  63 |
  64 | #L #T #U1 #U2 #V2 #l #HTU1 #HU12 #HUV2 #Z #Y #X1 #X2 #H1 #H2 #H3 destruct
  65
  66
  67
  68
  69
  70
  71
  72
  73
  74
  75
  76
  77
  78
  79
  80 lemma snta_inv_appl_aux: ∀h,l0. (∀L1,L2,T1,T2,U,l.
  81                                  l < l0 + 1 → ⦃h, L1⦄ ⊢ T1 :[l] U →
  82                                  L1 ➡ L2 → L2 ⊢ T1 ➡* T2 → ⦃h, L2⦄ ⊢ T2 :[l] U
  83                                 ) →
  84                          ∀L,T,U,l2. ⦃h, L⦄ ⊢ T :[l2] U →
  85                          ∀Z,Y,X1,X2. T = ⓐZ.ⓛY.X1 → U = ⓐZ.ⓛY.X2 → l0 = l2 →
  86                          ∃∃l1. ⦃h, L⦄ ⊢ Z :[l1+1] Y & ⦃h, L.ⓛY⦄ ⊢ X1 :[l2] X2.
  87 #h #l0 #IH #L #T #U #l2 * -L -T -U -l2
  88 [
  89 |
  90 |
  91 |
  92 | #L #V #W1 #W2 #T #U #l1 #l2 #HVW2 #HTU #Z #Y #X1 #X2 #H1 #H2 #H3 destruct -IH
  93   elim (snta_inv_abst … HTU) -HTU /2 width=2/
  94 | #L #V #T #U #W #l #HTU #HUW #Z #Y #X1 #X2 #H1 #H2 #H3 destruct
  95   elim (snta_inv_abst … HTU) -HTU #Y0 #l0 #HY0 #HX12
  96 |
  97 | #L #T #U1 #U2 #V2 #l #HTU1 #HU12 #HUV2 #Z #Y #X1 #X2 #H1 #H2 #H3 destruct
  98
  99    /2 width=2/
 100
 101
 102 axiom pippo: ∀h,l0. (∀L1,L2,T1,T2,U,l.
 103                 l < l0 + 1 → ⦃h, L1⦄ ⊢ T1 :[l] U →
 104                 L1 ➡ L2 → L2 ⊢ T1 ➡* T2 → ⦃h, L2⦄ ⊢ T2 :[l] U
 105              ) →
 106              ∀L,T1,U1,l. ⦃h, L⦄ ⊢ T1 :[l] U1 →
 107              ∀V2,W2,T2. L ⊢ T1 ➡* ⓐV2.ⓛW2.T2 → l0 = l →
 108              ∃l0. ⦃h, L2⦄ ⊢ V2 :[l0+1] W2.
 109 (*
 110 #h #l #IH #L1 #T1 #U1 #l1 * -L1 -T1 -U1 -l1
 111 [
 112 |
 113 |
 114 |
 115 | #L1 #V1 #W1 #T1 #U1 #l1 #HVW1 #HTU1 #Y1 #X1 #H1 #L2 #Y2 #HL12 #HY12 #Z2 #X2 #HX12 #H2 destruct
 116   elim (IH ??? Y2 … HVW1 HL12 ?) -HVW1 // [2: /3 width=1/ ] -HY12 #l21 #HY2W1 #H1l21 #H2l21
 117   elim (IH … HTU1 HL12 HX12) -IH -HTU1 -HL12 -HX12 // #l22 #H #_ #H2l22
 118   elim (snta_inv_bind1 … H) -H #Z #X #HZ2 #_ #H
 119   elim (cpcs_inv_abst … H Abst W1) -H #H #_
 120   lapply (transitive_le … (l21+l22) … H1l21 ?) -H1l21 // #Hl21
 121   @(ex3_1_intro … Hl21) [2: /3 width=1/ ]
 122   @(snta_conv … W1) /2 width=2/ (**) (* explicit constructors *)
 123 | #L1 #V1 #T1 #U1 #W1 #l1 #HTU1 #HUW1 #Y1 #X1 #H1 #L2 #Y2 #HL12 #HY12 #Z2 #X2 #HX12 #H2 destruct
 124
 125 *)
 126 (* Properties on context-free parallel reduction for local environments *****)
 127 *)
 128 fact snta_ltpr_tpr_conf_aux: ∀h,l0. (∀L1,L2,T1,T2,U,l.
 129                                 l < l0 → ⦃h, L1⦄ ⊢ T1 :[l] U →
 130                                 L1 ➡ L2 → L2 ⊢ T1 ➡* T2 → ⦃h, L2⦄ ⊢ T2 :[l] U
 131                              ) →
 132                              ∀L1,T1,U,l. ⦃h, L1⦄ ⊢ T1 :[l] U → ∀L2. L1 ➡ L2 →
 133                              ∀T2. T1 ➡ T2 → l0 = l → ⦃h, L2⦄ ⊢ T2 :[l] U.
 134 #h #l0 #IH #L1 #T1 #U #l #H elim H -L1 -T1 -U -l
 135 [ #L1 #k1 #L2 #_ #T2 #H #_ -l0
 136   >(tpr_inv_atom1 … H) -H //
 137 | #L1 #K1 #V1 #W #U #i1 #l #HLK1 #_ #HWU #IHV1 #L2 #HL12 #T2 #H #Hl -IH
 138   >(tpr_inv_atom1 … H) -T2
 139   elim (ltpr_ldrop_conf … HLK1 … HL12) -HLK1 -HL12 #X #HLK2 #H
 140   elim (ltpr_inv_pair1 … H) -H #K2 #V2 #HK12 #HV12 #H destruct /3 width=6/
 141 | #L1 #K1 #W1 #V1 #U1 #i1 #l #HLK1 #HWV1 #HWU1 #IHWV1 #L2 #HL12 #T2 #H #Hl -IH
 142 (*
 143   >(tpr_inv_atom1 … H) -T2
 144   elim (ltpr_ldrop_conf … HLK1 … HL12) -HLK1 -HL12 #X #HLK2 #H
 145   elim (ltpr_inv_pair1 … H) -H #K2 #W2 #HK12 #HW12 #H destruct
 146   lapply (ldrop_fwd_ldrop2 … HLK2) #HLK
 147   elim (lift_total V1 0 (i+1)) #W #HW
 148   lapply (snta_lift h … HLK … HWU1 … HW) /2 width=1/ -HLK -HW
 149   elim (lift_total W2 0 (i+1)) #U2 #HWU2
 150   lapply (tpr_lift … HW12 … HWU1 … HWU2) -HWU1 #HU12
 151   @(snta_conv … U2) /2 width=1/ /3 width=6/ (**) (* explicit constructor, /3 width=6/ is too slow *)
 152 *)
 153 | #I #L1 #V1 #W1 #T1 #U1 #l1 #l2 #_ #_ #IHVW1 #IHTU1 #L2 #HL12 #X #H #Hl -IH
 154 (*
 155   elim (tpr_inv_bind1 … H) -H *
 156   [ #V2 #T #T2 #HV12 #HT1 #HT2 #H destruct
 157     lapply (IHVW1 … HL12 … HV12) #HV2W1
 158     lapply (IHVW1 L2 … V1 ?) // -IHVW1 #HWV1
 159     lapply (IHTU1 (L2.ⓑ{I}V2) … HT1) -HT1 /2 width=1/ #HTU1
 160     lapply (IHTU1 (L2.ⓑ{I}V1) ? T1 ?) -IHTU1 // /2 width=1/ -HL12 #H
 161     lapply (tps_lsubs_trans … HT2 (L2.ⓑ{I}V2) ?) -HT2 /2 width=1/ #HT2
 162     lapply (snta_tps_conf … HTU1 … HT2) -T #HT2U1
 163     elim (snta_fwd_correct … H) -H #U2 #HU12
 164     @(snta_conv … (ⓑ{I}V2.U1)) /2 width=2/ /3 width=1/ (**) (* explicit constructor, /4 width=6/ is too slow *)
 165   | #T #HT1 #HTX #H destruct
 166     lapply (IHVW1 … HL12 V1 ?) -IHVW1 // #HVW1
 167     lapply (IHTU1 (L2.ⓓV1) … HT1) -T1 /2 width=1/ -L1 #H
 168     elim (snta_fwd_correct … H) #T1 #HUT1
 169     elim (snta_ldrop_conf … H L2 0 1 ? ?) -H // /2 width=1/ #T0 #U0 #HTU0 #H #HU10
 170     lapply (delift_inv_lift1_eq … H L2 … HTX) -H -HTX /2 width=1/ #H destruct
 171     @(snta_conv … HTU0) /2 width=2/
 172   ]
 173 *)
 174 | #L1 #V1 #W11 #W2 #T1 #U1 #l1 #l2 #_ #_ #IHVW1 #IHTU1 #L2 #HL12 #X #H #Hl -IH
 175 (*
 176   elim (tpr_inv_appl1 … H) -H *
 177   [ #V2 #Y #HV12 #HY #H destruct
 178     elim (tpr_inv_abst1 … HY) -HY #W2 #T2 #HW12 #HT12 #H destruct
 179     lapply (IHTU1 L2 ? (ⓛW1.T1) ?) // #H
 180     elim (snta_fwd_correct … H) -H #X #H
 181     elim (snta_inv_bind1 … H) -H #W #U #HW #HU #_
 182     @(snta_conv … (ⓐV2.ⓛW1.U1)) /4 width=2/ (**) (* explicit constructor, /5 width=5/ is too slow *)
 183   | #V2 #W2 #T0 #T2 #HV12 #HT02 #H1 #H2 destruct
 184     lapply (IHVW1 … HL12 … HV12) #HVW2
 185     lapply (IHVW1 … HL12 V1 ?) -IHVW1 // #HV1W2
 186     lapply (IHTU1 … HL12 (ⓛW2.T2) ?) -IHTU1 -HL12 /2 width=1/ -HT02 #H1
 187     elim (snta_fwd_correct … H1) #T #H2
 188     elim (snta_inv_bind1 … H1) -H1 #W #U2 #HW2 #HTU2 #H
 189     elim (cpcs_inv_abst … H Abst W2) -H #_ #HU21
 190     elim (snta_inv_bind1 … H2) -H2 #W0 #U0 #_ #H #_ -T -W0
 191     lapply (lsubsn_snta_trans … HTU2 (L2.ⓓV2) ?) -HTU2 /2 width=1/ #HTU2
 192     @(snta_conv … (ⓓV2.U2)) /2 width=2/ /3 width=2/ (**) (* explicit constructor, /4 width=5/ is too slow *)
 193   | #V0 #V2 #W0 #W2 #T0 #T2 #_ #_ #_ #_ #H destruct
 194   ]
 195 *)
 196 | #L1 #V1 #T1 #U1 #W1 #l #_ #HUW1 #IHTU1 #_ #L2 #HL12 #X #H #Hl
 197   elim (tpr_inv_appl1 … H) -H *
 198   [ #V2 #T2 #HV12 #HT12 #H destruct
 199     lapply (cpr_tpr … HV12 L2) #HV
 200     elim (snta_fwd_correct h L2 (ⓐV1.T1) (ⓐV1.U1) (l+1) ?) [2: /3 width=6/ ] #U
 201     @(snta_conv … (ⓐV2.U1)) /2 width=1/ -HV12 /4 width=8 by snta_pure, cprs_flat_dx/ (**) (* explicit constructor, /4 width=8/ is too slow without trace *)
 202   | #V2 #W0 #T0 #T2 #HV12 #HT02 #H1 #H2 destruct
 203     lapply (IHTU1 … HL12 (ⓛW0.T2) ? ?) -IHTU1 // /2 width=1/ -T0 #H1
 204     lapply (IH … (ⓐV2.U1) … HUW1 HL12 ?) // /3 width=1/ #H2
 205     lapply (snta_pure … H1 H2) -H2 #H
 206     elim (snta_inv_bind1 … H1) -H1 #V0 #U2 #l1 #HWV0 #HTU2 #HU21
 207     @(snta_conv … (ⓓV2.U2)) (**) (* explicit constructor *)
 208     [2:
 209 (*
 210         @snta_bind /3 width=2/ /3 width=6/ (**) (* /4 width=6/ is a bit slow *)
 211 *)
 212     |3: @(cpcs_cpr_conf … (ⓐV1.ⓛW0.U2)) /2 width=1/
 213     |4: /2 width=5/
 214     | skip
 215     ]
 216 (*
 217     elim (snta_fwd_pure1 … H) -H #T1 #W2 #HVW2 #HUT1 #HTW1
 218
 219     elim (cpcs_inv_abst1 … HU21) #W3 #U3 #HU13 #H
 220     elim (cprs_inv_abst … H Abst W0) -H #HW03 #_
 221     elim (pippo … IH … HUW1 ? V2 W3 U3 HL12 ? ?) -IH -HUW1 -HL12 // /3 width=1/ -HU13 #l2 #HV2W3
 222     lapply (snta_conv h L2 V2 W3 W0 V0 (l1+1) ? ? ?) /2 width=1/ -HV2W3 -HW03 -HWV0 #HV2W0
 223 *)
 224 (* SEGMENT 1.5
 225     lapply (IH … HV1 … HL12 … HV12) -HV1 -HV12 /width=5/ #HB
 226     lapply (IH … HB0  … HL12 W2 ?) -HB0 /width=5/ #HB0
 227     lapply (IH … HA0 … (L2.ⓛW2) … HT02) -IH -HA0 -HT02 /width=5/ -T0 /2 width=1/ -L1 -V1 /4 width=7/
 228
 229 axiom pippo: ⦃h, L⦄ ⊢ ⓐV.X : Y →
 230              ∃∃W,T. L ⊢ X ➡* ⓛW.T & ⦃h, L⦄ ⊢ ⓐV : W.
 231
 232 *)
 233 (* SEGMENT 2
 234 | #L1 #T1 #U1 #W1 #_ #_ #IHTU1 #IHUW1 #L2 #d #e #HL12 #X #H
 235   elim (tpss_inv_flat1 … H) -H #U2 #T2 #HU12 #HT12 #H destruct
 236   lapply (cpr_tpss … HU12) /4 width=4/
 237 | #L1 #T1 #U11 #U12 #U #_ #HU112 #_ #IHTU11 #IHU12 #L2 #d #e #HL12 #T2 #HT12
 238   @(snta_conv … U11) /2 width=5/ (**) (* explicot constructor, /3 width=7/ is too slow *)
 239 ]
 240 qed.
 241 *)
 242
 243 (* SEGMENT 3
 244 fact snta_ltpr_tpr_conf_aux: ∀h,L,T,L1,T1,U. ⦃h, L1⦄ ⊢ T1 : U → L = L1 → T = T1 →
 245                             ∀L2. L1 ➡ L2 → ∀T2. T1 ➡ T2 → ⦃h, L2⦄ ⊢ T2 : U.
 246
 247
 248   | #V0 #V2 #W0 #W2 #T0 #T2 #HV10 #HW02 #HT02 #HV02 #H1 #H2 destruct
 249     elim (snta_inv_abbr … HT1) -HT1 #B0 #HW0 #HT0
 250     lapply (IH … HW0  … HL12 … HW02) -HW0 /width=5/ #HW2
 251     lapply (IH … HV1 … HL12 … HV10) -HV1 -HV10 /width=5/ #HV0
 252     lapply (IH … HT0 … (L2.ⓓW2) … HT02) -IH -HT0 -HT02 /width=5/ -V1 -T0 /2 width=1/ -L1 -W0 #HT2
 253     @(snta_abbr … HW2) -HW2
 254     @(snta_appl … HT2) -HT2 /3 width=7/ (**) (* explict constructors, /5 width=7/ is too slow *)
 255   ]
 256 | #L1 #V1 #T1 #A #HV1 #HT1 #H1 #H2 #L2 #HL12 #X #H destruct
 257   elim (tpr_inv_cast1 … H) -H
 258   [ * #V2 #T2 #HV12 #HT12 #H destruct
 259     lapply (IH … HV1 … HL12 … HV12) -HV1 -HV12 /width=5/ #HV2
 260     lapply (IH … HT1 … HL12 … HT12) -IH -HT1 -HL12 -HT12 /width=5/ -L1 -V1 -T1 /2 width=1/
 261   | -HV1 #HT1X
 262      lapply (IH … HT1 … HL12 … HT1X) -IH -HT1 -HL12 -HT1X /width=5/
 263   ]
 264 ]
 265 qed.
 266
 267 lemma snta_ltpr_tpr_conf: ∀h,L1,T1,U. ⦃h, L1⦄ ⊢ T1 : U → ∀L2. L1 ➡ L2 →
 268                          ∀T2. T1 ➡ T2 → ⦃h, L2⦄ ⊢ T2 : U.
 269
 270 /2 width=9/ qed.
 271
 272 axiom snta_ltpr_conf: ∀L1,T,A. L1 ⊢ T : A → ∀L2. L1 ➡ L2 → L2 ⊢ T : A.
 273 /2 width=5/ qed.
 274
 275 axiom snta_tpr_conf: ∀L,T1,A. L ⊢ T1 : A → ∀T2. T1 ➡ T2 → L ⊢ T2 : A.
 276 /2 width=5/ qed.
 277 *)
 278 *)*)