The goal of this lecture note is to prove the soundness and the completeness of a function that satisfies a specification. For example:
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)).
Proposition soundness_of_recursive_addition :
forall add : nat -> nat -> nat,
recursive_specification_of_addition add ->
forall i j k : nat,
add i j = k ->
i + j = k.
Proposition completeness_of_recursive_addition :
forall add : nat -> nat -> nat,
recursive_specification_of_addition add ->
forall i j k : nat,
i + j = k ->
add i j = k.
In words:
I can resist everything except temptation.
The temptation is strong to be clever about this, and so let’s succumb to it and state a Eureka lemma that will make it possible to prove soundness and completeness as corollaries:
Lemma about_a_recursive_addition :
forall add : nat -> nat -> nat,
recursive_specification_of_addition add ->
forall i j : nat,
add i j = i + j.
This lemma is proved by routine induction, and the two propositions above follow as corollaries:
Proposition soundness_of_recursive_addition :
forall add : nat -> nat -> nat,
recursive_specification_of_addition add ->
forall i j k : nat,
add i j = k ->
i + j = k.
Proof.
intros add S_add i j k H_k.
symmetry.
rewrite <- H_k.
exact (about_a_recursive_addition add S_add i j).
Qed.
Proposition completeness_of_recursive_addition :
forall add : nat -> nat -> nat,
recursive_specification_of_addition add ->
forall i j k : nat,
i + j = k ->
add i j = k.
Proof.
intros add S_add i j k H_k.
rewrite <- H_k.
exact (about_a_recursive_addition add S_add i j).
Qed.
Still, it is instructive to prove each of these propositions independently. They give rise to situations where we have the use for three new tactics: injection, discriminate, and contradiction.
On the occasion, an assumption consists in an equality over composite values, e.g., pairs. The injection tactic makes it possible to name the equalities of the components of these pairs. Here is a simple example:
Lemma about_decomposing_a_pair_using_the_injection_tactic :
forall i j : nat,
(i, j) = (0, 1) ->
i = 0 /\ j = 1.
Proof.
intros i j H_ij.
The *goals* window then reads:
i, j : nat
H_ij : (i, j) = (0, 1)
============================
i = 0 /\ j = 1
Applying the injection tactic to H_ij creates a chain of implications equating the components of the pair, depth first and from left to right:
injection H_ij.
The *goals* window then reads:
i, j : nat
H_ij : (i, j) = (0, 1)
============================
j = 1 -> i = 0 -> i = 0 /\ j = 1
Rather than forcing its user to then use the intro rule, tCPA offers them the option to name the resulting assumptions:
Restart.
intros i j H_ij.
injection H_ij as H_i H_j.
The *goals* window then reads:
i, j : nat
H_i : i = 0
H_j : j = 1
============================
i = 0 /\ j = 1
It is then simple to complete the proof:
exact (conj H_i H_j).
Qed.
The order of the equations matches that of the pairs at hand. In the example above, let us modify (i, j) = (0, 1) into (i, 1) = (0, j), and prove the modified lemma:
Lemma about_decomposing_a_pair_using_the_injection_tactic' :
forall i j : nat,
(i, 1) = (0, j) ->
i = 0 /\ j = 1.
Proof.
intros i j H_ij.
injection H_ij as H_i H_j.
The *goals* window then reads:
i, j : nat
H_i : i = 0
H_j : 1 = j
============================
i = 0 /\ j = 1
Because of the modification, the assumption H_j now reads 1 = j. The rest of the proof takes this swap into account:
symmetry in H_j.
exact (conj H_i H_j).
Qed.
The nesting of values is arbitrary:
Lemma about_decomposing_a_pair_of_pairs_using_the_injection_tactic :
forall a b c d: nat,
((a, 1), (2, d)) = ((0, b), (c, 3)) ->
a = 0 /\ b = 1 /\ c = 2 /\ d = 3.
Proof.
intros a b c d H_abcd.
injection H_abcd as H_a H_b H_c H_d.
The *goals* window then reads:
a, b, c, d : nat
H_a : a = 0
H_b : 1 = b
H_c : 2 = c
H_d : d = 3
============================
a = 0 /\ b = 1 /\ c = 2 /\ d = 3
The rest of the proof is in the accompanying .v file.
On occasion, when enumerating cases, we find ourselves with something that does not hold among the assumptions:
Warning
Using the contradiction tactic does not mean that we are performing a proof by contradiction (i.e., assuming that a hypothesis does not hold, deriving a contradiction, and concluding that the hypothesis must hold, based on the law of the excluded middle). It is just an unfortunate homonymy.
For a first example, consider the following proposition:
Proposition true_is_not_false :
true <> false.
Proof.
unfold not.
intro H_absurd.
discriminate H_absurd.
Qed.
Since A <> B is syntactic sugar for A = B -> False, let us make do without this syntactic sugar:
Proof.
unfold not.
The *goals* window then reads:
============================
true = false -> False
Since the goal is an implication, we use the intro tactic, naming this premiss H_absurd:
intro H_absurd.
The *goals* window then reads:
H_absurd : true = false
============================
False
The assumption is a Leibniz equality where the left-hand side uses one datatype constructor (namely false) and the right-hand side uses another datatype constructor (namely true). That is the reason of being for the discriminate tactic:
discriminate H_absurd.
And the proof is complete.
For a second example, consider the following proposition:
Proposition now_what :
(forall n : nat, n = S n) <-> 0 = 1.
The beginning of its proof is business as usual:
Proof.
split.
- intro H_n_Sn.
At that point the *goals* window reads:
H_n_Sn : forall n : nat, n = S n
============================
0 = 1
The goal is an instance of H_n_Sn:
Check (H_n_Sn 0).
Indeed the *response* window reads:
H_n_Sn 0
: 0 = 1
We can therefore conclude this subgoal and move to the other one:
exact (H_n_Sn 0).
- intro H_absurd.
The *goals* window then reads:
H_absurd : 0 = 1
============================
forall n : nat, n = S n
The assumption 0 = 1 is an equality involving distinct data constructors (namely 0 and S since 1 is syntactic sugar for S O). So we use the discriminate tactic to complete the proof:
discriminate H_absurd.
Alternatively, we could also use the discriminate tactic to prove the first implication:
Restart.
split.
- intro H_n_Sn.
At that point the *goals* window reads:
H_n_Sn : forall n : nat, n = S n
============================
0 = 1
Applying H_n_Sn to any natural number yields an equality that does not hold. For example:
Check (H_n_Sn 42).
Then the *response* window reads:
H_n_Sn 42
: 42 = 43
We can then apply the discriminate tactic to this equality to complete this subgoal:
discriminate (H_n_Sn 42).
Here is a similar example:
Proposition what_now :
forall n : nat,
n = S n <-> 0 = 1.
The beginning of its proof is business as usual:
Proof.
intro n.
split.
- intro H_n.
At that point the *goals* window reads:
n : nat
H_n : n = S n
============================
0 = 1
A quick search leads us to Lemma n_Sn:
Search (_ <> S _).
Check (n_Sn n).
Indeed the *response* window reads:
n_Sn n
: n <> S n
Since n <> S n is syntactic sugar for n = S n -> False, let us make it appear as such:
assert (H_tmp := n_Sn n).
unfold not in H_tmp.
The *goals* window now reads:
n : nat
H_n : n = S n
H_tmp : n = S n -> False
============================
0 = 1
Applying H_tmp to H_n yields False:
Check (H_tmp H_n).
Indeed the *response* window reads:
H_tmp H_n
: False
We can thus apply the contradiction tactic to this application to complete proving this subgoal and move on to the next:
contradiction (H_tmp H_n).
-
The *goals* window now reads:
n : nat
============================
0 = 1 -> n = S n
We can then proceed as in the previous example: name the assumption 0 = 1 and exploit the fact that it equates two values with distinct data constructors:
- intro H_absurd.
discriminate H_absurd.
Qed.
We can now revisit the proposition about the soundness of functions that satisfy the recursive specification of addition (see the accompanying .v file). In the course of proving this proposition, the *goals* window reads:
add : nat -> nat -> nat
S_add_O : forall y : nat, add 0 y = y
S_add_S : forall x' y : nat, add (S x') y = S (add x' y)
i' : nat
IHi' : forall j k : nat, add i' j = k -> i' + j = k
j, k : nat
H_add : S (add i' j) = k
============================
S i' + j = k
The next step in this proof is to distinguish whether k denotes zero or the successor of another Peano number (let us name it k'). To this end, we use the case tactic (which is akin to the destruct tactic):
case k as [ | k'].
This tactic creates two subgoals, one where k denotes O and the other where k denotes S k'.
In the first case, the *goals* window reads:
add : nat -> nat -> nat
S_add_O : forall y : nat, add 0 y = y
S_add_S : forall x' y : nat, add (S x') y = S (add x' y)
i' : nat
IHi' : forall j k : nat, add i' j = k -> i' + j = k
j : nat
H_add : S (add i' j) = 0
============================
S i' + j = 0
This first case is proved using the discriminate tactic:
+ discriminate H_add.
In the second case, the *goals* window reads:
add : nat -> nat -> nat
S_add_O : forall y : nat, add 0 y = y
S_add_S : forall x' y : nat, add (S x') y = S (add x' y)
i' : nat
IHi' : forall j k : nat, add i' j = k -> i' + j = k
j, k' : nat
H_add : S (add i' j) = S k'
============================
S i' + j = S k'
Using the injection tactic gets rid of the S constructor in H_add, so that we can use the induction hypothesis:
+ injection H_add as H_add.
Check (IHi' j k').
The *response* window then reads:
IHi' j k' : add i' j = k' -> i' + j = k'
Applying the induction hypothesis further gives us an actionable Leibniz equality:
Check (IHi' j k' H_add).
Indeed the *response* window reads:
IHi' j k' H_add : i' + j = k'
We can now revisit the proposition about the completeness of functions that satisfy the recursive specification of addition (see the accompanying .v file). In this revisitation, the induction step is proved using case, discriminate, and injection.
Out of the soundness and the completeness, we can prove properties as corollaries of other properties. For example, knowing that addition over Peano numbers is associative (Nat.add_assoc), we can prove that any function that satisfies the recursive specification of addition is also associative:
Corollary associativity_of_recursive_addition :
forall add : nat -> nat -> nat,
recursive_specification_of_addition add ->
forall i j k : nat,
add i (add j k) = add (add i j) k.
Witness the accompanying .v file, we can use either about_a_recursive_addition or soundness_of_recursive_addition 4 times, one for each occurrence of add in the goal, and then Nat.add_assoc. In the latter case, we also use the property that equality is reflexive, eq_refl.
Likewise, assuming that we have proved that any function that satisfies the recursive specification of addition is also commutative, we can prove that the resident addition over Peano numbers is commutative:
Lemma commutativity_of_recursive_addition :
forall add : nat -> nat -> nat,
recursive_specification_of_addition add ->
forall i j : nat,
add i j = add j i.
Proof.
Admitted. (* for the sake of the argument *)
Corollary commutativity_of_Nat_dot_add :
forall add : nat -> nat -> nat,
recursive_specification_of_addition add ->
forall i j : nat,
i + j = j + i.
Witness the accompanying .v file, we can use either about_a_recursive_addition or completeness_of_recursive_addition and eq_refl twice, one for each occurrence of + in the goal, and then commutativity_of_recursive_addition.
Prove the soundness and the completeness of a function that satisfies the tail-recursive specification of addition.