From 0b6924f05ef6beb775345f3fb2ad21a009ab3baa Mon Sep 17 00:00:00 2001 From: msozeau Date: Sat, 29 Mar 2008 11:20:45 +0000 Subject: Fix test-suite files, change conflicting notation "->rel" and the others to "-R>" and the like. Split more precisely in inference of case predicate between the new code which currently works only for matched variables and the old one which works better on variables appearing in matched terms types (the two could also be merged). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10729 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/Classes/Morphisms.v | 6 ++++-- theories/Classes/RelationClasses.v | 12 +++++++----- 2 files changed, 11 insertions(+), 7 deletions(-) (limited to 'theories') 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') (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) 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 "" := 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 -- cgit v1.2.3