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 的事情时有点循环：

This tactic applies to any goal. It generalizes the conclusion with respect to some term.

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

Answer 1

据我所知，revert只是generalize的一种更简单的形式，对于新手来说通常更容易使用：它与intro相反。使用 generalize 的风格，您可以做更多事情（尤其是术语和类型之间的依赖性）。

Answer 2

是的，generalize更强大。通过用 generalize 模拟 revert，您已经证明它至少具有与 revert 相同的功能。请注意 generalize 适用于任何 terms、revert——仅适用于 identifiers.

例如，revert无法执行手册中的示例：

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

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

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

至于"circularity"的定义，真正的解释就在例子下面：

If the goal is G and t is a subterm of type T in the goal, then generalize t replaces the goal by forall x:T, G0 where G0 is obtained from G by replacing all occurrences of t by 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

Coq 中的还原策略和泛化策略有什么区别？

What's the difference between revert and generalize tactics in Coq?

coq

coq-tactic