From 5e24c923ea53c31c3e167c4ff7851877ded646c1 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Sat, 1 Dec 2012 17:07:33 +0000 Subject: [PATCH] - lambda: parallel reduction to obtain diamond property - list: local "norm" notation removed in favour of "card" core notation --- .../contribs/lambda/delifting_substitution.ma | 13 ++- .../lambda/labelled_sequential_computation.ma | 93 ++++++++++++++++++ .../lambda/labelled_sequential_reduction.ma | 96 ++++++++++++++++++- matita/matita/contribs/lambda/lift.ma | 7 ++ .../contribs/lambda/parallel_reduction.ma | 81 ++++++++++++++++ matita/matita/contribs/lambda/policy.txt | 14 +++ matita/matita/contribs/lambda/preamble.ma | 2 +- .../matita/contribs/lambda/redex_pointer.ma | 4 +- .../contribs/lambda/redex_pointer_sequence.ma | 21 ++++ matita/matita/lib/basics/lists/list.ma | 3 +- matita/matita/lib/basics/relations.ma | 3 + 11 files changed, 323 insertions(+), 14 deletions(-) create mode 100644 matita/matita/contribs/lambda/labelled_sequential_computation.ma create mode 100644 matita/matita/contribs/lambda/parallel_reduction.ma create mode 100644 matita/matita/contribs/lambda/policy.txt create mode 100644 matita/matita/contribs/lambda/redex_pointer_sequence.ma diff --git a/matita/matita/contribs/lambda/delifting_substitution.ma b/matita/matita/contribs/lambda/delifting_substitution.ma index 3d4c2150b..11ce88761 100644 --- a/matita/matita/contribs/lambda/delifting_substitution.ma +++ b/matita/matita/contribs/lambda/delifting_substitution.ma @@ -111,8 +111,8 @@ theorem dsubst_lift_ge: ∀h,D,M,d1,d2. d1 + h ≤ d2 → ] qed. -theorem subst_subst_ge: ∀D1,D2,M,d1,d2. d1 ≤ d2 → - [d2 ⬐ D2] [d1 ⬐ D1] M = [d1 ⬐ [d2 - d1 ⬐ D2] D1] [d2 + 1 ⬐ D2] M. +theorem dsubst_dsubst_ge: ∀D1,D2,M,d1,d2. d1 ≤ d2 → + [d2 ⬐ D2] [d1 ⬐ D1] M = [d1 ⬐ [d2 - d1 ⬐ D2] D1] [d2 + 1 ⬐ D2] M. #D1 #D2 #M elim M -M [ #i #d1 #d2 #Hd12 elim (lt_or_eq_or_gt i d1) #Hid1 [ lapply (lt_to_le_to_lt … Hid1 Hd12) -Hd12 #Hid2 @@ -134,9 +134,12 @@ theorem subst_subst_ge: ∀D1,D2,M,d1,d2. d1 ≤ d2 → ] qed. -theorem subst_subst_lt: ∀D1,D2,M,d1,d2. d2 < d1 → - [d2 ⬐ [d1 - d2 -1 ⬐ D1] D2] [d1 ⬐ D1] M = [d1 - 1 ⬐ D1] [d2 ⬐ D2] M. +theorem dsubst_dsubst_lt: ∀D1,D2,M,d1,d2. d2 < d1 → + [d2 ⬐ [d1 - d2 -1 ⬐ D1] D2] [d1 ⬐ D1] M = [d1 - 1 ⬐ D1] [d2 ⬐ D2] M. #D1 #D2 #M #d1 #d2 #Hd21 lapply (ltn_to_ltO … Hd21) #Hd1 ->subst_subst_ge in ⊢ (???%); /2 width=1/ dsubst_dsubst_ge in ⊢ (???%); /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/ +#A #D #d dsubst_dsubst_ge // +qed. + +theorem lsred_mono: ∀p. singlevalued … (lsred p). +#p #M #N1 #H elim H -p -M -N1 +[ #A #D #N2 #H elim (lsred_inv_beta … H ????) -H [4,5: // |2,3: skip ] #A0 #H1 #H2 destruct // (**) (* simplify line *) +| #p #A #C #_ #IHAC #N2 #H elim (lsred_inv_abst … H ??) -H [3: // |2: skip ] #C0 #HAC #H destruct /3 width=1/ (**) (* simplify line *) +| #p #B #D #A #_ #IHBD #N2 #H elim (lsred_inv_appl_sn … H ?????) -H [5,6: // |2,3,4: skip ] #D0 #HBD #H destruct /3 width=1/ (**) (* simplify line *) +| #p #B #A #C #_ #IHAC #N2 #H elim (lsred_inv_appl_dx … H ?????) -H [5,6: // |2,3,4: skip ] #C0 #HAC #H destruct /3 width=1/ (**) (* simplify line *) +] +qed-. diff --git a/matita/matita/contribs/lambda/lift.ma b/matita/matita/contribs/lambda/lift.ma index 817c0c1d7..8f2199fc3 100644 --- a/matita/matita/contribs/lambda/lift.ma +++ b/matita/matita/contribs/lambda/lift.ma @@ -239,3 +239,10 @@ elim (le_inv_plus_l … Hd12) -Hd12 #Hd12 #Hh1d2 lapply (sym_eq term … H) -H >(plus_minus_m_m … Hh1d2) in ⊢ (???%→?); -Hh1d2 #H elim (lift_inv_lift_le … Hd12 … H) -H -Hd12 /2 width=3/ qed-. + +definition liftable: predicate (relation term) ≝ λR. + ∀h,M1,M2. R M1 M2 → ∀d. R (↑[d, h] M1) (↑[d, h] M2). + +definition deliftable: predicate (relation term) ≝ λR. + ∀h,N1,N2. R N1 N2 → ∀d,M1. ↑[d, h] M1 = N1 → + ∃∃M2. R M1 M2 & ↑[d, h] M2 = N2. diff --git a/matita/matita/contribs/lambda/parallel_reduction.ma b/matita/matita/contribs/lambda/parallel_reduction.ma new file mode 100644 index 000000000..4cb204bb9 --- /dev/null +++ b/matita/matita/contribs/lambda/parallel_reduction.ma @@ -0,0 +1,81 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "multiplicity.ma". + +(* PARALLEL REDUCTION (SINGLE STEP) *****************************************) + +(* Note: the application "(A B)" is represented by "@B.A" + as for labelled sequential reduction +*) +inductive pred: relation term ≝ +| pred_vref: ∀i. pred (#i) (#i) +| pred_abst: ∀A,C. pred A C → pred (𝛌.A) (𝛌.C) +| pred_appl: ∀B,D,A,C. pred B D → pred A C → pred (@B.A) (@D.C) +| pred_beta: ∀B,D,A,C. pred B D → pred A C → pred (@B.𝛌.A) ([⬐D]C) +. + +interpretation "parallel reduction" + 'ParRed M N = (pred M N). + +notation "hvbox( M break ⥤ break term 46 N )" + non associative with precedence 45 + for @{ 'ParRed $M $N }. + +lemma pred_refl: reflexive … pred. +#M elim M -M // /2 width=1/ +qed. + +lemma pred_inv_vref: ∀M,N. M ⥤ N → ∀i. #i = M → #i = N. +#M #N * -M -N // +[ #A #C #_ #i #H destruct +| #B #D #A #C #_ #_ #i #H destruct +| #B #D #A #C #_ #_ #i #H destruct +] +qed-. + +lemma pred_inv_abst: ∀M,N. M ⥤ N → ∀A. 𝛌.A = M → + ∃∃C. A ⥤ C & 𝛌.C = N. +#M #N * -M -N +[ #i #A0 #H destruct +| #A #C #HAC #A0 #H destruct /2 width=3/ +| #B #D #A #C #_ #_ #A0 #H destruct +| #B #D #A #C #_ #_ #A0 #H destruct +] +qed-. + +lemma pred_lift: liftable pred. +#h #M1 #M2 #H elim H -M1 -M2 normalize // /2 width=1/ +#D #D #A #C #_ #_ #IHBD #IHAC #d