Stream: Coq users

Topic: Passing names generated by "fresh" to other tactics


view this post on Zulip Justin Kelm (Dec 07 2023 at 02:55):

Let's say I have a tactic for branching a match depending on the value of foo applied to the discriminee:

Ltac destruct_foo :=
  match goal with | |- context[match ?d with _ => _ end] =>
  let F := fresh "F" in destruct (foo d) as [F|F] end.

And let's say that now, in the context of a larger tactic that calls on destruct_foo, I want to use this hypothesis F, say to do rewrite F. In some situations I may be able to do a match goal and contextually find this hypothesis in order to use it, but in other situations hypotheses other than F will also match the syntax. Not to mention this is just inconvenient to write out each time.

Ideally, I would want something like let F := destruct_foo in rewrite F to work as expected. Is there any convenient approximation for what I want?

view this post on Zulip Paolo Giarrusso (Dec 07 2023 at 04:14):

One common approach is Ltac destruct_foo tac := ... let F := fresh in destruct ...; tac F; end. then destruct_foo (fun F => rewrite F).

view this post on Zulip Paolo Giarrusso (Dec 07 2023 at 04:15):

Basically, you pass to destruct_foo a function that takes "destruct_foo's" result.

view this post on Zulip Paolo Giarrusso (Dec 07 2023 at 04:19):

In general, this is called continuation-passing style, if that rings a bell.

view this post on Zulip Justin Kelm (Dec 07 2023 at 05:04):

Yeah, it does ring a bell, and your example is very helpful. Thank you!


Last updated: Jun 22 2024 at 16:02 UTC