在Coq中使用存在定理

Question

我在Coq中有以下定理：Theorem T : exists x:A, P x.我希望能够在随后的证明中使用此值。 I.E.我想说的是这样的：“让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.