support for nat-labeled reflexive and transitive closure added to lambdadelta

diff --git a/matita/matita/contribs/lambdadelta/ground_2/lstar.ma b/matita/matita/contribs/lambdadelta/ground_2/lstar.ma
new file mode 100644 (file)
index 0000000..ae707f2
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/ground_2/lstar.ma
@@ -0,0 +1,20 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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 "arithmetics/lstar.ma".
+
+(* PROPERTIES OF NAT-LABELED REFLEXIVE AND TRANSITIVE CLOSURE ***************)
+
+definition llstar: ∀A:Type[0]. ∀B. (A→relation B) → nat → (A→relation B) ≝
+                   λA,B,R,l,a. lstar … (R a) l.

diff --git a/matita/matita/lib/arithmetics/lstar.ma b/matita/matita/lib/arithmetics/lstar.ma
index ddd4113e325b8028b013c14c231f1d958007e31f..e3dcd55d6b86ac03e6c7ab48330b77698ae120d2 100644 (file)
--- a/matita/matita/lib/arithmetics/lstar.ma
+++ b/matita/matita/lib/arithmetics/lstar.ma
@@ -48,6 +48,11 @@ lemma lstar_step: ∀B,R,b1,b2. R b1 b2 → lstar B R 1 b1 b2.
 /2 width=3/
 qed.
 
+lemma lstar_dx: ∀B,R,l,b1,b. lstar B R l b1 b → ∀b2. R b b2 →
+                lstar B R (l+1) b1 b2.
+#B #R #l #b1 #b #H @(lstar_ind_l … l b1 H) -l -b1 /2 width=1/ /3 width=3/
+qed.
+
 lemma lstar_inv_O: ∀B,R,l,b1,b2. lstar B R l b1 b2 → 0 = l → b1 = b2.
 #B #R #l #b1 #b2 * -l -b1 -b2 //
 #b1 #b #_ #l #b2 #_ <plus_n_Sm #H destruct
@@ -90,10 +95,12 @@ elim (lstar_inv_S … b2 H (l1+l2)) -H // #b #Hb1 #Hb2
 elim (IHl1 … Hb2) -IHl1 -Hb2 /3 width=3/
 qed-.
 
-lemma lstar_dx: ∀B,R,l,b1,b. lstar B R l b1 b → ∀b2. R b b2 →
-                lstar B R (l+1) b1 b2.
-#B #R #l #b1 #b #H @(lstar_ind_l … l b1 H) -l -b1 /2 width=1/ /3 width=3/
-qed.
+lemma lstar_inv_S_dx: ∀B,R,l,b1,b2. lstar B R (l+1) b1 b2 →
+                      ∃∃b. lstar B R l b1 b & R b b2.
+#B #R #l #b1 #b2 #H
+elim (lstar_inv_ltransitive B R … H) -H #b #Hb1 #H
+lapply (lstar_inv_step B R … H) -H /2 width=3/
+qed-.
 
 inductive lstar_r (B:Type[0]) (R: relation B): ℕ → relation B ≝
 | lstar_r_O: ∀b. lstar_r B R 0 b b
@@ -133,3 +140,7 @@ lemma lstar_ind_r: ∀B,R,b1. ∀P:relation2 ℕ B.
 #B #R #b1 #P #H1 #H2 #l #b2 #Hb12
 @(lstar_ind_r_aux … H1 H2 … Hb12) //
 qed-.
+
+lemma lstar_Conf3: ∀A,B,S,R. Conf3 A B S R → ∀l. Conf3 A B S (lstar … R l).
+#A #B #S #R #HSR #l #b #a1 #Ha1 #a2 #H @(lstar_ind_r … l a2 H) -l -a2 // /2 width=3/
+qed-.

diff --git a/matita/matita/lib/basics/relations.ma b/matita/matita/lib/basics/relations.ma
index a43ed63252a37e64c768326422f7dae3147678c4..fb0423cea315bf5ceda6185c8fe95e3060221a67 100644 (file)
--- a/matita/matita/lib/basics/relations.ma
+++ b/matita/matita/lib/basics/relations.ma
@@ -61,6 +61,10 @@ definition confluent1: ∀A. relation A → predicate A ≝ λA,R,a0.
 definition confluent: ∀A. predicate (relation A) ≝ λA,R.
                       ∀a0. confluent1 … R a0.
 
+(* triangular confluence of two relations *)
+definition Conf3: ∀A,B. relation2 A B → relation A → Prop ≝ λA,B,S,R.
+                  ∀b,a1. S a1 b → ∀a2. R a1 a2 → S a2 b.
+
 (* Reflexive closure ************)
 
 definition RC: ∀A:Type[0]. relation A → relation A ≝

diff --git a/matita/matita/lib/basics/star.ma b/matita/matita/lib/basics/star.ma
index 6592592aa6f092861531fa9e95e97fa841559e06..00a23b633a206017c0fce733f605a111adc681c0 100644 (file)
--- a/matita/matita/lib/basics/star.ma
+++ b/matita/matita/lib/basics/star.ma
@@ -258,9 +258,6 @@ lemma TC_star_ind_dx: ∀A,R. reflexive A R →
 @(TC_ind_dx … P ? H … Ha12) /3 width=4/
 qed-.
 
-definition Conf3: ∀A,B. relation2 A B → relation A → Prop ≝ λA,B,S,R.
-                  ∀b,a1. S a1 b → ∀a2. R a1 a2 → S a2 b.
-
 lemma TC_Conf3: ∀A,B,S,R. Conf3 A B S R → Conf3 A B S (TC … R).
 #A #B #S #R #HSR #b #a1 #Ha1 #a2 #H elim H -a2 /2 width=3/
 qed.