List Induction: Tricks, Lemmas, and Daphne-Based Proof Techniques

Session Context and Goals

• Instructor aims to finish list induction and to demonstrate practical proof techniques rather than introduce new material.
• Focus on finding the right statement to prove, using auxiliary lemmas when needed, and keeping proofs smooth and mechanical.
• Topic of the day: a simple, instructive case where the proof doesn’t go through out of the box, not because of proving the wrong thing but due to a missing step that is best supplied by a lemma.
• The example begins from a function dup_all that doubles every element in a list and compares two quantities:
  • dup_all xs doubles each element in xs
  • append xs xs appends the list to itself
  • The assertion: dupall xs has length 2 × length(xs). Meanwhile, length(append xs xs) also equals 2 × length(xs), but append xs xs is not the same list as dupall xs; equality of the two lists would require stronger statements.
• The goal: show that if we double every element in the list, the length is twice the original length, which should coincide with the length of xs appended to xs, but not imply the lists are equal.
• The broader technique: use auxiliary lemmas (like length properties of append) to unlock the main goal; sometimes it is beneficial to temporarily assume an auxiliary fact as an axiom and prove it later (proof-by-lemma or loan approach). This is a common practice in real proofs and in teaching how to interact with proof assistants like Daphne.
• Instructor highlights the learning intent: train eyes to spot when a lemma is needed, and how to splice it into the proof workflow, observing that automation may not do everything automatically.

Definitions and Key Functions

• dup_all (list a): double each element in the list
  • Definition intuition (conceptual):
  • dup_all nil = nil
  • dupall (cons k xs) = cons k (cons k (dupall xs))
  • Consequence: ext{length}( ext{dup ext{_}all} ext{ } xs) = 2 imes ext{length}(xs)
  • Note: append xs xs has the same length but a different structure; the two lists are not equal in general, so equality would require a separate argument.
• append (xs, ys): standard list append
  • Definitions (typical):
  • ext{append}
    il ys = ys
  • $ext{append}( ext{cons } x ext{ xs}) ys = ext{cons } x\big( ext{append } ext{xs} ys\big)$
  • Key behavior: recursion is defined on the first argument (xs); there is no case for a cons in the second argument.
• length (lst): standard length function; used to relate dup_all and append in the discussion.
• sum_one (list of int): standard summation over a list
  • Typical definition:
  • ext{sum ext{_}one}([]) = 0
  • $ext{sum ext{<em>}one}(x::xs) = x + ext{sum ext{</em>}one}(xs)$
• sum_two (list of int, int): a nonstandard summation that accumulates into a second argument
  • Definition pattern:
  • ext{sum ext{_}two}([], a) = a
  • $ext{sum ext{<em>}two}(x::xs, a) = ext{sum ext{</em>}two}(xs, a + x)$
  • Observed relationship: sumtwo(l, a) can be related to sumone(l) by a simple invariant:
  • $ext{sum ext{<em>}two}(l, a) = a + ext{sum ext{</em>}one}(l)$
• lmax (list of numbers): a function to compute the maximum; the instructor uses it to illustrate a pitfall with induction on a complicated recursive pattern where the recursive call changes more than one argument.
  • The key observation: if in a recursive definition the call updates both the second argument and the first argument, a direct induction on the first argument (the list) can fail for properties about the result unless the invariant is carefully structured.
• reverse/ref (two-argument accumulator variant): an efficient list reversal function using an accumulator
  • ref l a has the effect of moving the head of l to the front of a, accumulating the reversed list in a
  • Intuition:
  • If l = nil, ref nil a = a
  • If l = x :: xs, then ref (x::xs) a = ref xs (x :: a)
  • Efficiency: the naive reverse (walking with append) is O(n^2); the accumulator-based ref runs in O(n).
  • The variant used in the talk has two extra parameters (a and b) to illustrate more general invariants and how to tie the arguments together in a proof.

Core Proof Techniques and Insights

• Induction strategy on lists
  • Base case: nil works cleanly in many proofs.
  • Inductive step: typical approach is to assume the property for xs and prove for (x::xs). Problems arise when the recursive step of the function updates more than the first argument; a straight induction may not be sufficient.
• Auxiliary lemmas and “leap of faith” in proofs
  • When stuck, propose an auxiliary lemma that captures a necessary invariant, and see if it unlocks the main proof.
  • Example: length(append k (cons x l)) = 1 + length(append k l)
  • Initially, you may treat such a lemma as an axiom to keep going (to demonstrate the main idea or to allow a proof search like Daphne to proceed).
  • Later, you discharge the axiom by actually proving the lemma within the theory (open parentheses, closing parentheses convention in the talk).
• Proof discovery and automation (Daphne-like tools)
  • The technique of “splicing the nugget” is used to guide the prover to the proof path.
  • If the automated search misses a crucial nugget, you insert a small, true lemma and try again.
  • This mirrors real research practice: you don’t always prove everything in one step; you build the right lemmas and then complete the main proof.
• Structuring a proof around an invariant or relation between arguments
  • In many proofs where a function’s recursion changes multiple arguments, the natural invariant involves a relation among all arguments (e.g., ref l a b is related to ref a (append l b)).
  • Such invariants can often be discovered by thinking about what the recursive call does to the structure of the data and the accumulator.
• Important caveat about correctness of lemmas
  • If you temporarily treat a lemma as an axiom, you must revisit and discharge it; otherwise you introduce an unsound proof.
  • The talk emphasizes that ignoring structural details (like parentheses or exact definitions) can mislead an automated prover into a seemingly proven statement; you must verify with the actual definitions.

Worked Examples and Walkthroughs

• Example A: dup_all and append
  • Goal: show that duplicating all elements yields a list whose length is twice the original length, and compare to append xs xs.
  • Challenge: append’s recursive definition only recurses on its first argument; if the concatenation is in the second argument’s position, the standard rewrite rules don’t apply directly.
  • Strategy: introduce an auxiliary lemma about how length interacts with append when a cons is in the second position:
  • Lemma: $ext{length}( ext{append } k ( ext{cons } x ext{ l})) = 1 + ext{length}( ext{append } k ext{ l})$
  • Process: try to prove the main statement with a temporary axiom for the auxiliary lemma; use it to complete the main proof; then prove the axiom and discharge it.
  • Note: the lecturer demonstrates that if you drop the auxiliary lemma or misplace it, the automatic proof may fail or look like it is proven due to missing parentheses; correctness requires discharging the axiom properly.
• Example B: sumone and sumtwo
  • Problem setup: relate two ways of summing elements of a list; sumtwo accumulates into a second argument a, while sumone returns the sum directly.
  • Target relation (invariant): for all lists l and integers a,
  • $ext{sum ext{<em>}two}(l, a) = a + ext{sum ext{</em>}one}(l)$
  • Approach: prove by induction on l. Base case l = [] gives a = a + 0, so holds. Inductive step: for l = x::xs, use the inductive hypothesis on xs with accumulator a + x to show the equality.
  • Insight: a clean invariant exists showing how sumtwo connects to sumone, which makes the proof mechanical once the invariant is stated.
• Example C: list reversal and the ref function (accumulator-based reversal)
  • Goal: prove that reversing a list twice yields the original list (ref (ref l nil nil) = l).
  • Key idea: identify that the recursive call in ref changes the inner arguments (l and a) in a way that makes a naïve induction tricky. This motivates looking for a general invariant relating ref with append, namely how reversed sections combine when the accumulator changes.
  • General lemma used:
  • $ext{ref}( ext{ref}(l, a, b)) = ext{ref}(a, ext{append}(l, b))$
  • Interpreted as: composing two ref steps is the same as applying ref to the accumulator a with the list formed by appending l to b.
  • Strategy: prove the above lemma (or as a corollary) and then derive the base property ref (ref l nil nil) = l.
  • Practical note: the talk emphasizes that this lemma may be nontrivial; you may try to prove a stronger or a more general version, such as showing that the two definitions of ref are equivalent, but that is optional and can be moderately difficult.
  • The narrative shows a stepwise approach: propose the lemma, attempt to prove it, realize there are subtleties (e.g., need another lemma such as Nil, append nil of l, etc.), and then refine until the proof closes.

Induction Patterns: Pitfalls and Remedies

• lmax example as a cautionary tale
  • Attempting to prove a property about lmax by induction on cons x xs fails because the recursive call in lmax changes both arguments; the standard induction pattern “for all lists of the form cons x xs” is not suitable to capture the needed invariant.
  • Correct approach: either reframe the induction as standard induction on the list structure:
  • For all lists xs, P(xs) holds, with base case P([]) and step P(xs) to P(x::xs) using IH on xs.
  • The moral: when a function’s recursive call updates more than one argument, you may need a more general invariant or a different induction principle (e.g., induction on the entire list structure, not on a subterm).
• Reversal, complexity, and efficiency as a motivating context
  • The discussion ties back to practical concerns: the straightforward reverse using append has quadratic time complexity, while the accumulator-based ref yields linear complexity.
  • This illustrates why induction proofs often go hand in hand with complexity reasoning: understanding the recursive structure informs both correctness proofs and efficiency analyses.

Complexity and Efficiency Considerations

• Naive reverse using append:
  • Walking through the list l of length n, and for each step performing an append that traverses the accumulated portion leads to about O(n^2) recursive calls.
• Optimized reverse with an accumulator (ref):
  • A single pass through the list suffices, yielding O(n) time complexity in ideal terms (plus the cost of cons operations).
• Practical takeaway: understand the recursion pattern to reason about both correctness and efficiency; choosing the right invariant or the right accumulator-based version can dramatically improve performance.

Proof Strategy Toolkit (Lessons for Daphne-like Tools)

• When stuck à la Daphne:
  • Step 1: restate the goal and try a small calculation to see exactly where the obstruction lies.
  • Step 2: identify a likely auxiliary lemma that would resolve the obstruction (e.g., a property about append with cons in the second argument).
  • Step 3: temporarily declare the auxiliary lemma as an axiom (a loan) to see if the main proof can proceed.
  • Step 4: attempt to complete the main proof under the axiom; if successful, proceed to prove and discharge the axiom, replacing the axiom with a proper proof.
  • Step 5: if the axiom proves insufficient, reevaluate and look for a more general invariant or a different lemma; sometimes a second auxiliary lemma is needed.
• Key caution: do not keep an axiom indefinitely; prove and discharge it to ensure soundness.
• Takeaway on automation: many proofs require human-guided hints (lemmas and invariants) to enable automatic provers to find the path; the human-proof pattern can be taught and practiced.

Real-World Relevance and Philosophical Notes

• The material illustrates formal reasoning, program verification, and the careful architecture of proofs, which is central to reliable software and mathematics.
• The examples emphasize the subtlety of induction when functions mutate multiple arguments across recursive calls, a common source of hidden bugs in proofs and implementations.
• Discussion ties to the broader themes of invariants, recursion structure, and the trade-offs between simplicity of a definition and the ease of proving its properties.
• There is a normative message about proof practice: anticipate where lemmas will be needed, practice developing them, and use proof assistants as a partner rather than a black box.

Short-Answer Prompts and Practice Ideas

• Prove the auxiliary lemma:
  • Lemma: for any list k, x, l, with x being an element and k a list,
  • $ext{length}( ext{append } k ( ext{cons } x ext{ l})) = 1 + ext{length}( ext{append } k ext{ l})$
  • Try to prove this by induction on k or on l, and explain why one choice is more natural than the other.
• Prove the sum_two invariant:
  • Show that for all lists l and integers a,
  • $ext{sum ext{<em>}two}(l, a) = a + ext{sum ext{</em>}one}(l)$
  • Use induction on l and the definition of sum_two.
• Prove the reversal identity via the lemma
  • State and prove the general lemma:
  • $ext{ref}( ext{ref}(l, a, b)) = ext{ref}(a, ext{append}(l, b))$
  • Then derive the base property: $ext{ref}( ext{ref}(l, ext{nil}, ext{nil})) = l$
• Compare the naive reverse vs the accumulator-based reverse in terms of time complexity and space usage; provide a short proof sketch of the O(n^2) vs O(n) behavior.
• Reflect on lmax induction issue: explain why standard induction on cons x xs fails and how induction on the list as a whole can address the problem.

Quick Reference of Key Equations (LaTeX)

• Length of dupall: $ext{length}( ext{dup ext{</em>}all} ext{ } xs) = 2 imes ext{length}(xs)$
• Length of append with cons in second arg: $ext{length}( ext{append } k ( ext{cons } x ext{ l})) = 1 + ext{length}( ext{append } k ext{ l})$
• Sumtwo invariant: ext{sum ext{}two}(l, a) = a + ext{sum ext{_}one}(l)
• Reversal lemma (invariant form): $ext{ref}( ext{ref}(l, a, b)) = ext{ref}(a, ext{append}(l, b))$
• Final reversal property (base case): $ext{ref}( ext{ref}(l, ext{nil}, ext{nil})) = l$
• Complexity intuition: naive reverse via append is O(n^2) time; accumulator-based reverse is O(n) time.

Note about the Style of the Session

• The notes capture a lecture-style walkthrough: it includes both concrete definitions and the meta-cognitive process of proof discovery (where to insert lemmas, when to use axioms, how to discharge them).
• The goal is to provide a compact, exam-ready set of notes that preserves the intuition, the structure of the proofs, and the reasoning patterns demonstrated by the lecturer.