How to teach generalizing the induction hypothesis?

Question

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:

1. 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.)

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

Answer 1

The following observation about your question 2 might be too obvious, but one simple way to recognize when you need to strengthen the induction hypothesis is to notice that when you try to prove your theorem by induction, you can't quite seem to derive the $n$th case by assuming the $(n-1)$st case; it seems that you need something a bit stronger than the $(n-1)$st case, that you don't know how to prove. So, articulate exactly what that stronger statement is, and see if you can prove that by induction instead.