List Induction and Higher-Order Reasoning in Daphne

Core idea of list induction
- Base case: properties hold for the empty list.
- Step case: if a property P holds for a list xs, then it also holds for the list with an element prepended, i.e., for cons x xs.
- This is preserved by prefixing: proving P for the empty list and showing that prefixing any element preserves P suffices to prove P for all lists.
- Practical note: ordered as a proof rule, mirroring the way we define recursive functions (base for nil, step for cons).
- Important nuance: in practice, some real programs or proofs may seem to require more than one base case (e.g., singleton lists). Strictly, the standard list induction principle uses one base case (empty list), but you can often simulate additional base cases by analyzing special subcases inside the step, or by transforming the goal into a form suitable for the standard induction rule.
Higher-order functions and map in Daphne
- Daphne supports higher-order functions: you can pass a function as an argument to another function.
- Signature of map (conceptual): if you pass a function f: T → T and a list of T, you get back a list of T by applying f to each element.
- Definition by pattern matching on lists:
- map f nil = nil
- map f (cons h t) = cons (f h) (map f t)
- Example: if f(n) = n + 1 and the list is [1, 4, 2, 5], then map f [1,4,2,5] = [2,5,3,6].
- Intuition: map is a familiar higher-order function you may know from Haskell; in Daphne it is treated as a first-class function with a straightforward recursive definition.
Proving simple properties about map using list induction
- Theorem: map preserves length. That is, for any list xs and function f, $\text{length}(\text{map}(f, xs)) = \text{length}(xs).$
- Proof outline via list induction on xs
- Base case: xs = nil
  - map f nil = nil; length(nil) = 0; length(map f nil) = length(nil) = 0; equality holds.
- Inductive hypothesis (IH): for some list xs, $\text{length}(\text{map}(f, xs)) = \text{length}(xs).$
- Step case: xs = cons a xs'
  - map f (cons a xs') = cons (f a) (map f xs')
  - length(cons (f a) (map f xs')) = 1 + length(map f xs')
  - by IH, length(map f xs') = length(xs')
  - hence length(map f (cons a xs')) = 1 + length(xs') = length(cons a xs')
- Practical note: when proving such lemmas, it’s helpful to unfold definitions (map, length) step-by-step and align left and right sides, often reasoning from left-hand side to right-hand side or vice versa to identify where IH is used.
- The speaker emphasizes that this can feel linear in presentation, but one can present proofs by working from left-to-right or right-to-left as long as the equalities chain correctly; the calculational style can be supported by a tool like Daphne.
- Conceptual takeaway: a proof can be viewed as a function that maps evidence for the assumptions to evidence for the conclusion (proofs-as-programs perspective).
The view that proofs are functions (Curry–Howard intuition)
- A proof of an implication A ⇒ B can be seen as a function that maps evidence of A to evidence of B.
- For a universal claim ∀x, P(x), the proof maps a new witness x to evidence that P(x) holds.
- When propositions are treated as types, a proof is essentially a program that produces a value (evidence) of the appropriate type.
- This viewpoint helps in understanding why proofs resemble computations and why induction steps resemble recursive function calls.
Using a calculational proof style and automation hints
- Daphne can automatically perform some inductions, but you can guide it by providing hints or reframing the goal (e.g., telling the tool not to automatically do induction in a given step).
- A calculational (calc) proof style helps to present a chain of equalities explicitly; sometimes the IH needs to be justified by a lemma or an intermediate equation rather than by a direct rewrite.
- The distinction between lemmas (auxiliary propositions) and the main proof can blur in automated settings; sometimes you expose a lemma to help the proof finder obtain a chain of equalities.
- In higher-order settings, the automator may still succeed because the recursive structure is preserved, but the human can supply the missing piece or the exact invocation of the IH.
Map and append: combining two lists in proofs with maps
- Problem setup: prove a property that involves two lists, e.g., map f (xs ++ ys) relates to (map f xs) ++ (map f ys).
- The challenge: list induction is naturally on one list (xs). When two lists are involved, you need to encode the property so that induction on one list suffices, or you must restructure the statement (e.g., for all xs, for all ys, P(xs, ys)) to fit the induction principle.
- Induction on xs to prove P(xs, ys) for all ys is often workable if the recursive call arguments do not change in a problematic way; if they do, you may need to appeal to IH on the diminishing argument while keeping the other arguments fixed.
- Example: map f (xs ++ ys) = (map f xs) ++ (map f ys)
- Base case: xs = nil
  - map f (nil ++ ys) = map f ys; map f nil ++ map f ys = nil ++ map f ys = map f ys; equality holds.
- Step case: xs = cons x xs'
  - map f ((x:xs') ++ ys) = map f (x : (xs' ++ ys)) = f x : map f (xs' ++ ys)
  - By IH on xs', map f (xs' ++ ys) = (map f xs') ++ (map f ys)
  - Therefore, f x : (map f (xs' ++ ys)) = f x : ((map f xs') ++ (map f ys))
  - This equals (map f (x:xs')) ++ (map f ys) by definitions of map and ++
- Conclusion: the property holds by induction on xs with the IH applied to the tail xs'.
- Takeaway: you can often prove a two-list property by a single induction on one list, provided the other arguments stay stable in the recursive call or you can incorporate them into the induction hypothesis appropriately.
Inductive data types and generation of induction principles
- In languages like Daphne, you can define a data type and a function simultaneously; from such a definition, an induction principle for that type is generated.
- Example idea (conceptual): define a type List with constructors nil and cons, and define a function (e.g., identity) on that type; the system can generate an induction principle such as: for any P: List A → Prop, if P(nil) and ∀a ∀xs, P(xs) → P(cons a xs), then ∀xs, P(xs).
- This illustrates that induction principles are not separate axioms but arise from inductive data type definitions and definitions over them.
- Practical implication: when introducing new inductive types, the associated induction principle follows automatically, enabling proofs by structural induction over the newly defined type.
Practical reflections from the lecture
- Real-world proofs often involve more complex or nonstandard definitions, which may necessitate additional base cases or case-splitting inside the step, but the core mechanism of list induction remains robust.
- It is permissible to use a variety of proof styles (unfolding definitions, calc chains, automation with hints) as long as the inductive structure is respected.
- The “two base case” intuition can arise from how the step case branches (e.g., a subcase inside the cons case), but it does not invalidate the single-base-case framework of list induction.
- The overall message: list induction is a flexible and reliable tool for proving properties about lists and recursively defined functions, including higher-order ones, in Daphne and similar systems.
Quick recap of key formulas to remember
- Map definition (list recursion):
  ext{map } f
  il =
  il \ ext{map } f igl( ext{cons } h null igr) = ext{cons } (f h)igl( ext{map } f nulligr)
- Length and map: preserving length
  $\text{length}(\text{map}(f, xs)) = \text{length}(xs)$
- Map distributes over append
  $\text{map}(f, xs \;+\; ys) = \text{map}(f, xs) \;+\; \text{map}(f, ys)$
- Optional structural definitions for append
  $\ ext{append}([], ys) = ys \ ext{append}((x:xs), ys) = x : ext{append}(xs, ys)$
- Induction principle for lists
- For any P: List A → Prop,
  if P(nil) and ∀a ∀xs, P(xs) → P(cons a xs), then ∀xs, P(xs).
Final takeaway
- List induction plus higher-order functions is a powerful combination in Daphne for proving properties about recursively defined functions on lists.
- The proof workflow often blends unfolding, IH application, and sometimes targeted lemmas or calculational steps, with the option to guide automated tools when needed.