在 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 生成的大型证明）。