Unit tests are sound whenever they always succeed for an implementation that satisfies the specification of the function to test.
The goal of this lecture note is to illustrate how the proof steps, in the course of the soundness proof, carry out the computation steps in the unit tests.
Let us revisit the recursive specification of addition:
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)).
Unit tests being intrinsically incomplete, here is a very incomplete unit-test function:
Definition test_add (candidate : nat -> nat -> nat) :=
(candidate 0 2 =? 2) && (candidate 2 0 =? 2) && (candidate 2 2 =? 4).
A unit-test function is said to be sound if it succeeds given a function that satisfies the given specification. Formally:
Theorem soundness_of_test_add_for_recursive_specification_of_addition :
forall add : nat -> nat -> nat,
recursive_specification_of_addition add ->
test_add add = true.
Let us start the proof:
Proof.
intro add.
unfold recursive_specification_of_addition.
intros [H_add_O H_add_S].
unfold test_add.
The *goal* window reads:
add : nat -> nat -> nat
H_add_O : forall y : nat, add 0 y = y
H_add_S : forall x' y : nat, add (S x') y = S (add x' y)
============================
(add 0 2 =? 2) && (add 2 0 =? 2) && (add 2 2 =? 4) = true
The left-most conjunct is an instance of H_add_O:
Check (H_add_O 2).
And indeed the *response* window reads:
H_add_O 2
: add 0 2 = 2
So let us replace add 0 2 by 2 in the goal:
rewrite -> (H_add_O 2).
The *goal* window reads:
add : nat -> nat -> nat
H_add_O : forall y : nat, add 0 y = y
H_add_S : forall x' y : nat, add (S x') y = S (add x' y)
============================
(2 =? 2) && (add 2 0 =? 2) && (add 2 2 =? 4) = true
Let us query the Arith library about the Boolean equality of two natural numbers:
Search (_ =? _).
The *response* window reads, among others:
beq_nat_refl: forall n : nat, true = (n =? n)
Let us instantiate beq_nat_refl:
Check (beq_nat_refl 2).
The *response* window reads:
beq_nat_refl 2
: true = (2 =? 2)
So let us replace (2 =? 2) by true in the goal:
rewrite <- (beq_nat_refl 2).
The *goal* window reads:
add : nat -> nat -> nat
H_add_O : forall y : nat, add 0 y = y
H_add_S : forall x' y : nat, add (S x') y = S (add x' y)
============================
true && (add 2 0 =? 2) && (add 2 2 =? 4) = true
Let us query the Bool library about true being left-neutral for Boolean conjunction:
Search (true && _ = _).
The *response* window reads:
andb_true_l: forall b : bool, true && b = b
To instantiate andb_true_l, we need to know whether && associates to the left or to the right:
Check (forall x y z : bool, x && (y && z) = (x && y) && z).
Since the *response* window reads forall x y z : bool, x && (y && z) = x && y && z : Prop, the answer is “to the left”. So let us instantiate andb_true_l with (add 2 0 =? 2):
Check (andb_true_l (add 2 0 =? 2)).
The *response* window reads:
andb_true_l (add 2 0 =? 2)
: true && (add 2 0 =? 2) = (add 2 0 =? 2)
So let us replace true && (add 2 0 =? 2) by (add 2 0 =? 2) in the goal:
rewrite -> (andb_true_l (add 2 0 =? 2)).
The *goal* window reads:
add : nat -> nat -> nat
H_add_O : forall y : nat, add 0 y = y
H_add_S : forall x' y : nat, add (S x') y = S (add x' y)
============================
(add 2 0 =? 2) && (add 2 2 =? 4) = true
It looks like the left-most conjunct is an instance of H_add_S:
Check (H_add_S 1 0).
And indeed the *response* window reads:
H_add_S 1 0
: add 2 0 = S (add 1 0)
On the other hand, it also looks like the right-most conjunct is also an instance of H_add_S:
H_add_S 1 2
: add 2 2 = S (add 1 2)
And indeed the *response* window reads:
H_add_S 1 2
: add 2 2 = S (add 1 2)
So let us treat them both at once by declaring a local lemma:
assert (H_add_2 : forall y : nat, add 2 y = S (S y)).
Proving this local lemma is simple:
{ intro y.
rewrite -> (H_add_S 1 y).
rewrite -> (H_add_S 0 y).
rewrite -> (H_add_O y).
reflexivity. }
The *goal* window now reads:
add : nat -> nat -> nat
H_add_O : forall y : nat, add 0 y = y
H_add_S : forall x' y : nat, add (S x') y = S (add x' y)
H_add_2 : forall y : nat, add 2 y = S (S y)
============================
(add 2 0 =? 2) && (add 2 2 =? 4) = true
We can use an instance of H_add_2 to simplify the left conjunct:
Check (H_add_2 0).
And indeed the *response* window reads:
H_add_2 0
: add 2 0 = 2
So let us replace add 2 0 by 2 in the goal:
rewrite -> (H_add_2 0).
The *goal* window now reads:
add : nat -> nat -> nat
H_add_O : forall y : nat, add 0 y = y
H_add_S : forall x' y : nat, add (S x') y = S (add x' y)
H_add_2 : forall y : nat, add 2 y = S (S y)
============================
(2 =? 2) && (add 2 2 =? 4) = true
As earlier, we can simplify 2 =? 2 to true and true && (add 2 2 =? 4) to (add 2 2 =? 4):
rewrite <- (beq_nat_refl 2).
rewrite -> (andb_true_l (add 2 2 =? 4)).
The *goal* window now reads:
add : nat -> nat -> nat
H_add_O : forall y : nat, add 0 y = y
H_add_S : forall x' y : nat, add (S x') y = S (add x' y)
H_add_2 : forall y : nat, add 2 y = S (S y)
============================
(add 2 2 =? 4) = true
Let us simplify add 2 2 into S (S 2), i.e., 4, using H_add_2:
rewrite -> (H_add_2 2).
The *goal* window now reads:
add : nat -> nat -> nat
H_add_O : forall y : nat, add 0 y = y
H_add_S : forall x' y : nat, add (S x') y = S (add x' y)
H_add_2 : forall y : nat, add 2 y = S (S y)
============================
(4 =? 4) = true
This is a job for beq_nat_refl:
rewrite <- (beq_nat_refl 4).
The *goal* window now reads:
add : nat -> nat -> nat
H_add_O : forall y : nat, add 0 y = y
H_add_S : forall x' y : nat, add (S x') y = S (add x' y)
H_add_2 : forall y : nat, add 2 y = S (S y)
============================
true = true
And we are one proof step away from concluding the proof:
reflexivity.
Qed.
In effect, we have carried out the computation of test_add add = true, proof step after proof step.
Prove that test_add is also sound for the tail-recursive specification of addition.
Occasionally, the goal involves expressions and proving this goal solely amounts to carry out the computation of these expressions. As an alternative to carrying out these computations proof step after proof step, tCPA offers the compute tactic that carries out these computations at once.
Let us revisit the soundness of the unit-test function for addition. We could reorder its proof steps so that we are left with a goal that is a candidate for the compute tactic:
Theorem soundness_of_test_add_for_the_recursive_specification_of_addition :
forall add : nat -> nat -> nat,
recursive_specification_of_addition add ->
test_add add = true.
Proof.
...
Restart.
intro add.
unfold recursive_specification_of_addition.
intros [H_add_O H_add_S].
unfold test_add.
rewrite -> (H_add_O 2).
assert (H_add_2 : forall y : nat, add 2 y = S (S y)).
{ intro y.
rewrite -> (H_add_S 1 y).
rewrite -> (H_add_S 0 y).
rewrite -> (H_add_O y).
reflexivity. }
rewrite -> (H_add_2 0).
rewrite -> (H_add_2 2).
The *goals* window then reads:
add : nat -> nat -> nat
H_add_O : forall y : nat, add 0 y = y
H_add_S : forall x' y : nat, add (S x') y = S (add x' y)
H_add_2 : forall y : nat, add 2 y = S (S y)
============================
(2 =? 2) && (2 =? 2) && (4 =? 4) = true
The remaining proof steps solely involve the equality predicate over Peano numbers and Boolean conjunctions. We could carry them out one small step at a time:
rewrite -> (H_add_2 0).
rewrite -> (H_add_2 2).
rewrite <- (beq_nat_refl 2).
rewrite -> (andb_true_l true).
rewrite -> (andb_true_l (4 =? 4)).
rewrite <- (beq_nat_refl 4).
reflexivity.
Or we could carry them out in one big step, using the compute tactic:
compute.
reflexivity.
In essence, the compute tactic systematically unfolds all the functions that are called, and then simplifies the result. So instead of using the compute tactic just above, we could just unfold the functions (and let tCPA carry out the subsequent simplifications):
unfold beq_nat. (* "e1 =? e2" is syntactic sugar for "beq_nat e1 e2" *)
unfold andb. (* "e1 && e2" is syntactic sugar for "andb e1 e2" *)
reflexivity.
Warning
The compute tactic is easy to misuse, e.g., over goals that are not solely proved using proof steps that correspond to computation steps.
Anton: What happens if we misuse this tactic?Alfrothul: Disaster city.Philip K. Dick (meditatively): That’s what it is.Mimer: Mr. Dick! Phil! Thanks for coming by!
Revisit Exercise 08 and prove the soundness of test_add for the tail-recursive specification of addition (a) using the compute tactic and (b) using the unfold tactic.
Created [09 Feb 2024]