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.

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

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.

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

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.

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).

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?

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.

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

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)?

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