A predicate is a Boolean-valued function. The goal of this lecture note is to study the soundness and completeness of predicates testing structural equality:
Definition is_a_sound_equality_predicate (V : Type) (eqb_V : V -> V -> bool) :=
forall v1 v2 : V,
eqb_V v1 v2 = true -> v1 = v2.
Definition is_a_complete_equality_predicate (V : Type) (eqb_V : V -> V -> bool) :=
forall v1 v2 : V,
v1 = v2 -> eqb_V v1 v2 = true.
Definition is_a_sound_and_complete_equality_predicate (V : Type) (eqb_V : V -> V -> bool) :=
forall v1 v2 : V,
eqb_V v1 v2 = true <-> v1 = v2.
See eqb_bool and soundness_and_completeness_of_eqb_bool in the accompanying file.
See eqb_nat and soundness_and_completeness_of_eqb_nat in the accompanying file.
Given a type and the corresponding equality predicate, we need to implement a function that maps two optional values to a boolean. There are 4 cases:
Definition specification_of_eqb_option (eqb_option : forall (V : Type), (V -> V -> bool) -> option V -> option V -> bool) :=
forall (V : Type)
(eqb_V : V -> V -> bool),
(forall v1 v2 : V,
eqb_option V eqb_V (Some v1) (Some v2) = eqb_V v1 v2)
/\
(forall v1 : V,
eqb_option V eqb_V (Some v1) None = false)
/\
(forall v2 : V,
eqb_option V eqb_V None (Some v2) = false)
/\
(eqb_option V eqb_V None None = true).
Definition eqb_option (V : Type) (eqb_V : V -> V -> bool) (ov1 ov2 : option V) : bool :=
...
Proposition eqb_option_satisfies_the_specification_of_eqb_option :
specification_of_eqb_option eqb_option.
The equality predicate for the option type is defined by cases:
first on its first argument:
Definition eqb_option (V : Type) (eqb_V : V -> V -> bool) (ov1 ov2 : option V) : bool :=
match ov1 with
Some v1 =>
...
| None =>
...
end.
and second on its second argument:
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 =>
...
| None =>
...
end
| None =>
match ov2 with
Some v2 =>
...
| None =>
...
end
end.
Based on the specification above, we can fill the 4 cases:
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.
That the implementation satisfies the specification is left as an exercise to the reader. And yes, it is a proof by cases.
Likewise, the soundness and completeness of this equality predicate are proved by cases:
Proposition soundness_and_completeness_of_eqb_option :
forall (V : Type)
(eqb_V : V -> V -> bool),
is_a_sound_and_complete_equality_predicate V eqb_V ->
is_a_sound_and_complete_equality_predicate (option V) (eqb_option V eqb_V).
Proof.
intros V eqb_V.
unfold is_a_sound_and_complete_equality_predicate.
intros H_both [v1 | ] [v2 | ]; unfold eqb_option.
- destruct (H_both v1 v2) as [H_sound H_complete].
split; intro H_v1_v2.
-- rewrite -> (H_sound H_v1_v2).
reflexivity.
-- injection H_v1_v2 as H_v1_v2.
exact (H_complete H_v1_v2).
- split; intro H_absurd; discriminate H_absurd.
- split; intro H_absurd; discriminate H_absurd.
- split; reflexivity.
Qed.
Pablito: What about an optional optional type?
Alfrothul: An optional optional type.
Pablito: Yes, like option (option V), given a type V.
Alfrothul: Well, that is going to be a massive definition by cases.
Pablito: Massive, yes, but systematic. Let me sketch its skeleton:
Definition option_eqb_option (V : Type) (eqb_V : V -> V -> bool) (oov1 oov2 : option (option V)) : bool :=
match oov1 with
Some ov1 =>
match oov2 with
Some ov2 =>
...
| None =>
...
end
| None =>
match oov2 with
Some ov2 =>
...
| None =>
...
end
end.
Alfrothul: Right, that’s for the outer layer of comparisons. And we can already fill the blanks for comparing Some ... and None and for comparing None and Some ....
Pablito: And for comparing None and None:
Definition option_eqb_option (V : Type) (eqb_V : V -> V -> bool) (oov1 oov2 : option (option V)) : bool :=
match oov1 with
Some ov1 =>
match oov2 with
Some ov2 =>
...
| None =>
false
end
| None =>
match oov2 with
Some ov2 =>
false
| None =>
true
end
end.
Alfrothul: Now for the next layer. Lemmesee:
Definition option_eqb_option (V : Type) (eqb_V : V -> V -> bool) (oov1 oov2 : option (option V)) : bool :=
match oov1 with
Some ov1 =>
match oov2 with
Some ov2 =>
match ov1 with
Some v1 =>
match ov2 with
Some v2 =>
...
| None =>
...
end
| None =>
match ov2 with
Some v2 =>
...
| None =>
...
end
end
| None =>
false
end
| None =>
match oov2 with
Some ov2 =>
false
| None =>
true
end
end.
Pablito: Right, that’s for the inner layer of comparisons. Let me fill the blanks for comparing Some ... and None and for comparing None and Some ..., as well as for comparing None and None:
Definition option_eqb_option (V : Type) (eqb_V : V -> V -> bool) (oov1 oov2 : option (option V)) : bool :=
match oov1 with
Some ov1 =>
match oov2 with
Some ov2 =>
match ov1 with
Some v1 =>
match ov2 with
Some v2 =>
...
| None =>
false
end
| None =>
match ov2 with
Some v2 =>
false
| None =>
true
end
end
| None =>
false
end
| None =>
match oov2 with
Some ov2 =>
false
| None =>
true
end
end.
Alfrothul: The remaining case is to compare v1 and v2.
Pablito: Which we do using the given equality predicate, eqb_V:
Definition option_eqb_option (V : Type) (eqb_V : V -> V -> bool) (oov1 oov2 : option (option V)) : bool :=
match oov1 with
Some ov1 =>
match oov2 with
Some ov2 =>
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
| None =>
false
end
| None =>
match oov2 with
Some ov2 =>
false
| None =>
true
end
end.
Alfrothul: All right, that was massive but doable.
Pablito: Because it was systematic.
Anton (jumping in): The corresponding soundness and completeness should be equally massive and systematic.
Pablito: It should look like something like this, like:
Proposition soundness_and_completeness_of_option_eqb_option :
forall (V : Type)
(eqb_V : V -> V -> bool),
is_a_sound_and_complete_equality_predicate V eqb_V ->
is_a_sound_and_complete_equality_predicate (option (option V)) (option_eqb_option V eqb_V).
Alfrothul: Like it or not.
Anton: Well, this is not California and this is not a social media, so let’s move on:
Proof.
intros V eqb_V.
unfold is_a_sound_and_complete_equality_predicate.
Pablito: Proof by cases, here we come:
intros H_both [[v1 | ] | ] [[v2 | ] | ]; unfold option_eqb_option.
Alfrothul: Nice use of the semicolon, Pablito. The *goals* window reads:
V : Type
eqb_V : V -> V -> bool
H_both : forall v1 v2 : V, eqb_V v1 v2 = true <-> v1 = v2
v1, v2 : V
H_sound : eqb_V v1 v2 = true -> v1 = v2
H_complete : v1 = v2 -> eqb_V v1 v2 = true
============================
eqb_V v1 v2 = true <-> Some (Some v1) = Some (Some v2)
Anton: The goal is an equivalence, i.e., a bi-implication, i.e., the conjunction of two implications, so we don’t really have the choice, do we. Let’s consider each of the implications in turn.
Pablito: And name their premises upfront while we are at it:
split; intro H_v1_v2.
Alfrothul: Another nice use of the semicolon, Pablito.
Anton: The first case follows from the soundness of eqb_V:
-- rewrite -> (H_sound H_v1_v2).
reflexivity.
Pablito: And the second from its completeness:
-- injection H_v1_v2 as H_v1_v2.
exact (H_complete H_v1_v2).
Alfrothul: And the remaining cases are trivial:
- split; intro H_absurd; discriminate H_absurd.
- split; intro H_absurd; discriminate H_absurd.
- split; intro H_absurd; discriminate H_absurd.
- split; reflexivity.
- split; intro H_absurd; discriminate H_absurd.
- split; intro H_absurd; discriminate H_absurd.
- split; intro H_absurd; discriminate H_absurd.
- split; reflexivity.
Qed.
Pablito: So, massive and systematic.
Dana (pensive): But a bit redundant, no?
Pablito, Alfrothul, and Anton: Redundant?
Dana: Well, yes. For example, eqb_option_option could be defined in terms of eqb_option:
Definition eqb_option_option' (V : Type) (eqb_V : V -> V -> bool) (oov1 oov2 : option (option V)) : bool :=
match oov1 with
Some ov1 =>
match oov2 with
Some ov2 =>
eqb_option V eqb_V ov1 ov2
| None =>
false
end
| None =>
match oov2 with
Some ov2 =>
false
| None =>
true
end
end.
Pablito, Alfrothul, and Anton: Uh oh.
Dana (warming up): In fact, since option (option V) is defined by layering the option type, couldn’t we also define its equality predicate by layering eqb_option?
Anton: OMG. You mean something like:
Definition eqb_option_option'' (V : Type) (eqb_V : V -> V -> bool) : option (option V) -> option (option V) -> bool :=
eqb_option (option V) (eqb_option V eqb_V).
Dana: Well, that definition does it, doesn’t it?
Loki: “How do you know?”
Anton: You make it sounds like a quote.
Loki: Because it is one. From Mae West. To W. C. Fields. In My Little Chickadee.
Halcyon: A classic.
Dana: Right. Well, however obscure the reference (it was a black-and-white movie, for crying out loud), your point does stand, and we cannot ignore it:
Proposition equivalence_of_eqb_option_option_and_eqb_option_option'' :
forall (V : Type)
(eqb_V : V -> V -> bool)
(oov1 oov2 : option (option V)),
eqb_option_option V eqb_V oov1 oov2 = eqb_option_option'' V eqb_V oov1 oov2.
Loki: That’s the spirit!
Pablito (seeing his chance): Let me handle this:
Proof.
intros V eqb_V oov1 oov2.
reflexivity.
Qed.
Dana, Anton, and Alfrothul clap their hands.
Pablito (catching his breath, and slightly red in the face): Thank you. I know that I should first have stated fold-unfold lemmas for each of the predicates, since they are recursive, but they are fully applied here and so all we would have done with these lemmas is unfolding the successive calls to the predicates one by one. So using the unfold tactic twice makes sense here, and since the reflexivity includes that, I just cut the chase. Huh, can we move on now?
Alfrothul: Sure. Now that the predicate is defined by layering the predicate for the option type, should we prove its soundness and completeness by layering the soundness and completeness for the option type?
Dana: Let’s give it a shot:
Proposition soundness_and_completeness_of_eqb_option_option'' :
forall (V : Type)
(eqb_V : V -> V -> bool),
is_a_sound_and_complete_equality_predicate V eqb_V ->
is_a_sound_and_complete_equality_predicate (option (option V)) (eqb_option_option'' V eqb_V).
Proof.
intros V eqb_V H_V.
Anton: Let me try something:
Check (soundness_and_completeness_of_eqb_option V eqb_V H_V).
Pablito: The *response* window reads:
soundness_and_completeness_of_eqb_option V eqb_V H_V
: is_a_sound_and_complete_equality_predicate (option V) (eqb_option V eqb_V)
Alfrothul: Aha. Let me try something else:
Check (soundness_and_completeness_of_eqb_option (option V) (eqb_option V eqb_V)).
Pablito: The *response* window reads:
soundness_and_completeness_of_eqb_option (option V) (eqb_option V eqb_V)
: is_a_sound_and_complete_equality_predicate (option V) (eqb_option V eqb_V) ->
is_a_sound_and_complete_equality_predicate (option (option V)) (eqb_option (option V) (eqb_option V eqb_V))
Anton and Alfrothul: So if we put two and two together:
Check (soundness_and_completeness_of_eqb_option (option V) (eqb_option V eqb_V) (soundness_and_completeness_of_eqb_option V eqb_V H_V)).
Pablito: Yes! The *response* window reads:
soundness_and_completeness_of_eqb_option (option V) (eqb_option V eqb_V)
(soundness_and_completeness_of_eqb_option V eqb_V H_V)
: is_a_sound_and_complete_equality_predicate (option (option V)) (eqb_option (option V) (eqb_option V eqb_V))
Dana: How about we inline the call to eqb_option_option'' in the goal:
unfold eqb_option_option''.
Pablito: Good idea. The *goals* window reads:
V : Type
eqb_V : V -> V -> bool
H_V : is_a_sound_and_complete_equality_predicate V eqb_V
============================
is_a_sound_and_complete_equality_predicate (option (option V)) (eqb_option (option V) (eqb_option V eqb_V))
Dana: What a marvelous coincidence:
exact (soundness_and_completeness_of_eqb_option (option V) (eqb_option V eqb_V) (soundness_and_completeness_of_eqb_option V eqb_V H_V)).
Qed.
Mimer: Guys, that was elegant.
Dana, Anton, Alfrothul, and Pablito: Thank you.
See eqb_pair and soundness_and_completeness_of_eqb_pair in the accompanying file.
See eqb_list and soundness_and_completeness_of_eqb_list in the accompanying file.
Complete the remaining proofs in the accompanying file.
Implement an equality predicate of type nat * bool -> nat * bool -> bool and prove its soundness and completeness.
Implement an equality predicate of type list (nat * bool) -> list (nat * bool) -> bool and prove its soundness and completeness.
Implement an equality predicate of type list nat * list bool -> list nat * list bool -> bool and prove its soundness and completeness.
Implement an equality predicate of type option (nat * bool) -> option (nat * bool) -> bool and prove its soundness and completeness.
Implement an equality predicate of type option nat * option bool -> option nat * option bool -> bool and prove its soundness and completeness.
Implement an equality predicate of type option bool * list unit -> option bool * list unit -> bool and prove its soundness and completeness.
Hint: the unit value in tCPA is written tt and has type unit.
Implement an equality predicate of type list (list (nat * bool)) -> list (list (nat * bool)) -> bool and prove its soundness and completeness.
Implement an equality predicate of type list (option (list (option nat))) -> list (option (list (option nat))) -> bool and prove its soundness and completeness.
Implement an equality predicate of type option (list (option (list nat))) -> option (list (option (list nat))) -> bool and prove its soundness and completeness.
Properly aligned the name is_a_sound_and_complete_equality_predicate with that of the resource file, thanks to Zhuang Ruotong’s eagle eye [08 Apr 2024]
Created [08 Mar 2024]