Stream: Coq users

Topic: Ltac newbie question about using destruct in the tactics


view this post on Zulip k32 (Jan 07 2021 at 18:40):

Hi! Ltac newbie question: sometimes I find myself writing ugly tactics like this:

Ltac foo x :=
  let a := fresh in
  let b := fresh in
  ...
  destruct x as [a b c d e f...];
  ...

Is there a nicer way to introduce temporary variables other than calling fresh multiple times followed by destruct or inversion tactic or something like refine (match x with ...) ? What is the best practice for writing tactics that perform matching on terms with complex constructors?

view this post on Zulip Paolo Giarrusso (Jan 07 2021 at 18:42):

Depends. Which is the reason you're not using "destruct x" or "destruct x as [?????]" or...?

view this post on Zulip k32 (Jan 07 2021 at 18:46):

I want to control names of the variables introduced by destruct, and perhaps do something meaningful to them later in the tactic.

view this post on Zulip Paolo Giarrusso (Jan 07 2021 at 18:47):

So I’d use ? except for the names you actually need later?

view this post on Zulip Paolo Giarrusso (Jan 07 2021 at 18:48):

For the rest, “control” = call fresh by hand, instead of via ?, what else could exist?

view this post on Zulip k32 (Jan 07 2021 at 18:49):

I see, thanks. I thought maybe there was some shortcut for introducing fresh variables in-place.

view this post on Zulip Li-yao (Jan 07 2021 at 19:17):

If it's a product (one constructor) one approach is to apply projections instead of destructing x, but you have to be careful to do it everywhere.


Last updated: Feb 04 2023 at 22:29 UTC