From 6b649aba925b6f7462da07599fe67ebb12a3460e Mon Sep 17 00:00:00 2001
From: Samuel Mimram <samuel.mimram@ens-lyon.org>
Date: Wed, 28 Jul 2004 21:54:47 +0000
Subject: Imported Upstream version 8.0pl1

---
 theories/Relations/Relation_Definitions.v | 78 +++++++++++++++++++++++++++++++
 1 file changed, 78 insertions(+)
 create mode 100755 theories/Relations/Relation_Definitions.v

(limited to 'theories/Relations/Relation_Definitions.v')

diff --git a/theories/Relations/Relation_Definitions.v b/theories/Relations/Relation_Definitions.v
new file mode 100755
index 00000000..e115b0b0
--- /dev/null
+++ b/theories/Relations/Relation_Definitions.v
@@ -0,0 +1,78 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(*i $Id: Relation_Definitions.v,v 1.6.2.1 2004/07/16 19:31:16 herbelin Exp $ i*)
+
+Section Relation_Definition.
+
+   Variable A : Type.
+   
+   Definition relation := A -> A -> Prop.
+
+   Variable R : relation.
+   
+
+Section General_Properties_of_Relations.
+
+  Definition reflexive : Prop := forall x:A, R x x.
+  Definition transitive : Prop := forall x y z:A, R x y -> R y z -> R x z.
+  Definition symmetric : Prop := forall x y:A, R x y -> R y x.
+  Definition antisymmetric : Prop := forall 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 (R1 R2:relation) : Prop :=
+    forall x y:A, R1 x y -> R2 x y.
+
+  Definition same_relation (R1 R2:relation) : Prop :=
+    inclusion R1 R2 /\ inclusion R2 R1.
+   
+  Definition commut (R1 R2:relation) : Prop :=
+    forall x y:A,
+      R1 y x -> forall z:A, R2 z y ->  exists2 y' : A, R2 y' x & R1 z y'.
+
+End Relations_of_Relations.
+
+   
+End Relation_Definition.
+
+Hint Unfold reflexive transitive antisymmetric symmetric: sets v62.
+
+Hint 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.
+
+Hint Unfold inclusion same_relation commut: sets v62.
\ No newline at end of file
-- 
cgit v1.2.3