From 5613a25cee29ef32a597cb4b44e8f2f4d71c4df0 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Sun, 9 Dec 2012 17:59:03 +0000 Subject: [PATCH] - lambda: first half of the standardization theorem is proved! --- .../lambda/labelled_hap_computation.ma | 13 +++-- .../contribs/lambda/labelled_hap_reduction.ma | 1 - .../lambda/labelled_sequential_computation.ma | 17 ++++-- matita/matita/contribs/lambda/pointer.ma | 11 +++- .../matita/contribs/lambda/pointer_order.ma | 16 ++++-- .../contribs/lambda/pointer_sequence.ma | 52 +++++++++++++++++-- .../matita/contribs/lambda/st_computation.ma | 21 ++++++++ matita/matita/lib/basics/lists/lstar.ma | 6 ++- 8 files changed, 117 insertions(+), 20 deletions(-) diff --git a/matita/matita/contribs/lambda/labelled_hap_computation.ma b/matita/matita/contribs/lambda/labelled_hap_computation.ma index 5cd7678d1..1fb6fcd18 100644 --- 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 e1f279f67..324ffdad9 100644 --- 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 1f32ee8e0..4a7392a76 100644 --- 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 8d7afa1aa..74977c390 100644 --- 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 ddcc3fd9e..ffd1e725d 100644 --- 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 9a93f27ff..9f4e63cd6 100644 --- 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 028cd8a41..97b5a7211 100644 --- 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 aafe8f5b7..fa0cdb5aa 100644 --- 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-. -- 2.39.2