This lecture note describes the simple idea to provide the same expressive power to reason about a recursive function as in an inductive specification, namely rewrite rules for base cases and induction steps, to be able to fold and to unfold calls to recursive functions.
Warning
This chapter is under revision.
Let us revisit yet again the addition function:
Definition recursive_specification_of_addition (add : nat -> nat -> nat) :=
(forall y : nat,
add O y = y)
/\
(forall x' y : nat,
add (S x') y = S (add x' y)).
Fixpoint add (i j : nat) : nat :=
match i with
O =>
j
| S i' =>
S (add i' j)
end.
To reason about add the way we reason about any function that satisfies the recursive specification of addition, all we need is the following two fold-unfold lemmas:
Lemma fold_unfold_add_O :
forall j : nat,
add O j =
j.
Proof.
Admitted.
Lemma fold_unfold_add_S :
forall i' j : nat,
add (S i') j =
S (add i' j).
Proof.
Admitted.
To wit:
Theorem add_satisfies_the_recursive_specification_of_addition :
recursive_specification_of_addition add.
Proof.
unfold recursive_specification_of_addition.
split.
- exact fold_unfold_add_O.
- exact fold_unfold_add_S.
Qed.
The fold-unfold lemmas are mechanical to write: they simply capture what is the result of applying add in the base case and what is the result of applying add in the induction step. And they are proved using the fold_unfold_tactic tactic provided in the header of the accompanying file:
Lemma fold_unfold_add_O :
forall j : nat,
add O j =
j.
Proof.
fold_unfold_tactic add.
Qed.
Lemma fold_unfold_add_S :
forall i' j : nat,
add (S i') j =
S (add i' j).
Proof.
fold_unfold_tactic add.
Qed.
State (and prove) the fold-unfold lemmas associated with the power function.
Fixpoint power (x n : nat) : nat :=
match n with
O =>
1
| S n' =>
x * (power x n')
end.
There are two fold-unfold lemmas, one for each case of the exponent:
Lemma fold_unfold_power_O :
forall x : nat,
power x O =
1.
Proof.
fold_unfold_tactic power.
Qed.
Lemma fold_unfold_power_S :
forall x n' : nat,
power x (S n') =
x * (power x n').
Proof.
fold_unfold_tactic power.
Qed.
Implement a tail-recursive version of the power function that uses an accumulator and prove its equivalence with the implementation in Exercise 16.
See the accompanying .v file for how this solution comes about.
It all starts with the lambda-lifted implementation of the power function with an accumulator:
Fixpoint power_acc (x n a : nat) : nat :=
match n with
O =>
a
| S n' =>
power_acc x n' (x * a)
end.
Definition power_alt (x n : nat) : nat :=
power_acc x n 1.
Since power_acc is recursive, we equip it with two fold-unfold lemmas, one for O and one for S:
Lemma fold_unfold_power_acc_O :
forall x a : nat,
power_acc x 0 a =
a.
Proof.
fold_unfold_tactic power_acc.
Qed.
Lemma fold_unfold_power_acc_S :
forall x n' a : nat,
power_acc x (S n') a =
power_acc x n' (x * a).
Proof.
fold_unfold_tactic power_acc.
Qed.
We are now equipped to reason equationally about these two implementations to prove their equivalence:
Theorem power_and_power_alt_are_equivalent :
forall x n : nat,
power x n = power_alt x n.
Proof.
intros x n.
The first step is to obtain a goal that solely concerns functions that are defined recursively. Here, this is achieved by unfolding the call to power_alt:
unfold power_alt.
The *goal* window reads:
x, n : nat
============================
power x n = power_acc x n 1
As a rule, the main theorem is about the main function(s) and it is proved as a corollary of an auxiliary lemma which is about the auxiliary functions. Here we need to relate power and power_acc, which can only be done by suitably combining power x n and a in the left-hand side of the goal:
Lemma power_and_power_alt_are_equivalent_aux :
forall x n a : nat,
suitable_combination (power x n) a = power_acc x n a.
Proof.
But what is this suitable combination?
At this point of this kind of proof, there is nothing else to do but contemplate the situation. For example, we can make the following observations:
These observations suggest (Aha!) that a suitable combination is likely to be power x n * a:
Lemma power_and_power_alt_are_equivalent_aux :
forall x n a : nat,
power x n * a = power_acc x n a.
This “Eureka lemma” is proved by induction on n, using the Light of Inductil, i.e., by introducing a in the base case and in the induction step:
Proof.
intros x n.
induction n as [ | n' IHn'].
- intro a.
The *goals* window reads:
x, a : nat
============================
power x 0 * a = power_acc x 0 a
In this base case, We can use the fold-unfold lemmas for the O case:
rewrite -> (fold_unfold_power_O x).
rewrite -> (fold_unfold_power_acc_O x a).
The *goals* window reads:
x, a : nat
============================
1 * a = a
The goal is an instance of Nat.mul_1_l:
exact (Nat.mul_1_l a).
- intro a.
In this induction step, we can use the fold-unfold lemmas for the S case:
rewrite -> (fold_unfold_power_S x n').
rewrite -> (fold_unfold_power_acc_S x n' a).
The *goals* window reads:
x, n' : nat
IHn' : forall a : nat, power x n' * a = power_acc x n' a
a : nat
============================
x * power x n' * a = power_acc x n' (x * a)
The right-hand side of the goal can be obtained in an instance of the induction hypothesis:
Check (IHn' (x * a)).
Indeed the *response* window reads:
IHn' (x * a)
: power x n' * (x * a) = power_acc x n' (x * a)
Let us replace the right-hand side of the goal by the left-hand side of this instance of the induction hypothesis:
rewrite <- (IHn' (x * a)).
The *goals* window then reads:
x, n' : nat
IHn' : forall a : nat, power x n' * a = power_acc x n' a
a : nat
============================
x * power x n' * a = power x n' * (x * a)
We are at two proof steps of equality, using the commutativity and the associativity of multiplication:
rewrite -> (Nat.mul_comm x (power x n')).
Check Nat.mul_assoc.
symmetry.
exact (Nat.mul_assoc (power x n') x a).
Qed.
Thus equipped, the main theorem is indeed proved as a corollary of the auxiliary lemma:
Theorem power_and_power_alt_are_equivalent :
forall x n : nat,
power x n = power_alt x n.
Proof.
intros x n.
unfold power_alt.
Check (power_and_power_alt_are_equivalent_aux x n 1).
rewrite <- (Nat.mul_1_r (power x n)).
exact (power_and_power_alt_are_equivalent_aux x n 1).
Qed.
Prove the following theorem:
Theorem about_exponentiating_one :
forall n : nat,
power 1 n = 1.
Prove the following theorem:
Theorem about_exponentiating_a_product :
forall x y n : nat,
power (x * y) n = power x n * power y n.
See the accompanying .v file, and do note how the statement of the theorem is tested before it is proved.
Prove the following theorem:
Theorem about_exponentiating_with_a_sum :
forall x i j : nat,
power x (i + j) = power x i * power x j.
See the accompanying .v file, and do note how the statement of the theorem is tested before it is proved.
Provide two proofs for the following theorem, one by induction on y, and the other by induction on z:
Theorem about_exponentiating_with_a_product :
forall x y z : nat,
power x (y * z) = power (power x y) z.
Hint: The previous theorems about power might come handy here.
State (and prove) the fold-unfold lemmas associated with the Fibonacci function.
The Fibonacci function is implemented as follows:
Fixpoint fib (n : nat) : nat :=
match n with
0 =>
0
| S n' =>
match n' with
0 =>
1
| S n'' =>
fib n' + fib n''
end
end.
This recursive function gives rise to the following two fold-unfold lemmas:
Lemma fold_unfold_fib_O :
fib O =
0.
Proof.
fold_unfold_tactic fib.
Qed.
Lemma fold_unfold_fib_S :
forall n' : nat,
fib (S n') =
match n' with
0 =>
1
| S n'' =>
fib n' + fib n''
end.
Proof.
fold_unfold_tactic fib.
Qed.
If one wishes to have two more fold-unfold lemmas, they can be proved as corollaries of these two:
Corollary fold_unfold_fib_1 :
fib 1 =
1.
Proof.
rewrite -> (fold_unfold_fib_S 0).
reflexivity.
Qed.
Corollary fold_unfold_fib_SS :
forall n'' : nat,
fib (S (S n'')) =
fib (S n'') + fib n''.
Proof.
intro n''.
rewrite -> (fold_unfold_fib_S (S n'')).
reflexivity.
Qed.
Anton: These fold-unfold lemmas are a cornerstone of equational reasoning.
Mimer: Yes. And such as they are, the only original contribution of these lecture notes.
Dana: Still, a cornerstone.
Pablito: Oh, look, a warning:
Warning
fold_unfold_tactic is only to be used in the proofs of fold-unfold lemmas. Thanks.
The accompanying .v file contains
The fold-unfold lemmas are mechanically derived from the implementation of the mirror function:
Fixpoint mirror (V : Type) (t : binary_tree V) : binary_tree V :=
match t with
Leaf _ v =>
Leaf V v
| Node _ t1 t2 =>
Node V (mirror V t2) (mirror V t1)
end.
Lemma fold_unfold_mirror_Leaf :
forall (V : Type)
(v : V),
mirror V (Leaf V v) =
Leaf V v.
Proof.
fold_unfold_tactic mirror.
Qed.
Lemma fold_unfold_mirror_Node :
forall (V : Type)
(t1 t2 : binary_tree V),
mirror V (Node V t1 t2) =
Node V (mirror V t2) (mirror V t1).
Proof.
fold_unfold_tactic mirror.
Qed.
These fold-unfold lemmas are used in each proof.
The proof by cases illustrates how they precisely provide the expressive power of the specification:
Proposition there_is_at_least_one_mirror_function :
specification_of_mirror mirror.
Proof.
unfold specification_of_mirror.
split.
- exact fold_unfold_mirror_Leaf.
- exact fold_unfold_mirror_Node.
Qed.
The other proof is routine:
Theorem mirror_is_involutory :
forall (V : Type)
(t : binary_tree V),
mirror V (mirror V t) = t.
Proof.
intros V t.
induction t as [v | t1 IHt1 t2 IHt2].
- rewrite -> (fold_unfold_mirror_Leaf V v).
exact (fold_unfold_mirror_Leaf V v).
- rewrite -> (fold_unfold_mirror_Node V t1 t2).
rewrite -> (fold_unfold_mirror_Node V (mirror V t2) (mirror V t1)).
rewrite -> IHt1.
rewrite -> IHt2.
reflexivity.
Qed.
Let us revisit polymorphic binary trees with payloads in their leaves:
Inductive binary_tree (V : Type) : Type :=
Leaf : V -> binary_tree V
| Node : binary_tree V -> binary_tree V -> binary_tree V.
Implement a unit-test function test_mirrorp for the predicate mirrorp : forall V : Type, (V -> V -> bool) -> binary_tree V -> binary_tree V -> bool that tests whether given a type V for payloads and an equality predicate over V, two binary trees are mirrors of each other.
This unit-test function should contain the following tests:
Implement a predicate mirrorp : forall V : Type, (V -> V -> bool) -> binary_tree V -> binary_tree V -> bool that tests whether given a type V for payloads and an equality predicate over V, two binary trees mirror each other.
Hint: mirrorp is defined by recursion on its first argument and by cases on its second argument.
Check whether mirrorp passes the unit tests from Question a.
Does test_mirrorp provide code coverage for mirrorp? If so, explain why. If not, expand it with more tests until it does, and explain why the expanded unit-test function now provides code coverage.
State the fold-unfold lemmas associated to mirrorp.
Implement a function mirror : forall V : Type, binary_tree V -> binary_tree V that given a type V for payloads, mirrors a binary tree.
State the fold-unfold lemmas associated to mirror.
Assuming a type V for payloads and an equality predicate over V that is complete, prove that mirror is sound with respect to mirrorp.
Assuming a type V for payloads and an equality predicate over V that is sound, prove that mirror is complete with respect to mirrorp.
Food for thought (for the overachievers): Does mirrorp form an equivalence relation?
Structural induction is needed to reason about a Gallina function for the same reason as structural recursion was needed to implement this function.
So when a function is defined recursively on, say, its third argument (which tCPA tells us in the *response* window) and when the goal contains a call to this function,
Added exercises about the recursive power function [05 Jun 2025]
Reformatted the unit-test functions uniformly in the resource file [16 Feb 2025]
Fixed a typo in the first sentence of Exercise 23 (“with payloads in their nodes” instead of “with payloads in their leaves”), thanks to Ryan Sim’s eagle eye [16 Feb 2025]
Created [13 Feb 2025]