diff options
Diffstat (limited to 'theories')
| -rw-r--r-- | theories/Classes/Morphisms.v | 6 | ||||
| -rw-r--r-- | theories/Classes/RelationClasses.v | 12 |
2 files changed, 11 insertions, 7 deletions
diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v index 4765bf0eea..c7e199b62b 100644 --- a/theories/Classes/Morphisms.v +++ b/theories/Classes/Morphisms.v @@ -20,6 +20,8 @@ Require Import Coq.Program.Tactics. Require Import Coq.Relations.Relation_Definitions. Require Export Coq.Classes.RelationClasses. +Open Local Scope relation_scope. + Set Implicit Arguments. Unset Strict Implicit. @@ -445,7 +447,7 @@ Proof. Qed. Lemma inverse_respectful : forall (A : Type) (R : relation A) (B : Type) (R' : relation B), - inverse (R ==> R') <->rel (inverse R ==> inverse R'). + inverse (R ==> R') <R> (inverse R ==> inverse R'). Proof. intros. unfold flip, respectful. @@ -591,5 +593,5 @@ Program Instance {A : Type} => all_inverse_impl_morphism : Qed. Lemma inverse_pointwise_relation A (R : relation A) : - pointwise_relation (inverse R) <->rel inverse (pointwise_relation (A:=A) R). + pointwise_relation (inverse R) <R> inverse (pointwise_relation (A:=A) R). Proof. reflexivity. Qed. diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v index 3d5c6a7ee4..cb32b846d7 100644 --- a/theories/Classes/RelationClasses.v +++ b/theories/Classes/RelationClasses.v @@ -219,24 +219,26 @@ Program Instance [ sa : Equivalence a R, sb : Equivalence b R' ] => equiv_setoid Definition relation_equivalence {A : Type} : relation (relation A) := fun (R R' : relation A) => forall x y, R x y <-> R' x y. -Infix "<->rel" := relation_equivalence (at level 70). +Infix "<R>" := relation_equivalence (at level 70) : relation_scope. Class subrelation {A:Type} (R R' : relation A) := is_subrelation : forall x y, R x y -> R' x y. Implicit Arguments subrelation [[A]]. -Infix "->rel" := subrelation (at level 70). +Infix "-R>" := subrelation (at level 70) : relation_scope. Definition relation_conjunction {A} (R : relation A) (R' : relation A) : relation A := fun x y => R x y /\ R' x y. -Infix "//\\" := relation_conjunction (at level 55). +Infix "/R\" := relation_conjunction (at level 55) : relation_scope. Definition relation_disjunction {A} (R : relation A) (R' : relation A) : relation A := fun x y => R x y \/ R' x y. -Infix "\\//" := relation_disjunction (at level 55). +Infix "\R/" := relation_disjunction (at level 55) : relation_scope. + +Open Local Scope relation_scope. (** Relation equivalence is an equivalence, and subrelation defines a partial order. *) @@ -258,7 +260,7 @@ Program Instance subrelation_preorder : on the carrier. *) Class [ equ : Equivalence A eqA, PreOrder A R ] => PartialOrder := - partial_order_equivalence : relation_equivalence eqA (R //\\ flip R). + partial_order_equivalence : relation_equivalence eqA (R /R\ flip R). (** The equivalence proof is sufficient for proving that [R] must be a morphism |