Stream: Coq users

Topic: Ltac on shelved goals


view this post on Zulip adrianleh (Apr 21 2023 at 16:48):

Hi, is there a way to match on shelved goals using Ltac?

view this post on Zulip Paolo Giarrusso (Apr 21 2023 at 18:07):

You have the Unshelve command (to unshelve everything), the unshelve tactical (to use when creating shelved goals to unshelve them), shelve and shelve_unifiable to undo unshelve.

view this post on Zulip Paolo Giarrusso (Apr 21 2023 at 18:08):

And often shelved goals are really evars that can be recognized by using is_evar on the goal.

view this post on Zulip Paolo Giarrusso (Apr 21 2023 at 18:08):

TLDR: not AFAIK but there's lots that might help for many use cases

view this post on Zulip Adrian (Apr 21 2023 at 18:15):

Sorry, I think I wasn't specific enough about my issue. I have an Ltac that should do an autorewrite with some_db where the lemmas in some_db create a bunch of shelved goals then I'd like to run an Ltac on these shelved goals.

So intuitively what I though of doing

Ltac bar := ...
Ltac foo := autorewrite with some_db; Unshelve; try bar.

However Unshelve is not available within Ltac and using unshelve (try bar) also does not work

view this post on Zulip Kenji Maillard (Apr 21 2023 at 18:18):

you probably want to do unshelve (autorewrite with some_db); try bar.

view this post on Zulip Adrian (Apr 21 2023 at 18:30):

Thanks! I misunderstood what unshelve does!

view this post on Zulip Adrian (Apr 21 2023 at 18:41):

As a follow up: If I generalize my tactic to

Ltac foo tac :=  unshelve (ltac:(tac)); try bar; shelve_unifiable.

Doesn't work when using
foo (autorewrite with some_db) because it seems to not bracket properly (this also happens when I don't wrap tac as an ltac)

view this post on Zulip Rodolphe Lepigre (Apr 21 2023 at 19:03):

Maybe the following would help?

Tactic Notation "foo" tactic3(tac) :=
  unshelve tac; try bar; shelve_unifiable.

I never remember where arguments are thunked or not in Ltac.

view this post on Zulip Adrian (Apr 21 2023 at 19:29):

Thank you @Rodolphe Lepigre ! This works as intended


Last updated: Jun 20 2024 at 13:02 UTC