在 Coq 中：使用一个命令反转具有多个变量的存在量词？
In Coq: inversion of existential quantifier with multiple variables, with one command?
我正在研究一个存在假设的证明
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？
是的，通过为你想引入的对象指定绑定器，像这样：
inversion [a [b [v H']]].
请注意，destruct 也适用于此（使用相同的语法），它生成稍微简单的证明（通常，手册警告不要使用 inversion 生成的大型证明）。
您可以将模式列表 (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).
我正在研究一个存在假设的证明
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？
是的，通过为你想引入的对象指定绑定器，像这样：
inversion [a [b [v H']]].
请注意，destruct 也适用于此（使用相同的语法），它生成稍微简单的证明（通常，手册警告不要使用 inversion 生成的大型证明）。
您可以将模式列表 (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).