Stream: Coq users

Topic: ✔ Autosubst (2)


view this post on Zulip Ana de Almeida Borges (Oct 25 2022 at 17:48):

Yannick Forster said:

Depending on your use case, Autosubst 2 might be better to use than Autosubst 1. We are using it in the Coq Library of Undecidability to formalise first-order logic, second-order logic, STLC, and System F

Does this mean that, eg, the FOL syntax file is somehow auto-generated? Or where/how are you using Autosubst 2 in the Library of Undecidability?

view this post on Zulip Karl Palmskog (Oct 25 2022 at 18:12):

Autosubst 2 is written in Haskell and generates Coq code in the end that needs to be bundled, but I guess one can autogenerate it every time in CI... (so I don't know if that particular file is autogenerated)

view this post on Zulip Paolo Giarrusso (Oct 25 2022 at 23:53):

https://github.com/uds-psl/coq-library-undecidability/blob/6207468f34c21c1c07b391f02bd51e33a7553f86/theories/SystemF/Autosubst/syntax.v is much closer to the autogen output I've seen from Autosubst 2. https://github.com/uds-psl/coq-library-undecidability/search?q=autosubst finds more examples

view this post on Zulip Paolo Giarrusso (Oct 25 2022 at 23:55):

The code in Ana's link looks hand-written, but the maths and notations are in autosubst's style

view this post on Zulip Dominik Kirst (Oct 26 2022 at 07:29):

Paolo Giarrusso said:

The code in Ana's link looks hand-written, but the maths and notations are in autosubst's style

Exactly, the FOL syntax is Autosubst inspired and the System F syntax is really Autosubst generated. Another example of Autosubst generated code in the undecidability library is the syntax used for higher order unification.

view this post on Zulip Ana de Almeida Borges (Oct 26 2022 at 12:42):

Cool, thanks everyone

view this post on Zulip Notification Bot (Oct 26 2022 at 12:42):

Ana de Almeida Borges has marked this topic as resolved.


Last updated: Jan 28 2023 at 06:30 UTC