From 85a42e4a2a4c62818b6a98eff545e58ceb8770a4 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Tue, 16 Oct 2012 18:11:21 +0000 Subject: [PATCH] context-free parallel reduction on closures is confluent! --- .../contribs/lambda_delta/basic_2/notation.ma | 4 ++ .../basic_2/reducibility/fpr_cpr.ma | 2 +- .../basic_2/reducibility/fpr_fpr.ma | 26 ++++++++++ .../lambda_delta/basic_2/reducibility/tpr.ma | 50 +++++-------------- .../lambda_delta/basic_2/substitution/tps.ma | 15 ++++++ .../contribs/lambda_delta/ground_2/star.ma | 4 ++ matita/matita/lib/basics/relations.ma | 2 +- 7 files changed, 64 insertions(+), 39 deletions(-) create mode 100644 matita/matita/contribs/lambda_delta/basic_2/reducibility/fpr_fpr.ma diff --git a/matita/matita/contribs/lambda_delta/basic_2/notation.ma b/matita/matita/contribs/lambda_delta/basic_2/notation.ma index fbbb1085e..42f62ca15 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/notation.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/notation.ma @@ -398,6 +398,10 @@ notation "hvbox( ⦃ L1 ⦄ ⬌ * ⦃ L2 ⦄ )" non associative with precedence 45 for @{ 'FocalizedPConvStar $L1 $L2 }. +notation "hvbox( L1 ⊢ ⬌* break term 46 L2 )" + non associative with precedence 45 + for @{ 'CPConvStar $L1 $L2 }. + (* Dynamic typing ***********************************************************) notation "hvbox( ⦃ h , break L ⦄ ⊩ break term 46 T : break [ g ] )" diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/fpr_cpr.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/fpr_cpr.ma index e034710b2..7abd3f22f 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/fpr_cpr.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/fpr_cpr.ma @@ -14,7 +14,7 @@ include "basic_2/reducibility/cfpr_cpr.ma". -(* FOCALIZED PARALLEL REDUCTION ON CLOSURES *********************************) +(* CONTEXT-FREE PARALLEL REDUCTION ON CLOSURES ******************************) (* Advanced propertis *******************************************************) diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/fpr_fpr.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/fpr_fpr.ma new file mode 100644 index 000000000..3f7ac2ceb --- /dev/null +++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/fpr_fpr.ma @@ -0,0 +1,26 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "basic_2/reducibility/tpr_tpr.ma". +include "basic_2/reducibility/fpr.ma". + +(* CONTEXT-FREE PARALLEL REDUCTION ON CLOSURES ******************************) + +(* Main properties **********************************************************) + +theorem fpr_conf: bi_confluent … fpr. +#L0 #L1 #T0 #T1 * #HL01 #HT01 #L2 #T2 * >HL01 #HL12 #HT02 +elim (tpr_conf … HT01 HT02) -L0 -T0 #X #H1 #H2 +elim (tpr_fwd_shift1 … H1) #L #T #HL1 #H destruct /3 width=5/ +qed. diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/tpr.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/tpr.ma index b05484129..957b5f3a8 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/tpr.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/tpr.ma @@ -204,49 +204,25 @@ lemma tpr_inv_lref2: ∀T1,i. T1 ➡ #i → /2 width=3/ qed-. (* Basic forward lemmas *****************************************************) -(* + lemma tpr_fwd_shift1: ∀L1,T1,T. L1 @@ T1 ➡ T → - ∃∃L2,T2. L1 𝟙 L2 & T = L2 @@ T2. -#L1 @(lenv_ind_dx … L1) -L1 -[ #T1 #T #_ @ex2_2_intro [3: // |4: // |1,2: skip ] (**) (* /2 width=4/ does not work *) -| #I #L1 #V1 #IH #T1 #T >shift_append_assoc #H - elim (tpr_inv_bind1 … H) -H * - [ #V0 #T0 #X0 #_ #HT10 #HTX0 #H destruct - elim (IH … HT10) -IH -T1 #L2 #V2 #HL12 #H destruct - elim (tps_fwd_shift1 … HTX0) -V2 #L3 #X3 #HL23 #H destruct - lapply (ltop_trans … HL12 HL23) -L2 #HL13 - @(ex2_2_intro … (⋆.ⓑ{I}V0@@L3)) /2 width=4/ /3 width=1/ - | #T0 #_ #_ #H destruct - ] -] -qed-. -*) - - -(* - >shift_append_assoc >shift_append_assoc >shift_append_assoc >shift_append_assoc normalize #H + ∃∃L2,T2. |L1| = |L2| & T = L2 @@ T2. +#L1 @(lenv_ind_dx … L1) -L1 normalize +[ #T1 #T #HT1 + @(ex2_2_intro … (⋆)) // (**) (* explicit constructor *) +| #I #L1 #V1 #IH #T1 #X + >shift_append_assoc normalize #H elim (tpr_inv_bind1 … H) -H * - [ #V #T #T0 #HV1 #HT1 #HT0 #H destruct /2 width=1/ + [ #V0 #T0 #X0 #_ #HT10 #H0 #H destruct + elim (IH … HT10) -IH -T1 #L #T #HL1 #H destruct + elim (tps_fwd_shift1 … H0) -T #L2 #T2 #HL2 #H destruct + >append_length >HL1 >HL2 -L1 -L + @(ex2_2_intro … (⋆.ⓑ{I}V0@@L2) T2) [ >append_length ] // /2 width=3/ (**) (* explicit constructor *) | #T #_ #_ #H destruct ] - - lapply (IH … HT12) - - - >shift_append_assoc >shift_append_assoc >shift_append_assoc #HT12 - lapply (shift_inj … HT12) -HT12 - - - - #L2 #HL12 #I1 #I2 #V1 #V2 #T1 #T2 #H -elim (tpr_fwd_shift1 (L1.ⓑ{I1}V1) … H) -H #Y #X #HY #HX -elim (ltop_inv_pair1 … HY) -HY #L #V #HL1 #H destruct -elim (shift_inj (L2.ⓑ{I2}V2) … HX ?) -HX -[ #H1 #_ destruct /2 width=1/ -| lapply (ltop_fwd_length … HL1) -HL1 normalize // ] qed-. -*) + (* Basic_1: removed theorems 3: pr0_subst0_back pr0_subst0_fwd pr0_subst0 Basic_1: removed local theorems: 1: pr0_delta_tau diff --git a/matita/matita/contribs/lambda_delta/basic_2/substitution/tps.ma b/matita/matita/contribs/lambda_delta/basic_2/substitution/tps.ma index 0bde24417..ab11536bd 100644 --- a/matita/matita/contribs/lambda_delta/basic_2/substitution/tps.ma +++ b/matita/matita/contribs/lambda_delta/basic_2/substitution/tps.ma @@ -259,6 +259,21 @@ lemma tps_fwd_tw: ∀L,T1,T2,d,e. L ⊢ T1 ▶ [d, e] T2 → #{T1} ≤ #{T2}. /3 by monotonic_le_plus_l, le_plus/ (**) (* just /3 width=1/ is too slow *) qed-. +lemma tps_fwd_shift1: ∀L1,L,T1,T,d,e. L ⊢ L1 @@ T1 ▶[d, e] T → + ∃∃L2,T2. |L1| = |L2| & T = L2 @@ T2. +#L1 @(lenv_ind_dx … L1) -L1 normalize +[ #L #T1 #T #d #e #HT1 + @(ex2_2_intro … (⋆)) // (**) (* explicit constructor *) +| #I #L1 #V1 #IH #L #T1 #X #d #e + >shift_append_assoc normalize #H + elim (tps_inv_bind1 … H) -H + #V0 #T0 #_ #HT10 #H destruct + elim (IH … HT10) -IH -HT10 #L2 #T2 #HL12 #H destruct + >append_length >HL12 -HL12 + @(ex2_2_intro … (⋆.ⓑ{I}V0@@L2) T2) [ >append_length ] // /2 width=3/ (**) (* explicit constructor *) +] +qed-. + (* Basic_1: removed theorems 25: subst0_gen_sort subst0_gen_lref subst0_gen_head subst0_gen_lift_lt subst0_gen_lift_false subst0_gen_lift_ge subst0_refl subst0_trans diff --git a/matita/matita/contribs/lambda_delta/ground_2/star.ma b/matita/matita/contribs/lambda_delta/ground_2/star.ma index 3517eff98..2779a0940 100644 --- a/matita/matita/contribs/lambda_delta/ground_2/star.ma +++ b/matita/matita/contribs/lambda_delta/ground_2/star.ma @@ -35,6 +35,10 @@ definition transitive2: ∀A. ∀R1,R2: relation A. Prop ≝ λA,R1,R2. ∀a1,a0. R1 a1 a0 → ∀a2. R2 a0 a2 → ∃∃a. R2 a1 a & R1 a a2. +definition bi_confluent: ∀A,B. ∀R: bi_relation A B. Prop ≝ λA,B,R. + ∀a0,a1,b0,b1. R a0 b0 a1 b1 → ∀a2,b2. R a0 b0 a2 b2 → + ∃∃a,b. R a1 b1 a b & R a2 b2 a b. + lemma TC_strip1: ∀A,R1,R2. confluent2 A R1 R2 → ∀a0,a1. TC … R1 a0 a1 → ∀a2. R2 a0 a2 → ∃∃a. R2 a1 a & TC … R1 a2 a. diff --git a/matita/matita/lib/basics/relations.ma b/matita/matita/lib/basics/relations.ma index afb5d5aae..57403f356 100644 --- a/matita/matita/lib/basics/relations.ma +++ b/matita/matita/lib/basics/relations.ma @@ -161,5 +161,5 @@ interpretation "functional extentional equality" definition bi_relation: Type[0] → Type[0] → Type[0] ≝ λA,B.A→B→A→B→Prop. -definition bi_reflexive: ∀A,B. ∀R :bi_relation A B. Prop +definition bi_reflexive: ∀A,B. ∀R:bi_relation A B. Prop ≝ λA,B,R. ∀x,y. R x y x y. -- 2.39.2