8

从 Coq 参考手册（8.5p1）中，我的印象是revert的倒数intro，但generalize在一定程度上也是如此。例如，revert和generalize dependent下面似乎是一样的。

Goal forall x y: nat, 1 + x = 2 + y -> 1 + x + 5 = 7 + y.
intros x y. revert x y.
intros x y. generalize dependent y. generalize dependent x.

只是generalize比 更强大revert吗？

此外，文档在解释有关以下内容时有点循环generalize：

这种策略适用于任何目标。它概括了关于某个术语的结论。

generalize类似于 lambda 演算中的抽象运算符？

4

2 回答 2

7

是的，generalize更强大。您已经证明它至少具有与revert使用 模拟相同的revert功能generalize。请注意，它generalize适用于任何条款——revert仅适用于标识符。

例如，revert不能做手册中的例子：

  x, y : nat
  ============================
  0 <= x + y + y

Coq < generalize (x + y + y).
1 subgoal

  x, y : nat
  ============================
  forall n : nat, 0 <= n

至于定义的“循环性”，真正的解释就在例子的正下方：

如果目标是G并且t是目标中类型的子项，T则将目标generalize t替换为forall x:T, G0whereG0是G通过替换所有出现的tby来获得的x。

本质上，这表示generalize将您的目标包含在 中forall，用新变量 ( x) 替换某些术语。

当然，generalize使用时应该谨慎小心，因为使用后可能会得到一个错误的陈述来证明：

Goal forall x y, x > 0 -> 0 < x + y + y.
  intros x y H.
  generalize dependent (x + y + y).

(* results in this proof state: *)
  x, y : nat
  H : x > 0
  ============================
   forall n : nat, 0 < n
于 2016-06-28T06:53:41.797 回答
1

据我记得，revert它只是 的一种更简单的形式generalize，对于新手来说通常更容易使用：它与intro. 使用 的风格generalize，您可以做更多事情（尤其是在术语和类型之间存在依赖关系的情况下）。

于 2016-06-28T06:52:45.327 回答