From bb397726bff29389cdcb649a8c37484395b3b85e Mon Sep 17 00:00:00 2001
From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Fri, 11 Mar 2011 07:17:06 +0000
Subject: [PATCH] added star.ma (star closure of a relation)

---
 matita/matita/lib/basics/star.ma | 85 ++++++++++++++++++++++++++++++++
 1 file changed, 85 insertions(+)
 create mode 100644 matita/matita/lib/basics/star.ma

diff --git a/matita/matita/lib/basics/star.ma b/matita/matita/lib/basics/star.ma
new file mode 100644
index 000000000..8e850c697
--- /dev/null
+++ b/matita/matita/lib/basics/star.ma
@@ -0,0 +1,85 @@
+(*
+    ||M||  This file is part of HELM, an Hypertextual, Electronic        
+    ||A||  Library of Mathematics, developed at the Computer Science     
+    ||T||  Department of the University of Bologna, Italy.                     
+    ||I||                                                                 
+    ||T||  
+    ||A||  This file is distributed under the terms of the 
+    \   /  GNU General Public License Version 2        
+     \ /      
+      V_______________________________________________________________ *)
+
+include "basics/relations.ma".
+
+(********** relations **********)
+
+inductive star (A:Type[0]) (R:relation A) (a:A): A → Prop ≝
+  |inj: ∀b,c.star A R a b → R b c → star A R a c
+  |refl: star A R a a.
+
+theorem trans_star: ∀A,R,a,b,c. 
+  star A R a b → star A R b c → star A R a c.
+#A #R #a #b #c #Hab #Hbc (elim Hbc) /2/
+qed.
+
+theorem star_star: ∀A,R. exteqR … (star A R) (star A (star A R)).
+#A #R #a #b % /2/ #H (elim H) /2/
+qed.
+
+definition subR ≝ λA.λR,S:relation A.(∀a,b. R a b → S a b).
+
+lemma monotonic_star: ∀A,R,S. subR A R S → subR A (star A R) (star A S).
+#A #R #S #subRS #a #b #H (elim H) /3/
+qed.
+
+lemma sub_star: ∀A,R,S. subR A R (star A S) → 
+  subR A (star A R) (star A S).
+#A #R #S #Hsub #a #b #H (elim H) /3/
+qed.
+
+theorem sub_star_to_eq: ∀A,R,S. subR A R S → subR A S (star A R) → 
+  exteqR … (star A R) (star A S).
+#A #R #S #sub1 #sub2 #a #b % /2/
+qed.
+
+(* equiv -- smallest equivalence relation containing R *)
+
+inductive equiv (A:Type[0]) (R:relation A) : A → A → Prop ≝
+  |inje: ∀a,b,c.equiv A R a b → R b c → equiv A R a c
+  |refle: ∀a,b.equiv A R a b
+  |syme: ∀a,b.equiv A R a b → equiv A R b a.
+  
+theorem trans_equiv: ∀A,R,a,b,c. 
+  equiv A R a b → equiv A R b c → equiv A R a c.
+#A #R #a #b #c #Hab #Hbc (inversion Hbc) /2/
+qed.
+ 
+theorem equiv_equiv: ∀A,R. exteqR … (equiv A R) (equiv A (equiv A R)).
+#A #R #a #b % /2/  
+qed.
+
+lemma monotonic_equiv: ∀A,R,S. subR A R S → subR A (equiv A R) (equiv A S).
+#A #R #S #subRS #a #b #H (elim H) /3/
+qed.
+
+lemma sub_equiv: ∀A,R,S. subR A R (equiv A S) → 
+  subR A (equiv A R) (equiv A S).
+#A #R #S #Hsub #a #b #H (elim H) /2/
+qed.
+
+theorem sub_equiv_to_eq: ∀A,R,S. subR A R S → subR A S (equiv A R) → 
+  exteqR … (equiv A R) (equiv A S).
+#A #R #S #sub1 #sub2 #a #b % /2/
+qed.
+
+(* well founded part of a relation *)
+
+inductive WF (A:Type[0]) (R:relation A) : A → Prop ≝
+  | wf : ∀b.(∀a. R a b → WF A R a) → WF A R b.
+
+lemma WF_antimonotonic: ∀A,R,S. subR A R S → 
+  ∀a. WF A S a → WF A R a.
+#A #R #S #subRS #a #HWF (elim HWF) #b
+#H #Hind % #c #Rcb @Hind @subRS //
+qed.
+
-- 
2.39.2