diff options
| author | msozeau | 2009-02-04 17:38:19 +0000 |
|---|---|---|
| committer | msozeau | 2009-02-04 17:38:19 +0000 |
| commit | d1f92d3bc420d0a5115a4533ca59b17f6b823515 (patch) | |
| tree | cdd790d47f3c3348320f23fd9b20fedb2cc05be4 | |
| parent | 14e4261beb81ba792dc1e42ddf52f24c04596150 (diff) | |
Fix [subrelation] clauses that privileged the weakest. Better impl args
for [PartialOrder] typeclass.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11882 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | theories/Classes/Morphisms.v | 6 | ||||
| -rw-r--r-- | theories/Classes/RelationClasses.v | 5 |
2 files changed, 6 insertions, 5 deletions
diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v index 111d85f742..fa3684b74b 100644 --- a/theories/Classes/Morphisms.v +++ b/theories/Classes/Morphisms.v @@ -118,7 +118,7 @@ Proof. simpl_relation. apply subr. apply H. apply subl. apply H0. Qed. (** And of course it is reflexive. *) -Instance morphisms_subrelation_refl : ! subrelation A R R | 10. +Instance morphisms_subrelation_refl : ! subrelation A R R. Proof. simpl_relation. Qed. (** [Morphism] is itself a covariant morphism for [subrelation]. *) @@ -151,10 +151,10 @@ Hint Extern 5 (@Morphism _ _ _) => subrelation_tac : typeclass_instances. (** Essential subrelation instances for [iff], [impl] and [pointwise_relation]. *) -Instance iff_impl_subrelation : subrelation iff impl. +Instance iff_impl_subrelation : subrelation iff impl | 2. Proof. firstorder. Qed. -Instance iff_inverse_impl_subrelation : subrelation iff (inverse impl). +Instance iff_inverse_impl_subrelation : subrelation iff (inverse impl) | 2. Proof. firstorder. Qed. Instance pointwise_subrelation {A} `(sub : subrelation B R R') : diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v index 659289f889..b058f67baa 100644 --- a/theories/Classes/RelationClasses.v +++ b/theories/Classes/RelationClasses.v @@ -368,7 +368,7 @@ Proof. intro A. exact (@predicate_implication_preorder (cons A (cons A nil))). Q We give an equivalent definition, up-to an equivalence relation on the carrier. *) -Class PartialOrder A eqA `{equ : Equivalence A eqA} R `{preo : PreOrder A R} := +Class PartialOrder {A} eqA `{equ : Equivalence A eqA} R `{preo : PreOrder A R} := partial_order_equivalence : relation_equivalence eqA (relation_conjunction R (inverse R)). (** The equivalence proof is sufficient for proving that [R] must be a morphism @@ -377,7 +377,8 @@ Class PartialOrder A eqA `{equ : Equivalence A eqA} R `{preo : PreOrder A R} := Instance partial_order_antisym `(PartialOrder A eqA R) : ! Antisymmetric A eqA R. Proof with auto. - reduce_goal. pose proof partial_order_equivalence as poe. do 3 red in poe. + reduce_goal. + pose proof partial_order_equivalence as poe. do 3 red in poe. apply <- poe. firstorder. Qed. |