The goal of this lecture note is to spell out the soundness and completeness of equality predicates:
The equality predicate for Boolean values, i.e., values of type bool, is defined in the Bool library. It is denoted by Bool.eqb (or just eqb if we have imported this library).
Its soundness and completeness is also proved in this library:
eqb_true_iff: forall a b : bool, eqb a b = true <-> a = b
Nevertheless, in the accompanying file, we have spelled out both the soundness and the completeness of the equality predicate for Boolean values:
Theorem soundness_of_equality_over_booleans :
forall b1 b2 : bool,
Bool.eqb b1 b2 = true -> b1 = b2.
Theorem completeness_of_equality_over_booleans :
forall b1 b2 : bool,
b1 = b2 -> Bool.eqb b1 b2 = true.
We have also treated the remaining case that seemingly is unstated:
Corollary soundness_of_equality_over_booleans_the_remaining_case :
forall b1 b2 : bool,
eqb b1 b2 = false -> b1 <> b2.
Corollary completeness_of_equality_over_booleans_the_remaining_case :
forall b1 b2 : bool,
b1 <> b2 -> eqb b1 b2 = false.
As it happens, this remaining case holds as a corollary of soundness and completeness.
The equality predicate for Peano numbers, i.e., values of type nat, is defined in the Arith library. It is denoted both by Nat.eqb and beq_nat, and is endowed with the infix notation =?.
Its soundness and completeness is also proved in this library:
Nat.eqb_eq: forall n m : nat, (n =? m) = true <-> n = m
Verify that the remaining case (i.e., what happens for Peano numbers that are not equal) holds as a corollary of soundness and completeness.
A polymorphic value is a value that is parameterized by a type. Accordingly, equality predicates for polymorphic values are parameterized with an equality predicate for values of that type.
The soundness and the completeness of a polymorphic predicate will depend on the soundness and the completeness of the equality predicate for the parameterized type.
The following lemma will be useful to extract the soundness property and the completeness property from a property of both soundness and completeness:
Lemma from_one_equivalence_to_two_implications :
forall (V : Type)
(eqb_V : V -> V -> bool),
(forall v1 v2 : V,
eqb_V v1 v2 = true <-> v1 = v2) ->
(forall v1 v2 : V,
eqb_V v1 v2 = true -> v1 = v2)
/\
(forall v1 v2 : V,
v1 = v2 -> eqb_V v1 v2 = true).
The equality predicate for optional values is implemented as follows:
Definition eqb_option (V : Type) (eqb_V : V -> V -> bool) (ov1 ov2 : option V) : bool :=
match ov1 with
| Some v1 =>
match ov2 with
| Some v2 =>
eqb_V v1 v2
| None =>
false
end
| None =>
match ov2 with
| Some v2 =>
false
| None =>
true
end
end.
It is parameterized with an equality predicate over the underlying values.
Its soundness and completeness is stated as follows:
Theorem soundness_and_completeness_of_equality_over_optional_values :
forall (V : Type)
(eqb_V : V -> V -> bool),
(forall v1 v2 : V,
eqb_V v1 v2 = true <-> v1 = v2) ->
forall ov1 ov2 : option V,
eqb_option V eqb_V ov1 ov2 = true <-> ov1 = ov2.
Verify that the remaining case (i.e., what happens for optional values that are not equal) holds as a corollary of soundness and completeness.
The equality predicate for pairs is implemented as follows:
Definition eqb_pair (V : Type) (eqb_V : V -> V -> bool) (W : Type) (eqb_W : W -> W -> bool) (p1 p2 : V * W) : bool :=
let (v1, w1) := p1 in
let (v2, w2) := p2 in
eqb_V v1 v2 && eqb_W w1 w2.
It is parameterized with an equality predicate for each of the values that are paired.
Its soundness and completeness is stated as follows:
Theorem soundness_and_completeness_of_equality_over_pairs :
forall (V : Type)
(eqb_V : V -> V -> bool),
(forall v1 v2 : V,
eqb_V v1 v2 = true <-> v1 = v2) ->
forall (W : Type)
(eqb_W : W -> W -> bool),
(forall w1 w2 : W,
eqb_W w1 w2 = true <-> w1 = w2) ->
forall p1 p2 : V * W,
eqb_pair V eqb_V W eqb_W p1 p2 = true <-> p1 = p2.
Verify that the remaining case (i.e., what happens for pairs that are not equal) holds as a corollary of soundness and completeness.
The polymorphic type of binary trees with payloads in the leaves is declared as follows:
Inductive binary_tree (V : Type) : Type :=
Leaf : V -> binary_tree V
| Node : binary_tree V -> binary_tree V -> binary_tree V.
The equality predicate for binary trees is implemented as follows:
Fixpoint eqb_binary_tree (V : Type) (eqb_V : V -> V -> bool) (t1 t2 : binary_tree V) : bool :=
match t1 with
Leaf _ v1 =>
match t2 with
Leaf _ v2 =>
eqb_V v1 v2
| Node _ t11 t12 =>
false
end
| Node _ t11 t12 =>
match t2 with
Leaf _ v2 =>
false
| Node _ t21 t22 =>
eqb_binary_tree V eqb_V t11 t21
&&
eqb_binary_tree V eqb_V t12 t22
end
end.
Obviously it gives rise two two fold-unfold lemmas, one when the first given tree is a leaf, and the other when it is a node.
Its soundness is stated as follows:
Theorem soundness_of_equality_over_binary_trees :
forall (V : Type)
(eqb_V : V -> V -> bool),
(forall v1 v2 : V,
eqb_V v1 v2 = true -> v1 = v2) ->
forall t1 t2 : binary_tree V,
eqb_binary_tree V eqb_V t1 t2 = true ->
t1 = t2.
This theorem is proved by induction on t1:
Proof.
intros V eqb_V C_eqb_V t1.
induction t1 as [v1 | t11 IHt11 t12 IHt12].
Let us focus on the base case:
-
The *goals* window reads:
V : Type
eqb_V : V -> V -> bool
C_eqb_V : forall v1 v2 : V, eqb_V v1 v2 = true -> v1 = v2
v1 : V
============================
forall t2 : binary_tree V, eqb_binary_tree V eqb_V (Leaf V v1) t2 = true -> Leaf V v1 = t2
We use the intros tactic to name the assumptions about t2 and the intensional equality of the two trees. Since t2 is destructured in the program, we destructure it too in the proof:
intros [v2 | t21 t22] H_eqb.
Let us focus on the first subgoal:
--
The *goals* window reads:
V : Type
eqb_V : V -> V -> bool
C_eqb_V : forall v1 v2 : V, eqb_V v1 v2 = true -> v1 = v2
v1, v2 : V
H_eqb : eqb_binary_tree V eqb_V (Leaf V v1) (Leaf V v2) = true
============================
Leaf V v1 = Leaf V v2
Let us use the fold-unfold lemma for leaves in H_eqb:
rewrite -> (fold_unfold_eqb_binary_tree_Leaf V eqb_V v1 (Leaf V v2)) in H_eqb.
The *goals* window reads:
V : Type
eqb_V : V -> V -> bool
C_eqb_V : forall v1 v2 : V, eqb_V v1 v2 = true -> v1 = v2
v1, v2 : V
H_eqb : eqb_V v1 v2 = true
============================
Leaf V v1 = Leaf V v2
Applying H_eqb to v1, v2, and C_eqb_V yields a Leibniz equality, v1 = v2, which we can use to rewrite the goal, which makes both sides of the equal sign the same, and so we can complete the proof of the base case using the reflexivity tactic:
rewrite -> (C_eqb_V v1 v2 H_eqb).
reflexivity.
Let us focus on the next subgoal:
--
The *goals* window reads:
V : Type
eqb_V : V -> V -> bool
C_eqb_V : forall v1 v2 : V, eqb_V v1 v2 = true -> v1 = v2
v1 : V
t21, t22 : binary_tree V
H_eqb : eqb_binary_tree V eqb_V (Leaf V v1) (Node V t21 t22) = true
============================
Leaf V v1 = Node V t21 t22
The equality in the goal obviously does not hold, so let us see whether another equality does not hold among the assumptions. To this end, let us use our faithful fold-unfold lemma for leaves:
rewrite -> (fold_unfold_eqb_binary_tree_Leaf V eqb_V v1 (Node V t21 t22)) in H_eqb.
Sure enough, the *goals* window now reads:
V : Type
eqb_V : V -> V -> bool
C_eqb_V : forall v1 v2 : V, eqb_V v1 v2 = true -> v1 = v2
v1 : V
t21, t22 : binary_tree V
H_eqb : false = true
============================
Leaf V v1 = Node V t21 t22
This is a job for the discriminate tactic:
discriminate H_eqb.
The base case is now proved, so let us turn to the induction step and start it in the same manner as we did in the base case. The current goal is replaced by two subgoals (one if the second tree is a leaf, the other if it is a node). Let us focus on the first:
- intros [v2 | t21 t22] H_eqb.
--
The *goals* window reads:
V : Type
eqb_V : V -> V -> bool
C_eqb_V : forall v1 v2 : V, eqb_V v1 v2 = true -> v1 = v2
t11, t12 : binary_tree V
IHt11 : forall t2 : binary_tree V, eqb_binary_tree V eqb_V t11 t2 = true -> t11 = t2
IHt12 : forall t2 : binary_tree V, eqb_binary_tree V eqb_V t12 t2 = true -> t12 = t2
v2 : V
H_eqb : eqb_binary_tree V eqb_V (Node V t11 t12) (Leaf V v2) = true
============================
Node V t11 t12 = Leaf V v2
The equality in the goal obviously does not hold, so let us see whether another equality does not hold among the assumptions. To this end, let us use our trusty fold-unfold lemma for nodes:
rewrite -> (fold_unfold_eqb_binary_tree_Node V eqb_V t11 t12 (Leaf V v2)) in H_eqb.
Sure enough, the *goals* window now reads:
V : Type
eqb_V : V -> V -> bool
C_eqb_V : forall v1 v2 : V, eqb_V v1 v2 = true -> v1 = v2
t11, t12 : binary_tree V
IHt11 : forall t2 : binary_tree V, eqb_binary_tree V eqb_V t11 t2 = true -> t11 = t2
IHt12 : forall t2 : binary_tree V, eqb_binary_tree V eqb_V t12 t2 = true -> t12 = t2
v2 : V
H_eqb : false = true
============================
Node V t11 t12 = Leaf V v2
This is another job for the discriminate tactic, and then we can turn to the other subgoal:
discriminate H_eqb.
--
The *goals* window reads:
V : Type
eqb_V : V -> V -> bool
C_eqb_V : forall v1 v2 : V, eqb_V v1 v2 = true -> v1 = v2
t11, t12 : binary_tree V
IHt11 : forall t2 : binary_tree V, eqb_binary_tree V eqb_V t11 t2 = true -> t11 = t2
IHt12 : forall t2 : binary_tree V, eqb_binary_tree V eqb_V t12 t2 = true -> t12 = t2
t21, t22 : binary_tree V
H_eqb : eqb_binary_tree V eqb_V (Node V t11 t12) (Node V t21 t22) = true
============================
Node V t11 t12 = Node V t21 t22
Aha, another use of our valorous fold-unfold lemma for nodes among the assumptions:
rewrite -> (fold_unfold_eqb_binary_tree_Node V eqb_V t11 t12 (Node V t21 t22)) in H_eqb.
The *goals* window reads:
V : Type
eqb_V : V -> V -> bool
C_eqb_V : forall v1 v2 : V, eqb_V v1 v2 = true -> v1 = v2
t11, t12 : binary_tree V
IHt11 : forall t2 : binary_tree V, eqb_binary_tree V eqb_V t11 t2 = true -> t11 = t2
IHt12 : forall t2 : binary_tree V, eqb_binary_tree V eqb_V t12 t2 = true -> t12 = t2
t21, t22 : binary_tree V
H_eqb : eqb_binary_tree V eqb_V t11 t21 && eqb_binary_tree V eqb_V t12 t22 = true
============================
Node V t11 t12 = Node V t21 t22
H_eqb now equates a Boolean conjunction with true, and each of the induction hypotheses use a component of this conjunction. Let’s seek help in the libraries:
Search (_ && _ = true -> _ /\ _).
The proof assistant obediently informs us of:
andb_prop: forall a b : bool, a && b = true -> a = true /\ b = true
in the *response* window. Let us check it out:
Check (andb_prop (eqb_binary_tree V eqb_V t11 t21) (eqb_binary_tree V eqb_V t12 t22)).
The *response* window now reads:
andb_prop (eqb_binary_tree V eqb_V t11 t21) (eqb_binary_tree V eqb_V t12 t22)
: eqb_binary_tree V eqb_V t11 t21 && eqb_binary_tree V eqb_V t12 t22 = true ->
eqb_binary_tree V eqb_V t11 t21 = true /\ eqb_binary_tree V eqb_V t12 t22 = true
Since the premise of the implication is precisely what H_eqb denotes, let us check it out again:
Check (andb_prop (eqb_binary_tree V eqb_V t11 t21) (eqb_binary_tree V eqb_V t12 t22) H_eqb).
The *response* window now reads:
andb_prop (eqb_binary_tree V eqb_V t11 t21) (eqb_binary_tree V eqb_V t12 t22) H_eqb
: eqb_binary_tree V eqb_V t11 t21 = true /\ eqb_binary_tree V eqb_V t12 t22 = true
Let us name the components of this pair:
destruct (andb_prop (eqb_binary_tree V eqb_V t11 t21) (eqb_binary_tree V eqb_V t12 t22) H_eqb) as [H_eqb_1 H_eqb_2].
The *goals* window now reads:
V : Type
eqb_V : V -> V -> bool
C_eqb_V : forall v1 v2 : V, eqb_V v1 v2 = true -> v1 = v2
t11, t12 : binary_tree V
IHt11 : forall t2 : binary_tree V, eqb_binary_tree V eqb_V t11 t2 = true -> t11 = t2
IHt12 : forall t2 : binary_tree V, eqb_binary_tree V eqb_V t12 t2 = true -> t12 = t2
t21, t22 : binary_tree V
H_eqb : eqb_binary_tree V eqb_V t11 t21 && eqb_binary_tree V eqb_V t12 t22 = true
H_eqb_1 : eqb_binary_tree V eqb_V t11 t21 = true
H_eqb_2 : eqb_binary_tree V eqb_V t12 t22 = true
============================
Node V t11 t12 = Node V t21 t22
We are now in position to use the first induction hypothesis:
Check (IHt11 t21 H_eqb_1).
The *response* window now reads:
IHt11 t21 H_eqb_1
: t11 = t21
Let us use this Leibniz equality in the goal, and likewise with the other induction hypothesis:
rewrite -> (IHt11 t21 H_eqb_1).
rewrite -> (IHt12 t22 H_eqb_2).
The goal is now the equality Node V t21 t22 = Node V t21 t22, which we prove with the reflexivity tactic, which completes the proof.
Completeness is stated as follows:
Theorem completeness_of_equality_over_binary_trees :
forall (V : Type)
(eqb_V : V -> V -> bool),
(forall v1 v2 : V,
v1 = v2 -> eqb_V v1 v2 = true) ->
forall t1 t2 : binary_tree V,
t1 = t2 ->
eqb_binary_tree V eqb_V t1 t2 = true.
This theorem is also proved by induction over t1, using the injection tactic to distill the Leibniz equality of two binary trees into the Leibniz equality of their components.
All in all, soundness and completeness is stated and proved as follows:
Theorem soundness_and_completeness_of_equality_over_binary_trees :
forall (V : Type)
(eqb_V : V -> V -> bool),
(forall v1 v2 : V,
eqb_V v1 v2 = true <-> v1 = v2) ->
forall t1 t2 : binary_tree V,
eqb_binary_tree V eqb_V t1 t2 = true <-> t1 = t2.
Proof.
intros V eqb_V SC_eqb_V t1 t2.
Check (from_one_equivalence_to_two_implications V eqb_V SC_eqb_V).
destruct (from_one_equivalence_to_two_implications V eqb_V SC_eqb_V) as [S_eqb_V C_eqb_V].
split.
- exact (soundness_of_equality_over_binary_trees V eqb_V S_eqb_V t1 t2).
- exact (completeness_of_equality_over_binary_trees V eqb_V C_eqb_V t1 t2).
It is, however, possible to prove soundness and completeness at once, i.e., in one induction proof, as spelled out in the accompanying file.
Verify that the remaining case (i.e., what happens for binary trees that are not equal) holds as a corollary of soundness and completeness.
Pablito: Did you notice that each of the soundness and completeness theorems about the equality of binary trees is proved using the Light of Inductil?
Halcyon: Come again?
Pablito: For example, look at the last theorem in the accompanying file:
Theorem soundness_and_completeness_of_equality_over_binary_trees :
forall (V : Type)
(eqb_V : V -> V -> bool),
(forall v1 v2 : V,
eqb_V v1 v2 = true <-> v1 = v2) ->
forall t1 t2 : binary_tree V,
eqb_binary_tree V eqb_V t1 t2 = true <-> t1 = t2.
Halcyon: Looking.
Pablito: The equivalence stated by this theorem is quantified by a type (V), the equality predicate associated with this type (eqb_V), the soundness and the completeness of this predicate, and two trees (t1 and t2).
Halcyon: Yes.
Pablito: The theorem is proved by induction on t1, and this induction starts right after naming the type, the equality predicate, the soundness and completeness of this predicate, and t1:
intros V eqb_V SC_eqb_V t1.
induction t1 as [v1 | t11 IHt11 t12 IHt12].
Halcyon: Ah, right, t2 is not named before starting the induction.
Pablito: Yup. It gives two stronger induction hypotheses. These induction hypotheses are parameterized by t2, which makes it possible for the proof to go through.
Created [22 Feb 2024]