Structuring programs, structuring proofs

The message of this chapter is that the structure of the proof about a program should follow the (control) structure of this program.

A theorem for the main function, auxiliary lemmas for auxiliary functions

In a general way, there are the main functions and we state and prove main theorems about them. When these main functions call auxiliary functions, we state and prove auxiliary lemmas about these auxiliary functions. And just as the main functions call the auxiliary functions, the main theorems are proved as corollaries of the auxiliary lemmas.

Typically, the auxiliary functions are recursive and so the auxiliary lemmas are proved by induction. And just as typically, the main functions are not recursive and so they are not proved by induction.

Eureka lemmas

The concept of “Eureka lemma” was introduced in Week 05 to relate a recursive function and an auxiliary function that uses an accumulator. A Eureka lemma about an accumulator-based function typically quantifies the accumulator and then states a general property of the computation that somehow we find illuminating.

Executive summary

• Properties of recursive functions should be proved by induction and properties of non-recursive functions should not be proved by induction.

• A property about a non-recursive function that calls a recursive function should be proved as a corollary of a lemma about this recursive function, and this lemma should be proved by induction.

• Lemmas suggest themselves first as something utilitarian. It is then up to us to carve them into something useful.

Help! My recursive function doesn’t espouse my inductive data type!

On the occasion – e.g., to reason about Fibonacci numbers, or to reason about a tail-recursive parity predicate that uses no accumulator – our implementations do not follow the traditional program pattern over Peano numbers:

Fixpoint foo (n : nat) : ... :=
  match n with
    O =>
    ...
  | S n' =>
    let ih := foo n'
    in ...
  end.

Then we invariably encounter trouble when trying to reason about these implementations using mathematical induction.

The accompanying .v file illustrates (1) how this trouble arises and (2) how to overcome it.

Anton: I thought I was being smart in my program.

Alfrothul: Right. But then you need to be supersmart in your proof.

Bong-sun: You mean like when we use an accumulator?

Dana: Right. Hello, Eureka lemmas...

Resources

• The .v file for the present lecture note (latest version: 22 Feb 2025).

Version

Completed Section Help! My recursive function doesn’t espouse my inductive data type! [22 Feb 2025]

Created [21 Feb 2025]