在 Coq 中使用存在定理

【问题标题】：Using an existential theorem in Coq在 Coq 中使用存在定理
【发布时间】：2012-08-31 11:50:13
【问题描述】：

我在 Coq 中有以下定理：Theorem T : exists x:A, P x. 我希望能够在后续证明中使用这个值。 IE。我想说的是：“让o 表示一个值，使得P o。我知道o 存在于定理T...”

我该怎么做？提前致谢！

【问题讨论】：

【解决方案1】：

从数学上讲，您需要为 ∃ 构造函数应用消除规则。通用消除策略elim 有效。

elim T; intro o.

愚蠢的例子：

Parameter A : Prop.
Parameter P : A -> Prop.
Axiom T : exists x:A, P x.
Parameter G : Prop.
Axiom U : forall x:A, P x -> G.
Goal G.
Proof.
elim T; intro o.
apply U.
Qed.

【讨论】：