Stream: Coq users

Topic: Unable to compile a copy of Morphisms.v from std. library


view this post on Zulip Cosmo Viola (Jan 08 2024 at 14:00):

Hello, I'm trying to do work using the setoid automation in the standard library where the theorems I want to prove are proof-relevant. To deal with this, I'm trying to change the definitions of the proofs in Morphisms.v to end in Defined rather than Qed, so that I can reason about the proofs that the automation produces. However, I've not been able to compile even the unaltered Morphisms.v file myself. When I try to compile Morphisms.v by calling coqc Morphisms.v from the command line in my project directory, coqc returns
File "./Morphisms.v", line 405, characters 4-17: Error: Tactic failure: Setoid library not loaded.
If I try to add an import for Coq.Setoids.Setoid to the file, I instead get the warnings and error

File "./Morphisms.v", line 96, characters 2-131:
Warning: Notation "_ ++> _" was already used in scope signature_scope.
[notation-overridden,parsing]
File "./Morphisms.v", line 99, characters 2-131:
Warning: Notation "_ ==> _" was already used in scope signature_scope.
[notation-overridden,parsing]
File "./Morphisms.v", line 102, characters 2-138:
Warning: Notation "_ --> _" was already used in scope signature_scope.
[notation-overridden,parsing]
File "./Morphisms.v", line 110, characters 0-23:
Warning: Notation "_ ++> _" was already used in scope signature_scope.
[notation-overridden,parsing]
File "./Morphisms.v", line 110, characters 0-23:
Warning: Notation "_ ==> _" was already used in scope signature_scope.
[notation-overridden,parsing]
File "./Morphisms.v", line 110, characters 0-23:
Warning: Notation "_ --> _" was already used in scope signature_scope.
[notation-overridden,parsing]
File "./Morphisms.v", line 558, characters 4-13:
Error:
Tactic failure: setoid rewrite failed: Unable to satisfy the following constraints:
UNDEFINED EVARS:
 ?X34==[A R0 R1 H m H0 |- relation A] (internal placeholder) {?r}
 ?X35==[A R0 R1 H m H0 (do_subrelation:=Classes.Morphisms.do_subrelation)
         |- Classes.Morphisms.Proper
              (relation_equivalence ==>
               ?X34@{__:=A; __:=R0; __:=R1; __:=H; __:=m; __:=H0} ==>
               flip impl) Proper] (internal placeholder) {?p}
 ?X36==[A R0 R1 H m H0
         |- Classes.Morphisms.ProperProxy
              ?X34@{__:=A; __:=R0; __:=R1; __:=H; __:=m; __:=H0} m]
         (internal placeholder) {?p0}
.

Presumably the warnings are because Setoid exports those notations. I am able to compile a copy of Setoid.v in my project directory, so the issue is specific to the file. How do I properly compile this file so I can make my edits? I'm using Coq v8.9.1.

view this post on Zulip Gaëtan Gilbert (Jan 08 2024 at 14:03):

you can try just Require Setoid (without Import)
but I'm not sure the definitions from your file would be used over the ones from stdlib

view this post on Zulip Cosmo Viola (Jan 08 2024 at 20:48):

Gaëtan Gilbert said:

you can try just Require Setoid (without Import)
but I'm not sure the definitions from your file would be used over the ones from stdlib

Doing this does remove the warnings, but the error message still remains. My intention is to not import the stdlib version of Morphisms.v and instead import my modified version, so presumably the definitions from my file would be the only ones available in my development.

view this post on Zulip Paolo Giarrusso (Jan 08 2024 at 22:50):

But the rewrite tactic knows which version of setoid to use thanks to Register commands.

view this post on Zulip Paolo Giarrusso (Jan 08 2024 at 22:51):

The warnings are a distraction; the error shows that rewrite is searching for an instance of Classes.Morphisms.Proper, and the qualification suggests this is the version from the stdlib not from your library.

view this post on Zulip Paolo Giarrusso (Jan 09 2024 at 00:37):

Sorry: I assumed Register was used, but in fact the classes to use are hardcoded (https://github.com/coq/coq/issues/16901). If Coq switched to Register, it'd be easier to plug in your own version.

Of course, you'd need to use a newer Coq, not 8.9.1 (tho the issue appears current).

view this post on Zulip Cosmo Viola (Jan 09 2024 at 09:48):

Paolo Giarrusso said:

Sorry: I assumed Register was used, but in fact the classes to use are hardcoded (https://github.com/coq/coq/issues/16901). If Coq switched to Register, it'd be easier to plug in your own version.

Of course, you'd need to use a newer Coq, not 8.9.1 (tho the issue appears current).

Given that the issue is still open, then, is my only reasonable option to make the proofs in Morphisms.v transparent to fork the standard library, like you had suggested in the thread linked in that issue?

view this post on Zulip Paolo Giarrusso (Jan 09 2024 at 11:37):

Another option might be to edit Morphisms.v: you want to redo the proofs, but you're also redeclaring classes in there, and you don't need to. However, you might need to remove the original instances with Remove Hints.

view this post on Zulip Paolo Giarrusso (Jan 09 2024 at 11:39):

And Remove Hints doesn't work on Hint Extern, so this might be a blocker.

view this post on Zulip Cosmo Viola (Jan 10 2024 at 10:42):

Paolo Giarrusso said:

Another option might be to edit Morphisms.v: you want to redo the proofs, but you're also redeclaring classes in there, and you don't need to. However, you might need to remove the original instances with Remove Hints.

I'm not sure I quite understand what you're suggesting here, probably because I'm not deeply familiar with how this automation works. If I edit my copy of Morphisms.v, but the rewriting is hardcoded to use the version in the standard library, wouldn't the setoid automation still use the proofs from the copy of Morphisms.v in the standard library? Or is it that the automation only sees the proofs in Morphisms.v via the Hint statements, so the hints could be removed and replaced (but most of them are Extern, as you mentioned)?

view this post on Zulip Paolo Giarrusso (Jan 10 2024 at 15:24):

Right, my understanding is that the class names is hardcoded, but the hints to use aren't


Last updated: Jun 13 2024 at 21:01 UTC