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

Question

有人可以给我一个简单的 Coq 中存在实例化和存在泛化的例子吗？当我想证明，使用的一些exists x, P在哪里时，我经常想命名（例如），并操纵 P。这可以是 Coq 中的一个吗？PPropxxx0

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.