context-free parallel reduction on closures is confluent!

diff --git a/matita/matita/contribs/lambda_delta/basic_2/notation.ma b/matita/matita/contribs/lambda_delta/basic_2/notation.ma
index fbbb1085ef32e7de8ab354d97f0128d0cdd61449..42f62ca150ece12d772be435e13308a9ec37bbc3 100644 (file)
--- 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 e034710b2f2af3f2ec9a2dc9b823b6e717971aec..7abd3f22fa73b5e4c9c1f206cdc0bc13a2a64a9c 100644 (file)
--- 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 (file)
index 0000000..3f7ac2c
--- /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 b054841290378e47540af1f6e70610e1fb31e9f4..957b5f3a89926458ddf3feaa3371b7bc68766e0d 100644 (file)
--- 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 0bde244171dedc979a8d303b1785f43b45ed3ac2..ab11536bdf4db831547641e2ffadce07e5338283 100644 (file)
--- 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 3517eff98f8ae4187352097ffb812e1fd01d0bbf..2779a0940c35c8e8dcc49983d25e6b612da4c24b 100644 (file)
--- 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 afb5d5aae05515a1c9801c45abb9064f2a55a91f..57403f35698436ae1d8defc9e5fdf02257d678cb 100644 (file)
--- 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.