Sometimes when I use `intros`

with a destructuring pattern I would like to name and keep some intermediate term as a transparent definition, e.g.

```
Goal forall {A B C}, A * B * C -> True.
Proof.
(* what I can currently do *)
intros ??? [[a b] c]. pose (x := (a,b)).
(* what I would like to do: no explicit naming of the destructured components required, nor rebuilding the possibly large term *)
intros ??? [([??] as x) ?].
```

Is there a way to hack some tactic notation to get this kind of behaviour ?

Ok, one way to get that behaviour is to just bind a variable and use pose + destruct:

```
intros ??? [x c].
let x' := fresh "x" in rename x into x'; pose (x := x'); destruct x' as [??].
(* Is it possible to write a tactic notation to have `split z as pat.` expand to the tactic above for z:= x and pat := [??] ?*)
```

Don't know about Ltac, in ssreflect there is `/[dup]`

that may help

I thought about `/[dup]`

but that loses the definition of pattern. Though there is probably some way to add another notation in `ssr_ipat`

to do what I have in mind..

Have you tried combining it with `+`

(and maybe multiple `=>`

, just wild guess, I haven't tried).

(nevermind, I see what you want now, sorry no idea)

Last updated: May 19 2024 at 16:02 UTC