coq - coq 中的存在实例化和泛化

Question

有人能给我一个 Coq 中存在实例化和存在泛化的简单例子吗？当我想证明exists x, P ，其中 P是一些 Prop使用 x ，我经常想命名x (如 x0 或类似的)，并操纵 P。这可以是 Coq 中的一个吗？

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.