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?
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
andt
is a subterm of typeT
in the goal, thengeneralize t
replaces the goal byforall x:T, G0
whereG0
is obtained fromG
by replacing all occurrences oft
byx
.
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
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).
If you love us? You can donate to us via Paypal or buy me a coffee so we can maintain and grow! Thank you!
Donate Us With