Inconsistent `RewriteRelation` instances
We currently have just the following instance (add by @jjourdan):
Instance sqsubseteq_rewrite `{SqSubsetEq A} : RewriteRelation (⊑).
No such instances exist for other binary relations.
In order to make the Ssrreflect rewrite
tactic to work for ⊑
, we need such an instance. It turns out that for equiv
we do not need it, since the Coq standard library contains the following instance:
equivalence_rewrite_relation:
∀ (A : Type) (eqA : relation A), Equivalence eqA → RewriteRelation eqA
Now there are some solutions:
- Add
RewriteRelation
instances for all operational type classes for binary operations, e.g.subseteq
. - Add a
RewriteRelation
instance for anyPreOrder
. - The latter, but by making an pull request for the Coq standard library.