coq - 存在数量詞: インスタンスの参照方法

Question

ある性質を満たすオブジェクトが存在することを示す定理があります。オブジェクトを構成することによって、この定理を証明しました。次に、別の証明として、第 2 の定理のステートメントで、第 1 の定理で定義されたオブジェクトを参照したいと思います。Qed ではなく Defined でプルーフを閉じれば、オブジェクトにアクセスできるはずですが、アクセスする方法がわかりません。例えば：

定理 T1: 存在 x, P x. 証拠。...定義されています。

定理 T2: T1 で構築された同じ x に対して、Q x \/ R x。証拠。... ケド。

これをCoqでどのように表現しますか?

Answer 1

この場合、定義を使用してオブジェクト (x) を定義するだけです。

Definition object : (...) := 
  ...

Theorem T1 : exists x, P x.
  Proof.
  exists object.
    ...
  Qed.

Theorem T2 : ...

ここで、T2 の証明はこの同じオブジェクトを使用します。生のプルーフオブジェクトをより簡単に操作できるようにするため、特定の戦術 (つまり、正確、これが Prop にあるものである場合は 2 倍) がここで役立つことに気付くかもしれません。