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.

added 1 commit

• bbdbb1c1 - Improve the doc for the `RewriteRelation equiv` instance.

Compare with previous version

removed S-waiting-for-author label

added S-waiting-for-review label

assigned to @robbertkrebbers

Thanks for the update. Let me summarize to see if I understand correctly. We need RewriteRelation instances for two reasons:

• If we want to rewrite with a relation with ssr's rewrite tactic
• To infer intermediate relations when rewriting below multiple function symbols/morphisms as you outlined in !273 (comment 77031)

I think the current code makes sense. I left a small comment.

I expect this MR to be backwards compatible, so we can merge it before Coq's MR (that avoids the need for overlays).

removed S-waiting-for-review label

added 1 commit

• c355607c - Wrap the comment

Compare with previous version

resolved all threads

Thanks, the corresponding PR should go through entirely once this is merged. Then you can start putting ! ! modes on Reflexive... etc (we did in MetaCoq for example and it worked well). Coq's stdlib is not yet up-to the task, but that's the next step for me.

Well, we can do that once we depend on a version of Coq that contains the PR (https://github.com/coq/coq/pull/13969, I assume). Which will take at least a year.

But we are used to these turn/around times so that's okay, I just added it to the list at https://gitlab.mpi-sws.org/iris/iris/-/wikis/coq-bugs. :)

enabled an automatic merge when the pipeline for c355607c succeeds

Ok, great, going to merge then. Thanks!

merged

mentioned in commit 2af35753

@robbertkrebbers how does it work for iris to update its ref on stdpp? It apparently forces a specific commit.

It requires updating the opam file in Iris. I have just done that, see iris@8b085901

If you need that again, you can either open an MR, or ask one of the Iris devs to update the file directly

Thanks!

Ah, in turn Coq's CI gets the iris version from the examples repo, can you bump it there as well?

Done, see examples@f9b9e929.