Fabian Kunze (Nov 14 2020 at 20:46): Fabian Kunze (Nov 14 2020 at 20:46):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])?
Paolo Giarrusso (Nov 14 2020 at 21:45):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)
Paolo Giarrusso (Nov 14 2020 at 21:46):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
Pierre-Marie Pédrot (Nov 14 2020 at 23:10):There exists a dreaded, undocumented decompose record tactic.
Pierre-Marie Pédrot (Nov 14 2020 at 23:10):I wouldn't recommend its use though.
Pierre-Marie Pédrot (Nov 14 2020 at 23:10):Correction: it is documented.
Pierre-Marie Pédrot (Nov 14 2020 at 23:11):But it doesn't let you pick names, so meh.
Last updated: Oct 13 2024 at 01:02 UTC