Notes on Induction, Towers of Hanoi, and Lists: From Numbers to Lists, with Automating Proofs and Structural Induction

Induction on natural numbers and lists

• Lists over a type with a single element U (only one possible value, e.g., star) are essentially the same as natural numbers: a list is determined entirely by its length. The induction principle for such lists specialises to the usual induction on natural numbers.
• Intuition: lists are like natural numbers on steroids; when there is only one element, a list’s structure is completely captured by its length, so induction behaves the same as against naturals.
• Motivation: use Towers of Hanoi as a concrete example to practice inductive proofs, and to contrast automated proof (Daphne) with human-guided reasoning.

Towers of Hanoi: a motivating example for induction

• Game setup: 3 pegs (poles), start with all disks on pole 1, sizes strictly decreasing from bottom to top; goal is to move all disks to pole 3.
• Rules: move one disk at a time; never place a larger disk on top of a smaller one.
• Question: How many moves are needed as a function of the number of disks n?
• Standard recursive strategy (proof-by-induction flavor):
  • If n = 0, no moves are needed.
  • For n > 0: move the top n−1 disks from pole 1 to pole 2, move the largest disk from pole 1 to pole 3, then move the n−1 disks from pole 2 to pole 3.
• Two simple programs that compute the moves count:
  • Hanoi1(n):
  • Base: Hanoi1(0) = 0
  • Step: Hanoi1(n) = 1 + 2 * Hanoi1(n - 1)
  • In the transcript it’s described as: the move of the largest disk plus two times moving n−1 disks.
  • Hanoi2(n, a): an accumulator-based version to make tail-recursive proofs possible:
  • Base: Hanoi2(0, a) = a
  • Step: Hanoi2(n, a) = 1 + 2 * Hanoi2(n - 1, a)
  • When run with a = 0, Hanoi2(n, 0) computes Hanoi1(n).
• Observations about correctness and proof structure:
  • Proving Hanoi1(n) = Hanoi2(n, 0) by induction requires a property that relates both arguments that change in the recursive call (n and the accumulator a).
  • If the inductive hypothesis only mentions the first argument changing (n) and not the accumulator a, the induction step may stall because the second argument also changes in the recursive call.
  • This motivates generalizing the induction hypothesis to a property P(n, a) that quantifies over all possible a (accumulators).

Why the naive induction can fail and how to fix it

• The problem with a single-argument induction: in the step, Hanoi2(n, a) references Hanoi2(n−1, a) and the a changes as well in many constructions, so the inductive step needs to account for how the second argument changes.
• The fix: prove a relation that holds for all n and for all possible accumulators a. Concretely, consider a property P(n, a) and prove:
  • For all n and all a: Hanoi2(n, a) = Hanoi1(n) + a * (Hanoi1(n) + 1).
  • This expresses that the accumulator simply adds a multiple of the per-step increment (Hanoi1(n) + 1).
• Why this form works: (i) it matches the observed pattern in concrete calculations, and (ii) it accommodates the fact that the recursive call changes both arguments, so the IH must cover both.
• Numerical pattern exploration (informal):
  • For n = 3, Hanoi1(3) = 7. Then Hanoi2(3, a) yields values for a = 0, 1, 2, 3 as 7, 15, 23, 31 respectively.
  • The differences are 8, 8, 8 (constant per increment in a), which equals Hanoi1(3) + 1.
  • For n = 4, the pattern doubles in the step size (8 becomes 16), consistent with the same rule but with a larger base value.
• Concluding the pattern: the relation
  • $ext{Hanoi2}(n, a) = ext{Hanoi1}(n) + a imes ( ext{Hanoi1}(n) + 1)$
  • implies, in particular, for a = 0, $ext{Hanoi2}(n, 0) = ext{Hanoi1}(n).$
• This leads to a compact proof strategy where you prove a two-argument lemma, then recover the original one-argument equality as a corollary by setting a = 0.

General proof strategy for recursive programs with multiple changing arguments

• When the recursive call changes more than one argument, you should:
  • Form a relation that includes all changing arguments (a, n, etc.).
  • Prove that relation holds for all values of the changing arguments (often by induction on the natural number parameter while treating the other parameters as variables).
  • Use the general relation to derive the specific goal (e.g., Hanoi1(n) = Hanoi2(n, 0)).
• In the talk, this is framed as a general approach to induction: you can choose P(n) or P(n, a) or any property that suits the recursive call pattern, and then prove P for all relevant arguments.
• The talk contrasts manual reasoning with automated proof, noting that Daphne can automatically prove the reformulated two-argument lemma once the statement is in the right shape and the right helper facts are provided.

Using a lemma to guide automated proving (Daphne)

• The prover works by attempting to prove whatever you ask, using default arithmetic facts and induction rules, but does not invent arbitrary facts.
• If the goal would require a known lemma that hasn’t been supplied, the automated prover may fail.
• Remedy: supply the prover with a lemma (a previously proven or intuitively obvious fact) and/or reformulate the goal to include a parameter that you can reference in the lemma.
• In the transcript, supplying the lemma (e.g., a relation that holds for all n and a) makes the automatic proof succeed; this is done by explicitly letting the prover use the lemma (e.g., a lemma relating Hanoi2(n, 0) to Hanoi1(n)).
• Example approach (high level):
  • Prove NOY1(n) := Hanoi1(n) (or an equivalent two-argument form) as a lemma and then use this lemma within the main induction to finish the proof automatically.
• The speaker also mentions “proof by calculation” as an alternative: deriving the equality by explicit calculation and then annotating steps for the prover to accept, including handling parentheses and the use of arithmetic facts.
• Annotating steps: to keep the prover honest and to guide it, you can annotate certain equalities with justifications (e.g., “by Hanoi(n)”, or “by arithmetic”). The transcript shows a moment of difficulty with an annotation placement and demonstrates the practical challenges of using a theorem prover.

Induction on lists: dual to induction on numbers

• Transition from natural numbers to lists is achieved by viewing lists as built from a base (empty) and a constructor (cons).
• Induction on lists follows the same domino-like intuition: the base case is the empty list, and the step case shows that if the property P holds for an arbitrary tail xs, then it holds for the list consisting of an arbitrary head a prepended to xs, i.e., for a :: xs.
• Base case for lists: P(nil) should hold.
• Step case: assume P(xs) and show P(a :: xs) for an arbitrary element a.
• This universal quantification over the head a is crucial: to prove a property for all lists, you must be able to instantiate the head with any element.
• The domino analogy: tipping the empty list is the first domino; then, for any chosen head a, if P holds for the tail, P holds for a :: tail, and so on for all lists.

Structural induction on lists vs. induction on numbers

• In Haskell, and in many functional languages, lists are defined via two constructors:
  • Nil (the empty list)
  • Cons :: a -> List a -> List a
• In the transcript’s Dafni language, the analogous idea is presented with explicit constructors and a data-type definition that produces two constructors (Nil and Cons) and two simple operations to build lists.
• The induction principle for lists in this setting is structural induction:
  • Base case: P(Nil) holds.
  • Step: for any head x and any tail xs, if P(xs) then P(Cons x xs).
• The data type definition implicitly defines two functions, akin to nil (empty list) and cons (prefix an element), which construct lists from smaller pieces.
• The speaker draws parallels between Haskell’s notation and Dafni’s explicit prefixing (cons) form, highlighting the practical similarity of the concepts across the two systems.

Key formulas and notations discussed

• Tower of Hanoi move count (natural numbers):
  • Base: $Hanoi1(0) = 0.$
  • Recurrence: $Hanoi1(n) = 1 + 2 \cdot Hanoi1(n-1) \quad \text{for } n \ge 1.$
• Tail-recursive variant with accumulator a:
  • Base: $Hanoi2(0, a) = a.$
  • Recurrence: $Hanoi2(n, a) = 1 + 2 \cdot Hanoi2(n-1, a) \quad \text{for } n \ge 1.$
• Relationship observed between the two versions:
  • $Hanoi2(n, 0) = Hanoi1(n).$
• Pattern-led generalization (two-argument relation):
  • Conjectured: $Hanoi2(n, a) = Hanoi1(n) + a \cdot (Hanoi1(n) + 1).$
  • This implies, in particular, that for all n, a: $Hanoi2(n, a) = Hanoi1(n) + a \cdot (Hanoi1(n) + 1).$
  • Corollary: setting a = 0 recovers the original one-argument equality, i.e., $Hanoi2(n, 0) = Hanoi1(n).$
• A closed-form for Hanoi1(n) (from the recurrence):
  • $Hanoi1(n) = 2^n - 1 ext{ for } n \ge 0.$
• Induction on lists (structure):
  • Base: P(Nil).
  • Step: for any element a and list xs, if P(xs) then P(Cons a xs).
• Haskell vs Dafni notation (conceptual parallels):
  • Haskell: data List a = Nil | Cons a (List a)
  • Dafni: explicit Nil and Cons constructors; list construction via prefixing elements.

Practical takeaways and connections

• Induction must be tailored to the specific recursive structure: whenever a recursive call changes multiple arguments, the inductive hypothesis should quantify over all those changing arguments (e.g., produce a P(n, a) that captures the relation for all a).
• When proving properties of recursive functions, a two-parameter lemma can be both natural and powerful, especially for automated provers that need guidance about which facts to use.
• Automating proofs often requires revealing intermediate lemmas (e.g., a relation between Hanoi2(n, a) and Hanoi1(n)) so the prover can reuse them; otherwise it may fail to prove a seemingly simple statement.
• The Towers of Hanoi serves as a rich teaching example where pattern recognition (from concrete values) leads to a general inductive invariant, guiding both manual proofs and formal automation.
• Induction on lists is a natural extension of induction on numbers, with the added complexity of universally-quantified head elements to ensure the property holds for all possible lists; this is the core idea behind structural induction.
• The practical programming-language perspective (Haskell vs Dafni) reinforces that the underlying mathematical principles (induction, recursion, structural recursion) are the same, even if syntax differs.

Quick recap of the main ideas

• Induction on natural numbers uses base case n = 0 and step case transforming n to n+1; for lists, the base case is the empty list and the step case adds a new head element.
• Towers of Hanoi provides a canonical recursive structure: move n−1 disks, move largest, move n−1 disks again; yields the recurrence $Hanoi1(n) = 1 + 2\cdot Hanoi1(n-1)$ with $Hanoi1(0) = 0$ and hence $Hanoi1(n) = 2^n - 1.$
• An accumulator version (Hanoi2) demonstrates how a tail-recursive form can lead to a different inductive pathway; the two-argument relation is often necessary to capture all changing parts of the recursion.
• Generalizing the IH to cover all changing arguments and identifying the right lemma are key steps for successful automated proofs; human insight helps discover the right invariant or lemma.
• Induction on lists uses the structural nature of the data type (Nil or Cons) and requires the head element to be arbitrary, captured by the ∀ quantifier, to prove properties for all lists.

Data type definitions (conceptual checklist)

• Lists are built from Nil and Cons:
  • Nil represents the empty list.
  • Cons a xs prepends an element a to an existing list xs.
• Inductive proof principle follows from the data-type structure: base case for Nil, step for Cons a xs assuming P(xs) to prove P(Cons a xs).
• In Dafni vs Haskell translation, the same idea is encoded with explicit constructors and a clear structural induction rule; the key ideas remain the same across languages.