coq 中的存在实例化和泛化

Posted 2023-03-28

【中文标题】coq 中的存在实例化和泛化

【英文标题】：existential instantiation and generalization in coq

【发布时间】：2012-05-21 13:26:41

【问题描述】：

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

【问题讨论】：

我知道过去这里有过 coq 问题，但我怀疑随着更多网站的引入，coq 问题的最佳位置现在是cs.stackexchange.com（我自己对碎片化不太满意，但是这是生活中的事实......）

@andrewcooke This hasn't been established conclusively. 我的感觉是，如果目标是完成证明，那么 Coq 问题更关注 SO，如果目标是理解为什么要证明，则在 Computer Science技术工作或不工作，但这是一条非常细的线。专业知识分布在Stack Overflow、Computer Science 和Theoretical Computer Science。

【参考方案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.

【讨论】：

使用 Coq 主干，您可以在证明结束时将未实例化的存在转化为子目标——这是我长期以来一直希望的。

对the previous comment 的补充：这可以通过Grab Existential Variables. 完成