coq - 在 Coq 中使用存在定理

Question

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

我该怎么做？提前致谢！

Answer 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.