Disclaimer:

It's not simple, but it might be useful. The context in which it happend is algorithms, but it would be great if someone could test if this approach is useful during other courses, e.g. when introducing induction. Reason why I'm writing about this here is, that when I did the exercise described below, my students (not all, but a lot) had this "being enlightened" face expression, and as it was not about the algorithm itself, then it had to be about the other thing and in that case it was induction (i.e. it seemed that they grasped something important about induction).

Exercise:

The task was on dynamic algorithms and was given as follows:

A company plans to organize a party. The hierarchy of employees is a rooted tree (not necessarily binary), and each employee can be characterized by a form of sociability, given by a positive number. Write a program that will pick the guests so that:

• no guest would meet their immediate superior at the party,
• the sum of sociability coefficients is maximal,
• the company founder (the root of the tree) has to be at the party.

The program should output a single number, namely the sum of sociability coefficients of the guests.

The algorithm to calculate it is easy, let the symbol $\mathcal{T}$ denote the set of abstract people with their hierarchies

\begin{align*} \newcommand{soc}{\mathtt{sociability}} \newcommand{sub}{\mathtt{subordinates}} \newcommand{with}{\mathtt{with}} \newcommand{without}{\mathtt{without}} \soc &: \mathcal{T} \to \mathbb{R}^+\\ \sub &: \mathcal{T} \to 2^\mathcal{T} \\ \end{align*} then in mathematical notation it would be \begin{align*} \with(t)&= \soc(t) + \sum_{s\ \in\ \sub(t)} \without(s), \\ \without(t) &= \sum_{s\ \in\ \sub(t)} \max\big\{ \with(s), \without(s) \big\}. \end{align*}

where the result will be given by $\with$ as the founder has to be included. Now, the challenge is to prove that it is optimal (i.e. it returns the correct result). The proof is via induction on the structure of the tree, that is, we start from leaves and then go up to the root, with the assumption that each time when make the step in some node, all its subtrees are already done.

The base step is easy, as for each leaf we have $\sub(l) = \varnothing$ so \begin{align}\with(l) &= \soc(l) \\ \without(l) &= 0 \end{align} what is obviously true.

Now, for the induction step, $\with(t)$ requires all the subtrees to skip their roots, and besides that they are all independent, so we can just take the sociability of $t$ and add all the optimal subsolutions (we can use them because of the induction hypothesis) and that is exactly what the formula is doing. As for $\without(t)$ the $t$ itself isn't a guest, so from each subtree we can pick the best option and sum it all together. This works, but only because we know that the subsolutions were calculated correctly from induction hypothesis, the shape of the tree ensures, that there weren't any circular arguments.

Sometimes students benefit from an alternative proof: take an optimal solution and prove that one returned by the algorithm isn't worse. Again, prove it via induction on the structure of the tree, the hypothesis being that our algorithm returns an optimal subsolution for each node of the tree. Base case is easy, because there is no choice available in the leaves. For the inner nodes we show that our algorithm returns a pick of guests at least as good as the optimal solution (in $\with$ it follows from induction hypothesis and the fact that all the numbers are positive, for $\without$ it follows from properties of $\max$ function).

Some commentary:

Each time I did this it was an introductory course in programming, and for many the first time where they would see a non-linear induction (in fact this can be proved with induction on the height of the tree, but I did complicate it on purpose). Drawing a diagram with arrows, describing how the induction progresses and how it relies on the subtrees being already calculated helps a lot. After this exercise the topic would come back again several times and students would have much easier time proving that some algorithm (e.g. the Ackermann function) terminates.

Of course, it is hard to draw any reliable conclusions from this experience (it might be just a coincidence that it worked for me), so it would be great if someone could test it themselves. I'd also love to hear your opinions and suggestions.

I hope this helps $\ddot\smile$