From 2d35cd1602d585ecb2c6623a1b2bd1e0c81aa93b Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Tue, 18 Dec 2012 16:50:35 +0000 Subject: [PATCH] - star.ma: strip lemma and confluence of star - lambda: confluence of labelled sequential reduction completed! --- .../contribs/lambda/delifting_substitution.ma | 16 ++-- .../lambda/labelled_sequential_computation.ma | 61 ++++++++++++- .../contribs/lambda/parallel_computation.ma | 87 +++++++++++++++++++ matita/matita/contribs/lambda/term.ma | 33 +++++-- matita/matita/contribs/lambda/xoa.conf.xml | 1 + matita/matita/contribs/lambda/xoa.ma | 8 ++ matita/matita/contribs/lambda/xoa_notation.ma | 10 +++ matita/matita/lib/basics/star.ma | 18 ++++ 8 files changed, 216 insertions(+), 18 deletions(-) create mode 100644 matita/matita/contribs/lambda/parallel_computation.ma diff --git a/matita/matita/contribs/lambda/delifting_substitution.ma b/matita/matita/contribs/lambda/delifting_substitution.ma index aa9d9586c..fe45c35a2 100644 --- a/matita/matita/contribs/lambda/delifting_substitution.ma +++ b/matita/matita/contribs/lambda/delifting_substitution.ma @@ -143,23 +143,21 @@ qed. definition dsubstable_dx: predicate (relation term) ≝ λR. ∀D,M1,M2. R M1 M2 → ∀d. R ([d ↙ D] M1) ([d ↙ D] M2). -(* -definition dsubstable_sn: predicate (relation term) ≝ λR. - ∀D1,D2. R D1 D2 → ∀M,d. R ([d ↙ D1] M) ([d ↙ D2] M). -*) + definition dsubstable: predicate (relation term) ≝ λR. ∀D1,D2. R D1 D2 → ∀M1,M2. R M1 M2 → ∀d. R ([d ↙ D1] M1) ([d ↙ D2] M2). lemma star_dsubstable_dx: ∀R. dsubstable_dx R → dsubstable_dx (star … R). #R #HR #D #M1 #M2 #H elim H -M2 // /3 width=3/ qed. -(* -lemma star_dsubstable_sn: ∀R. dsubstable_sn R → dsubstable_sn (star … R). -#R #HR #D1 #D2 #H elim H -D2 // /3 width=3/ -qed. -*) + lemma lstar_dsubstable_dx: ∀T,R. (∀t. dsubstable_dx (R t)) → ∀l. dsubstable_dx (lstar T … R l). #T #R #HR #l #D #M1 #M2 #H @(lstar_ind_l ????????? H) -l -M1 // /3 width=3/ qed. + +lemma star_dsubstable: ∀R. reflexive ? R → + dsubstable R → dsubstable (star … R). +#R #H1R #H2 #D1 #D2 #H elim H -D2 /3 width=1/ /3 width=5/ +qed. diff --git a/matita/matita/contribs/lambda/labelled_sequential_computation.ma b/matita/matita/contribs/lambda/labelled_sequential_computation.ma index f305f90cb..837c9668d 100644 --- a/matita/matita/contribs/lambda/labelled_sequential_computation.ma +++ b/matita/matita/contribs/lambda/labelled_sequential_computation.ma @@ -13,7 +13,7 @@ (**************************************************************************) include "pointer_sequence.ma". -include "labelled_sequential_reduction.ma". +include "parallel_computation.ma". (* LABELLED SEQUENTIAL COMPUTATION (MULTISTEP) ******************************) @@ -26,6 +26,18 @@ notation "hvbox( M break ↦* [ term 46 s ] break term 46 N )" non associative with precedence 45 for @{ 'SeqRedStar $M $s $N }. +lemma lsreds_refl: reflexive … (lsreds (◊)). +// +qed. + +lemma lsreds_step_sn: ∀p,M1,M. M1 ↦[p] M → ∀s,M2. M ↦*[s] M2 → M1 ↦*[p::s] M2. +/2 width=3/ +qed-. + +lemma lsreds_step_dx: ∀s,M1,M. M1 ↦*[s] M → ∀p,M2. M ↦[p] M2 → M1 ↦*[s@p::◊] M2. +/2 width=3/ +qed-. + lemma lsreds_step_rc: ∀p,M1,M2. M1 ↦[p] M2 → M1 ↦*[p::◊] M2. /2 width=1/ qed. @@ -52,11 +64,11 @@ lemma lsred_compatible_rc: ho_compatible_rc lsreds. /3 width=1/ qed. -lemma lsred_compatible_sn: ho_compatible_sn lsreds. +lemma lsreds_compatible_sn: ho_compatible_sn lsreds. /3 width=1/ qed. -lemma lsred_compatible_dx: ho_compatible_dx lsreds. +lemma lsreds_compatible_dx: ho_compatible_dx lsreds. /3 width=1/ qed. @@ -80,6 +92,19 @@ theorem lsreds_trans: ltransitive … lsreds. /2 width=3 by lstar_ltransitive/ qed-. +lemma lsreds_compatible_appl: ∀r,B1,B2. B1 ↦*[r] B2 → ∀s,A1,A2. A1 ↦*[s] A2 → + @B1.A1 ↦*[(sn:::r)@dx:::s] @B2.A2. +#r #B1 #B2 #HB12 #s #A1 #A2 #HA12 +@(lsreds_trans … (@B2.A1)) /2 width=1/ +qed. + +lemma lsreds_compatible_beta: ∀r,B1,B2. B1 ↦*[r] B2 → ∀s,A1,A2. A1 ↦*[s] A2 → + @B1.𝛌.A1 ↦*[(sn:::r)@(dx:::sn:::s)@◊::◊] [↙B2] A2. +#r #B1 #B2 #HB12 #s #A1 #A2 #HA12 +@(lsreds_trans … (@B2.𝛌.A1)) /2 width=1/ -r -B1 +@(lsreds_step_dx … (@B2.𝛌.A2)) // /3 width=1/ +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 // @@ -88,3 +113,33 @@ 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-. + +theorem lsreds_preds: ∀s,M1,M2. M1 ↦*[s] M2 → M1 ⤇* M2. +#s #M1 #M2 #H @(lstar_ind_l ????????? H) -s -M1 // +#a #s #M1 #M #HM1 #_ #IHM2 +@(preds_step_sn … IHM2) -M2 /2 width=2/ +qed. + +lemma pred_lsreds: ∀M1,M2. M1 ⤇ M2 → ∃r. M1 ↦*[r] M2. +#M1 #M2 #H elim H -M1 -M2 /2 width=2/ +[ #A1 #A2 #_ * /3 width=2/ +| #B1 #B2 #A1 #A2 #_ #_ * #r #HB12 * /3 width=2/ +| #B1 #B2 #A1 #A2 #_ #_ * #r #HB12 * /3 width=2/ +qed-. + +theorem preds_lsreds: ∀M1,M2. M1 ⤇* M2 → ∃r. M1 ↦*[r] M2. +#M1 #M2 #H elim H -M2 /2 width=2/ +#M #M2 #_ #HM2 * #r #HM1 +elim (pred_lsreds … HM2) -HM2 #s #HM2 +lapply (lsreds_trans … HM1 … HM2) -M /2 width=2/ +qed-. + +theorem lsreds_conf: ∀s1,M0,M1. M0 ↦*[s1] M1 → ∀s2,M2. M0 ↦*[s2] M2 → + ∃∃r1,r2,M. M1 ↦*[r1] M & M2 ↦*[r2] M. +#s1 #M0 #M1 #HM01 #s2 #M2 #HM02 +lapply (lsreds_preds … HM01) -s1 #HM01 +lapply (lsreds_preds … HM02) -s2 #HM02 +elim (preds_conf … HM01 … HM02) -M0 #M #HM1 #HM2 +elim (preds_lsreds … HM1) -HM1 +elim (preds_lsreds … HM2) -HM2 /2 width=5/ +qed-. diff --git a/matita/matita/contribs/lambda/parallel_computation.ma b/matita/matita/contribs/lambda/parallel_computation.ma new file mode 100644 index 000000000..af64cc09c --- /dev/null +++ b/matita/matita/contribs/lambda/parallel_computation.ma @@ -0,0 +1,87 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "parallel_reduction.ma". + +(* PARALLEL COMPUTATION (MULTISTEP) *****************************************) + +definition preds: relation term ≝ star … pred. + +interpretation "parallel computation" + 'ParRedStar M N = (preds M N). + +notation "hvbox( M ⤇* break term 46 N )" + non associative with precedence 45 + for @{ 'ParRedStar $M $N }. + +lemma preds_refl: reflexive … preds. +// +qed. + +lemma preds_step_sn: ∀M1,M. M1 ⤇ M → ∀M2. M ⤇* M2 → M1 ⤇* M2. +/2 width=3/ +qed-. + +lemma preds_step_dx: ∀M1,M. M1 ⤇* M → ∀M2. M ⤇ M2 → M1 ⤇* M2. +/2 width=3/ +qed-. + +lemma preds_step_rc: ∀M1,M2. M1 ⤇ M2 → M1 ⤇* M2. +/2 width=1/ +qed. + +lemma preds_compatible_abst: compatible_abst preds. +/3 width=1/ +qed. + +lemma preds_compatible_sn: compatible_sn preds. +/3 width=1/ +qed. + +lemma preds_compatible_dx: compatible_dx preds. +/3 width=1/ +qed. + +lemma preds_compatible_appl: compatible_appl preds. +/3 width=1/ +qed. + +lemma preds_lift: liftable preds. +/2 width=1/ +qed. + +lemma preds_inv_lift: deliftable_sn preds. +/3 width=3 by star_deliftable_sn, pred_inv_lift/ +qed-. + +lemma preds_dsubst_dx: dsubstable_dx preds. +/2 width=1/ +qed. + +lemma preds_dsubst: dsubstable preds. +/2 width=1/ +qed. + +theorem preds_trans: transitive … preds. +/2 width=3 by trans_star/ +qed-. + +lemma preds_strip: ∀M0,M1. M0 ⤇* M1 → ∀M2. M0 ⤇ M2 → + ∃∃M. M1 ⤇ M & M2 ⤇* M. +/3 width=3 by star_strip, pred_conf/ +qed-. + +theorem preds_conf: confluent … preds. +/3 width=3 by star_confluent, pred_conf/ +qed-. diff --git a/matita/matita/contribs/lambda/term.ma b/matita/matita/contribs/lambda/term.ma index 92a838fb4..2e08b861e 100644 --- a/matita/matita/contribs/lambda/term.ma +++ b/matita/matita/contribs/lambda/term.ma @@ -47,12 +47,33 @@ notation "hvbox( 𝛌 . term 46 A )" notation "hvbox( @ term 46 C . break term 46 A )" non associative with precedence 46 for @{ 'Application $C $A }. -(* -definition appl_compatible_dx: predicate (relation term) ≝ λR. - ∀B,A1,A2. R A1 A2 → R (@B.A1) (@B.A2). -lemma star_appl_compatible_dx: ∀R. appl_compatible_dx R → - appl_compatible_dx (star … R). +definition compatible_abst: predicate (relation term) ≝ λR. + ∀A1,A2. R A1 A2 → R (𝛌.A1) (𝛌.A2). + +definition compatible_sn: predicate (relation term) ≝ λR. + ∀A,B1,B2. R B1 B2 → R (@B1.A) (@B2.A). + +definition compatible_dx: predicate (relation term) ≝ λR. + ∀B,A1,A2. R A1 A2 → R (@B.A1) (@B.A2). + +definition compatible_appl: predicate (relation term) ≝ λR. + ∀B1,B2. R B1 B2 → ∀A1,A2. R A1 A2 → + R (@B1.A1) (@B2.A2). + +lemma star_compatible_abst: ∀R. compatible_abst R → compatible_abst (star … R). +#R #HR #A1 #A2 #H elim H -A2 // /3 width=3/ +qed. + +lemma star_compatible_sn: ∀R. compatible_sn R → compatible_sn (star … R). +#R #HR #A #B1 #B2 #H elim H -B2 // /3 width=3/ +qed. + +lemma star_compatible_dx: ∀R. compatible_dx R → compatible_dx (star … R). #R #HR #B #A1 #A2 #H elim H -A2 // /3 width=3/ qed. -*) + +lemma star_compatible_appl: ∀R. reflexive ? R → + compatible_appl R → compatible_appl (star … R). +#R #H1R #H2R #B1 #B2 #H elim H -B2 /3 width=1/ /3 width=5/ +qed. diff --git a/matita/matita/contribs/lambda/xoa.conf.xml b/matita/matita/contribs/lambda/xoa.conf.xml index 223be4324..9f923b7ae 100644 --- a/matita/matita/contribs/lambda/xoa.conf.xml +++ b/matita/matita/contribs/lambda/xoa.conf.xml @@ -9,6 +9,7 @@ xoa_notation basics/pts.ma 2 2 + 2 3 3 2 3 3 4 3 diff --git a/matita/matita/contribs/lambda/xoa.ma b/matita/matita/contribs/lambda/xoa.ma index 1e82edec7..5f029c5fc 100644 --- a/matita/matita/contribs/lambda/xoa.ma +++ b/matita/matita/contribs/lambda/xoa.ma @@ -24,6 +24,14 @@ inductive ex2_2 (A0,A1:Type[0]) (P0,P1:A0→A1→Prop) : Prop ≝ interpretation "multiple existental quantifier (2, 2)" 'Ex P0 P1 = (ex2_2 ? ? P0 P1). +(* multiple existental quantifier (2, 3) *) + +inductive ex2_3 (A0,A1,A2:Type[0]) (P0,P1:A0→A1→A2→Prop) : Prop ≝ + | ex2_3_intro: ∀x0,x1,x2. P0 x0 x1 x2 → P1 x0 x1 x2 → ex2_3 ? ? ? ? ? +. + +interpretation "multiple existental quantifier (2, 3)" 'Ex P0 P1 = (ex2_3 ? ? ? P0 P1). + (* multiple existental quantifier (3, 2) *) inductive ex3_2 (A0,A1:Type[0]) (P0,P1,P2:A0→A1→Prop) : Prop ≝ diff --git a/matita/matita/contribs/lambda/xoa_notation.ma b/matita/matita/contribs/lambda/xoa_notation.ma index b14f46cec..a978cb1b7 100644 --- a/matita/matita/contribs/lambda/xoa_notation.ma +++ b/matita/matita/contribs/lambda/xoa_notation.ma @@ -24,6 +24,16 @@ notation < "hvbox(∃∃ ident x0 , ident x1 break . term 19 P0 break & term 19 non associative with precedence 20 for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.$P1) }. +(* multiple existental quantifier (2, 3) *) + +notation > "hvbox(∃∃ ident x0 , ident x1 , ident x2 break . term 19 P0 break & term 19 P1)" + non associative with precedence 20 + for @{ 'Ex (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P0) (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P1) }. + +notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 break . term 19 P0 break & term 19 P1)" + non associative with precedence 20 + for @{ 'Ex (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P1) }. + (* multiple existental quantifier (3, 2) *) notation > "hvbox(∃∃ ident x0 , ident x1 break . term 19 P0 break & term 19 P1 break & term 19 P2)" diff --git a/matita/matita/lib/basics/star.ma b/matita/matita/lib/basics/star.ma index 892cff583..5ac7d91fb 100644 --- a/matita/matita/lib/basics/star.ma +++ b/matita/matita/lib/basics/star.ma @@ -421,3 +421,21 @@ lemma bi_star_ind_dx: ∀A,B,R,a2,b2. ∀P:relation2 A B. P a2 b2 → | #H12 @(bi_TC_ind_dx ?????????? H12) -a1 -b1 /2 width=5/ -H /3 width=5/ ] qed-. + +(* ************ confluence of star *****************) + +lemma star_strip: ∀A,R. confluent A R → + ∀a0,a1. star … R a0 a1 → ∀a2. R a0 a2 → + ∃∃a. R a1 a & star … R a2 a. +#A #R #HR #a0 #a1 #H elim H -a1 /2 width=3/ +#a #a1 #_ #Ha1 #IHa0 #a2 #Ha02 +elim (IHa0 … Ha02) -a0 #a0 #Ha0 #Ha20 +elim (HR … Ha1 … Ha0) -a /3 width=5/ +qed-. + +lemma star_confluent: ∀A,R. confluent A R → confluent A (star … R). +#A #R #HR #a0 #a1 #H elim H -a1 /2 width=3/ +#a #a1 #_ #Ha1 #IHa0 #a2 #Ha02 +elim (IHa0 … Ha02) -a0 #a0 #Ha0 #Ha20 +elim (star_strip … HR … Ha0 … Ha1) -a /3 width=5/ +qed-. -- 2.39.2