matita/matita/contribs/lambdadelta/basic_2/dynamic/cpms_cpr.ma

   1
   2 include "basic_2/rt_computation/cpms_lpr.ma".
   3 (*
   4 lemma cpm_lsubr_trans (h) (n) (G) (L1) (T1):
   5       ∀T2. ⦃G,L1⦄ ⊢ T1 ➡[↑n,h] T2 → ∀L2. L1 ⫃ L2 →
   6       ∃∃T0. ⦃G,L2⦄ ⊢ T1 ➡[↑n,h] T0 & ⦃G,L2⦄ ⊢ T0 ➡*[h] T2.
   7 #h #m #G #L1 #T1 #T2
   8 @(insert_eq_0 … (↑m)) #n #H
   9 @(cpm_ind … H) -n -G -L1 -T1 -T2
  10 [
  11 |
  12 | #n #G #K1 #V1 #V2 #W2 #_ #IH #HVW2 #Hm #L2 #H destruct
  13   elim (lsubr_inv_bind1 … H) -H *
  14   [ #K2 #HK #H destruct
  15     elim (IH … HK) -K1 [| // ] #V0 #HV10 #HV02
  16     elim (lifts_total V0 (𝐔❴1❵)) #W0 #HVW0
  17     lapply (cpms_lifts_bi … HV02 (Ⓣ) … (K2.ⓓV1) … HVW0 … HVW2) -V2
  18     [ /3 width=2 by drops_refl, drops_drop/ ] #HW02
  19     /3 width=3 by cpm_delta, ex2_intro/
  20   | #K2 #VX #WX #HK #H1 #H2 destruct
  21     elim (IH … HK) -K1 [| // ] #X0 #H1 #H2
  22     elim (cpm_inv_cast1 … H1) -H1 [ * || * ]
  23     [ #W0 #V0 #HW0 #HV0 #H destruct
  24         @(ex2_intro … (#0)) [ // |
  25   | #I1 #I2 #K2 #VX #HK #H1 #H2 destruct
  26
  27 |
  28 |
  29 | #n #p #I #G #L1 #V1 #V2 #T1 #T2 #_ #_ #IHV #IHT #L2 #HL
  30   elim (IHV … HL) -IHV #V0 #HV01 #HV02
  31   elim (IHT (L2.ⓑ{I}V1)) [| /2 width=1 by lsubr_bind/ ] -L1 #T0 #HT10 #HT02
  32   @(ex2_intro … (ⓑ{p,I}V1.T0)) /3 width=3 by cprs_step_sn, cpms_bind, cpm_bind/ (**) (* full auto a bit slow *)
  33 |
  34 |
  35 |  //
  36 *)
  37 (*
  38 lemma cpr_cpm_trans_swap_lsubr_lpr (h) (G) (L1) (T1):
  39       ∀T. ⦃G,L1⦄ ⊢ T1 ➡[h] T → ∀L. L ⫃ L1 →
  40       ∀L2. ⦃G,L⦄ ⊢ ➡[h] L2 → ∀n2,T2. ⦃G,L2⦄ ⊢ T ➡[n2,h] T2 →
  41       ∃∃T0. ⦃G,L⦄ ⊢ T1 ➡[n2,h] T0 & ⦃G,L⦄ ⊢ T0 ➡*[h] T2.
  42 #h #G #L1 #T1 @(fqup_wf_ind_eq (Ⓣ) … G L1 T1) -G -L1 -T1
  43 #G0 #L0 #T0 #IH #G #L1 * [| * [| * ]]
  44 [ (*
  45   #I #HG #HL #HT #X #H1 #L2 #HL12 #m2 #X2 #H2 destruct
  46   elim (cpr_inv_atom1 … H1) -H1 [|*: * ]
  47   [ #H destruct
  48     elim (cpm_inv_atom1 … H2) -H2 *
  49     [ #H1 #H2 destruct /3 width=3 by cpm_cpms, ex2_intro/
  50     | #s #H1 #H2 #H3 destruct /2 width=3 by ex2_intro/
  51     | #K2 #V #V2 #HV2 #HVT2 #H1 #H2 destruct
  52       elim (lpr_inv_pair_dx … HL12) -HL12 #K1 #V1 #HK12 #HV1 #H destruct
  53       elim (IH … HV1 … HK12 … HV2) -K2 -V -IH
  54       [| /2 width=1 by fqu_fqup, fqu_lref_O/ ] #V0 #HV10 #HV02
  55       elim (lifts_total V0 (𝐔❴1❵)) #T0 #HVT0
  56       lapply (cpms_lifts_bi … HV02 (Ⓣ) … (K1.ⓓV1) … HVT0 … HVT2) -V2
  57       [ /3 width=2 by drops_refl, drops_drop/ ] #HT02
  58       /3 width=3 by cpm_delta, ex2_intro/
  59     | #n2 #K2 #W #W2 #HW2 #HWT2 #H1 #H2 #H3 destruct
  60       elim (lpr_inv_pair_dx … HL12) -HL12 #K1 #W1 #HK12 #HW1 #H destruct
  61       elim (IH … HW1 … HK12 … HW2) -K2 -W -IH
  62       [| /2 width=1 by fqu_fqup, fqu_lref_O/ ] #W0 #HW10 #HW02
  63       elim (lifts_total W0 (𝐔❴1❵)) #T0 #HWT0
  64       lapply (cpms_lifts_bi … HW02 (Ⓣ) … (K1.ⓛW1) … HWT0 … HWT2) -W2
  65       [ /3 width=2 by drops_refl, drops_drop/ ] #HT02
  66       /3 width=3 by cpm_ell, ex2_intro/
  67     | #I2 #K2 #T2 #i #HT2 #HTU2 #H1 #H2 destruct
  68       elim (lpr_inv_bind_dx … HL12) -HL12 #I1 #K1 #HK12 #_ #H destruct
  69       elim (IH … (#i) … HK12 … HT2) -I2 -K2 -IH
  70       [|*: /2 width=1 by fqu_fqup/ ] #T0 #HT10 #HT02
  71       elim (lifts_total T0 (𝐔❴1❵)) #U0 #HTU0
  72       lapply (cpms_lifts_bi … HT02 (Ⓣ) … (K1.ⓘ{I1}) … HTU0 … HTU2) -T2
  73       [ /3 width=2 by drops_refl, drops_drop/ ] #HU02
  74       /3 width=3 by cpm_lref, ex2_intro/
  75     ]
  76   | #K1 #V1 #V #HV1 #HVT #H1 #H2 destruct
  77     elim (lpr_inv_pair_sn … HL12) -HL12 #K2 #V0 #HK12 #_ #H destruct
  78     elim (cpm_inv_lifts_sn … H2 (Ⓣ) … HVT) -X
  79     [|*: /3 width=2 by drops_refl, drops_drop/ ] -V0 #V2 #HVT2 #HV2
  80     elim (IH … HV1 … HK12 … HV2) -K2 -V -IH
  81     [| /2 width=1 by fqu_fqup, fqu_lref_O/ ] #V0 #HV10 #HV02
  82     elim (lifts_total V0 (𝐔❴1❵)) #T0 #HVT0
  83     lapply (cpms_lifts_bi … HV02 (Ⓣ) … (K1.ⓓV1) … HVT0 … HVT2) -V2
  84     [ /3 width=2 by drops_refl, drops_drop/ ] #HT02
  85     /3 width=3 by cpm_delta, ex2_intro/
  86   | #I1 #K1 #T #i #HT1 #HTU #H1 #H2 destruct
  87     elim (lpr_inv_bind_sn … HL12) -HL12 #I2 #K2 #HK12 #_ #H destruct
  88     elim (cpm_inv_lifts_sn … H2 (Ⓣ) … HTU) -X
  89     [|*: /3 width=2 by drops_refl, drops_drop/ ] -I2 #T2 #HTU2 #HT2
  90     elim (IH … HT1 … HK12 … HT2) -K2 -T -IH
  91     [| /2 width=1 by fqu_fqup/ ] #T0 #HT10 #HT02
  92     elim (lifts_total T0 (𝐔❴1❵)) #U0 #HTU0
  93     lapply (cpms_lifts_bi … HT02 (Ⓣ) … (K1.ⓘ{I1}) … HTU0 … HTU2) -T2
  94     [ /3 width=2 by drops_refl, drops_drop/ ] #HU02
  95     /3 width=3 by cpm_lref, ex2_intro/
  96   ]
  97 *)
  98 | (*
  99   #p #I #V1 #T1 #HG #HL #HT #X #H1 #L2 #HL12 #n2 #X2 #H2
 100   elim (cpm_inv_bind1 … H1) -H1 *
 101   [ #V #T #HV1 #HT1 #H destruct
 102     elim (cpm_inv_bind1 … H2) -H2 *
 103     [ #V2 #T2 #HV2 #HT2 #H destruct
 104       elim (IH … HT1 … HT2) -T
 105       [|*: /2 width=1 by lpr_pair/ ] #T0 #HT10 #HT02
 106       elim (IH … HV1 … HL12 … HV2) -L2 -V -IH
 107       [| // ] #V0 #HV10 #HV02
 108       /4 width=7 by cpms_bind, cpms_step_sn, cpm_bind, ex2_intro/
 109     | #X #HXT #HX2 #H1 #H2 destruct
 110       elim (cpm_lifts_sn … HX2 (Ⓣ) … (L2.ⓓV) … HXT) -HX2
 111       [| /3 width=2 by drops_refl, drops_drop/ ] #T2 #HXT2 #HT2
 112       elim (IH … HT1 … HT2) -HT2 -IH
 113       [|*: /2 width=1 by lpr_pair/ ] -L2 #T0 #HT10 #HT02
 114       /3 width=6 by cpms_zeta_dx, cpm_bind, ex2_intro/
 115     ]
 116   | #X1 #HXT1 #HX1 #H1 #H2 destruct
 117     elim (IH … HX1 … HL12 … H2) -L2 -X -IH
 118     [| /2 width=1 by fqup_zeta/ ] #X0 #HX10 #HX02
 119     /3 width=3 by cpm_zeta, ex2_intro/
 120   ]
 121 *)
 122 | #V1 #T1 #HG #HL #HT #X #H1 #L #HL1 #L2 #HL2 #m2 #X2 #H2 destruct
 123   elim (cpm_inv_appl1 … H1) -H1 *
 124   [ (*
 125     #V #T #HV1 #HT1 #H destruct
 126     elim (cpm_inv_appl1 … H2) -H2 *
 127     [ #V2 #T2 #HV2 #HT2 #H destruct
 128       elim (IH … HV1 … HL12 … HV2) -V [| // ] #V0 #HV10 #HV02
 129       elim (IH … HT1 … HL12 … HT2) -L2 -T -IH [| // ] #T0 #HT10 #HT02
 130       /3 width=5 by cpms_appl, cpm_appl, ex2_intro/
 131     | #q #V2 #WX #W2 #TX #T2 #HV2 #HW2 #HT2 #H1 #H2 destruct
 132       elim (IH … HV1 … HL12 … HV2) -V [| // ] #V0 #HV10 #HV02
 133       elim (IH … HT1 … HL12 m2 (ⓛ{q}W2.T2)) -IH -HT1
 134       [|*: /2 width=1 by cpm_bind/ ] -L2 -WX -TX #T0 #HT10 #HT02
 135       /4 width=9 by cprs_step_dx, cpms_appl, cpm_beta, cpm_appl, ex2_intro/
 136     | #q #V2 #U2 #WX #W2 #TX #T2 #HV2 #HVU2 #HW2 #HT2 #H1 #H2 destruct
 137       elim (IH … HV1 … HL12 … HV2) -V [| // ] #V0 #HV10 #HV02
 138       elim (IH … HT1 … HL12 m2 (ⓓ{q}W2.T2)) -IH -HT1
 139       [|*: /2 width=1 by cpm_bind/ ] -L2 -WX -TX #T0 #HT10 #HT02
 140       /4 width=11 by cprs_step_dx, cpms_appl, cpm_theta, cpm_appl, ex2_intro/
 141     ]
 142     *)
 143   | #p #V #W1 #W #TX1 #T #HV1 #HW1 #HT1 #H1 #H3 destruct
 144     elim (cpm_inv_abbr1 … H2) -H2 *
 145     [ #X3 #T2 #H2 #HT2 #H destruct
 146       elim (cpr_inv_cast1 … H2) -H2 [ * ]
 147       [ #W2 #V2 #HW2 #HV2 #H destruct
 148         elim (IH … HT1 (L.ⓓⓝW1.V1) … HT2) -T
 149         [|*: /4 width=3 by lsubr_beta, lpr_pair, cpm_cast, lsubr_cpm_trans/ ] #T0 #HT10 #HT02
 150         elim (IH … HV1 … HL1 … HL2 … HV2) -V [| // ] #V0 #HV10 #HV02
 151         elim (IH … HW1 … HL1 … HL2 … HW2) -L2 -W -IH [| // ] #W0 #HW10 #HW02
 152         @(ex2_intro … (ⓓ{p}ⓝW1.V1.T0))
 153         [ @cpm_beta //
 154
 155            /2 width=1 by cpm_beta/
 156       | /3 width=7 by cprs_step_dx, cpms_appl, cpm_beta/
 157
 158        @cprs_step_dx [| @(cpms_appl … HT02 … HV02) | /2 width=1 by cpm_beta/
 159       @cpms_beta
 160 *)