Logo Questions Linux Laravel Mysql Ubuntu Git Menu
 

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

Tags:

coq

coq-tactic

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?

like image 410
thor Avatar asked Jun 28 '16 04:06

thor


2 Answers

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
like image 137
Anton Trunov Avatar answered Nov 11 '22 12:11

Anton Trunov


From what I recall, revert is just a simpler form of generalize, which is usually easier to use for newcomers: it is the opposite of intro. Using a flavor of generalize, you can do much more (especially with dependency between terms and types).

like image 27
Vinz Avatar answered Nov 11 '22 12:11

Vinz