Coq의 실존 정리 사용

Question

Coq에 다음 정리가 있습니다. Theorem T : exists x:A, P x. 다음 값으로이 값을 사용할 수 있기를 원합니다. I.E.

어떻게 이런 짓을 했을까

"... o 내가 o가 정리 T가 존재 함을 알 수 있도록 P o 값을 표현하자."내가 좋아하는 뭔가하고 싶은 말은? 미리 감사드립니다.

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.