From: Ferruccio Guidi Date: Sun, 23 Dec 2012 15:02:32 +0000 (+0000) Subject: - we introduced the pointer_step rc in the perspective of proving X-Git-Tag: make_still_working~1373 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=bde429ac54e48de74b3d8b1df72dfcb86aa9bae5;p=helm.git - we introduced the pointer_step rc in the perspective of proving results on head normal forms - some renaming --- diff --git a/matita/matita/contribs/lambda/labeled_sequential_computation.ma b/matita/matita/contribs/lambda/labeled_sequential_computation.ma new file mode 100644 index 000000000..4c2a6fc9e --- /dev/null +++ b/matita/matita/contribs/lambda/labeled_sequential_computation.ma @@ -0,0 +1,145 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "pointer_list.ma". +include "parallel_computation.ma". + +(* LABELED SEQUENTIAL COMPUTATION (MULTISTEP) *******************************) + +definition lsreds: ptrl → relation term ≝ lstar … lsred. + +interpretation "labelled sequential computation" + 'SeqRedStar M s N = (lsreds s M N). + +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. + +lemma lsreds_inv_nil: ∀s,M1,M2. M1 ↦*[s] M2 → ◊ = s → M1 = M2. +/2 width=5 by lstar_inv_nil/ +qed-. + +lemma lsreds_inv_cons: ∀s,M1,M2. M1 ↦*[s] M2 → ∀q,r. q::r = s → + ∃∃M. M1 ↦[q] M & M ↦*[r] M2. +/2 width=3 by lstar_inv_cons/ +qed-. + +lemma lsreds_inv_step_rc: ∀p,M1,M2. M1 ↦*[p::◊] M2 → M1 ↦[p] M2. +/2 width=1 by lstar_inv_step/ +qed-. + +lemma lsreds_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 lsred_compatible_rc: ho_compatible_rc lsreds. +/3 width=1/ +qed. + +lemma lsreds_compatible_sn: ho_compatible_sn lsreds. +/3 width=1/ +qed. + +lemma lsreds_compatible_dx: ho_compatible_dx lsreds. +/3 width=1/ +qed. + +lemma lsreds_lift: ∀s. liftable (lsreds s). +/2 width=1/ +qed. + +lemma lsreds_inv_lift: ∀s. deliftable_sn (lsreds s). +/3 width=3 by lstar_deliftable_sn, lsred_inv_lift/ +qed-. + +lemma lsreds_dsubst: ∀s. dsubstable_dx (lsreds s). +/2 width=1/ +qed. + +theorem lsreds_mono: ∀s. singlevalued … (lsreds s). +/3 width=7 by lstar_singlevalued, lsred_mono/ +qed-. + +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:::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/ +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 // +#p #s #M1 #M #HM1 #_ #IHM2 +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/labeled_sequential_reduction.ma b/matita/matita/contribs/lambda/labeled_sequential_reduction.ma new file mode 100644 index 000000000..7dd2bccb3 --- /dev/null +++ b/matita/matita/contribs/lambda/labeled_sequential_reduction.ma @@ -0,0 +1,143 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "pointer.ma". +include "multiplicity.ma". + +(* 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". + Theoretical Computer Science 155(1), Elsevier (1996), pp. 85-109. +*) +inductive lsred: ptr → relation term ≝ +| lsred_beta : ∀B,A. lsred (◊) (@B.𝛌.A) ([↙B]A) +| 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) +. + +interpretation "labelled sequential reduction" + 'SeqRed M p N = (lsred p M N). + +(* Note: we do not use → since it is reserved by CIC *) +notation "hvbox( M break ↦ [ term 46 p ] break term 46 N )" + non associative with precedence 45 + for @{ 'SeqRed $M $p $N }. + +lemma lsred_inv_vref: ∀p,M,N. M ↦[p] N → ∀i. #i = M → ⊥. +#p #M #N * -p -M -N +[ #B #A #i #H destruct +| #p #A1 #A2 #_ #i #H destruct +| #p #B1 #B2 #A #_ #i #H destruct +| #p #B #A1 #A2 #_ #i #H destruct +] +qed-. + +lemma lsred_inv_nil: ∀p,M,N. M ↦[p] N → ◊ = p → + ∃∃B,A. @B. 𝛌.A = M & [↙B] A = N. +#p #M #N * -p -M -N +[ #B #A #_ destruct /2 width=4/ +| #p #A1 #A2 #_ #H destruct +| #p #B1 #B2 #A #_ #H destruct +| #p #B #A1 #A2 #_ #H destruct +] +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 → + ∃∃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 #_ #q #H destruct +| #p #B1 #B2 #A #HB12 #q #H destruct /2 width=6/ +| #p #B #A1 #A2 #_ #q #H destruct +] +qed-. + +lemma lsred_inv_dx: ∀p,M,N. M ↦[p] N → ∀q. dx::q = p → + ∃∃B,A1,A2. A1 ↦[q] A2 & @B.A1 = M & @B.A2 = N. +#p #M #N * -p -M -N +[ #B #A #q #H destruct +| #p #A1 #A2 #_ #q #H destruct +| #p #B1 #B2 #A #_ #q #H destruct +| #p #B #A1 #A2 #HA12 #q #H destruct /2 width=6/ +] +qed-. + +lemma lsred_fwd_mult: ∀p,M,N. M ↦[p] N → #{N} < #{M} * #{M}. +#p #M #N #H elim H -p -M -N +[ #B #A @(le_to_lt_to_lt … (#{A}*#{B})) // + normalize /3 width=1 by lt_minus_to_plus_r, lt_times/ (**) (* auto: too slow without trace *) +| // +| #p #B #D #A #_ #IHBD + @(lt_to_le_to_lt … (#{B}*#{B}+#{A})) [ /2 width=1/ ] -D -p +| #p #B #A #C #_ #IHAC + @(lt_to_le_to_lt … (#{B}+#{A}*#{A})) [ /2 width=1/ ] -C -p +] +@(transitive_le … (#{B}*#{B}+#{A}*#{A})) [ /2 width=1/ ] +>distributive_times_plus normalize /2 width=1/ +qed-. + +lemma lsred_lift: ∀p. liftable (lsred p). +#p #h #M1 #M2 #H elim H -p -M1 -M2 normalize /2 width=1/ +#B #A #d dsubst_dsubst_ge // +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_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/labelled_sequential_computation.ma b/matita/matita/contribs/lambda/labelled_sequential_computation.ma deleted file mode 100644 index f62864831..000000000 --- a/matita/matita/contribs/lambda/labelled_sequential_computation.ma +++ /dev/null @@ -1,145 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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 "pointer_list.ma". -include "parallel_computation.ma". - -(* LABELLED SEQUENTIAL COMPUTATION (MULTISTEP) ******************************) - -definition lsreds: ptrl → relation term ≝ lstar … lsred. - -interpretation "labelled sequential computation" - 'SeqRedStar M s N = (lsreds s M N). - -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. - -lemma lsreds_inv_nil: ∀s,M1,M2. M1 ↦*[s] M2 → ◊ = s → M1 = M2. -/2 width=5 by lstar_inv_nil/ -qed-. - -lemma lsreds_inv_cons: ∀s,M1,M2. M1 ↦*[s] M2 → ∀q,r. q::r = s → - ∃∃M. M1 ↦[q] M & M ↦*[r] M2. -/2 width=3 by lstar_inv_cons/ -qed-. - -lemma lsreds_inv_step_rc: ∀p,M1,M2. M1 ↦*[p::◊] M2 → M1 ↦[p] M2. -/2 width=1 by lstar_inv_step/ -qed-. - -lemma lsreds_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 lsred_compatible_rc: ho_compatible_rc lsreds. -/3 width=1/ -qed. - -lemma lsreds_compatible_sn: ho_compatible_sn lsreds. -/3 width=1/ -qed. - -lemma lsreds_compatible_dx: ho_compatible_dx lsreds. -/3 width=1/ -qed. - -lemma lsreds_lift: ∀s. liftable (lsreds s). -/2 width=1/ -qed. - -lemma lsreds_inv_lift: ∀s. deliftable_sn (lsreds s). -/3 width=3 by lstar_deliftable_sn, lsred_inv_lift/ -qed-. - -lemma lsreds_dsubst: ∀s. dsubstable_dx (lsreds s). -/2 width=1/ -qed. - -theorem lsreds_mono: ∀s. singlevalued … (lsreds s). -/3 width=7 by lstar_singlevalued, lsred_mono/ -qed-. - -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 // -#p #s #M1 #M #HM1 #_ #IHM2 -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/labelled_sequential_reduction.ma b/matita/matita/contribs/lambda/labelled_sequential_reduction.ma deleted file mode 100644 index 40d518846..000000000 --- a/matita/matita/contribs/lambda/labelled_sequential_reduction.ma +++ /dev/null @@ -1,136 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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 "pointer.ma". -include "multiplicity.ma". - -(* LABELLED SEQUENTIAL REDUCTION (SINGLE STEP) ******************************) - -(* Note: the application "(A B)" is represented by "@B.A" following: - F. Kamareddine and R.P. Nederpelt: "A useful λ-notation". - Theoretical Computer Science 155(1), Elsevier (1996), pp. 85-109. -*) -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_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) -. - -interpretation "labelled sequential reduction" - 'SeqRed M p N = (lsred p M N). - -(* Note: we do not use → since it is reserved by CIC *) -notation "hvbox( M break ↦ [ term 46 p ] break term 46 N )" - non associative with precedence 45 - for @{ 'SeqRed $M $p $N }. - -lemma lsred_inv_vref: ∀p,M,N. M ↦[p] N → ∀i. #i = M → ⊥. -#p #M #N * -p -M -N -[ #B #A #i #H destruct -| #p #A1 #A2 #_ #i #H destruct -| #p #B1 #B2 #A #_ #i #H destruct -| #p #B #A1 #A2 #_ #i #H destruct -] -qed-. - -lemma lsred_inv_nil: ∀p,M,N. M ↦[p] N → ◊ = p → - ∃∃B,A. @B. 𝛌.A = M & [↙B] A = N. -#p #M #N * -p -M -N -[ #B #A #_ destruct /2 width=4/ -| #p #A1 #A2 #_ #H destruct -| #p #B1 #B2 #A #_ #H destruct -| #p #B #A1 #A2 #_ #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 #B #A1 #A2 #_ #q #H destruct -] -qed-. - -lemma lsred_inv_dx: ∀p,M,N. M ↦[p] N → ∀q. dx::q = p → - ∃∃B,A1,A2. A1 ↦[q] A2 & @B.A1 = M & @B.A2 = N. -#p #M #N * -p -M -N -[ #B #A #q #H destruct -| #p #A1 #A2 #_ #q #H destruct -| #p #B1 #B2 #A #_ #q #H destruct -| #p #B #A1 #A2 #HA12 #q #H destruct /2 width=6/ -] -qed-. - -lemma lsred_fwd_mult: ∀p,M,N. M ↦[p] N → #{N} < #{M} * #{M}. -#p #M #N #H elim H -p -M -N -[ #B #A @(le_to_lt_to_lt … (#{A}*#{B})) // - normalize /3 width=1 by lt_minus_to_plus_r, lt_times/ (**) (* auto: too slow without trace *) -| // -| #p #B #D #A #_ #IHBD - @(lt_to_le_to_lt … (#{B}*#{B}+#{A})) [ /2 width=1/ ] -D -p -| #p #B #A #C #_ #IHAC - @(lt_to_le_to_lt … (#{B}+#{A}*#{A})) [ /2 width=1/ ] -C -p -] -@(transitive_le … (#{B}*#{B}+#{A}*#{A})) [ /2 width=1/ ] ->distributive_times_plus normalize /2 width=1/ -qed-. - -lemma lsred_lift: ∀p. liftable (lsred p). -#p #h #M1 #M2 #H elim H -p -M1 -M2 normalize /2 width=1/ -#B #A #d dsubst_dsubst_ge // -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 *) -] -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