Declare `equiv` as a rightful rewrite relation, when an `Equiv` instance is available.

This makes Iris & Perennial compatible with Coq PR #13969. Should be entirely backwards compatible.

Equiv is a Coq typeclass... so rewriting with that will not work any more for ssreflect users unless they also add a line like this?

resolved all threads

added 1 commit

• b144619d - Apply 1 suggestion(s) to 1 file(s)

Compare with previous version

It's an stdpp typeclass, not a Coq one unless I'm reading it wrong

The ssreflect issue is solved entirely: if the relation is ?R then we'll find iff, or eq depending on the type (but again that does not really matter, this query is ignored), if it's defined then we will look up if there is an Equivalence R just like before the PR.

Ah, you are right of course... I keep mixing up which typeclasses come from where.

In that case I am in fact quite surprised that rewriting with equiv works without the RewriteRelation instance.

I agree, that's confusing.

@jung:

In that case I am in fact quite surprised that rewriting with equiv works without the RewriteRelation instance.

By default, prior to @mattam82's PR, it would look for Equivalence, and for any reasonable equiv there's a corresponding Equivalence instance. In https://github.com/coq/coq/pull/13969 @mattam82 wrote:

In the last version I just pushed, RewriteRelation has no mode but won't fire Equivalence ?R constraints anymore, so Equivalence can also have mode ! ! without disrupting anything.

See also #10

I suppose the proper fix to that issue is:

Add RewriteRelation instances for all operational type classes for binary operations, e.g. subseteq.

@mattam82 There are some pending discussions. Let me know if this MR is blocked on action by me. If not, no rush :)

added S-waiting-for-author label

changed the description

@mattam82 Any update on this (and the Coq PR in question)?

From the std++/Iris side, we are very much interested in improving the setoid mechanism in Coq (and thus helping to get the PR through), but we also would like to understand what's happening in this mechanism. If it helps, we would also be available for a brief call to discuss some of the open issues in this MR and the Coq PR.

Status update: Blocked on @mattam82 getting back to their Coq PR.

added 1 commit

• 3671f349 - Apply 2 suggestion(s) to 1 file(s)

Compare with previous version

I'm on the PR again now, and the CI is blocked on this (backwards compatible) MR. We can have a call to settle the remaining questions if you like.