I just finished teaching a class on using proof assistants (in this case, Agda) to write provably correct programs. Reflecting on how it went, the biggest difficulty I noticed the students having was that they had a lot of trouble working out how to generalize the induction hypothesis. They were generally able to work out how to prove theorems by induction (even with numerous quantifiers in the statement), as long as they didn't have to generalize the hypothesis.

This is obviously one of the key skills underpinning "mathematical maturity", but it's also not a skill I feel I have good handle on how to teach. My current idea is to come up with a list of exercises where they have to work out a generalization, but I'd really also like to be able to explain some of the strategies they should use, and I'm having trouble putting that into words.

So my question is twofold:

Suggest some of your favorite small examples where the proof requires a generalization. (It doesn't have to be a nontrivial generalization -- it just needs to be a generalization! Also, I want to do this in a proof assistant, so sticking with basic properties of basic algebraic structures is helpful.)

How do you explain how to recognize when to generalize, and how do you explain how you should generalize the induction hypothesis?

1more comment