coq - 在 Coq 中使用存在定理

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

我该怎么做？
提前致谢!

最佳答案

从数学上讲，您需要对 ∃ 构造函数应用消除规则。通用消除策略 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.

关于coq - 在 Coq 中使用存在定理，我们在Stack Overflow上找到一个类似的问题：https://stackoverflow.com/questions/12214778/