- the PARTIAL COMMIT continues, we issue the "reduction" component

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / reduction / cpx_lift.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_lift.ma
index e3ac0af1990cc4a1af9b14960082d238ab69d427..f0337ff95fa4a181ca776b9237fbab7713f81236 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_lift.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_lift.ma
@@ -14,7 +14,6 @@
 
 include "basic_2/substitution/drop_drop.ma".
 include "basic_2/multiple/fqus_alt.ma".
-include "basic_2/static/sta.ma".
 include "basic_2/static/da.ma".
 include "basic_2/reduction/cpx.ma".
 
@@ -22,21 +21,29 @@ include "basic_2/reduction/cpx.ma".
 
 (* Advanced properties ******************************************************)
 
-lemma sta_cpx: ∀h,g,G,L,T1,T2,l. ⦃G, L⦄ ⊢ T1 •[h] T2 →
-               ⦃G, L⦄ ⊢ T1 ▪[h, g] l+1 → ⦃G, L⦄ ⊢ T1 ➡[h, g] T2.
-#h #g #G #L #T1 #T2 #l #H elim H -G -L -T1 -T2
-[ /3 width=4 by cpx_st, da_inv_sort/
-| #G #L #K #V1 #V2 #W2 #i #HLK #_ #HVW2 #IHV12 #H
+fact sta_cpx_aux: ∀h,g,G,L,T1,T2,l2,l1. ⦃G, L⦄ ⊢ T1 •*[h, l2] T2 → l2 = 1 →
+                  ⦃G, L⦄ ⊢ T1 ▪[h, g] l1+1 → ⦃G, L⦄ ⊢ T1 ➡[h, g] T2.
+#h #g #G #L #T1 #T2 #l2 #l1 #H elim H -G -L -T1 -T2 -l2
+[ #G #L #l2 #k #H0 destruct normalize
+  /3 width=4 by cpx_st, da_inv_sort/
+| #G #L #K #V1 #V2 #W2 #i #l2 #HLK #_ #HVW2 #IHV12 #H0 #H destruct
   elim (da_inv_lref … H) -H * #K0 #V0 [| #l0 ] #HLK0
   lapply (drop_mono … HLK0 … HLK) -HLK0 #H destruct /3 width=7 by cpx_delta/
-| #G #L #K #W1 #W2 #V1 #i #HLK #_ #HWV1 #IHW12 #H
-  elim (da_inv_lref … H) -H * #K0 #W0 [| #l1 ] #HLK0
-  lapply (drop_mono … HLK0 … HLK) -HLK0 #H destruct /3 width=7 by cpx_delta/
+| #G #L #K #V1 #V2 #i #_ #_ #_ #H destruct
+| #G #L #K #V1 #V2 #W2 #i #l2 #HLK #HV12 #HVW2 #_ #H0 #H
+  lapply (discr_plus_xy_y … H0) -H0 #H0 destruct
+  elim (da_inv_lref … H) -H * #K0 #V0 [| #l1 ] #HLK0
+  lapply (drop_mono … HLK0 … HLK) -HLK0 #H destruct
+  /4 width=7 by cpx_delta, cpr_cpx, lstas_cpr/
 | /4 width=2 by cpx_bind, da_inv_bind/
 | /4 width=3 by cpx_flat, da_inv_flat/
 | /4 width=3 by cpx_eps, da_inv_flat/
 ]
-qed.
+qed-.
+
+lemma sta_cpx: ∀h,g,G,L,T1,T2,l. ⦃G, L⦄ ⊢ T1 •*[h, 1] T2 →
+               ⦃G, L⦄ ⊢ T1 ▪[h, g] l+1 → ⦃G, L⦄ ⊢ T1 ➡[h, g] T2.
+/2 width=3 by sta_cpx_aux/ qed.
 
 (* Relocation properties ****************************************************)
 
@@ -155,7 +162,7 @@ lemma fqu_cpx_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐ ⦃G2, L2, T
 qed-.
 
 lemma fqu_sta_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐ ⦃G2, L2, T2⦄ →
-                     ∀U2. ⦃G2, L2⦄ ⊢ T2 •[h] U2 →
+                     ∀U2. ⦃G2, L2⦄ ⊢ T2 •*[h, 1] U2 →
                      ∀l. ⦃G2, L2⦄ ⊢ T2 ▪[h, g] l+1 →
                      ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ➡[h, g] U1 & ⦃G1, L1, U1⦄ ⊐ ⦃G2, L2, U2⦄.
 /3 width=5 by fqu_cpx_trans, sta_cpx/ qed-.
@@ -170,7 +177,7 @@ lemma fquq_cpx_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐⸮ ⦃G2, L
 qed-.
 
 lemma fquq_sta_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐⸮ ⦃G2, L2, T2⦄ →
-                      ∀U2. ⦃G2, L2⦄ ⊢ T2 •[h] U2 →
+                      ∀U2. ⦃G2, L2⦄ ⊢ T2 •*[h, 1] U2 →
                       ∀l. ⦃G2, L2⦄ ⊢ T2 ▪[h, g] l+1 →
                       ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ➡[h, g] U1 & ⦃G1, L1, U1⦄ ⊐⸮ ⦃G2, L2, U2⦄.
 /3 width=5 by fquq_cpx_trans, sta_cpx/ qed-.