theories/Relations

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@510 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 76 insertions, 0 deletions

diff --git a/theories/Relations/Relation_Definitions.v b/theories/Relations/Relation_Definitions.v
new file mode 100755
index 000000000..9d32ae9be
--- /dev/null
+++ b/theories/Relations/Relation_Definitions.v
@@ -0,0 +1,76 @@
+
+(* $Id$ *)
+
+Section Relation_Definition.
+
+   Variable A: Set.
+   
+   Definition relation :=  A -> A -> Prop.
+
+   Variable R: relation.
+   
+
+Section General_Properties_of_Relations.
+
+  Definition reflexive : Prop :=  (x: A) (R x x).
+  Definition transitive : Prop :=  (x,y,z: A) (R x y) -> (R y z) -> (R x z).
+  Definition symmetric : Prop :=  (x,y: A) (R x y) -> (R y x).
+  Definition antisymmetric : Prop :=  (x,y: A) (R x y) -> (R y x) -> x=y.
+
+  (* for compatibility with Equivalence in  ../PROGRAMS/ALG/  *)
+  Definition equiv := reflexive /\ transitive /\ symmetric.
+
+End General_Properties_of_Relations.
+
+
+
+Section Sets_of_Relations.
+
+   Record preorder : Prop := {
+       preord_refl  : reflexive;
+       preord_trans : transitive }.
+
+   Record order : Prop := {
+       ord_refl    : reflexive;
+       ord_trans   : transitive;
+       ord_antisym : antisymmetric }.
+
+   Record equivalence : Prop := {
+       equiv_refl  : reflexive;
+       equiv_trans : transitive;
+       equiv_sym   : symmetric }.
+   
+   Record PER : Prop := {
+       per_sym   : symmetric;
+       per_trans : transitive }.
+
+End Sets_of_Relations.
+
+
+
+Section Relations_of_Relations.
+
+  Definition inclusion : relation -> relation -> Prop :=
+      [R1,R2: relation] (x,y:A) (R1 x y) -> (R2 x y).
+
+  Definition same_relation : relation -> relation -> Prop :=
+      [R1,R2: relation] (inclusion R1 R2) /\ (inclusion R2 R1).
+   
+  Definition commut : relation -> relation -> Prop :=
+      [R1,R2:relation] (x,y:A) (R1 y x) -> (z:A) (R2 z y)
+                          -> (EX y':A |(R2 y' x) & (R1 z y')).
+
+End Relations_of_Relations.
+
+   
+End Relation_Definition.
+
+Hints Unfold reflexive transitive antisymmetric symmetric : sets v62.
+
+Hints Resolve Build_preorder Build_order Build_equivalence 
+	Build_PER preord_refl preord_trans 
+	ord_refl ord_trans ord_antisym
+	equiv_refl equiv_trans equiv_sym
+	per_sym per_trans : sets v62.
+
+Hints Unfold inclusion same_relation commut : sets v62.