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.
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_v1 (i j : nat) : nat :=
match i with
O =>
j
| S i' =>
S (add_v1 i' j)
end.
To reason about add_v1 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_v1_O :
forall j : nat,
add_v1 O j =
j.
Proof.
Admitted.
Lemma fold_unfold_add_v1_S :
forall i' j : nat,
add_v1 (S i') j =
S (add_v1 i' j).
Proof.
Admitted.
To wit:
Theorem add_v1_satisfies_the_recursive_specification_of_addition :
recursive_specification_of_addition add_v1.
Proof.
unfold recursive_specification_of_addition.
split.
- exact fold_unfold_add_v1_O.
- exact fold_unfold_add_v1_S.
Qed.
The fold-unfold lemmas are mechanical to write: they simply capture what is the result of applying add_v1 in the base case and what is the result of applying add_v1 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_v1_O :
forall j : nat,
add_v1 O j =
j.
Proof.
fold_unfold_tactic add_v1.
Qed.
Lemma fold_unfold_add_v1_S :
forall i' j : nat,
add_v1 (S i') j =
S (add_v1 i' j).
Proof.
fold_unfold_tactic add_v1.
Qed.
State (and prove) the fold-unfold lemmas associated with the power function.
Fixpoint power_v0 (x n : nat) : nat :=
match n with
O =>
1
| S n' =>
x * (power_v0 x n')
end.
There are two fold-unfold lemmas, one for each case of the exponent:
Lemma fold_unfold_power_v0_O :
forall x : nat,
power_v0 x O =
1.
Proof.
fold_unfold_tactic power_v0.
Qed.
Lemma fold_unfold_power_v0_S :
forall x n' : nat,
power_v0 x (S n') =
x * (power_v0 x n').
Proof.
fold_unfold_tactic power_v0.
Qed.
Implement a tail-recursive version of the power function that uses an accumulator and prove its equivalence with the implementation in Exercise 15.
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_v1_aux (x n a : nat) : nat :=
match n with
O =>
a
| S n' =>
power_v1_aux x n' (x * a)
end.
Definition power_v1 (x n : nat) : nat :=
power_v1_aux x n 1.
Since power_v1_aux is recursive, we equip it with two fold-unfold lemmas, one for O and one for S:
Lemma fold_unfold_power_v1_aux_O :
forall x a : nat,
power_v1_aux x 0 a =
a.
Proof.
fold_unfold_tactic power_v1_aux.
Qed.
Lemma fold_unfold_power_v1_aux_S :
forall x n' a : nat,
power_v1_aux x (S n') a =
power_v1_aux x n' (x * a).
Proof.
fold_unfold_tactic power_v1_aux.
Qed.
We are now equipped to reason equationally about these two implementations to prove their equivalence:
Theorem power_v0_and_power_v1_are_equivalent :
forall x n : nat,
power_v0 x n = power_v1 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_v1:
unfold power_v1.
The *goal* window reads:
x, n : nat
============================
power_v0 x n = power_v1_aux 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_v0 and power_v1_aux, which can only be done by suitably combining power_v0 x n and a in the left-hand side of the goal:
Lemma power_v0_and_power_v1_are_equivalent_aux :
forall x n a : nat,
suitable_combination (power_v0 x n) a = power_v1_aux 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_v0 x n * a:
Lemma power_v0_and_power_v1_are_equivalent_aux :
forall x n a : nat,
power_v0 x n * a = power_v1_aux 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_v0 x 0 * a = power_v1_aux x 0 a
In this base case, We can use the fold-unfold lemmas for the O case:
rewrite -> (fold_unfold_power_v0_O x).
rewrite -> (fold_unfold_power_v1_aux_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_v0_S x n').
rewrite -> (fold_unfold_power_v1_aux_S x n' a).
The *goals* window reads:
x, n' : nat
IHn' : forall a : nat, power_v0 x n' * a = power_v1_aux x n' a
a : nat
============================
x * power_v0 x n' * a = power_v1_aux 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_v0 x n' * (x * a) = power_v1_aux 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_v0 x n' * a = power_v1_aux x n' a
a : nat
============================
x * power_v0 x n' * a = power_v0 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_v0 x n')).
Check Nat.mul_assoc.
symmetry.
exact (Nat.mul_assoc (power_v0 x n') x a).
Qed.
Thus equipped, the main theorem is indeed proved as a corollary of the auxiliary lemma:
Theorem power_v0_and_power_v1_are_equivalent :
forall x n : nat,
power_v0 x n = power_v1 x n.
Proof.
intros x n.
unfold power_v1.
Check (power_v0_and_power_v1_are_equivalent_aux x n 1).
rewrite <- (Nat.mul_1_r (power_v0 x n)).
exact (power_v0_and_power_v1_are_equivalent_aux x n 1).
Qed.
State (and prove) the fold-unfold lemmas associated with the Fibonacci function.
The Fibonacci function is implemented as follows:
Fixpoint fib_v1 (n : nat) : nat :=
match n with
0 =>
0
| S n' =>
match n' with
0 =>
1
| S n'' =>
fib_v1 n' + fib_v1 n''
end
end.
This recursive function gives rise to the following two fold-unfold lemmas:
Lemma fold_unfold_fib_v1_O :
fib_v1 O =
0.
Proof.
fold_unfold_tactic fib_v1.
Qed.
Lemma fold_unfold_fib_v1_S :
forall n' : nat,
fib_v1 (S n') =
match n' with
0 =>
1
| S n'' =>
fib_v1 n' + fib_v1 n''
end.
Proof.
fold_unfold_tactic fib_v1.
Qed.
If one wishes to have two more fold-unfold lemmas, they can be proved as corollaries of these two:
Corollary fold_unfold_fib_v1_1 :
fib_v1 1 =
1.
Proof.
rewrite -> (fold_unfold_fib_v1_S 0).
reflexivity.
Qed.
Corollary fold_unfold_fib_v1_SS :
forall n'' : nat,
fib_v1 (S (S n'')) =
fib_v1 (S n'') + fib_v1 n''.
Proof.
intro n''.
rewrite -> (fold_unfold_fib_v1_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 nodes:
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 mirror 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 the executive summary about when to use the induction tactic [14 Feb 2024]
Created [09 Feb 2024]