Stream: Coq users

Topic: Setoid rewrite with no init


view this post on Zulip Patrick Nicodemus (Nov 24 2022 at 08:02):

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 Prop, 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?

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

view this post on Zulip 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.

view this post on Zulip 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...

view this post on Zulip Paolo Giarrusso (Nov 24 2022 at 15:28):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Ali Caglayan (Nov 24 2022 at 15:34):

Paolo Giarrusso said:

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

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.

view this post on Zulip Paolo Giarrusso (Nov 24 2022 at 15:35):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Ali Caglayan (Nov 24 2022 at 18:09):

I dived in and now am turning everything into a register

view this post on Zulip 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.

view this post on Zulip Patrick Nicodemus (Nov 24 2022 at 18:56):

Ali Caglayan said:

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.

Ok. I'm fine with that if other library maintainers are


Last updated: Jan 27 2023 at 00:03 UTC