Reasoning equationally about accumulator-based recursive functions

To goal of this lecture note is,

• conceptually, to transfer your reasoning skills from reasoning about programs that satisfy specifications to reasoning about programs;
• practically, to build muscle memory about induction proofs; and,
• concretely, to learn how to reason about recursive functions that use accumulators.

Warning

This chapter is under revision.

Resources

• The .v file for the present lecture note (latest version: 16 Feb 2025, with uniformly formatted unit-test functions).

A series of exercises

The accompanying file, contains several versions of the addition and multiplication functions:

• a recursive version of the addition function, add,
• a tail-recursive version of the addition function, add',
• a recursive version of the multiplication function, mul, that uses add,
• a recursive version of the multiplication function, mul', that uses add',
• a tail-recursive version of the multiplication function, mul_alt, that uses add, and
• a tail-recursive version of the multiplication function, mul'_alt, that uses add'.

As usual for functional programming, unit tests must be provided (and they are in the accompanying file).

As usual for equational reasoning about structurally recursive functions, fold-unfold lemmas must be provided (and some are in the accompanying file).

The following exercises provide a safe, unthreatening playground (you have carried out similar proofs in your handin for Week 04). Some of these induction proofs are routine, and they should be treated as such. Several others require Eureka lemmas, and it is part of the value of these exercises to state these lemmas and to prove them. The skills you will acquire, namely

• sprinting through routine proofs and
• identifying, stating, and proving Eureka lemmas

will prove valuable during the rest of this course (and beyond).

Exercise 24

Prove that O is left-neutral for add.

Exercise 25

Prove that O is left-neutral for add'.

Exercise 26

Prove that O is right-neutral for add.

Exercise 27

Prove that O is right-neutral for add'.

Exercise 28

Prove that add is associative.

Exercise 29

Prove that add' is associative.

Exercise 30

Prove that add is commutative.

Exercise 31

Prove that add' is commutative.

Exercise 32

Using add, implement a recursive version of the multiplication function, mul, unit-test it, and state its fold-unfold lemmas.

Solution for Exercise 32

See the accompanying file.

Exercise 33

Using add', implement a recursive version of the multiplication function, mul', unit-test it, and state its fold-unfold lemmas.

Solution for Exercise 33

See the accompanying file.

Exercise 34

Using add, implement a tail-recursive version of the multiplication function, mul_alt, unit-test it, and state its fold-unfold lemmas.

(Hint: this function is not recursive, it merely calls an auxiliary function that is (tail) recursive (and that uses an accumulator). Only write fold-unfold lemmas for this auxiliary function.)

Solution for Exercise 34

See the accompanying file.

Exercise 35

Using add', implement a tail-recursive version of the multiplication function, mul'_alt, unit-test it, and state its fold-unfold lemmas.

Solution for Exercise 35

See the accompanying file.

Exercise 36

Prove that mul, mul', mul_alt, and mul'_alt are equivalent.

Exercise 37

Prove that 0 is left-absorbing for mul, mul', mul_alt, and mul'_alt.

Exercise 38

Prove that 1 is left-neutral for mul, mul', mul_alt, and mul'_alt.

Exercise 39

Prove that 0 is right-absorbing for mul, mul', mul_alt, and mul'_alt.

Exercise 40

Prove that 1 is right-neutral for mul, mul', mul_alt, and mul'_alt.

Exercise 41

Prove that each of mul, mul', mul_alt, and mul'_alt is right-distributive over its own version of the addition function (i.e., mul is right-distributive over add, mul_alt is right-distributive over add, etc.).

Exercise 42

Prove that each of mul, mul_alt, mul', and mul'_alt is associative.

Exercise 43

Prove that each of mul, mul_alt, mul', and mul'_alt is commutative.

Exercise 44

Prove that each of mul, mul_alt, mul', and mul'_alt is left-distributive over its own version of the addition function (i.e., mul is left-distributive over add, mul_alt is left-distributive over add, etc.).

Resources

• The .v file for the present lecture note (latest version: 16 Feb 2025, with uniformly formatted unit-test functions).

Version

Reformatted the unit-test functions uniformly in the resource file [16 Feb 2025]

Updated with more uniform function names [14 Feb 2025]

Created [13 Feb 2025]