From b08fbe87149ae7c2e14dfd7485dbf50d6e7dbfe6 Mon Sep 17 00:00:00 2001
From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Sat, 7 Sep 2013 17:07:12 +0000
Subject: [PATCH] support for nat-labeled reflexive and transitive closure
 added to lambdadelta

---
 .../contribs/lambdadelta/ground_2/lstar.ma    | 20 +++++++++++++++++++
 matita/matita/lib/arithmetics/lstar.ma        | 19 ++++++++++++++----
 matita/matita/lib/basics/relations.ma         |  4 ++++
 matita/matita/lib/basics/star.ma              |  3 ---
 4 files changed, 39 insertions(+), 7 deletions(-)
 create mode 100644 matita/matita/contribs/lambdadelta/ground_2/lstar.ma

diff --git a/matita/matita/contribs/lambdadelta/ground_2/lstar.ma b/matita/matita/contribs/lambdadelta/ground_2/lstar.ma
new file mode 100644
index 000000000..ae707f2b9
--- /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 ddd4113e3..e3dcd55d6 100644
--- 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 a43ed6325..fb0423cea 100644
--- 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 6592592aa..00a23b633 100644
--- 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.
-- 
2.39.2