The goal of this lecture note is to play with the concepts of specification, implementation, satisfaction, unit tests, informal induction (yay, as in Machine Learning), and formal induction. The means to this end is to figure out which functions, if any, satisfy a series of specifications. Most specifications do not make it obvious which function exactly is specified (if one exists at all), hence the title.
This lecture note was inspired by Section 3.1 of Terence Tao‘s book Solving Mathematical Problems: A Personal Perspective, Oxford University Press, 2006.
Each mystery function is specified as follows:
Definition specification_of_the_mystery_function_XX (mf : ...) :=
...
This specification states conditions that the mystery function should satisfy... assuming that the specification uniquely determines a function, which we better prove:
Theorem there_is_at_most_one_mystery_function_XX :
forall f g : ...,
specification_of_the_mystery_function_XX f ->
specification_of_the_mystery_function_XX g ->
forall ...,
f ... = g ....
Assuming that this proof is successful, how can we figure out what this function does?
Pedestrian answer: one proceeds by tabulating the mystery function, incrementally constructing its graph and representing it as a unit test:
Definition unit_test_for_the_mystery_function_XX (mf : ...) :=
let b0 := (mf ... =x= ...) in
let b1 := (mf ... =x= ...) in
...
b0 && b1 && ....
where =x= denotes an infix Boolean comparison function and && denotes Boolean conjunction.
Typically, the tabulation follows the inductive structure of the codomain of the mystery function, until the aha! moment typical of this informal inductive reasoning, resulting in an implementation:
Definition mystery_function_XX := ...
To be on the safe side, one then verifies that the implementation passes the unit tests, i.e., that the following computation yields true:
Compute unit_test_for_the_mystery_function_XX mystery_function_XX.
And then one proves that the implementation also satisfies the specification:
Theorem there_is_at_least_one_mystery_function_XX :
specification_of_the_mystery_function_XX mystery_function_XX.
Typically, this proof is carried out by induction – a formal counterpart of the earlier informal induction.
So all in all, having proved
one has proved that there is exactly one function that satisfies the specification, and one has found this mystery function.
However, in the course of proving whether there is at most one mystery function that satisfies the specification, one may get stuck and realize that there is isn’t any. One then conjures two functions that satisfy the specification and that are distinct (i.e., that map at least one given input value to two distinct output values), and formally proves that the specification does not uniquely determine a function:
Theorem there_are_at_least_two_mystery_functions_XX :
exists f g : ...,
specification_of_the_mystery_function_XX f /\
specification_of_the_mystery_function_XX g /\
exists x : ...,
f x <> g x.
Or again one realizes that no functions exist that satisfy the specification:
Theorem there_are_zero_mystery_functions_XX :
forall mf : ...,
specification_of_the_mystery_function_XX mf ->
exists x : ...,
mf x <> mf x.
Since the two latter cases were covered in the earlier lecture note about Specifications, the rest of this lecture note illustrates the former case where the specification uniquely determines a function, however mysterious this function may seem.
Here is the specification of a mystery function:
Definition specification_of_the_mystery_function_00 (mf : nat -> nat) :=
(mf 0 = 1)
/\
(forall i j : nat,
mf (S (i + j)) = mf i + mf j).
That there is at most one such mystery function is proved by induction on n:
Theorem there_is_at_most_one_mystery_function_00 :
forall f g : nat -> nat,
specification_of_the_mystery_function_00 f ->
specification_of_the_mystery_function_00 g ->
forall n : nat,
f n = g n.
Let us start enumerating the graph of this mystery function by tabulating it:
* mf 0
= {first clause of the specification}
1
* mf 1
=
mf (S (0 + 0))
= {second clause of the specification}
mf 0 + mf 0
= {first clause of the specification, twice}
1 + 1
= 2
* mf 2
=
mf (S (1 + 0))
= {second clause of the specification}
mf 1 + mf 0
= {the item above and the first clause of the specification}
2 + 1
=
3
Let us represent this tabulation as a unit test:
Definition unit_test_for_the_mystery_function_00 (mf : nat -> nat) :=
let b0 := (mf 0 =? 1) in
let b1 := (mf 1 =? 2) in
let b2 := (mf 2 =? 3) in
b0 && b1 && b2.
where =? is an infix Boolean comparison function.
Eureka: the mystery function is the successor function:
Definition mystery_function_00 := S.
Let us check that this implementation passes the unit test:
Compute unit_test_for_the_mystery_function_00 mystery_function_00.
And finally let us prove that this implementation also satisfies the specification:
Theorem there_is_at_least_one_mystery_function_00 :
specification_of_the_mystery_function_00 mystery_function_00.
On the occasion, we may recognize the specification as a characteristic property:
Definition specification_of_the_mystery_function_03 (mf : nat -> bool) :=
(forall q : nat,
mf (2 * q) = true)
/\
(forall q : nat,
mf (S (2 * q)) = false).
Then it is up to us to recognize it as the Boolean-valued function (i.e., predicate) that detects whether its argument is even or not. We still need to prove
Created [16 Feb 2024]