Stream: Coq users

Topic: Ltac on shelved goals

adrianleh (Apr 21 2023 at 16:48):

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

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.

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.

Paolo Giarrusso (Apr 21 2023 at 18:08):

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

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

Kenji Maillard (Apr 21 2023 at 18:18):

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

Adrian (Apr 21 2023 at 18:30):

Thanks! I misunderstood what unshelve does!

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)

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.

Adrian (Apr 21 2023 at 19:29):

Thank you @Rodolphe Lepigre ! This works as intended

Last updated: Oct 13 2024 at 01:02 UTC