coq - Coq での存在定理の使用

Question

Coq には次の定理がありますTheorem T : exists x:A, P x.。この値を後続の証明で使用できるようにしたいです。IE私は次のようoなことを言いたいです:P ooT

どうすればいいですか？前もって感謝します！

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.