update in ground_2 and basic_2

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / rt_computation / lprs_cprs.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lprs_cprs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lprs_cprs.ma
index ff82ee0a575821cc667e4378c2d58207af84a51d..b910b2763c065d77282fd4abecb1d20acc43c315 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lprs_cprs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lprs_cprs.ma
@@ -48,14 +48,14 @@ lemma lprs_ind_alt: ∀G. ∀R:relation lenv.
 
 (* Properties on context-sensitive parallel computation for terms ***********)
 
-lemma lprs_cpr_trans: ∀G. c_r_transitive … (cpr G) (λ_. lprs G).
-/3 width=5 by c_r_trans_LTC2, lpr_cprs_trans/ qed-.
+lemma lprs_cpr_trans: ∀G. b_c_transitive … (cpr G) (λ_. lprs G).
+/3 width=5 by b_c_trans_CTC2, lpr_cprs_trans/ qed-.
 
 (* Basic_1: was just: pr3_pr3_pr3_t *)
-(* Note: alternative proof /3 width=5 by s_r_trans_LTC1, lprs_cpr_trans/ *)
-lemma lprs_cprs_trans: ∀G. c_rs_transitive … (cpr G) (λ_. lprs G).
-#G @c_r_to_c_rs_trans @c_r_trans_LTC2
-@c_rs_trans_TC1 /2 width=3 by lpr_cprs_trans/ (**) (* full auto too slow *)
+(* Note: alternative proof /3 width=5 by s_r_trans_CTC1, lprs_cpr_trans/ *)
+lemma lprs_cprs_trans: ∀G. b_rs_transitive … (cpr G) (λ_. lprs G).
+#G @b_c_to_b_rs_trans @b_c_trans_CTC2
+@b_rs_trans_TC1 /2 width=3 by lpr_cprs_trans/ (**) (* full auto too slow *)
 qed-.
 
 lemma lprs_cprs_conf_dx: ∀G,L0,T0,T1. ⦃G, L0⦄ ⊢ T0 ➡* T1 →
@@ -117,7 +117,7 @@ lemma cprs_inv_abbr1: ∀a,G,L,V1,T1,U2. ⦃G, L⦄ ⊢ ⓓ{a}V1.T1 ➡* U2 →
                       ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ➡* V2 & ⦃G, L.ⓓV1⦄ ⊢ T1 ➡* T2 &
                                U2 = ⓓ{a}V2.T2
                       ) ∨
-                      â\88\83â\88\83T2. â¦\83G, L.â\93\93V1â¦\84 â\8a¢ T1 â\9e¡* T2 & â¬\86[0, 1] U2 â\89¡ T2 & a = true.
+                      â\88\83â\88\83T2. â¦\83G, L.â\93\93V1â¦\84 â\8a¢ T1 â\9e¡* T2 & â¬\86[0, 1] U2 â\89\98 T2 & a = true.
 #a #G #L #V1 #T1 #U2 #H @(cprs_ind … H) -U2 /3 width=5 by ex3_2_intro, or_introl/
 #U0 #U2 #_ #HU02 * *
 [ #V0 #T0 #HV10 #HT10 #H destruct
@@ -140,3 +140,41 @@ qed-.
 lemma lprs_pair2: ∀I,G,L1,L2. ⦃G, L1⦄ ⊢ ➡* L2 →
                   ∀V1,V2. ⦃G, L2⦄ ⊢ V1 ➡* V2 → ⦃G, L1.ⓑ{I}V1⦄ ⊢ ➡* L2.ⓑ{I}V2.
 /3 width=3 by lprs_pair, lprs_cprs_trans/ qed.
+
+(* Advanced inversion lemmas ************************************************)
+
+(* Basic_2A1: uses: scpds_inv_abst1 *)
+lemma cpms_inv_abst_sn (n) (h) (G) (L):
+                       ∀p,V1,T1,X2. ⦃G, L⦄ ⊢ ⓛ{p}V1.T1 ➡*[n, h] X2 →
+                       ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ➡*[h] V2 & ⦃G, L.ⓛV1⦄ ⊢ T1 ➡*[n, h] T2 &
+                                X2 = ⓛ{p}V2.T2.
+#n #h #G #L #p #V1 #T1 #X2 #H
+@(cpms_ind_dx … H) -X2 /2 width=5 by ex3_2_intro/
+#n1 #n2 #X #X2 #_ * #V #T #HV1 #HT1 #H1 #H2 destruct
+elim (cpm_inv_abst1 … H2) -H2 #V2 #T2 #HV2 #HT2 #H2 destruct
+@ex3_2_intro [1,2,5: // ] 
+[ /2 width=3 by cprs_step_dx/
+| @(cpms_trans … HT1) -T1 -V2 -n1
+
+/3 width=5 by cprs_step_dx, cpms_step_dx, ex3_2_intro/  
+
+
+
+#d2 * #X #d1 #Hd21 #Hd1 #H1 #H2
+lapply (da_inv_bind … Hd1) -Hd1 #Hd1
+elim (lstas_inv_bind1 … H1) -H1 #U #HTU1 #H destruct
+elim (cprs_inv_abst1 … H2) -H2 #V2 #T2 #HV12 #HUT2 #H destruct
+/3 width=6 by ex4_2_intro, ex3_2_intro/
+qed-.
+
+lemma scpds_inv_abbr_abst: ∀h,o,a1,a2,G,L,V1,W2,T1,T2,d. ⦃G, L⦄ ⊢ ⓓ{a1}V1.T1 •*➡*[h, o, d] ⓛ{a2}W2.T2 →
+                           ∃∃T. ⦃G, L.ⓓV1⦄ ⊢ T1 •*➡*[h, o, d] T & ⬆[0, 1] ⓛ{a2}W2.T2 ≘ T & a1 = true.
+#h #o #a1 #a2 #G #L #V1 #W2 #T1 #T2 #d2 * #X #d1 #Hd21 #Hd1 #H1 #H2
+lapply (da_inv_bind … Hd1) -Hd1 #Hd1
+elim (lstas_inv_bind1 … H1) -H1 #U1 #HTU1 #H destruct
+elim (cprs_inv_abbr1 … H2) -H2 *
+[ #V2 #U2 #HV12 #HU12 #H destruct
+| /3 width=6 by ex4_2_intro, ex3_intro/
+]
+qed-.
+*)