coq - coqにおける存在例化と一般化

Question

Coqにおける存在例化と存在汎化の簡単な例を教えてもらえますか？を証明したいとき、を使用するものexists x, PはどこにPありますか、私はしばしば名前を付け（またはそのようなものとして）、Pを操作したいと思います。これはCoqの1つである可能性がありますか？Propxxx0

Answer 1

補題ではなく直接存在を証明する場合は、を使用できますeapply ex_intro。これにより、実存変数（記述?42）が導入されます。その後、用語を操作できます。証明を完了するには、最終的にその変数の値を作成する方法を提供する必要があります。これは、戦術を使用して明示的に行うことも、。instantiateなどの戦術を使用して暗黙的に行うこともできますeauto。

実存変数を操作するのは面倒なことが多いことに注意してください。多くの戦術は、すべての用語がインスタンス化され、サブゴールに存在を隠す可能性があることを前提としています。Qed「エラー：不完全なプルーフを保存しようとしました」と表示された場合にのみわかります。実存変数は、すぐにインスタンス化する計画がある場合にのみ使用してください。

これは、の使用法を示すばかげた例ですeapply。

Goal exists x, 1 + x = 3.
Proof.                        (* ⊢ exists x, 1 + x = 3 *)
  eapply ex_intro.            (* ⊢ 1 + ?42 = 3 *)
  simpl.                      (* ⊢ S ?42 = 3 *)
  apply f_equal.              (* ⊢ ?42 = 2 *)
  reflexivity.                (* proof completed *)
Qed.