Stream: Coq users

Topic: Ltac: Destruct nested pairs nicely


view this post on Zulip 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])?

view this post on Zulip 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 _).

view this post on Zulip Paolo Giarrusso (Nov 14 2020 at 21:45):

(yes, Fail Fail foo asserts success of foo without executing it)

view this post on Zulip 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.

view this post on Zulip Gaëtan Gilbert (Nov 14 2020 at 21:49):

the p seems like a bug

view this post on Zulip Pierre-Marie Pédrot (Nov 14 2020 at 23:10):

There exists a dreaded, undocumented decompose record tactic.

view this post on Zulip Pierre-Marie Pédrot (Nov 14 2020 at 23:10):

I wouldn't recommend its use though.

view this post on Zulip Pierre-Marie Pédrot (Nov 14 2020 at 23:10):

Correction: it is documented.

view this post on Zulip Pierre-Marie Pédrot (Nov 14 2020 at 23:11):

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


Last updated: Feb 08 2023 at 22:03 UTC