In Coq: inversion of existential quantifier with multiple variables, with one command?

Question

I am working through a proof in which there is a hypothesis

H : exists a b v, P a b v

If I use inversion H, then I recover

a : nat
H1 : exists b v, P a b v.

which is fine, but then I need to use inversion twice more to recover b and v. Is there a single command to recover a, b, v all at once?

Answer 1

You can use a list of patterns (p1 & ... & pn) for sequence of right-associative binary inductive constructors such as conj or ex_intro:

destruct H as (a & b & v & H).

Another nice example from the reference manual: if we have a hypothesis

H: A /\ (exists x, B /\ C /\ D)

Then, we can destruct it with

destruct H as (a & x & b & c & d).