coq - 在 Coq 中泛化存在变量

Question

我试图证明P ?x, whereP : A -> Prop和?x : A是一个存在变量。我可以证明forall a:A, P a，所以我需要推广P ?x到forall a:A, P a。

如果 ?x 是一个实例化变量 x，我可以简单地使用generalize x来生成forall x:A, P x. 然而，当我尝试generalize ?x时，Coq 返回一个语法错误。

这可能吗？我已经检查过了，Coq 似乎没有提供一种直观的方式来概括关于存在变量的陈述。

任何帮助将不胜感激。

Answer 1

P ?x不等价于forall x, P x，甚至不被它暗示。为了证明P ?x，你需要找到一些a这样P a成立的。有了你的假设，找到一些就足够了a : A。换句话说，你需要证明域不为空（或者更准确地说，你需要证明域中存在一个元素）。

在这里，如果你有一些a : A，你可以使用instantiate (1 := A). 愚蠢的例子：

Parameter A : Set.
Parameter P : A -> Prop.
Goal (forall a, P a) -> A -> exists x, P x.
Proof.
  intros H a. eexists. instantiate (1 := a). apply H.
Qed.