From 73798a12d39b03e1823b93c1364a86d14e2eec0a Mon Sep 17 00:00:00 2001 From: msozeau Date: Tue, 29 Apr 2008 12:30:25 +0000 Subject: Fix eauto still using delta when it shouldn't (should make CoRN compile in reasonable time), add (unfinished) documentation on type classes. Put some classes into Prop explicitely as singleton inductive types are no longer in Prop by default even if all the arguments are (is that really what we want? roconnor says no). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10868 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/Classes/RelationClasses.v | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) (limited to 'theories/Classes') diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v index a57914fdd..015eb7323 100644 --- a/theories/Classes/RelationClasses.v +++ b/theories/Classes/RelationClasses.v @@ -42,7 +42,7 @@ Class Reflexive A (R : relation A) := reflexivity : forall x, R x x. Class Irreflexive A (R : relation A) := - irreflexivity : forall x, R x x -> False. + irreflexivity :> Reflexive A (complement R). Class Symmetric A (R : relation A) := symmetry : forall x y, R x y -> R y x. @@ -86,15 +86,15 @@ Program Instance [ Transitive A R ] => flip_Transitive : Transitive (flip R). Program Instance [ Reflexive A (R : relation A) ] => Reflexive_complement_Irreflexive : Irreflexive (complement R). -Program Instance [ Irreflexive A (R : relation A) ] => - Irreflexive_complement_Reflexive : Reflexive (complement R). - Next Obligation. Proof. + unfold complement. red. intros H. - apply (irreflexivity H). + intros H' ; apply H'. + apply (reflexivity H). Qed. + Program Instance [ Symmetric A (R : relation A) ] => complement_Symmetric : Symmetric (complement R). Next Obligation. @@ -152,13 +152,13 @@ Program Instance eq_Transitive : Transitive (@eq A). (** A [PreOrder] is both Reflexive and Transitive. *) -Class PreOrder A (R : relation A) := +Class PreOrder A (R : relation A) : Prop := PreOrder_Reflexive :> Reflexive R ; PreOrder_Transitive :> Transitive R. (** A partial equivalence relation is Symmetric and Transitive. *) -Class PER (carrier : Type) (pequiv : relation carrier) := +Class PER (carrier : Type) (pequiv : relation carrier) : Prop := PER_Symmetric :> Symmetric pequiv ; PER_Transitive :> Transitive pequiv. @@ -178,7 +178,7 @@ Program Instance [ PER A (R : relation A), PER B (R' : relation B) ] => (** The [Equivalence] typeclass. *) -Class Equivalence (carrier : Type) (equiv : relation carrier) := +Class Equivalence (carrier : Type) (equiv : relation carrier) : Prop := Equivalence_Reflexive :> Reflexive equiv ; Equivalence_Symmetric :> Symmetric equiv ; Equivalence_Transitive :> Transitive equiv. -- cgit v1.2.3