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

Question

From the Coq reference manual (8.5p1), my impression is that revert is the inverse of intro, but so is generalize to a certain extent. For example, revert and generalize dependent below seem to be the same.

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. 

Is it just that generalize is more powerful than revert?

Also, the documentation is a bit circular in explaining things about generalize:

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

Is generalize similar to the abstraction operator in lambda calculus?

Answer 1

Yes, generalize is more powerful. You've demonstrated it has at least the same power as revert by simulating revert with generalize. Notice that generalize works on any terms, revert -- only on identifiers.

For example, revert cannot do the example from the manual:

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

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

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

As for "circularity" of the definition, the real explanation is right below the example:

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.

Essentially, this says generalize wraps your goal in forall, replacing some term with a fresh variable (x).

Of course, generalize should be used with some thought and caution, since one can get a false statement to prove after using it:

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