update in basic_2

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / equivalence / scpes_scpes.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/equivalence/scpes_scpes.ma b/matita/matita/contribs/lambdadelta/basic_2/equivalence/scpes_scpes.ma
index 2f8bcd9620fa746a01cdb43895de31ebac0f162e..24ea20ec0e13475a71a6cd75d75bb274dbf135a7 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/equivalence/scpes_scpes.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/equivalence/scpes_scpes.ma
@@ -19,44 +19,51 @@ include "basic_2/equivalence/scpes.ma".
 
 (* Advanced inversion lemmas ************************************************)
 
-lemma scpes_inv_abst2: ∀h,g,a,G,L,T1,T2,W2,l1,l2. ⦃G, L⦄ ⊢ T1 •*⬌*[h, g, l1, l2] ⓛ{a}W2.T2 →
-                       ∃∃W,T. ⦃G, L⦄ ⊢ T1 •*➡*[h, g, l1] ⓛ{a}W.T & ⦃G, L⦄ ⊢ W2 ➡* W & 
-                              ⦃G, L.ⓛW2⦄ ⊢ T2 •*➡*[h, g, l2] T.
-#h #g #a #G #L #T1 #T2 #W2 #l1 #l2 * #T0 #HT10 #H
+lemma scpes_inv_abst2: ∀h,o,a,G,L,T1,T2,W2,d1,d2. ⦃G, L⦄ ⊢ T1 •*⬌*[h, o, d1, d2] ⓛ{a}W2.T2 →
+                       ∃∃W,T. ⦃G, L⦄ ⊢ T1 •*➡*[h, o, d1] ⓛ{a}W.T & ⦃G, L⦄ ⊢ W2 ➡* W & 
+                              ⦃G, L.ⓛW2⦄ ⊢ T2 •*➡*[h, o, d2] T.
+#h #o #a #G #L #T1 #T2 #W2 #d1 #d2 * #T0 #HT10 #H
 elim (scpds_inv_abst1 … H) -H #W #T #HW2 #HT2 #H destruct /2 width=5 by ex3_2_intro/
 qed-.
 
 (* Advanced properties ******************************************************)
 
-lemma scpes_refl: ∀h,g,G,L,T,l1,l2. l2 ≤ l1 → ⦃G, L⦄ ⊢ T ▪[h, g] l1 →
-                  ⦃G, L⦄ ⊢ T •*⬌*[h, g, l2, l2] T.
-#h #g #G #L #T #l1 #l2 #Hl21 #Hl1
-elim (da_inv_sta … Hl1) #U #HTU
-elim (lstas_total … HTU l2) -U /3 width=3 by scpds_div, lstas_scpds/
+lemma scpes_refl: ∀h,o,G,L,T,d1,d2. d2 ≤ d1 → ⦃G, L⦄ ⊢ T ▪[h, o] d1 →
+                  ⦃G, L⦄ ⊢ T •*⬌*[h, o, d2, d2] T.
+#h #o #G #L #T #d1 #d2 #Hd21 #Hd1
+elim (da_lstas … Hd1 … d2) #U #HTU #_
+/3 width=3 by scpds_div, lstas_scpds/
 qed.
 
-lemma lstas_scpes_trans: ∀h,g,G,L,T1,l0,l1. ⦃G, L⦄ ⊢ T1 ▪[h, g] l0 → l1 ≤ l0 →
-                         ∀T. ⦃G, L⦄ ⊢ T1 •*[h, l1] T →
-                         ∀T2,l,l2. ⦃G, L⦄ ⊢ T •*⬌*[h,g,l,l2] T2 → ⦃G, L⦄ ⊢ T1 •*⬌*[h,g,l1+l,l2] T2.
-#h #g #G #L #T1 #l0 #l1 #Hl0 #Hl10 #T #HT1 #T2 #l #l2 *
+lemma lstas_scpes_trans: ∀h,o,G,L,T1,d0,d1. ⦃G, L⦄ ⊢ T1 ▪[h, o] d0 → d1 ≤ d0 →
+                         ∀T. ⦃G, L⦄ ⊢ T1 •*[h, d1] T →
+                         ∀T2,d,d2. ⦃G, L⦄ ⊢ T •*⬌*[h,o,d,d2] T2 → ⦃G, L⦄ ⊢ T1 •*⬌*[h,o,d1+d,d2] T2.
+#h #o #G #L #T1 #d0 #d1 #Hd0 #Hd10 #T #HT1 #T2 #d #d2 *
 /3 width=3 by scpds_div, lstas_scpds_trans/ qed-.
 
+(* Properties on parallel computation for terms *****************************)
+
+lemma cprs_scpds_div: ∀h,o,G,L,T1,T. ⦃G, L⦄ ⊢ T1 ➡* T →
+                      ∀d. ⦃G, L⦄ ⊢ T1 ▪[h, o] d →
+                      ∀T2,d2. ⦃G, L⦄ ⊢ T2 •*➡*[h, o, d2] T →
+                      ⦃G, L⦄⊢ T1 •*⬌*[h, o, 0, d2] T2.
+#h #o #G #L #T1 #T #HT1 #d #Hd elim (da_lstas … Hd 0)
+#X1 #HTX1 #_ elim (cprs_strip … HT1 X1) -HT1
+/3 width=5 by scpds_strap1, scpds_div, lstas_cpr, ex4_2_intro/
+qed.
+
 (* Main properties **********************************************************)
 
-theorem scpes_trans: ∀h,g,G,L,T1,T,l1,l. ⦃G, L⦄ ⊢ T1 •*⬌*[h, g, l1, l] T →
-                     ∀T2,l2. ⦃G, L⦄ ⊢ T •*⬌*[h, g, l, l2] T2 → ⦃G, L⦄ ⊢ T1 •*⬌*[h, g, l1, l2] T2.
-#h #g #G #L #T1 #T #l1 #l * #X1 #HT1X1 #HTX1 #T2 #l2 * #X2 #HTX2 #HT2X2
-elim (scpds_conf_eq … HTX1 … HTX2) -T -l /3 width=5 by scpds_cprs_trans, scpds_div/
+theorem scpes_trans: ∀h,o,G,L,T1,T,d1,d. ⦃G, L⦄ ⊢ T1 •*⬌*[h, o, d1, d] T →
+                     ∀T2,d2. ⦃G, L⦄ ⊢ T •*⬌*[h, o, d, d2] T2 → ⦃G, L⦄ ⊢ T1 •*⬌*[h, o, d1, d2] T2.
+#h #o #G #L #T1 #T #d1 #d * #X1 #HT1X1 #HTX1 #T2 #d2 * #X2 #HTX2 #HT2X2
+elim (scpds_conf_eq … HTX1 … HTX2) -T -d /3 width=5 by scpds_cprs_trans, scpds_div/
 qed-.
 
-theorem scpes_canc_sn: ∀h,g,G,L,T,T1,l,l1. ⦃G, L⦄ ⊢ T •*⬌*[h, g, l, l1] T1 →
-                       ∀T2,l2. ⦃G, L⦄ ⊢ T •*⬌*[h, g, l, l2] T2 → ⦃G, L⦄ ⊢ T1 •*⬌*[h, g, l1, l2] T2.
-#h #g #G #L #T #T1 #l #l1 #HT1
-@scpes_trans /2 width=1 by scpes_sym/ (**) (* full auto raises NTypeChecker failure *)
-qed-.
+theorem scpes_canc_sn: ∀h,o,G,L,T,T1,d,d1. ⦃G, L⦄ ⊢ T •*⬌*[h, o, d, d1] T1 →
+                       ∀T2,d2. ⦃G, L⦄ ⊢ T •*⬌*[h, o, d, d2] T2 → ⦃G, L⦄ ⊢ T1 •*⬌*[h, o, d1, d2] T2.
+/3 width=4 by scpes_trans, scpes_sym/ qed-.
 
-theorem scpes_canc_dx: ∀h,g,G,L,T1,T,l1,l. ⦃G, L⦄ ⊢ T1 •*⬌*[h, g, l1, l] T →
-                       ∀T2,l2. ⦃G, L⦄ ⊢ T2 •*⬌*[h, g, l2, l] T → ⦃G, L⦄ ⊢ T1 •*⬌*[h, g, l1, l2] T2.
-#h #g #G #L #T1 #T #l1 #l #HT1 #T2 #l2 #HT2
-@(scpes_trans … HT1) -T1 -l1 /2 width=1 by scpes_sym/ (**) (* full auto raises NTypeChecker failure *)
-qed-.
+theorem scpes_canc_dx: ∀h,o,G,L,T1,T,d1,d. ⦃G, L⦄ ⊢ T1 •*⬌*[h, o, d1, d] T →
+                       ∀T2,d2. ⦃G, L⦄ ⊢ T2 •*⬌*[h, o, d2, d] T → ⦃G, L⦄ ⊢ T1 •*⬌*[h, o, d1, d2] T2.
+/3 width=4 by scpes_trans, scpes_sym/ qed-.