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