X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Fbasics%2Frelations.ma;h=f469ddca29f72fe1eeaeea9d50752fefed34aad2;hb=d183f23928164d2de911298f5f2232be54e49300;hp=59aad912df75b687b4c2ebe7481dc2e9f5ca0a47;hpb=409f569bde067546830df25cd0b1ca898573f66a;p=helm.git

diff --git a/matita/matita/lib/basics/relations.ma b/matita/matita/lib/basics/relations.ma
index 59aad912d..f469ddca2 100644
--- a/matita/matita/lib/basics/relations.ma
+++ b/matita/matita/lib/basics/relations.ma
@@ -11,10 +11,21 @@
 
 include "basics/logic.ma".
 
+(********** predicates *********)
+
+definition predicate: Type[0] → Type[0]
+≝ λA.A→Prop.
+
 (********** relations **********)
 definition relation : Type[0] → Type[0]
 ≝ λA.A→A→Prop. 
 
+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 reflexive: ∀A.∀R :relation A.Prop
 ≝ λA.λR.∀x:A.R x x.
 
@@ -37,7 +48,49 @@ 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).
 
-(********** functions **********)
+(********** 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).
+    
+definition Rintersection ≝ λA.λR1,R2:relation A.λa,b.R1 a b ∧ R2 a b.
+interpretation "interesecion of relations" 'intersects R1 R2 = (Rintersection ? R1 R2).
+
+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).
+
+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).
@@ -77,8 +130,9 @@ injective A B f → injective B C g → injective A C (λx.g (f x)).
 
 (* extensional equality *)
 
+(* moved inside sets.ma
 definition exteqP: ∀A:Type[0].∀P,Q:A→Prop.Prop ≝
-λA.λP,Q.∀a.iff (P a) (Q a).
+λA.λP,Q.∀a.iff (P a) (Q a). *)
 
 definition exteqR: ∀A,B:Type[0].∀R,S:A→B→Prop.Prop ≝
 λA,B.λR,S.∀a.∀b.iff (R a b) (S a b).
@@ -86,11 +140,12 @@ definition exteqR: ∀A,B:Type[0].∀R,S:A→B→Prop.Prop ≝
 definition exteqF: ∀A,B:Type[0].∀f,g:A→B.Prop ≝
 λA,B.λf,g.∀a.f a = g a.
 
+(*
 notation " x \eqP y " non associative with precedence 45 
 for @{'eqP A $x $y}.
 
 interpretation "functional extentional equality" 
-'eqP A x y = (exteqP A x y).
+'eqP A x y = (exteqP A x y). *)
 
 notation "x \eqR y" non associative with precedence 45 
 for @{'eqR ? ? x y}.
@@ -104,3 +159,17 @@ 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. ∀x,y. R x y x y.
+
+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.