basic lemmas

[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 8b6a79be5deec90a9f7820287174045f277bb533..f469ddca29f72fe1eeaeea9d50752fefed34aad2 100644 (file)
--- a/matita/matita/lib/basics/relations.ma
+++ b/matita/matita/lib/basics/relations.ma
@@ -23,6 +23,9 @@ 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 reflexive: ∀A.∀R :relation A.Prop
 ≝ λA.λR.∀x:A.R x x.
 
@@ -62,6 +65,11 @@ definition inv ≝ λA.λR:relation A.λa,b.R b a.
 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/
@@ -151,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.