CODEWITHSUNDEEP
existscoqinversion
Mitchell Buckley
Mitchell Buckley

Reputation: 118

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

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?

Upvotes: 3

Views: 782

Answers (2)

Anton Trunov
Anton Trunov

Reputation: 15424

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).

Upvotes: 3

pintoch
pintoch

Reputation: 2488

Yes, by specifying binders for the objects you want to introduce, like this:

inversion [a [b [v H']]].

Note that destruct also works here (with the same syntax), it generates a slightly simpler proof (In general, the manual warns against large proofs generated by inversion).

Upvotes: 2

Related Questions