X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fdynamic%2Fcpms_cpr.ma;fp=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fdynamic%2Fcpms_cpr.ma;h=cdcb23adf484834f2cff6ea6027ef06acb1a17a4;hb=de3a41b9a4e51dc1b09adce800273adf5ffa1215;hp=0000000000000000000000000000000000000000;hpb=c27d792e734c91a9b80cf8456e2c755aae24e994;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cpms_cpr.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cpms_cpr.ma
new file mode 100644
index 000000000..cdcb23adf
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cpms_cpr.ma
@@ -0,0 +1,160 @@
+
+include "basic_2/rt_computation/cpms_lpr.ma".
+(*
+lemma cpm_lsubr_trans (h) (n) (G) (L1) (T1):
+      ∀T2. ⦃G,L1⦄ ⊢ T1 ➡[↑n,h] T2 → ∀L2. L1 ⫃ L2 →
+      ∃∃T0. ⦃G,L2⦄ ⊢ T1 ➡[↑n,h] T0 & ⦃G,L2⦄ ⊢ T0 ➡*[h] T2.
+#h #m #G #L1 #T1 #T2
+@(insert_eq_0 … (↑m)) #n #H
+@(cpm_ind … H) -n -G -L1 -T1 -T2
+[ 
+|
+| #n #G #K1 #V1 #V2 #W2 #_ #IH #HVW2 #Hm #L2 #H destruct
+  elim (lsubr_inv_bind1 … H) -H *
+  [ #K2 #HK #H destruct
+    elim (IH … HK) -K1 [| // ] #V0 #HV10 #HV02
+    elim (lifts_total V0 (𝐔❴1❵)) #W0 #HVW0
+    lapply (cpms_lifts_bi … HV02 (Ⓣ) … (K2.ⓓV1) … HVW0 … HVW2) -V2
+    [ /3 width=2 by drops_refl, drops_drop/ ] #HW02
+    /3 width=3 by cpm_delta, ex2_intro/
+  | #K2 #VX #WX #HK #H1 #H2 destruct
+    elim (IH … HK) -K1 [| // ] #X0 #H1 #H2
+    elim (cpm_inv_cast1 … H1) -H1 [ * || * ]
+    [ #W0 #V0 #HW0 #HV0 #H destruct
+        @(ex2_intro … (#0)) [ // | 
+  | #I1 #I2 #K2 #VX #HK #H1 #H2 destruct   
+    
+|
+|
+| #n #p #I #G #L1 #V1 #V2 #T1 #T2 #_ #_ #IHV #IHT #L2 #HL
+  elim (IHV … HL) -IHV #V0 #HV01 #HV02
+  elim (IHT (L2.ⓑ{I}V1)) [| /2 width=1 by lsubr_bind/ ] -L1 #T0 #HT10 #HT02
+  @(ex2_intro … (ⓑ{p,I}V1.T0)) /3 width=3 by cprs_step_sn, cpms_bind, cpm_bind/ (**) (* full auto a bit slow *)
+| 
+|
+|  //   
+*)
+(*
+lemma cpr_cpm_trans_swap_lsubr_lpr (h) (G) (L1) (T1):
+      ∀T. ⦃G,L1⦄ ⊢ T1 ➡[h] T → ∀L. L ⫃ L1 →
+      ∀L2. ⦃G,L⦄ ⊢ ➡[h] L2 → ∀n2,T2. ⦃G,L2⦄ ⊢ T ➡[n2,h] T2 →
+      ∃∃T0. ⦃G,L⦄ ⊢ T1 ➡[n2,h] T0 & ⦃G,L⦄ ⊢ T0 ➡*[h] T2.
+#h #G #L1 #T1 @(fqup_wf_ind_eq (Ⓣ) … G L1 T1) -G -L1 -T1
+#G0 #L0 #T0 #IH #G #L1 * [| * [| * ]]
+[ (*
+  #I #HG #HL #HT #X #H1 #L2 #HL12 #m2 #X2 #H2 destruct
+  elim (cpr_inv_atom1 … H1) -H1 [|*: * ]
+  [ #H destruct
+    elim (cpm_inv_atom1 … H2) -H2 *
+    [ #H1 #H2 destruct /3 width=3 by cpm_cpms, ex2_intro/
+    | #s #H1 #H2 #H3 destruct /2 width=3 by ex2_intro/
+    | #K2 #V #V2 #HV2 #HVT2 #H1 #H2 destruct
+      elim (lpr_inv_pair_dx … HL12) -HL12 #K1 #V1 #HK12 #HV1 #H destruct
+      elim (IH … HV1 … HK12 … HV2) -K2 -V -IH
+      [| /2 width=1 by fqu_fqup, fqu_lref_O/ ] #V0 #HV10 #HV02
+      elim (lifts_total V0 (𝐔❴1❵)) #T0 #HVT0
+      lapply (cpms_lifts_bi … HV02 (Ⓣ) … (K1.ⓓV1) … HVT0 … HVT2) -V2
+      [ /3 width=2 by drops_refl, drops_drop/ ] #HT02
+      /3 width=3 by cpm_delta, ex2_intro/
+    | #n2 #K2 #W #W2 #HW2 #HWT2 #H1 #H2 #H3 destruct
+      elim (lpr_inv_pair_dx … HL12) -HL12 #K1 #W1 #HK12 #HW1 #H destruct
+      elim (IH … HW1 … HK12 … HW2) -K2 -W -IH
+      [| /2 width=1 by fqu_fqup, fqu_lref_O/ ] #W0 #HW10 #HW02
+      elim (lifts_total W0 (𝐔❴1❵)) #T0 #HWT0
+      lapply (cpms_lifts_bi … HW02 (Ⓣ) … (K1.ⓛW1) … HWT0 … HWT2) -W2
+      [ /3 width=2 by drops_refl, drops_drop/ ] #HT02
+      /3 width=3 by cpm_ell, ex2_intro/
+    | #I2 #K2 #T2 #i #HT2 #HTU2 #H1 #H2 destruct
+      elim (lpr_inv_bind_dx … HL12) -HL12 #I1 #K1 #HK12 #_ #H destruct
+      elim (IH … (#i) … HK12 … HT2) -I2 -K2 -IH
+      [|*: /2 width=1 by fqu_fqup/ ] #T0 #HT10 #HT02
+      elim (lifts_total T0 (𝐔❴1❵)) #U0 #HTU0
+      lapply (cpms_lifts_bi … HT02 (Ⓣ) … (K1.ⓘ{I1}) … HTU0 … HTU2) -T2
+      [ /3 width=2 by drops_refl, drops_drop/ ] #HU02
+      /3 width=3 by cpm_lref, ex2_intro/
+    ]
+  | #K1 #V1 #V #HV1 #HVT #H1 #H2 destruct
+    elim (lpr_inv_pair_sn … HL12) -HL12 #K2 #V0 #HK12 #_ #H destruct
+    elim (cpm_inv_lifts_sn … H2 (Ⓣ) … HVT) -X
+    [|*: /3 width=2 by drops_refl, drops_drop/ ] -V0 #V2 #HVT2 #HV2
+    elim (IH … HV1 … HK12 … HV2) -K2 -V -IH
+    [| /2 width=1 by fqu_fqup, fqu_lref_O/ ] #V0 #HV10 #HV02
+    elim (lifts_total V0 (𝐔❴1❵)) #T0 #HVT0
+    lapply (cpms_lifts_bi … HV02 (Ⓣ) … (K1.ⓓV1) … HVT0 … HVT2) -V2
+    [ /3 width=2 by drops_refl, drops_drop/ ] #HT02
+    /3 width=3 by cpm_delta, ex2_intro/
+  | #I1 #K1 #T #i #HT1 #HTU #H1 #H2 destruct
+    elim (lpr_inv_bind_sn … HL12) -HL12 #I2 #K2 #HK12 #_ #H destruct
+    elim (cpm_inv_lifts_sn … H2 (Ⓣ) … HTU) -X
+    [|*: /3 width=2 by drops_refl, drops_drop/ ] -I2 #T2 #HTU2 #HT2
+    elim (IH … HT1 … HK12 … HT2) -K2 -T -IH
+    [| /2 width=1 by fqu_fqup/ ] #T0 #HT10 #HT02
+    elim (lifts_total T0 (𝐔❴1❵)) #U0 #HTU0
+    lapply (cpms_lifts_bi … HT02 (Ⓣ) … (K1.ⓘ{I1}) … HTU0 … HTU2) -T2
+    [ /3 width=2 by drops_refl, drops_drop/ ] #HU02
+    /3 width=3 by cpm_lref, ex2_intro/
+  ]
+*)
+| (*
+  #p #I #V1 #T1 #HG #HL #HT #X #H1 #L2 #HL12 #n2 #X2 #H2
+  elim (cpm_inv_bind1 … H1) -H1 *
+  [ #V #T #HV1 #HT1 #H destruct
+    elim (cpm_inv_bind1 … H2) -H2 *
+    [ #V2 #T2 #HV2 #HT2 #H destruct
+      elim (IH … HT1 … HT2) -T
+      [|*: /2 width=1 by lpr_pair/ ] #T0 #HT10 #HT02
+      elim (IH … HV1 … HL12 … HV2) -L2 -V -IH
+      [| // ] #V0 #HV10 #HV02
+      /4 width=7 by cpms_bind, cpms_step_sn, cpm_bind, ex2_intro/
+    | #X #HXT #HX2 #H1 #H2 destruct
+      elim (cpm_lifts_sn … HX2 (Ⓣ) … (L2.ⓓV) … HXT) -HX2
+      [| /3 width=2 by drops_refl, drops_drop/ ] #T2 #HXT2 #HT2
+      elim (IH … HT1 … HT2) -HT2 -IH
+      [|*: /2 width=1 by lpr_pair/ ] -L2 #T0 #HT10 #HT02
+      /3 width=6 by cpms_zeta_dx, cpm_bind, ex2_intro/
+    ]
+  | #X1 #HXT1 #HX1 #H1 #H2 destruct
+    elim (IH … HX1 … HL12 … H2) -L2 -X -IH
+    [| /2 width=1 by fqup_zeta/ ] #X0 #HX10 #HX02
+    /3 width=3 by cpm_zeta, ex2_intro/
+  ]
+*)
+| #V1 #T1 #HG #HL #HT #X #H1 #L #HL1 #L2 #HL2 #m2 #X2 #H2 destruct
+  elim (cpm_inv_appl1 … H1) -H1 *
+  [ (*
+    #V #T #HV1 #HT1 #H destruct
+    elim (cpm_inv_appl1 … H2) -H2 *
+    [ #V2 #T2 #HV2 #HT2 #H destruct
+      elim (IH … HV1 … HL12 … HV2) -V [| // ] #V0 #HV10 #HV02
+      elim (IH … HT1 … HL12 … HT2) -L2 -T -IH [| // ] #T0 #HT10 #HT02
+      /3 width=5 by cpms_appl, cpm_appl, ex2_intro/
+    | #q #V2 #WX #W2 #TX #T2 #HV2 #HW2 #HT2 #H1 #H2 destruct
+      elim (IH … HV1 … HL12 … HV2) -V [| // ] #V0 #HV10 #HV02
+      elim (IH … HT1 … HL12 m2 (ⓛ{q}W2.T2)) -IH -HT1
+      [|*: /2 width=1 by cpm_bind/ ] -L2 -WX -TX #T0 #HT10 #HT02
+      /4 width=9 by cprs_step_dx, cpms_appl, cpm_beta, cpm_appl, ex2_intro/
+    | #q #V2 #U2 #WX #W2 #TX #T2 #HV2 #HVU2 #HW2 #HT2 #H1 #H2 destruct
+      elim (IH … HV1 … HL12 … HV2) -V [| // ] #V0 #HV10 #HV02
+      elim (IH … HT1 … HL12 m2 (ⓓ{q}W2.T2)) -IH -HT1
+      [|*: /2 width=1 by cpm_bind/ ] -L2 -WX -TX #T0 #HT10 #HT02
+      /4 width=11 by cprs_step_dx, cpms_appl, cpm_theta, cpm_appl, ex2_intro/
+    ]
+    *)
+  | #p #V #W1 #W #TX1 #T #HV1 #HW1 #HT1 #H1 #H3 destruct
+    elim (cpm_inv_abbr1 … H2) -H2 *
+    [ #X3 #T2 #H2 #HT2 #H destruct
+      elim (cpr_inv_cast1 … H2) -H2 [ * ]
+      [ #W2 #V2 #HW2 #HV2 #H destruct
+        elim (IH … HT1 (L.ⓓⓝW1.V1) … HT2) -T
+        [|*: /4 width=3 by lsubr_beta, lpr_pair, cpm_cast, lsubr_cpm_trans/ ] #T0 #HT10 #HT02
+        elim (IH … HV1 … HL1 … HL2 … HV2) -V [| // ] #V0 #HV10 #HV02
+        elim (IH … HW1 … HL1 … HL2 … HW2) -L2 -W -IH [| // ] #W0 #HW10 #HW02
+        @(ex2_intro … (ⓓ{p}ⓝW1.V1.T0))
+        [ @cpm_beta //
+          
+           /2 width=1 by cpm_beta/
+      | /3 width=7 by cprs_step_dx, cpms_appl, cpm_beta/
+      
+       @cprs_step_dx [| @(cpms_appl … HT02 … HV02) | /2 width=1 by cpm_beta/
+      @cpms_beta
+*)