将 `P(?x)` 转换为 `exists x,P(x)`，为 Coq 中的不同子目标提供不同的实例化

Question

我的目标是存在变量 ?x。为了证明这一点，我需要解构一个项 t，并且在解构 t 生成的不同情况下，实例化 ?x 的项应该不同才能正确。

当我证明完第一个案例后，Coq 根据我的第一个案例实例化 ?x，这使得第二个案例无法证明。有没有办法将

P(?x)

形式的目标变成

exists x,P(x)

？ 或者还有其他方法可以解决我遇到的问题吗？

Answer 1

存在变量只是您不知道如何或不想写的术语的快捷方式。特别是，它只有一个实例化，因为它代表一个尚未明确编写的固定术语。特别是，

exists x, P x

在逻辑上并不意味着

P ?x

。就您而言，我认为解决方案是永远不要引入

?x

，即避免引入它的策略（通常是

eapply

）。