The Coq mailing list

[Cody Roux <cody.roux AT andrew.cmu.edu>]

Hi Bruno!

    This happens all the time when proving inductive properties about 
say, programing language semantics. I think Cedric gave a nice example, 
but almost every lemma and theorem up to

    forall n m k, (n * m) * k = n * (m * k)

uses these kinds of generalizations. Try it in Coq!

Another classic example is:

    rev (rev l) = l

where rev is the reverse function on lists. It's also a nice case where 
an intermediary lemma is really required.

Best,

Cody


On 06/11/2014 01:42 AM, Bruno Woltzenlogel Paleo wrote:
> Hi Cedric,
>
> > When you perform some induction, you sometimes need to generalize your goal.
> This is interesting. Could you state a simple (if possible, "simplest") 
> example goal where this happens?
>
> Thanks!
> Best regards,
>
> Bruno