coq - 存在量词：如何引用实例

Question

我有一个定理，我证明存在满足某些属性的对象。我通过构造对象证明了这个定理。然后，在另一个证明中，我想在第二个定理的陈述中引用第一个定理中定义的对象。我知道如果我使用 Defined 而不是 Qed 关闭我的证明，该对象应该是可访问的，但我不知道如何访问它。例如：

定理 T1：存在 x，P x。证明。... 定义。

定理 T2：对于在 T1 中构造的相同 x，Q x \/ R x。证明。... Qed。

我如何在 Coq 中表达这一点？

Answer 1

在这种情况下，您应该简单地使用定义来定义对象 (x)。

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

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

Theorem T2 : ...

T2 的证明使用相同的对象。您可能会发现某些策略（即，精确的，双重的，如果这是存在于 Prop 中的东西）将在这里为您提供帮助，因为它们让您更轻松地操作原始证明对象。