Reasoning about arithmetical 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; and,
• practically, to build muscle memory about induction proofs.

Resources

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

A series of exercises

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

• a recursive version of the addition function, add_v1,
• a tail-recursive version of the addition function, add_v2,
• a recursive version of the multiplication function, mul_v11, that uses add_v1,
• a recursive version of the multiplication function, mul_v12, that uses add_v2,
• a tail-recursive version of the multiplication function, mul_v21, that uses add_v1, and
• a tail-recursive version of the multiplication function, mul_v22, that uses add_v2.

(The tail-recursive versions of the multiplication function you will actually need to implement.)

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 03). 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 19

Prove that O is left-neutral for add_v1.

Exercise 20

Prove that O is left-neutral for add_v2.

Exercise 21

Prove that O is right-neutral for add_v1.

Exercise 22

Prove that O is right-neutral for add_v2.

Exercise 23

Prove that add_v1 is associative.

Exercise 24

Prove that add_v2 is associative.

Exercise 25

Prove that add_v1 is commutative.

Exercise 26

Prove that add_v2 is commutative.

Exercise 27

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

Solution for Exercise 27

See the accompanying file.

Exercise 28

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

Solution for Exercise 28

See the accompanying file.

Exercise 29

Using add_v1, implement a tail-recursive version of the multiplication function, mul_v21, 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.)

Exercise 30

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

Exercise 31

Prove that mul_v11, mul_v12, mul_v21, and mul_v22 are equivalent.

Exercise 32

Prove that 0 is left-absorbing with respect to mul_v11, mul_v12, mul_v21, and mul_v22.

Exercise 33

Prove that 1 is left-neutral with respect to mul_v11, mul_v12, mul_v21, and mul_v22.

Exercise 34

Prove that 0 is right-absorbing with respect to mul_v11, mul_v12, mul_v21, and mul_v22.

Exercise 35

Prove that 1 is right-neutral with respect to mul_v11, mul_v12, mul_v21, and mul_v22.

Exercise 36

Prove that each of mul_v11, mul_v12, mul_v21, and mul_v22 is right-distributive over its own version of the addition function (i.e., mul_v11 is right-distributive over add_v1, mul_v12 is right-distributive over add_v2, etc.).

Exercise 37

Prove that each of mul_v11, mul_v12, mul_v21, and mul_v22 is associative.

Exercise 38

Prove that each of mul_v11, mul_v12, mul_v21, and mul_v22 is commutative.

Exercise 39

Prove that each of mul_v11, mul_v12, mul_v21, and mul_v22 is left-distributive over its own version of the addition function (i.e., mul_v11 is left-distributive over add_v1, mul_v12 is left-distributive over add_v2, etc.).

Resources

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

Version

Created [09 Feb 2024]