The goal of this chapter is to illustrate how to use a specification to state another specification.
Here are again the specifications of the addition function over Peano numbers, one recursive, and one tail recursive:
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)).
Definition tail_recursive_specification_of_addition (add : nat -> nat -> nat) :=
(forall y : nat,
add O y = y)
/\
(forall x' y : nat,
add (S x') y = add x' (S y)).
In Week 03, we have proved properties such as the following one:
Theorem O_is_left_neutral_for_recursive_addition :
forall add : nat -> nat -> nat,
recursive_specification_of_addition add ->
forall n : nat,
add 0 n = n.
Here is a recursive specification of the multiplication function over natural numbers:
Definition recursive_specification_of_multiplication (mul : nat -> nat -> nat) :=
forall add : nat -> nat -> nat,
recursive_specification_of_addition add ->
(forall y : nat,
mul O y = 0)
/\
(forall x' y : nat,
mul (S x') y = add (mul x' y) y).
This specification assumes (and therefore is parameterized by) an addition function that satisfies the recursive specification of addition.
Dana: How about we prove that for any function that satisfies the specification of multiplication, 0 is left-absorbing:
Property O_is_left_absorbing_wrt_multiplication :
forall add : nat -> nat -> nat,
recursive_specification_of_addition add ->
forall mul : nat -> nat -> nat,
recursive_specification_of_multiplication mul ->
forall y : nat,
mul 0 y = 0.
Anton: Well, we can start the proof by assuming an addition function and a multiplication function:
Proof.
intros add S_add mul S_mul.
Pablito: The *goals* window reads as follows:
add : nat -> nat -> nat
S_add : recursive_specification_of_addition add
mul : nat -> nat -> nat
S_mul : recursive_specification_of_multiplication mul
============================
forall y : nat, mul 0 y = 0
Anton: For convenience, let us keep S_mul among the assumptions, and let us destructure its component via a temporary copy:
assert (S_tmp := S_mul).
unfold recursive_specification_of_multiplication in S_tmp.
Pablito: The *goals* window reads as follows:
add : nat -> nat -> nat
S_add : recursive_specification_of_addition add
mul : nat -> nat -> nat
S_mul : recursive_specification_of_multiplication mul
S_tmp : forall add : nat -> nat -> nat,
recursive_specification_of_addition add ->
(forall y : nat, mul 0 y = 0) /\
(forall x' y : nat, mul (S x') y = add (mul x' y) y)
============================
forall y : nat, mul 0 y = 0
Anton: Let’s see. S_tmp expects an addition function – which we have in the form of add – and a proof that this function satisfies the specification of addition – which we have in the form of S_add:
Check (S_tmp add S_add).
Pablito: The *response* window reads as follows:
S_tmp add S_add
: (forall y : nat, mul 0 y = 0) /\ (forall x' y : nat, mul (S x') y = add (mul x' y) y)
Anton: Let us destructure this conjunction and meaningfully name its components:
destruct (S_tmp add S_add) as [S_mul_O _].
Pablito: The *goals* window reads as follows:
add : nat -> nat -> nat
S_add : recursive_specification_of_addition add
mul : nat -> nat -> nat
S_mul : recursive_specification_of_multiplication mul
S_tmp : forall add : nat -> nat -> nat,
recursive_specification_of_addition add ->
(forall y : nat, mul 0 y = 0) /\ (forall x' y : nat, mul (S x') y = add (mul x' y) y)
S_mul_O : forall y : nat, mul 0 y = 0
============================
forall y : nat, mul 0 y = 0
Anton: The temporary assumption has fulfilled its mission, so let us discard it:
clear S_tmp.
Pablito: The *goals* window reads as follows:
add : nat -> nat -> nat
S_add : recursive_specification_of_addition add
mul : nat -> nat -> nat
S_mul : recursive_specification_of_multiplication mul
S_mul_O : forall y : nat, mul 0 y = 0
============================
forall y : nat, mul 0 y = 0
Anton: Since the goal lies among the assumptions, we can complete the proof:
exact S_mul_O.
Halcyon: Yay!
Bong-sun: Hum.
Dana: Yes?
Bong-sun: Do we really need to quantify add in the statement of Property O_is_left_absorbing_wrt_multiplication?
Dana: Hum indeed. What if we didn’t?
Bong-sun: Let’s see:
Property O_is_left_absorbing_wrt_multiplication_alt :
forall mul : nat -> nat -> nat,
recursive_specification_of_multiplication mul ->
forall y : nat,
mul 0 y = 0.
Dana: Right. Now the proof starts as before – minus add and the specification of addition, since they are not in the statement:
Proof.
intros mul S_mul.
assert (S_tmp := S_mul).
unfold recursive_specification_of_multiplication in S_tmp.
Pablito (diligent): The *goals* window reads:
mul : nat -> nat -> nat
S_mul : recursive_specification_of_multiplication mul
S_tmp : forall add : nat -> nat -> nat,
recursive_specification_of_addition add ->
(forall y : nat, mul 0 y = 0) /\ (forall x' y : nat, mul (S x') y = add (mul x' y) y)
============================
forall y : nat, mul 0 y = 0
Bong-sun: Oh. We need an addition function and its specification to use S_tmp.
Dana: Assume we have one, namely add_v1:
Fixpoint add_v1 (i j : nat) : nat :=
match i with
O =>
j
| S i' =>
S (add_v1 i' j)
end.
Bong-sun: We now have a first argument for S_tmp:
Check (S_tmp add_v1).
Pablito (obligingly): The *response* window reads:
S_tmp add_v1
: recursive_specification_of_addition add_v1 ->
(forall y : nat, mul 0 y = 0) /\ (forall x' y : nat, mul (S x') y = add_v1 (mul x' y) y)
Alfrothul: And assume that we have proved that add_v1 satisfies the recursive specication of the addition function:
Theorem add_v1_satisfies_the_recursive_specification_of_addition :
recursive_specification_of_addition add_v1.
Proof.
Admitted.
Bong-sun: Ah, right. So we also have a second argument for S_tmp:
Check (S_tmp add_v1 add_v1_satisfies_the_recursive_specification_of_addition).
Pablito: The *response* window reads:
S_tmp add_v1 add_v1_satisfies_the_recursive_specification_of_addition
: (forall y : nat, mul 0 y = 0) /\ (forall x' y : nat, mul (S x') y = add_v1 (mul x' y) y)
Dana: So we are good to go:
destruct (S_tmp add_v1 add_v1_satisfies_the_recursive_specification_of_addition) as [S_mul_O _].
clear S_tmp.
exact S_mul_O.
Bong-sun: OK. So we don’t need to quantify add in the statement of Property O_is_left_absorbing_wrt_multiplication if we already have declared an addition function and if we have proved that it satisfies the specification of addition.
Mimer: Yup.
Alfrothul: Along the same line, we prove that for any function that satisfies the specification of multiplication, 1 is left neutral:
Property SO_is_left_neutral_wrt_multiplication :
forall add : nat -> nat -> nat,
recursive_specification_of_addition add ->
forall mul : nat -> nat -> nat,
recursive_specification_of_multiplication mul ->
forall y : nat,
mul 1 y = y.
Anton (wisely): In other words, 1 is a left identity.
Bong-sun: As before, we can start the proof by assuming such a function and that this function satisfies the specification of multiplication, and let us tease out the specification of both base case and induction step for this assumed function.
Pablito: Dibs on this proof! Let us get started:
Proof.
intros add S_add mul S_mul.
Dana: This looks like a case of mutatis mutandis.
Halcyon: Maybe so, but now is not the time to speak Latin, quod erat demonstrandum notwithstanding. Let us do mathematics and dance on the music of the spheres!
Dana: Er, you’re OK, Halcyon?
Halcyon: Joking. Please, Pablito.
Pablito: Thanks. Now for teasing out the specification of the base case and of induction step assumed function... Let me alias S_mul and then destructure the denotation of the alias:
assert (S_tmp := S_mul).
unfold recursive_specification_of_multiplication in S_tmp.
Check (S_tmp add S_add).
destruct (S_tmp add S_add) as [S_mul_O S_mul_S].
clear S_tmp.
Halcyon: The *goals* window reads as follows:
add : nat -> nat -> nat
S_add : recursive_specification_of_addition add
mul : nat -> nat -> nat
S_mul : recursive_specification_of_multiplication mul
S_mul_O : forall y : nat, mul 0 y = 0
S_mul_S : forall x' y : nat, mul (S x') y = add (mul x' y) y
============================
forall y : nat, mul 1 y = y
Pablito: Assuming such a y, the goal is an instance of S_mul_S:
intro y.
Check (S_mul_S 0 y).
Halcyon: The *response* window reads as follows:
S_mul_S 0 y
: mul 1 y = add (mul 0 y) y
Pablito: We can thus replace mul 1 y in the goal by add (mul 0 y) y using the rewrite tactic from left to right:
rewrite -> (H_mul_S 0 y).
Halcyon: The *goals* window now reads:
add : nat -> nat -> nat
S_add : recursive_specification_of_addition add
mul : nat -> nat -> nat
S_mul : recursive_specification_of_multiplication mul
S_mul_O : forall y : nat, mul 0 y = 0
S_mul_S : forall x' y : nat, mul (S x') y = add (mul x' y) y
y : nat
============================
add (mul 0 y) y = y
Pablito (on a roll): The goal contains an instance of S_mul_O, so let us replace mul 0 y by 0 using the rewrite tactic from left to right:
rewrite -> (S_mul_O y).
Halcyon: The *goals* window now reads:
add : nat -> nat -> nat
S_add : recursive_specification_of_addition add
mul : nat -> nat -> nat
S_mul : recursive_specification_of_multiplication mul
S_mul_O : forall y : nat, mul 0 y = 0
S_mul_S : forall x' y : nat, mul (S x') y = add (mul x' y) y
y : nat
============================
add 0 y = y
Pablito: Since add satisfies the specification of addition, we can use Property O_is_neutral_on_the_left_of_add:
Check (O_is_neutral_on_the_left_of_add add S_add y).
Halcyon: The *response* window reads:
O_is_left_neutral_wrt_addition add S_add y
: add 0 y = y
Pablito: Since this instance of Property O_is_neutral_on_the_left_of_add coincides with the goal, we can complete the proof:
exact (O_is_left_neutral_wrt_addition add S_add y).
Dana: So, mutatis mutandis?
Pablito (who followed the wiktionary pointer): Mutatis mutandis.
Prove that 0 is right absorbing with respect to multiplication:
Property O_is_right_absorbing_wrt_multiplication :
forall add : nat -> nat -> nat,
recursive_specification_of_addition add ->
forall mul : nat -> nat -> nat,
recursive_specification_of_multiplication mul ->
forall x : nat,
mul x 0 = 0.
The solution is in the accompanying file.
Prove that 1 is right neutral with respect to multiplication:
Property SO_is_right_neutral_wrt_multiplication :
forall add : nat -> nat -> nat,
recursive_specification_of_addition add ->
forall mul : nat -> nat -> nat,
recursive_specification_of_multiplication mul ->
forall x : nat,
mul x 1 = x.
(In other words, 1 is a right identity).
The solution is in the accompanying file.
Prove that multiplication is right-distributive over addition:
Property multiplication_is_right_distributive_over_addition :
forall add : nat -> nat -> nat,
recursive_specification_of_addition add ->
forall mul : nat -> nat -> nat,
recursive_specification_of_multiplication mul ->
forall x y z : nat,
mul (add x y) z = add (mul x z) (mul y z).
Prove that multiplication is associative:
Property multiplication_is_associative :
forall add : nat -> nat -> nat,
recursive_specification_of_addition add ->
forall mul : nat -> nat -> nat,
recursive_specification_of_multiplication mul ->
forall x y z : nat,
mul x (mul y z) = mul (mul x y) z.
Prove that multiplication is commutative:
Property multiplication_is_commutative :
forall add : nat -> nat -> nat,
recursive_specification_of_addition add ->
forall mul : nat -> nat -> nat,
recursive_specification_of_multiplication mul ->
forall x y : nat,
mul x y = mul y x.
Prove that multiplication is left-distributive over addition:
Property multiplication_is_left_distributive_over_addition :
forall add : nat -> nat -> nat,
recursive_specification_of_addition add ->
forall mul : nat -> nat -> nat,
recursive_specification_of_multiplication mul ->
forall x y z : nat,
mul x (add y z) = add (mul x y) (mul x z).
This property can be proved as a corollary of multiplication being commutative (Exercise 05) and right-distributive over addition (Exercise 03):
Proof.
intros add S_add mul S_mul z x y.
rewrite -> (multiplication_is_commutative mul S_mul z (add x y)).
rewrite -> (multiplication_is_commutative mul S_mul z x).
rewrite -> (multiplication_is_commutative mul S_mul z y).
exact (multiplication_is_right_distributive_over_addition add S_add mul S_mul x y z).
Qed.
(Note the judicious introduction of z, x, and y, in that order.)
Anton: All these properties must already exist in the libraries.
Alfrothul: Let’s start with 0 being left-absorbing with respect to multiplication:
Search (0 * _ = 0).
Anton: Bingo. The *response* window reads:
Nat.mul_0_l : forall n : nat, 0 * n = 0
Dana: The library naming conventions being what they are, let me make an educated guess:
Check Nat.mul_0_r.
Alfrothul: Righto. The *response* window reads:
Nat.mul_0_r : forall n : nat, n * 0 = 0
Anton: What about 1 being left-neutral with respect to multiplication? Let me see:
Search (1 * _ = _).
Alfrothul: The library provides:
Nat.mul_1_l: forall n : nat, 1 * n = n
Pablito: I got this:
Check Nat.mul_1_r.
Dana: You got it indeed, Pablito:
Nat.mul_1_r : forall n : nat, n * 1 = n
Anton: As for multiplication being right-distributive over addition:
Search ((_ + _) * _ = _).
Alfrothul: The librarians have been there and done that:
Nat.mul_add_distr_r : forall n m p : nat, (n + m) * p = n * p + m * p
Anton: And logically:
Check Nat.mul_add_distr_l.
Alfrothul: Indeed. Check out the *response* window:
Nat.mul_add_distr_l : forall n m p : nat, n * (m + p) = n * m + n * p
Pablito: What about the associativity of multiplication? Let me see:
Search ((_ * _) * _ = _).
Alfrothul: The *response* window displays several answers, one of them being:
mult_assoc_reverse: forall n m p : nat, n * m * p = n * (m * p)
Anton: How about we change the association in the query:
Search (_ * (_ * _) = _).
Alfrothul: Ah, right:
Nat.mul_assoc: forall n m p : nat, n * (m * p) = n * m * p
Pablito: And let me guess:
Check Nat.mul_comm.
Dana: Good guess:
Nat.mul_comm : forall n m : nat, n * m = m * n
Bong-sun: The same should hold for addition, right?
Dana: Yes it does. Identity element for addition on the left, here we come:
Check Nat.add_0_l.
Bong-sun: Indeed:
Nat.add_0_l : forall n : nat, 0 + n = n
Pablito: Let me guess:
Check Nat.add_0_r.
Bong-sun: Indeed:
Nat.add_0_r : forall n : nat, n + 0 = n
Anton: Let me guess too:
Check Nat.add_comm.
Pablito: Indeed:
Nat.add_comm : forall n m : nat, n + m = m + n
Alfrothul: My turn:
Check Nat.add_assoc.
Pablito: Indeed:
Nat.add_assoc : forall n m p : nat, n + (m + p) = n + m + p
Bong-sun: Good logic in the names of the Nat library.
Dana: Yup. We don’t need to remember them all, we can just reconstruct them based on the naming convention.
Loki: They could be shorter though, e.g., three letters. Nat.add_com would be simpler, wouldn’t it?
Mimer: Great idea, Loki. Then associativity in the Coq Proof Assistant would be so much more fun.
Halcyon (wistfully): What’s in a name?
Created [09 Feb 2024]