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
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?
Depends. Which is the reason you're not using "destruct x" or "destruct x as [?????]" or...?
I want to control names of the variables introduced by destruct, and perhaps do something meaningful to them later in the tactic.
So I’d use ? except for the names you actually need later?
For the rest, “control” = call fresh by hand, instead of via ?, what else could exist?
I see, thanks. I thought maybe there was some shortcut for introducing fresh variables in-place.
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