Coq：1つのコマンドで複数の変数を持つ存在量限定子の逆転？

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

あなたはこのようなconjやex_introとして右結合バイナリ誘導コンストラクタのシーケンスのためのパターン(p1 & ... & pn)のリストを使用することができます。

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によって生成された大きな校正に対して警告します）。