diff options
Diffstat (limited to 'theories/Classes/RelationClasses.v')
| -rw-r--r-- | theories/Classes/RelationClasses.v | 10 |
1 files changed, 10 insertions, 0 deletions
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) := |