coq 中的存在实例化和泛化

Question

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

Answer 1

如果你要直接证明存在而不是通过引理，你可以使用@987654321@ 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.