3

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?

4

2 回答 2

3

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).
于 2016-07-09T21:29:10.213 回答
2

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

于 2016-07-09T15:30:40.997 回答