The Coq mailing list

["Yevgeniy Makarov" <emakarov AT gmail.com>]

Hello,

You can do recursive proof construction using the tactic language
Ltac. It would be more natural not to use variables x and y in the
context. The reason is that Coq is a functional language, and the
values of variables cannot be changed once it is set. (A variable can
be cleared and introduced again, but only if the it is not used in any
object that continues to exists.) So instead I suggest using x and y
as arguments to a recursive tactic.

Consider the following example:

Definition f (x : nat) := x + 1.

Definition test (y : nat) := y = 5.

Ltac search x := try (exists x; compute; reflexivity); search (f x).

Goal exists y, test y.
search 0.

If "reflexivity" does not work for the current x, then the tactic
calls itself with the new value for x. Note that "compute" above is
optional since "reflexivity" normalizes both side of the equation.

Hope this helps.

Evgeny