Setoid rewrite with no init · Coq users

The coq-HoTT homotopy type theory library does not import Coq.Init or anything like that. I don't think they want anything dealing with Prop in the namespace, in particular the standard equality proposition, or the notations in the Init.Notations file.

Can anybody think of a way to make use of the CRelation / CMorphism setoid rewriting machinery without introducing the standard init files? Or how could the Prop-heavy stuff and the notations be hidden by the user so the user cannot accidentally invoke something from these files/?

I am worried that solving this problem would involve substantially rewriting the rewrite.ml file which is a scary thought.

Paolo Giarrusso (Nov 24 2022 at 15:26):

forking coq/theories/Classes/C*.v is probably unavoidable, the problem seems that rewrite.ml hardcodes where those files are installed.

Paolo Giarrusso (Nov 24 2022 at 15:27):

Technically, if you only install coq-core but not coq-stdlib, you can already write your own version of those files, and that might be enough for today...

Paolo Giarrusso (Nov 24 2022 at 15:28):

"enough" needs scare quotes: nobody who installs the stdlib will be able to use your code :-|

Paolo Giarrusso (Nov 24 2022 at 15:31):

What rewrite.ml should do is let the library register needed definitions with Coq via the Register command, so I filed https://github.com/coq/coq/issues/16901.

Paolo Giarrusso (Nov 24 2022 at 15:33):

For instance, both the stdlib and the hott libraries can tell Coq what library symbol to use as equality:

Register eq as core.identity.type.

Ali Caglayan (Nov 24 2022 at 15:34):

Not the case unfortuantely due to how "coqlib" is detected internally. Even coqc --config fails without the stdlib being at least present. There is nothing stopping us from cleaning this up, its just lack of dev time.

Paolo Giarrusso (Nov 24 2022 at 15:35):

not surprised, but that's a hack anyway, and switching to Register seems more important?

Ali Caglayan (Nov 24 2022 at 15:35):

Yeah, having the right Register's implemented is just a matter of doing it, I don't think there are any technical limitations.

Ali Caglayan (Nov 24 2022 at 15:36):

@Patrick Nicodemus What you can do is use the stdlib setoid rewrite in the HoTT library. Sure it will be annoying to have Coq.* back in the namespace but it can be cleaned up in time.

Ali Caglayan (Nov 24 2022 at 15:37):

I would suggest you get setoid rewriting working using the stdlib without sinking time into how things need to be setup as that can be cleaned up later.

Ali Caglayan (Nov 24 2022 at 18:09):

Ali Caglayan (Nov 24 2022 at 18:10):

I hope one day this entire part of the code will be cleaned up and pleasent to work on. Today that is not the case.

Stream: Coq users

Topic: Setoid rewrite with no init

Patrick Nicodemus (Nov 24 2022 at 08:02):