the decentralization of core notation continues ...

[helm.git] / matita / matita / lib / basics / relations.ma

diff --git a/matita/matita/lib/basics/relations.ma b/matita/matita/lib/basics/relations.ma
index 55b26b8aefe71f567dda9b9bd34761a79ed4442f..3133682dbc372fc1e2bdb4b9fe1c76393f070b89 100644 (file)
--- a/matita/matita/lib/basics/relations.ma
+++ b/matita/matita/lib/basics/relations.ma
@@ -10,6 +10,8 @@
       V_______________________________________________________________ *)
 
 include "basics/logic.ma".
+include "basics/core_notation/compose_2.ma".
+include "basics/core_notation/subseteq_2.ma".
 
 (********** predicates *********)
 
@@ -23,6 +25,12 @@ definition relation : Type[0] → Type[0]
 definition relation2 : Type[0] → Type[0] → Type[0]
 ≝ λA,B.A→B→Prop.
 
+definition relation3 : Type[0] → Type[0] → Type[0] → Type[0]
+≝ λA,B,C.A→B→C→Prop.
+
+definition relation4 : Type[0] → Type[0] → Type[0] → Type[0] → Type[0]
+≝ λA,B,C,D.A→B→C→D→Prop.
+
 definition reflexive: ∀A.∀R :relation A.Prop
 ≝ λA.λR.∀x:A.R x x.
 
@@ -45,7 +53,33 @@ definition tight_apart: ∀A.∀eq,ap:relation A.Prop
 definition antisymmetric: ∀A.∀R:relation A.Prop
 ≝ λA.λR.∀x,y:A. R x y → ¬(R y x).
 
+definition singlevalued: ∀A,B. predicate (relation2 A B) ≝ λA,B,R.
+                         ∀a,b1. R a b1 → ∀b2. R a b2 → b1 = b2.
+
+definition confluent1: ∀A. relation A → predicate A ≝ λA,R,a0.
+                       ∀a1. R a0 a1 → ∀a2. R a0 a2 →
+                       ∃∃a. R a1 a & R a2 a. 
+
+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 ≝
+               λA,R,x,y. R … x y ∨ x = y.
+
+lemma RC_reflexive: ∀A,R. reflexive A (RC … R).
+/2 width=1/ qed.
+
 (********** operations **********)
+definition Rcomp ≝ λA.λR1,R2:relation A.λa1,a2.
+  ∃am.R1 a1 am ∧ R2 am a2.
+interpretation "relation composition" 'compose R1 R2 = (Rcomp ? R1 R2).
+
 definition Runion ≝ λA.λR1,R2:relation A.λa,b. R1 a b ∨ R2 a b.
 interpretation "union of relations" 'union R1 R2 = (Runion ? R1 R2).
     
@@ -54,10 +88,36 @@ interpretation "interesecion of relations" 'intersects R1 R2 = (Rintersection ?
 
 definition inv ≝ λA.λR:relation A.λa,b.R b a.
 
+(*********** sub relation ***********)
 definition subR ≝ λA.λR,S:relation A.(∀a,b. R a b → S a b).
 interpretation "relation inclusion" 'subseteq R S = (subR ? R S).
 
-(**********P functions **********)
+lemma sub_reflexive : 
+  ∀T.∀R:relation T.R ⊆ R.
+#T #R #x //
+qed.
+
+lemma sub_comp_l:  ∀A.∀R,R1,R2:relation A.
+  R1 ⊆ R2 → R1 ∘ R ⊆ R2 ∘ R.
+#A #R #R1 #R2 #Hsub #a #b * #c * /4/
+qed.
+
+lemma sub_comp_r:  ∀A.∀R,R1,R2:relation A.
+  R1 ⊆ R2 → R ∘ R1 ⊆ R ∘ R2.
+#A #R #R1 #R2 #Hsub #a #b * #c * /4/
+qed.
+
+lemma sub_assoc_l: ∀A.∀R1,R2,R3:relation A.
+  R1 ∘ (R2 ∘ R3) ⊆ (R1 ∘ R2) ∘ R3.
+#A #R1 #R2 #R3 #a #b * #c * #Hac * #d * /5/
+qed.
+
+lemma sub_assoc_r: ∀A.∀R1,R2,R3:relation A.
+  (R1 ∘ R2) ∘ R3 ⊆ R1 ∘ (R2 ∘ R3).
+#A #R1 #R2 #R3 #a #b * #c * * #d * /5 width=5/ 
+qed.
+
+(************* functions ************)
 
 definition compose ≝
   λA,B,C:Type[0].λf:B→C.λg:A→B.λx:A.f (g x).
@@ -126,3 +186,39 @@ for @{'eqF ? ? f g}.
 interpretation "functional extentional equality" 
 'eqF A B f g = (exteqF A B f g).
 
+(********** relations on unboxed pairs **********)
+
+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
+≝ λA,B,R. ∀a,b. R a b a b.
+
+definition bi_symmetric: ∀A,B. ∀R: bi_relation A B. Prop ≝ λA,B,R.
+                         ∀a1,a2,b1,b2. R a2 b2 a1 b1 → R a1 b1 a2 b2.
+
+definition bi_transitive: ∀A,B. ∀R: bi_relation A B. Prop ≝ λA,B,R.
+                          ∀a1,a,b1,b. R a1 b1 a b →
+                          ∀a2,b2. R a b a2 b2 → R a1 b1 a2 b2.
+
+definition bi_RC: ∀A,B:Type[0]. bi_relation A B → bi_relation A B ≝
+                  λA,B,R,a1,b1,a2,b2. R … a1 b1 a2 b2 ∨ (a1 = a2 ∧ b1 = b2).
+
+lemma bi_RC_reflexive: ∀A,B,R. bi_reflexive A B (bi_RC … R).
+/3 width=1/ qed.
+
+(********** relations on unboxed triples **********)
+
+definition tri_relation: Type[0] → Type[0] → Type[0] → Type[0]
+≝ λA,B,C.A→B→C→A→B→C→Prop.
+
+definition tri_reflexive: ∀A,B,C. ∀R:tri_relation A B C. Prop
+≝ λA,B,C,R. ∀a,b,c. R a b c a b c.
+
+definition tri_symmetric: ∀A,B,C. ∀R: tri_relation A B C. Prop ≝ λA,B,C,R.
+                          ∀a1,a2,b1,b2,c1,c2.
+                          R a2 b2 c2 a1 b1 c1 → R a1 b1 c1 a2 b2 c2.
+
+definition tri_transitive: ∀A,B,C. ∀R: tri_relation A B C. Prop ≝ λA,B,C,R.
+                           ∀a1,a,b1,b,c1,c. R a1 b1 c1 a b c →
+                           ∀a2,b2,c2. R a b c a2 b2 c2 → R a1 b1 c1 a2 b2 c2.