Stream: Coq users

Topic: Ltac newbie question about using destruct in the tactics

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?

Paolo Giarrusso (Jan 07 2021 at 18:42):

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

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.

Paolo Giarrusso (Jan 07 2021 at 18:47):

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

Paolo Giarrusso (Jan 07 2021 at 18:48):

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

k32 (Jan 07 2021 at 18:49):

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

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: Sep 23 2023 at 08:01 UTC