Coq中的还原策略和广义策略有什么区别？

Question

从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类似于演算抽象操作？

Answer 1

是的，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是目标中 type 的子项T，则通过替换所有出现的bygeneralize t来将目标替换为forall x:T, G0whereG0获得。Gtx

本质上，这表示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