- lambda: first half of the standardization theorem is proved!

[helm.git] / matita / matita / contribs / lambda / labelled_sequential_computation.ma

diff --git a/matita/matita/contribs/lambda/labelled_sequential_computation.ma b/matita/matita/contribs/lambda/labelled_sequential_computation.ma
index fd096c0951199008e7f8bc526a0581dda8499e98..4a7392a7646eaff25e913ebfc1e9919f28e5d69b 100644 (file)
--- a/matita/matita/contribs/lambda/labelled_sequential_computation.ma
+++ b/matita/matita/contribs/lambda/labelled_sequential_computation.ma
@@ -12,17 +12,12 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "redex_pointer_sequence.ma".
+include "pointer_sequence.ma".
 include "labelled_sequential_reduction.ma".
 
 (* LABELLED SEQUENTIAL COMPUTATION (MULTISTEP) ******************************)
 
-(* Note: this comes from "star term lsred" *)
-inductive lsreds: rpseq → relation term ≝
-| lsreds_nil : ∀M. lsreds (◊) M M
-| lsreds_cons: ∀p,M1,M. M1 ⇀[p] M →
-               ∀s,M2. lsreds s M M2 → lsreds (p::s) M1 M2
-.
+definition lsreds: pseq → relation term ≝ lstar … lsred.
 
 interpretation "labelled sequential computation"
    'SeqRedStar M s N = (lsreds s M N).
@@ -31,63 +26,60 @@ notation "hvbox( M break ⇀* [ term 46 s ] break term 46 N )"
    non associative with precedence 45
    for @{ 'SeqRedStar $M $s $N }.
 
-lemma lsred_lsreds: ∀p,M1,M2. M1 ⇀[p] M2 → M1 ⇀*[p::◊] M2.
-/2 width=3/
+lemma lsreds_step_rc: ∀p,M1,M2. M1 ⇀[p] M2 → M1 ⇀*[p::◊] M2.
+/2 width=1/
 qed.
 
 lemma lsreds_inv_nil: ∀s,M1,M2. M1 ⇀*[s] M2 → ◊ = s → M1 = M2.
-#s #M1 #M2 * -s -M1 -M2 //
-#p #M1 #M #_ #s #M2 #_ #H destruct
+/2 width=5 by lstar_inv_nil/
 qed-.
 
 lemma lsreds_inv_cons: ∀s,M1,M2. M1 ⇀*[s] M2 → ∀q,r. q::r = s →
                        ∃∃M. M1 ⇀[q] M & M ⇀*[r] M2.
-#s #M1 #M2 * -s -M1 -M2
-[ #M #q #r #H destruct 
-| #p #M1 #M #HM1 #s #M2 #HM2 #q #r #H destruct /2 width=3/
-]
+/2 width=3 by lstar_inv_cons/
 qed-.
 
-lemma lsreds_inv_lsred: ∀p,M1,M2. M1 ⇀*[p::◊] M2 → M1 ⇀[p] M2.
-#p #M1 #M2 #H
-elim (lsreds_inv_cons … H ???) -H [4: // |2,3: skip ] #M #HM1 #H (**) (* simplify line *)
-<(lsreds_inv_nil … H ?) -H //
+lemma lsreds_inv_step_rc: ∀p,M1,M2. M1 ⇀*[p::◊] M2 → M1 ⇀[p] M2.
+/2 width=1 by lstar_inv_step/
 qed-.
 
-(* Note: "|s|" should be unparetesized *)
-lemma lsreds_fwd_mult: ∀s,M1,M2. M1 ⇀*[s] M2 → #{M2} ≤ #{M1} ^ (2 ^ (|s|)).
-#s #M1 #M2 #H elim H -s -M1 -M2 normalize //
-#p #M1 #M #HM1 #s #M2 #_ #IHM2
-lapply (lsred_fwd_mult … HM1) -p #HM1
-@(transitive_le … IHM2) -M2
-/3 width=1 by le_exp1, lt_O_exp, lt_to_le/ (**) (* auto: slow without trace *)
-qed-.
+lemma lsred_compatible_rc: ho_compatible_rc lsreds.
+/3 width=1/
+qed.
+
+lemma lsred_compatible_sn: ho_compatible_sn lsreds.
+/3 width=1/
+qed.
+
+lemma lsred_compatible_dx: ho_compatible_dx lsreds.
+/3 width=1/
+qed.
 
 lemma lsreds_lift: ∀s. liftable (lsreds s).
-#s #h #M1 #M2 #H elim H -s -M1 -M2 // /3 width=3/
+/2 width=1/
 qed.
 
-lemma lsreds_inv_lift: ∀s. deliftable (lsreds s).
-#s #h #N1 #N2 #H elim H -s -N1 -N2 /2 width=3/
-#p #N1 #N #HN1 #s #N2 #_ #IHN2 #d #M1 #HMN1
-elim (lsred_inv_lift … HN1 … HMN1) -N1 #M #HM1 #HMN
-elim (IHN2 … HMN) -N /3 width=3/
+lemma lsreds_inv_lift: ∀s. deliftable_sn (lsreds s).
+/3 width=3 by lstar_deliftable_sn, lsred_inv_lift/
 qed-.
 
 lemma lsreds_dsubst: ∀s. dsubstable_dx (lsreds s).
-#s #D #M1 #M2 #H elim H -s -M1 -M2 // /3 width=3/
+/2 width=1/
 qed.
 
 theorem lsreds_mono: ∀s. singlevalued … (lsreds s).
-#s #M #N1 #H elim H -s -M -N1
-[ /2 width=3 by lsreds_inv_nil/
-| #p #M #M1 #HM1 #s #N1 #_ #IHMN1 #N2 #H
-  elim (lsreds_inv_cons … H ???) -H [4: // |2,3: skip ] #M2 #HM2 #HMN2 (**) (* simplify line *)
-  lapply (lsred_mono … HM1 … HM2) -M #H destruct /2 width=1/
-]
+/3 width=7 by lstar_singlevalued, lsred_mono/
 qed-.
 
-theorem lsreds_trans: ∀s1,M1,M. M1 ⇀*[s1] M →
-                      ∀s2,M2. M ⇀*[s2] M2 → M1 ⇀*[s1@s2] M2.
-#s1 #M1 #M #H elim H -s1 -M1 -M normalize // /3 width=3/
+theorem lsreds_trans: ltransitive … lsreds.
+/2 width=3 by lstar_ltransitive/
+qed-.
+
+(* Note: "|s|" should be unparetesized *)
+lemma lsreds_fwd_mult: ∀s,M1,M2. M1 ⇀*[s] M2 → #{M2} ≤ #{M1} ^ (2 ^ (|s|)).
+#s #M1 #M2 #H @(lstar_ind_l ????????? H) -s -M1 normalize //
+#p #s #M1 #M #HM1 #_ #IHM2
+lapply (lsred_fwd_mult … HM1) -p #HM1
+@(transitive_le … IHM2) -M2
+/3 width=1 by le_exp1, lt_O_exp, lt_to_le/ (**) (* auto: slow without trace *)
 qed-.