Stream: Coq users

Topic: Get Hints out of Section


view this post on Zulip Thibaut Pérami (Sep 11 2023 at 15:25):

I have a long section (800LoC), that creates a new type and proves lots of lemmas about it, and put some of them into specific hint databases (both normal and rewrite). The proof of later lemmas in the section use both databases in their proof scripts. Then I close the section and the databases disappear. Is there a way to export that database outside the section so that user of the type can use the associated databases, or do I need to copy all the hint commands outside the section?

view this post on Zulip Paolo Giarrusso (Sep 11 2023 at 16:27):

sadly for now you need to copy the hints — or split the section. You want #[export] Hint Resolve/#[global] Hint Resolve, but this is still pending last I checked

view this post on Zulip Paolo Giarrusso (Sep 11 2023 at 16:29):

where "split the section" means

End your_section.
#[export] Hint Resolve ....
Section your_section.
(* abstract again over everything — hoping all assumptions can be auto-inferred when applying hints, but otherwise you'd have bigger problems *)
...

view this post on Zulip Paolo Giarrusso (Sep 11 2023 at 16:29):

and yeah, I agree this isn't great when you use hints to prove more hints :-|

view this post on Zulip Meven Lennon-Bertrand (Sep 11 2023 at 16:29):

To be sure, the difficulty is that hints can contain arbitrary tactic code, and that the section-closing mechanism cannot handle tactics, right?

view this post on Zulip Paolo Giarrusso (Sep 11 2023 at 16:30):

Hint Resolve can't use tactics

view this post on Zulip Paolo Giarrusso (Sep 11 2023 at 16:31):

and each Hint command gives semantics to attributes separately — you're talking of Hint Extern, which is orthogonal to Hint Resolve.

view this post on Zulip Gaëtan Gilbert (Sep 11 2023 at 16:31):

no, the difficulty is that nobody has written the section closing for Hint Resolve
also not clear we want to do it when the hint is an arbitrary term

view this post on Zulip Paolo Giarrusso (Sep 11 2023 at 16:32):

even having it just for constants would be very nice, especially since using arbitrary terms is somewhat discouraged already (I forget how officially beyond "PMP wants to drop that")

view this post on Zulip Paolo Giarrusso (Sep 11 2023 at 16:32):

existing issue https://github.com/coq/coq/issues/16048

view this post on Zulip Gaëtan Gilbert (Sep 11 2023 at 16:36):

ping @Pierre-Marie Pédrot


Last updated: Jun 13 2024 at 19:02 UTC