From bde429ac54e48de74b3d8b1df72dfcb86aa9bae5 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Sun, 23 Dec 2012 15:02:32 +0000 Subject: [PATCH] - we introduced the pointer_step rc in the perspective of proving results on head normal forms - some renaming --- ...n.ma => labeled_sequential_computation.ma} | 4 +- ...ion.ma => labeled_sequential_reduction.ma} | 37 +++++++++++-------- .../contribs/lambda/parallel_reduction.ma | 2 +- matita/matita/contribs/lambda/pointer.ma | 11 ++---- matita/matita/contribs/lambda/pointer_list.ma | 2 +- .../matita/contribs/lambda/pointer_order.ma | 19 +++++++++- .../matita/contribs/lambda/st_computation.ma | 4 +- 7 files changed, 48 insertions(+), 31 deletions(-) rename matita/matita/contribs/lambda/{labelled_sequential_computation.ma => labeled_sequential_computation.ma} (97%) rename matita/matita/contribs/lambda/{labelled_sequential_reduction.ma => labeled_sequential_reduction.ma} (83%) diff --git a/matita/matita/contribs/lambda/labelled_sequential_computation.ma b/matita/matita/contribs/lambda/labeled_sequential_computation.ma similarity index 97% rename from matita/matita/contribs/lambda/labelled_sequential_computation.ma rename to matita/matita/contribs/lambda/labeled_sequential_computation.ma index f62864831..4c2a6fc9e 100644 --- a/matita/matita/contribs/lambda/labelled_sequential_computation.ma +++ b/matita/matita/contribs/lambda/labeled_sequential_computation.ma @@ -15,7 +15,7 @@ include "pointer_list.ma". include "parallel_computation.ma". -(* LABELLED SEQUENTIAL COMPUTATION (MULTISTEP) ******************************) +(* LABELED SEQUENTIAL COMPUTATION (MULTISTEP) *******************************) definition lsreds: ptrl → relation term ≝ lstar … lsred. @@ -99,7 +99,7 @@ lemma lsreds_compatible_appl: ∀r,B1,B2. B1 ↦*[r] B2 → ∀s,A1,A2. A1 ↦*[ 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. + @B1.𝛌.A1 ↦*[(sn:::r)@(dx:::rc:::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/ diff --git a/matita/matita/contribs/lambda/labelled_sequential_reduction.ma b/matita/matita/contribs/lambda/labeled_sequential_reduction.ma similarity index 83% rename from matita/matita/contribs/lambda/labelled_sequential_reduction.ma rename to matita/matita/contribs/lambda/labeled_sequential_reduction.ma index 40d518846..7dd2bccb3 100644 --- a/matita/matita/contribs/lambda/labelled_sequential_reduction.ma +++ b/matita/matita/contribs/lambda/labeled_sequential_reduction.ma @@ -15,7 +15,7 @@ include "pointer.ma". include "multiplicity.ma". -(* LABELLED SEQUENTIAL REDUCTION (SINGLE STEP) ******************************) +(* LABELED SEQUENTIAL REDUCTION (SINGLE STEP) *******************************) (* Note: the application "(A B)" is represented by "@B.A" following: F. Kamareddine and R.P. Nederpelt: "A useful λ-notation". @@ -23,7 +23,7 @@ include "multiplicity.ma". *) inductive lsred: ptr → relation term ≝ | lsred_beta : ∀B,A. lsred (◊) (@B.𝛌.A) ([↙B]A) -| lsred_abst : ∀p,A1,A2. lsred p A1 A2 → lsred (sn::p) (𝛌.A1) (𝛌.A2) +| lsred_abst : ∀p,A1,A2. lsred p A1 A2 → lsred (rc::p) (𝛌.A1) (𝛌.A2) | lsred_appl_sn: ∀p,B1,B2,A. lsred p B1 B2 → lsred (sn::p) (@B1.A) (@B2.A) | lsred_appl_dx: ∀p,B,A1,A2. lsred p A1 A2 → lsred (dx::p) (@B.A1) (@B.A2) . @@ -55,13 +55,22 @@ lemma lsred_inv_nil: ∀p,M,N. M ↦[p] N → ◊ = p → ] qed-. +lemma lsred_inv_rc: ∀p,M,N. M ↦[p] N → ∀q. rc::q = p → + ∃∃A1,A2. A1 ↦[q] A2 & 𝛌.A1 = M & 𝛌.A2 = N. +#p #M #N * -p -M -N +[ #B #A #q #H destruct +| #p #A1 #A2 #HA12 #q #H destruct /2 width=5/ +| #p #B1 #B2 #A #_ #q #H destruct +| #p #B #A1 #A2 #_ #q #H destruct +] +qed-. + lemma lsred_inv_sn: ∀p,M,N. M ↦[p] N → ∀q. sn::q = p → - (∃∃A1,A2. A1 ↦[q] A2 & 𝛌.A1 = M & 𝛌.A2 = N) ∨ ∃∃B1,B2,A. B1 ↦[q] B2 & @B1.A = M & @B2.A = N. #p #M #N * -p -M -N [ #B #A #q #H destruct -| #p #A1 #A2 #HA12 #q #H destruct /3 width=5/ -| #p #B1 #B2 #A #HB12 #q #H destruct /3 width=6/ +| #p #A1 #A2 #_ #q #H destruct +| #p #B1 #B2 #A #HB12 #q #H destruct /2 width=6/ | #p #B #A1 #A2 #_ #q #H destruct ] qed-. @@ -122,15 +131,13 @@ qed. theorem lsred_mono: ∀p. singlevalued … (lsred p). #p #M #N1 #H elim H -p -M -N1 -[ #B #A #N2 #H elim (lsred_inv_nil … H ?) -H // #D #C #H #HN2 destruct // -| #p #A1 #A2 #_ #IHA12 #N2 #H elim (lsred_inv_sn … H ??) -H [4: // |2: skip ] * (**) (* simplify line *) - [ #C1 #C2 #HC12 #H #HN2 destruct /3 width=1/ - | #D1 #D2 #C #_ #H destruct - ] -| #p #B1 #B2 #A #_ #IHB12 #N2 #H elim (lsred_inv_sn … H ??) -H [4: // |2: skip ] * (**) (* simplify line *) - [ #C1 #C2 #_ #H destruct - | #D1 #D2 #C #HD12 #H #HN2 destruct /3 width=1/ - ] -| #p #B #A1 #A2 #_ #IHA12 #N2 #H elim (lsred_inv_dx … H ??) -H [3: // |2: skip ] #D #C1 #C2 #HC12 #H #HN2 destruct /3 width=1/ (**) (* simplify line *) +[ #B #A #N2 #H elim (lsred_inv_nil … H ?) -H // + #D #C #H #HN2 destruct // +| #p #A1 #A2 #_ #IHA12 #N2 #H elim (lsred_inv_rc … H ??) -H [3: // |2: skip ] (**) (* simplify line *) + #C1 #C2 #HC12 #H #HN2 destruct /3 width=1/ +| #p #B1 #B2 #A #_ #IHB12 #N2 #H elim (lsred_inv_sn … H ??) -H [3: // |2: skip ] (**) (* simplify line *) + #D1 #D2 #C #HD12 #H #HN2 destruct /3 width=1/ +| #p #B #A1 #A2 #_ #IHA12 #N2 #H elim (lsred_inv_dx … H ??) -H [3: // |2: skip ] (**) (* simplify line *) + #D #C1 #C2 #HC12 #H #HN2 destruct /3 width=1/ ] qed-. diff --git a/matita/matita/contribs/lambda/parallel_reduction.ma b/matita/matita/contribs/lambda/parallel_reduction.ma index eaa8b7ce1..1d97b3b87 100644 --- a/matita/matita/contribs/lambda/parallel_reduction.ma +++ b/matita/matita/contribs/lambda/parallel_reduction.ma @@ -13,7 +13,7 @@ (**************************************************************************) include "length.ma". -include "labelled_sequential_reduction.ma". +include "labeled_sequential_reduction.ma". (* PARALLEL REDUCTION (SINGLE STEP) *****************************************) diff --git a/matita/matita/contribs/lambda/pointer.ma b/matita/matita/contribs/lambda/pointer.ma index 27f30b22c..d71574e74 100644 --- a/matita/matita/contribs/lambda/pointer.ma +++ b/matita/matita/contribs/lambda/pointer.ma @@ -18,17 +18,12 @@ include "term.ma". (* Policy: pointer step metavariables: c *) (* Note: this is a step of a path in the tree representation of a term: - rc (rectus) : not needed (we use sn instead) + rc (rectus) : proceed on the argument of an abstraction sn (sinister): proceed on the left argument of an application - or on the argument of an abstraction (this would be rc) dx (dexter) : proceed on the right argument of an application *) -(* Remark: the following breaks destruct because of δ-expansions - definition ptr_step: Type[0] ≝ bool. - definition sn: bool ≝ true. - definition dx: bool ≝ false. -*) inductive ptr_step: Type[0] ≝ +| rc: ptr_step | sn: ptr_step | dx: ptr_step . @@ -50,7 +45,7 @@ lemma in_whd_ind: ∀R:predicate ptr. R (◊) → qed-. definition compatible_rc: predicate (ptr→relation term) ≝ λR. - ∀p,A1,A2. R p A1 A2 → R (sn::p) (𝛌.A1) (𝛌.A2). + ∀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). diff --git a/matita/matita/contribs/lambda/pointer_list.ma b/matita/matita/contribs/lambda/pointer_list.ma index 82f704a78..becfc0a5e 100644 --- a/matita/matita/contribs/lambda/pointer_list.ma +++ b/matita/matita/contribs/lambda/pointer_list.ma @@ -33,7 +33,7 @@ lemma is_whd_append: ∀r. is_whd r → ∀s. is_whd s → is_whd (r@s). qed. definition ho_compatible_rc: predicate (ptrl→relation term) ≝ λR. - ∀s,A1,A2. R s A1 A2 → R (sn:::s) (𝛌.A1) (𝛌.A2). + ∀s,A1,A2. R s A1 A2 → R (rc:::s) (𝛌.A1) (𝛌.A2). definition ho_compatible_sn: predicate (ptrl→relation term) ≝ λR. ∀s,B1,B2,A. R s B1 B2 → R (sn:::s) (@B1.A) (@B2.A). diff --git a/matita/matita/contribs/lambda/pointer_order.ma b/matita/matita/contribs/lambda/pointer_order.ma index 92618412e..0b738215a 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 (rc::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_whd: ∀p,q. p ≺ q → in_whd q → in_whd 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-. @@ -85,7 +87,11 @@ 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. +lemma ple_rc: ∀p,q. dx::p ≤ rc::q. +/2 width=1/ +qed. + +lemma ple_sn: ∀p,q. rc::p ≤ sn::q. /2 width=1/ qed. @@ -106,6 +112,15 @@ lemma ple_skip_ple: ∀p. p ≤ ◊ → dx::p ≤ ◊. #p #q #Hpq #_ #H @(ple_step_sn … H) -H /2 width=1/ qed. +theorem ple_trans: transitive … ple. +/2 width=3/ +qed-. + +lemma ple_cons: ∀p,q. dx::p ≤ sn::q. +#p #q +@(ple_trans … (rc::q)) /2 width=1/ +qed. + lemma ple_dichotomy: ∀p1,p2:ptr. p1 ≤ p2 ∨ p2 ≤ p1. #p1 elim p1 -p1 [ * /2 width=1/ diff --git a/matita/matita/contribs/lambda/st_computation.ma b/matita/matita/contribs/lambda/st_computation.ma index a7ccb05fd..ebcc572a4 100644 --- a/matita/matita/contribs/lambda/st_computation.ma +++ b/matita/matita/contribs/lambda/st_computation.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "labelled_sequential_computation.ma". +include "labeled_sequential_computation.ma". include "pointer_list_standard.ma". (* KASHIMA'S "ST" COMPUTATION ***********************************************) @@ -151,7 +151,7 @@ lemma st_inv_lsreds_is_standard: ∀M,N. M ⓢ⤇* N → [ #s #M #i #Hs #HM lapply (is_whd_is_standard … Hs) -Hs /2 width=3/ | #s #M #A1 #A2 #Hs #HM #_ * #r #HA12 #Hr - lapply (lsreds_trans … HM (sn:::r) (𝛌.A2) ?) /2 width=1/ -A1 #HM + 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 #Hs #HM #_ #_ * #rb #HB12 #Hrb * #ra #HA12 #Hra lapply (lsreds_trans … HM (dx:::ra) (@B1.A2) ?) /2 width=1/ -A1 #HM -- 2.39.2