coq - 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

是的，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

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

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