我正在研究一个存在假设的证明
H : exists a b v, P a b v
如果我使用反转H，那么我恢复
a : nat
H1 : exists b v, P a b v.
这很好，但是我需要再使用两次反转来恢复 b 和 v。 是否有一个命令可以同时恢复 a、b、v？
最佳答案
您可以使用模式列表 (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).
关于exists - 在 Coq : inversion of existential quantifier with multiple variables, 中使用一个命令？，我们在Stack Overflow上找到一个类似的问题： https://stackoverflow.com/questions/38282636/