diff options
Diffstat (limited to 'theories/Classes')
| -rw-r--r-- | theories/Classes/Equivalence.v | 8 | ||||
| -rw-r--r-- | theories/Classes/RelationClasses.v | 10 |
2 files changed, 10 insertions, 8 deletions
diff --git a/theories/Classes/Equivalence.v b/theories/Classes/Equivalence.v index 03b0e9ad5..197786c8b 100644 --- a/theories/Classes/Equivalence.v +++ b/theories/Classes/Equivalence.v @@ -55,11 +55,6 @@ Program Instance equiv_reflexive [ sa : Equivalence A ] : Reflexive equiv. Program Instance equiv_symmetric [ sa : Equivalence A ] : Symmetric equiv. - Next Obligation. - Proof. - symmetry ; auto. - Qed. - Program Instance equiv_transitive [ sa : Equivalence A ] : Transitive equiv. Next Obligation. @@ -133,10 +128,7 @@ End Respecting. Program Instance pointwise_equivalence [ eqb : Equivalence B eqB ] : Equivalence (A -> B) (pointwise_relation eqB) | 9. - Solve Obligations using simpl_relation ; first [ reflexivity | (symmetry ; auto) ]. - Next Obligation. Proof. transitivity (y a) ; auto. Qed. - diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v index cfcd93c0a..c1d7f34ce 100644 --- a/theories/Classes/RelationClasses.v +++ b/theories/Classes/RelationClasses.v @@ -59,6 +59,16 @@ Hint Resolve @irreflexivity : ord. Unset Implicit Arguments. +(** A HintDb for relations. *) + +Ltac solve_relation := + match goal with + | [ |- ?R ?x ?x ] => reflexivity + | [ H : ?R ?x ?y |- ?R ?y ?x ] => symmetry ; exact H + end. + +Hint Extern 4 => solve_relation : relations. + (** We can already dualize all these properties. *) Program Instance flip_Reflexive [ Reflexive A R ] : Reflexive (flip R) := |