Stream: Coq users

Topic: Determining section variables used


view this post on Zulip Alex Sanchez-Stern (Jun 13 2023 at 19:40):

Is there a canonical way to find out what section variables were used by a proof? Best I can think of is by getting the type of the lemma before closing the section, then closing the section, then comparing to find which new binders exist after closing the section, and comparing those to the types of all section variables declared in the section. This seems kind of hacky and relies on a bunch of syntax heuristics though, is there a better way?

view this post on Zulip Emilio Jesús Gallego Arias (Jun 13 2023 at 19:42):

Yes, there is a better way but it is ML-only for the API. We can expose such API in SerAPI / coq-lsp tho, please open a ticket

view this post on Zulip Emilio Jesús Gallego Arias (Jun 13 2023 at 19:42):

The way is what the section closing mechanism does

view this post on Zulip Alex Sanchez-Stern (Jun 13 2023 at 19:48):

Created issues in the coq-lsp and coq-serapi repos. But, proof general seems to be able to do this (the coq-insert-suggested-dependencycommand), it doesn't use the ML api does it?

view this post on Zulip Emilio Jesús Gallego Arias (Jun 13 2023 at 19:51):

Oh, it may use the Suggest Proof Using command

view this post on Zulip Emilio Jesús Gallego Arias (Jun 13 2023 at 19:52):

So that command could also work for you, but I'm unsure how structured it is. Basically what I was proposing is implementing that command

view this post on Zulip Emilio Jesús Gallego Arias (Jun 13 2023 at 19:52):

in serapi / coq-lsp

view this post on Zulip Emilio Jesús Gallego Arias (Jun 13 2023 at 19:52):

as the functionality is there

view this post on Zulip Emilio Jesús Gallego Arias (Jun 13 2023 at 19:52):

See https://coq.inria.fr/refman/proofs/writing-proofs/proof-mode.html?highlight=suggest%20proof%20using#proof-using-options

view this post on Zulip Gaëtan Gilbert (Jun 13 2023 at 20:21):

you can do About my_lemma and it will say my_lemma uses section variables foo bar baz
since 8.17 https://github.com/coq/coq/pull/16208

view this post on Zulip Alex Sanchez-Stern (Jun 13 2023 at 20:58):

Went through the PG source a bit, it does indeed use Suggest Proof Using (it was easier to find once I knew what I was looking for. I would use the About command, but I work with older versions of Coq. I'll try Proof Using for now, and when the functionality gets added to coq-lsp or serapi I can use that too. Thanks!


Last updated: Jun 13 2024 at 19:02 UTC