Coq：使用多個變量反演存在量詞，用一個命令？

Question

我通過，其中有一個假設

H : exists a b v, P a b v 

如果我使用inversion H，然後我恢復

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

這是很好的，但後來我需要使用反轉兩次以證明工作恢復b和v。 是否有單一命令一次恢復a，b，v？

Answer 1

可以使用的模式(p1 & ... & pn)列表爲右結合的二元感性的構造如conj或ex_intro的序列：

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

從參考手冊另一個很好的例子：如果我們有一個假設

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

然後，我們可以用

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

破壞它

Answer 2

是的，通過指定粘結劑要介紹的對象，像這樣：

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

注意destruct也是在這裏工作（具有相同的語法），它生成一個稍微簡單的證明（一般情況下，該手冊警告由inversion生成的大樣張）。