Is there a concise way to destruct nested tuples e.g. `t : nat * nat * nat * nat * nat`

, in ltac?

For right-associative oeprators, one can use `&`

, e.g. on `H: A /\ B /\ C`

, we do `destruct H as (?&?&?) `

.

But to my knowledge, while tuples are written as `(a,b,c)`

, we can not destruct them in tactic scripts without nesting-hell (`destruct t as [[[[a b]c]d]e]`

)?

ouch, fair point. Seems you need `let`

for that:

```
Lemma foo (x : nat * nat * nat): nat.
Fail destruct x as (a & b & c).
Fail Fail destruct x as ((a & b) & c).
refine (let '(a, b, c) := x in _).
```

(yes, `Fail Fail foo`

asserts success of `foo`

without executing it)

actually, `let`

leaves an encoding artifact called `p`

, and doesn't clear `x`

, so you'd get:

```
refine (let '(a, b, c) := x in _); clear p x.
```

the `p`

seems like a bug

There exists a dreaded, undocumented `decompose record`

tactic.

I wouldn't recommend its use though.

Correction: it is documented.

But it doesn't let you pick names, so meh.

Last updated: Jun 18 2024 at 07:01 UTC