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

diff --git a/matita/matita/contribs/lambda/labelled_hap_computation.ma b/matita/matita/contribs/lambda/labelled_hap_computation.ma
index 5cd7678d1f78b64c4b1538a3951ce0729f217c8b..1fb6fcd180fec4084be345769ac517029f38c0bb 100644 (file)
--- a/matita/matita/contribs/lambda/labelled_hap_computation.ma
+++ b/matita/matita/contribs/lambda/labelled_hap_computation.ma
@@ -46,6 +46,10 @@ lemma lhap_inv_step_rc: ∀p,M1,M2. M1 ⓗ⇀*[p::◊] M2 → M1 ⓗ⇀[p] M2.
 /2 width=1 by lstar_inv_step/
 qed-.
 
+lemma lhap_compatible_dx: ho_compatible_dx lhap.
+/3 width=1/
+qed.
+
 lemma lhap_lift: ∀s. liftable (lhap s).
 /2 width=1/
 qed.
@@ -62,15 +66,10 @@ 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 lhap_appl: ∀s,B,A1,A2. A1 ⓗ⇀*[s] A2 → @B.A1 ⓗ⇀*[dx:::s] @B.A2.
-#s #B #A1 #A2 #H @(lstar_ind_l ????????? H) -s -A1 // /3 width=3/
-qed.
-
 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/

diff --git a/matita/matita/contribs/lambda/labelled_hap_reduction.ma b/matita/matita/contribs/lambda/labelled_hap_reduction.ma
index e1f279f67eaa65e285286429534bc2123a492fcb..324ffdad993f03a07132d1cfc95f5f5391ed7b39 100644 (file)
--- a/matita/matita/contribs/lambda/labelled_hap_reduction.ma
+++ b/matita/matita/contribs/lambda/labelled_hap_reduction.ma
@@ -12,7 +12,6 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "pointer_order.ma".
 include "labelled_sequential_reduction.ma".
 
 (* KASHIMA'S "HAP" COMPUTATION (LABELLED SINGLE STEP) ***********************)

diff --git a/matita/matita/contribs/lambda/labelled_sequential_computation.ma b/matita/matita/contribs/lambda/labelled_sequential_computation.ma
index 1f32ee8e00f182ca3c0b4fbc4cb1be13114f7838..4a7392a7646eaff25e913ebfc1e9919f28e5d69b 100644 (file)
--- a/matita/matita/contribs/lambda/labelled_sequential_computation.ma
+++ b/matita/matita/contribs/lambda/labelled_sequential_computation.ma
@@ -43,6 +43,18 @@ lemma lsreds_inv_step_rc: ∀p,M1,M2. M1 ⇀*[p::◊] M2 → M1 ⇀[p] M2.
 /2 width=1 by lstar_inv_step/
 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).
 /2 width=1/
 qed.
@@ -59,9 +71,8 @@ theorem lsreds_mono: ∀s. singlevalued … (lsreds s).
 /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.
-/2 width=3 by lstar_trans/
+theorem lsreds_trans: ltransitive … lsreds.
+/2 width=3 by lstar_ltransitive/
 qed-.
 
 (* Note: "|s|" should be unparetesized *)

diff --git a/matita/matita/contribs/lambda/pointer.ma b/matita/matita/contribs/lambda/pointer.ma
index 8d7afa1aa877867ccdc567cb2d72a6b75d5f0d2b..74977c3904f2dc7d59de1d5c175dc5855db44330 100644 (file)
--- a/matita/matita/contribs/lambda/pointer.ma
+++ b/matita/matita/contribs/lambda/pointer.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "preamble.ma".
+include "term.ma".
 
 (* POINTER ******************************************************************)
 
@@ -43,3 +43,12 @@ lemma in_head_ind: ∀R:predicate ptr. R (◊) →
 #R #H #IH #p elim p -p // -H *
 #p #IHp * #H1 #H2 destruct /3 width=1/
 qed-.
+
+definition compatible_rc: predicate (ptr→relation term) ≝ λR.
+                          ∀p,A1,A2. R p A1 A2 → R (rc::p) (𝛌.A1) (𝛌.A2).
+
+definition compatible_sn: predicate (ptr→relation term) ≝ λR.
+                          ∀p,B1,B2,A. R p B1 B2 → R (sn::p) (@B1.A) (@B2.A).
+
+definition compatible_dx: predicate (ptr→relation term) ≝ λR.
+                          ∀p,B,A1,A2. R p A1 A2 → R (dx::p) (@B.A1) (@B.A2).

diff --git a/matita/matita/contribs/lambda/pointer_order.ma b/matita/matita/contribs/lambda/pointer_order.ma
index ddcc3fd9ec2c2ee1d19370b5b7631222c620ccf8..ffd1e725d409351ec5908f4ee4e2280069a68515 100644 (file)
--- a/matita/matita/contribs/lambda/pointer_order.ma
+++ b/matita/matita/contribs/lambda/pointer_order.ma
@@ -20,7 +20,8 @@ include "pointer.ma".
          to serve as base for the order relations: p < q and p ≤ q *)
 inductive pprec: relation ptr ≝
 | pprec_nil : ∀c,q.   pprec (◊) (c::q)
-| ppprc_cons: ∀p,q.   pprec (dx::p) (sn::q)
+| ppprc_rc  : ∀p,q.   pprec (dx::p) (rc::q)
+| ppprc_sn  : ∀p,q.   pprec (dx::p) (sn::q)
 | pprec_comp: ∀c,p,q. pprec p q → pprec (c::p) (c::q)
 | pprec_skip:         pprec (dx::◊) ◊
 .
@@ -36,6 +37,7 @@ notation "hvbox(a break ≺ b)"
 lemma pprec_fwd_in_head: ∀p,q. p ≺ q → in_head q → in_head p.
 #p #q #H elim H -p -q // /2 width=1/
 [ #p #q * #H destruct
+| #p #q * #H destruct
 | #c #p #q #_ #IHpq * #H destruct /3 width=1/
 ]
 qed-.
@@ -60,6 +62,10 @@ lemma ple_step_sn: ∀p1,p,p2. p1 ≺ p → p ≤ p2 → p1 ≤ p2.
 /2 width=3/
 qed-.
 
+lemma ple_cons: ∀p,q. dx::p ≤ sn::q.
+/2 width=1/
+qed.
+
 lemma ple_skip: dx::◊ ≤ ◊.
 /2 width=1/
 qed.
@@ -81,11 +87,15 @@ lemma in_head_ple_nil: ∀p. in_head p → p ≤ ◊.
 #p #H @(in_head_ind … H) -p // /2 width=1/
 qed.
 
-theorem in_head_ple: ∀p. in_head p → ∀q. in_head q → p ≤ q.
+theorem in_head_ple: ∀p. in_head p → ∀q. p ≤ q.
 #p #H @(in_head_ind … H) -p //
-#p #Hp #IHp #q #H @(in_head_ind … H) -q /3 width=1/
+#p #_ #IHp * /3 width=1/ * #q /2 width=1/
 qed.
 
 lemma ple_nil_inv_in_head: ∀p. p ≤ ◊ → in_head p.
 #p #H @(star_ind_l ??????? H) -p // /2 width=3 by pprec_fwd_in_head/
 qed-.
+
+lemma ple_inv_in_head: ∀p. (∀q. p ≤ q) → in_head p.
+/2 width=1 by ple_nil_inv_in_head/
+qed-.

diff --git a/matita/matita/contribs/lambda/pointer_sequence.ma b/matita/matita/contribs/lambda/pointer_sequence.ma
index 9a93f27ff207781d11fcd320ff48695ece820143..9f4e63cd6e4f9dd0b6048c2ede1947447c5fcdcf 100644 (file)
--- a/matita/matita/contribs/lambda/pointer_sequence.ma
+++ b/matita/matita/contribs/lambda/pointer_sequence.ma
@@ -25,8 +25,54 @@ definition is_head: predicate pseq ≝ All … in_head.
 (* Note: to us, a "normal" computation contracts redexes in non-decreasing positions *)
 definition is_le: predicate pseq ≝ Allr … ple.
 
+lemma is_le_compatible: ∀c,s. is_le s → is_le (c:::s).
+#c #s elim s -s // #p * //
+#q #s #IHs * /3 width=1/
+qed.
+
+lemma is_le_cons: ∀p,s. is_le s → is_le ((dx::p)::sn:::s).
+#p #s elim s -s // #q1 * /2 width=1/
+#q2 #s #IHs * /4 width=1/
+qed.
+
+lemma is_le_append: ∀r. is_le r → ∀s. is_le s → is_le ((dx:::r)@sn:::s).
+#r elim r -r /3 width=1/ #p * /2 width=1/
+#q #r #IHr * /3 width=1/
+qed.
+
 theorem is_head_is_le: ∀s. is_head s → is_le s.
-#s elim s -s //
-#p #s elim s -s //
-#q #s #_ #IHs * #Hp * /4 width=1/
+#s elim s -s // #p * //
+#q #s #IHs * /3 width=1/
+qed.
+
+lemma is_le_in_head: ∀p. in_head p → ∀s. is_le s → is_le (p::s).
+#p #Hp * // /3 width=1/
+qed.
+
+theorem is_head_is_le_trans: ∀r. is_head r → ∀s. is_le s → is_le (r@s).
+#r elim r -r // #p *
+[ #_ * /2 width=1/
+| #q #r #IHr * /3 width=1/
+]
+qed.
+
+definition ho_compatible_rc: predicate (pseq→relation term) ≝ λR.
+                             ∀s,A1,A2. R s A1 A2 → R (rc:::s) (𝛌.A1) (𝛌.A2).
+
+definition ho_compatible_sn: predicate (pseq→relation term) ≝ λR.
+                             ∀s,B1,B2,A. R s B1 B2 → R (sn:::s) (@B1.A) (@B2.A).
+
+definition ho_compatible_dx: predicate (pseq→relation term) ≝ λR.
+                             ∀s,B,A1,A2. R s A1 A2 → R (dx:::s) (@B.A1) (@B.A2).
+
+lemma lstar_compatible_rc: ∀R. compatible_rc R → ho_compatible_rc (lstar … R).
+#R #HR #s #A1 #A2 #H @(lstar_ind_l ????????? H) -s -A1 // /3 width=3/
+qed.
+
+lemma lstar_compatible_sn: ∀R. compatible_sn R → ho_compatible_sn (lstar … R).
+#R #HR #s #B1 #B2 #A #H @(lstar_ind_l ????????? H) -s -B1 // /3 width=3/
+qed.
+
+lemma lstar_compatible_dx: ∀R. compatible_dx R → ho_compatible_dx (lstar … R).
+#R #HR #s #B #A1 #A2 #H @(lstar_ind_l ????????? H) -s -A1 // /3 width=3/
 qed.

diff --git a/matita/matita/contribs/lambda/st_computation.ma b/matita/matita/contribs/lambda/st_computation.ma
index 028cd8a41bfc3ae80657c7c21e7dfc4542fadd56..97b5a7211658473f115e6dbd63487fc160335fb0 100644 (file)
--- a/matita/matita/contribs/lambda/st_computation.ma
+++ b/matita/matita/contribs/lambda/st_computation.ma
@@ -41,3 +41,24 @@ axiom st_lift: liftable st.
 axiom st_inv_lift: deliftable_sn st.
 
 axiom st_dsubst: dsubstable st.
+
+lemma st_inv_lsreds_is_le: ∀M,N. M ⓢ⥤* N →
+                           ∃∃r. M ⇀*[r] N & is_le r.
+#M #N #H elim H -M -N
+[ #s #M #i #H
+  lapply (lhap_inv_lsreds … H)
+  lapply (lhap_inv_head … H) -H #H
+  lapply (is_head_is_le … H) -H /2 width=3/
+| #s #M #A1 #A2 #H #_ * #r #HA12 #Hr
+  lapply (lhap_inv_lsreds … H) #HM
+  lapply (lhap_inv_head … H) -H #Hs
+  lapply (lsreds_trans … HM (rc:::r) (𝛌.A2) ?) /2 width=1/ -A1 #HM
+  @(ex2_intro … HM) -M -A2 /3 width=1/
+| #s #M #B1 #B2 #A1 #A2 #H #_ #_ * #rb #HB12 #Hrb * #ra #HA12 #Hra
+  lapply (lhap_inv_lsreds … H) #HM
+  lapply (lhap_inv_head … H) -H #Hs
+  lapply (lsreds_trans … HM (dx:::ra) (@B1.A2) ?) /2 width=1/ -A1 #HM
+  lapply (lsreds_trans … HM (sn:::rb) (@B2.A2) ?) /2 width=1/ -B1 #HM
+  @(ex2_intro … HM) -M -B2 -A2 >associative_append /3 width=1/
+]
+qed-.

diff --git a/matita/matita/lib/basics/lists/lstar.ma b/matita/matita/lib/basics/lists/lstar.ma
index aafe8f5b7055da6393c2f463500c54395059f46c..fa0cdb5aaf4f570b8b4fc02d3f76038dab7300ba 100644 (file)
--- a/matita/matita/lib/basics/lists/lstar.ma
+++ b/matita/matita/lib/basics/lists/lstar.ma
@@ -13,6 +13,9 @@ include "basics/lists/list.ma".
 
 (* labelled reflexive and transitive closure ********************************)
 
+definition ltransitive: ∀A,B:Type[0]. predicate (list A → relation B) ≝ λA,B,R.
+                        ∀l1,b1,b. R l1 b1 b → ∀l2,b2. R l2 b b2 → R (l1@l2) b1 b2. 
+
 inductive lstar (A:Type[0]) (B:Type[0]) (R: A→relation B): list A → relation B ≝
 | lstar_nil : ∀b. lstar A B R ([]) b b
 | lstar_cons: ∀a,b1,b. R a b1 b →
@@ -72,7 +75,6 @@ theorem lstar_singlevalued: ∀A,B,R. (∀a. singlevalued ?? (R a)) →
 ]
 qed-.
 
-theorem lstar_trans: ∀A,B,R,l1,b1,b. lstar A B R l1 b1 b →
-                     ∀l2,b2. lstar A B R l2 b b2 → lstar A B R (l1@l2) b1 b2.
+theorem lstar_ltransitive: ∀A,B,R. ltransitive … (lstar A B R).
 #A #B #R #l1 #b1 #b #H @(lstar_ind_l ????????? H) -l1 -b1 normalize // /3 width=3/
 qed-.