X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambda%2Flabelled_hap_computation.ma;h=4441961e1319391ec6d0cae55ff69827014f3efa;hb=2199f327081f49b21bdcd23d702b5e07ea4f58ce;hp=e7804cb7c18a28b0214b27bd045becadf7b843d6;hpb=cdcfe9f97936f02dab1970ebf3911940bf0a4e29;p=helm.git

diff --git a/matita/matita/contribs/lambda/labelled_hap_computation.ma b/matita/matita/contribs/lambda/labelled_hap_computation.ma
index e7804cb7c..4441961e1 100644
--- a/matita/matita/contribs/lambda/labelled_hap_computation.ma
+++ b/matita/matita/contribs/lambda/labelled_hap_computation.ma
@@ -20,7 +20,7 @@ include "labelled_hap_reduction.ma".
 (* Note: this is the "head in application" computation of:
          R. Kashima: "A proof of the Standization Theorem in λ-Calculus". Typescript note, (2000).
 *)
-definition lhap: rpseq → relation term ≝ lstar … lhap1.
+definition lhap: pseq → relation term ≝ lstar … lhap1.
 
 interpretation "labelled 'hap' computation"
    'HApStar M p N = (lhap p M N).
@@ -29,7 +29,7 @@ notation "hvbox( M break ⓗ⇀* [ term 46 p ] break term 46 N )"
    non associative with precedence 45
    for @{ 'HApStar $M $p $N }.
 
-lemma lhap1_lhap: ∀p,M1,M2. M1 ⓗ⇀[p] M2 → M1 ⓗ⇀*[p::◊] M2.
+lemma lhap_step_rc: ∀p,M1,M2. M1 ⓗ⇀[p] M2 → M1 ⓗ⇀*[p::◊] M2.
 /2 width=1/
 qed.
 
@@ -42,10 +42,19 @@ lemma lhap_inv_cons: ∀s,M1,M2. M1 ⓗ⇀*[s] M2 → ∀q,r. q::r = s →
 /2 width=3 by lstar_inv_cons/
 qed-.
 
-lemma lhap_inv_lhap1: ∀p,M1,M2. M1 ⓗ⇀*[p::◊] M2 → M1 ⓗ⇀[p] M2.
+lemma lhap_inv_step_rc: ∀p,M1,M2. M1 ⓗ⇀*[p::◊] M2 → M1 ⓗ⇀[p] M2.
 /2 width=1 by lstar_inv_step/
 qed-.
 
+lemma lhap_inv_pos: ∀s,M1,M2. M1 ⓗ⇀*[s] M2 → 0 < |s| →
+                    ∃∃p,r,M. p::r = s & M1 ⓗ⇀[p] M & M ⓗ⇀*[r] M2.
+/2 width=1 by lstar_inv_pos/
+qed-.
+
+lemma lhap_compatible_dx: ho_compatible_dx lhap.
+/3 width=1/
+qed.
+
 lemma lhap_lift: ∀s. liftable (lhap s).
 /2 width=1/
 qed.
@@ -57,38 +66,34 @@ qed-.
 lemma lhap_dsubst: ∀s. dsubstable_dx (lhap s).
 /2 width=1/
 qed.
-(*
+
 theorem lhap_mono: ∀s. singlevalued … (lhap s).
 /3 width=7 by lstar_singlevalued, lhap1_mono/
 qed-.
-*)
-theorem lhap_trans: ∀s1,M1,M. M1 ⓗ⇀*[s1] M →
-                    ∀s2,M2. M ⓗ⇀*[s2] M2 → M1 ⓗ⇀*[s1@s2] M2.
-/2 width=3 by lstar_trans/
+
+theorem lhap_trans: ltransitive … lhap.
+/2 width=3 by lstar_ltransitive/
 qed-.
-(*
-lemma hap_appl: appl_compatible_dx hap.
-/3 width=1/
-qed.
-*)
-lemma lhap_spine_fwd: ∀s,M1,M2. M1 ⓗ⇀*[s] M2 → is_spine s.
-#s #M1 #M2 #H elim H -s -M1 -M2 //
-#p #M1 #M #HM1 #s #M2 #_ #IHM2
-lapply (lhap1_spine_fwd … HM1) -HM1 /2 width=1/ 
+
+lemma lhap_step_dx: ∀s,M1,M. M1 ⓗ⇀*[s] M →
+                    ∀p,M2. M ⓗ⇀[p] M2 → M1 ⓗ⇀*[s@p::◊] M2.
+#s #M1 #M #HM1 #p #M2 #HM2
+@(lhap_trans … HM1) /2 width=1/
 qed-.
 
-lemma lhap_lsreds_fwd: ∀s,M1,M2. M1 ⓗ⇀*[s] M2 → M1 ⇀*[s] M2.
-#s #M1 #M2 #H elim H -s -M1 -M2 //
-#p #M1 #M #HM1 #s #M2 #_ #IHM2
-lapply (lhap1_lsred_fwd … HM1) -HM1 /2 width=3/ 
+lemma head_lsreds_lhap: ∀s,M1,M2. M1 ⇀*[s] M2 → is_head s → M1 ⓗ⇀*[s] M2.
+#s #M1 #M2 #H @(lstar_ind_l ????????? H) -s -M1 //
+#a #s #M1 #M #HM1 #_ #IHM2 * /3 width=3/
+qed.
+
+lemma lhap_inv_head: ∀s,M1,M2. M1 ⓗ⇀*[s] M2 → is_head s.
+#s #M1 #M2 #H @(lstar_ind_l ????????? H) -s -M1 //
+#p #s #M1 #M #HM1 #_ #IHM2
+lapply (lhap1_inv_head … HM1) -HM1 /2 width=1/
 qed-.
 
-lemma lhap_le_fwd: ∀s,M1,M2. M1 ⓗ⇀*[s] M2 → is_le s.
-(*
-#M1 #M2 #H @(star_ind_l ??????? H) -M1 /3 width=3/
-#M1 #M #HM1 #H * #s * #H1s #H2s
-generalize in match HM1; -HM1 generalize in match M1; -M1
-@(star_ind_l ??????? H) -M
-[ #M1 #HM12 elim (hap1_lsred … HM12) -HM12 /4 width=3/
-| #M0 #M1 #HM01 #HM12 #_ #M #HM0 #HM02
-*)
+lemma lhap_inv_lsreds: ∀s,M1,M2. M1 ⓗ⇀*[s] M2 → M1 ⇀*[s] M2.
+#s #M1 #M2 #H @(lstar_ind_l ????????? H) -s -M1 //
+#p #s #M1 #M #HM1 #_ #IHM2
+lapply (lhap1_inv_lsred … HM1) -HM1 /2 width=3/
+qed-.