The Coq mailing list

[Guillaume Melquiond <guillaume.melquiond AT inria.fr>]

Le 16/01/2018 à 00:15, Ramkumar Ramachandra a écrit :

> I have the following problem, which I found very difficult to proceed 
> with, without the use of `generalize`:

> generalize (S steps).
> intro n; replace n with steps.

> What are n0 and n? Where are they used? Can I somehow use `specialize`?
>
> I'm having a hard time imagining where `generalize` would be useful, 
> because it seems like you'll always end up with absurd things like this 
> to prove.

That is because you are generalizing too much information. Instead, try

generalize (eq_refl (S steps)).
generalize (S steps) at -2.
intro n.

Best regards,

Guillaume