diff options
Diffstat (limited to 'theories/Relations/Relation_Definitions.v')
| -rw-r--r-- | theories/Relations/Relation_Definitions.v | 89 |
1 files changed, 44 insertions, 45 deletions
diff --git a/theories/Relations/Relation_Definitions.v b/theories/Relations/Relation_Definitions.v index 22ba7413..762da1ff 100644 --- a/theories/Relations/Relation_Definitions.v +++ b/theories/Relations/Relation_Definitions.v @@ -6,67 +6,66 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Relation_Definitions.v 8642 2006-03-17 10:09:02Z notin $ i*) +(*i $Id: Relation_Definitions.v 9245 2006-10-17 12:53:34Z notin $ i*) Section Relation_Definition. - Variable A : Type. - - Definition relation := A -> A -> Prop. + Variable A : Type. + + Definition relation := A -> A -> Prop. - Variable R : relation. + 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 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. -Section Sets_of_Relations. + End General_Properties_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 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. + 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'. - Definition inclusion (R1 R2:relation) : Prop := - forall x y:A, R1 x y -> R2 x y. + End Relations_of_Relations. - 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. @@ -75,4 +74,4 @@ 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 +Hint Unfold inclusion same_relation commut: sets v62. |