Earlier, we saw what to do when an existential declaration occurs in the goal (namely use the exists tactic and supply a witness). But what to to do when an existential declaration occurs among the assumptions? Answer: use the destruct tactic to decompose this existential declaration into a pair. The first component of the pair is the name of the witness and the second the name of the assumption that depends on this witness.
Here is a simple example:
Lemma truism :
forall P : nat -> Prop,
(exists n : nat,
P n) ->
exists n : nat,
P n.
The proof starts as usual:
Proof.
intros P H_P.
At that point the *goals* window reads:
P : nat -> Prop
H_P : exists n : nat, P n
============================
exists n : nat, P n
We could make short of this proof with exact H_P., but instead, for the sake of the illustration, let us destructure H_P into a pair, the first component of which is the name of the witness (n, our choice of name) and the second the name of the assumption that depends on this witness (H_Pn, our choice of name):
destruct H_P as [n H_Pn].
The *goals* window then reads:
P : nat -> Prop
n : nat
H_Pn : P n
============================
exists n0 : nat, P n0
Henk Barendregt: Ah, it’s just a naming convention.Kris Rose: A convenient one, though.Mimer: Prof. Barendregt, Dr. Rose, thanks for passing by!
Two things have happened:
The rest of the proof is smooth sailing: n is obviously the witness we are looking for, and the goal then coincides with the assumption named H_Pn:
exists n.
exact H_Pn.
As usual, the intros / destruct proof steps can be conflated into one:
intros P [n H_Pn].
exists n.
exact H_Pn.
Qed.
Here is another simple example:
Lemma other_truism :
forall P Q : nat -> Prop,
(exists n : nat,
P n /\ Q n) ->
exists m : nat,
P m \/ Q m.
The proof can start by naming P and Q and by naming the components of the existential:
Proof.
intros P Q [n [H_Pn H_Qn]].
The *goals* window then reads:
P, Q : nat -> Prop
n : nat
H_Pn : P n
H_Qn : Q n
============================
exists m : nat, P m \/ Q m
The rest of the proof is in the accompanying .v file.
Does the existential quantifier distribute over disjunction? Concretely:
Lemma about_the_existential_quantifier_and_disjunction :
forall P Q : nat -> Prop,
(exists n : nat, P n \/ Q n)
<->
((exists n : nat, P n)
\/
(exists n : nat, Q n)).
The beginning of the proof is unproblematically mechanical:
intros P Q.
split.
-
The *goals* window then reads:
P, Q : nat -> Prop
============================
(exists n : nat, P n \/ Q n) -> (exists n : nat, P n) \/ (exists n : nat, Q n)
The goal is an implication whose premise is an existential quantification over a disjunction. Let us name its components:
intros [n [H_P | H_Q]].
Two further subgoals are created (one with H_P and the other with H_Q among the assumptions). Proving them leads us to proving the converse implication, for whom the *goals* window reads:
P, Q : nat -> Prop
============================
(exists n : nat, P n) \/ (exists n : nat, Q n) -> exists n : nat, P n \/ Q n
The goal is an implication whose premise is a disjunction of existential quantifications. Let us name its components:
- intros [[n H_P] | [n H_Q]].
Two further subgoals are created (one with n and H_P and the other with n and H_Q among the assumptions). Proving them is mechanical.
Does the universal quantifier distribute over conjunction? Concretely:
Lemma about_the_universal_quantifier_and_conjunction :
forall P Q : nat -> Prop,
(forall n : nat, P n /\ Q n)
<->
((forall n : nat, P n)
/\
(forall n : nat, Q n)).
The beginning of the proof is unproblematically mechanical:
Proof.
intros P Q.
split.
- intro H_PQ.
split.
+ intro n.
The *goals* window then reads:
P, Q : nat -> Prop
H_PQ : forall n : nat, P n /\ Q n
n : nat
============================
P n
Applying H_PQ to n yields a conjunction, and we are after its left conjunct:
destruct (H_PQ n) as [H_Pn _].
The *goals* window now reads:
P, Q : nat -> Prop
H_PQ : forall n : nat, P n /\ Q n
n : nat
H_Pn : P n
============================
P n
The rest of the proof is mechanical.
Anton: And we should care about Exercise 01 why?
Mimer: How would you state a lemma to the effect that a natural number is either even or odd?
Anton: Well, like this:
Lemma even_or_odd :
forall n : nat,
(exists q : nat,
n = 2 * q)
\/
(exists q : nat,
n = S (2 * q)).
Alfrothul: Actually, I would write it like this:
Lemma even_or_odd' :
forall n : nat,
exists q : nat,
n = 2 * q
\/
n = S (2 * q).
Mimer: Are these statements equivalent?
Anton: Well...
Mimer: That’s why you should care.
Dana: Actually, I was also wondering about the way we write specifications.
Mimer: You did?
Dana: Well, yes. Take the addition function for example. We specified it with the universal quantifiers dropped in each clause:
Definition specification_of_addition (add : nat -> nat -> nat) :=
(forall m : nat,
add O m = m)
/\
(forall n' m : nat,
add (S n') m = S (add n' m)).
Mimer: Yes.
Dana: But why not specifying it by lifting all the quantifiers at the outset instead:
Definition specification_of_addition' (add : nat -> nat -> nat) :=
forall n' m : nat,
add O m = m
/\
add (S n') m = S (add n' m).
Mimer: Yes indeed – why not? Or why, for that matter?
Dana: And now you are going to refer to Exercise 02.
Pablito: May I interject a concept here?
Dana (who has seen that movie too): By all means. And then I’ll go home and brush all my teeth.
Pablito: But it’s not the same movie? Anyhow, in your example, one variable is quantified in the first conjunct and two in the second.
Dana: Yes.
Pablito: So Exercise 02 doesn’t quite fit. What we need is something like this lemma:
Lemma about_two_universal_quantifiers_and_conjunction :
forall (P : nat -> Prop)
(Q : nat -> nat -> Prop),
((forall j : nat, P j)
/\
(forall i j : nat, Q i j))
<->
(forall i j : nat, P j /\ Q i j).
Dana: Yes. At the risk of mansplaining, P is for the base case and is only quantified over one variable, and Q is for the induction step and is quantified over two variables.
Pablito: Thanks. Er... Would you like me to prove this lemma? <clickety clickety clickety click C-x C-s> Never mind, I just put the proof in the accompanying .v file.
Dana: Thanks. And now for the concept you wanted to interject?
Pablito: Right. We can prove the equivalence of the two specifications of addition as a corollary of this lemma:
Proposition the_two_specifications_of_addition_are_equivalent :
forall add : nat -> nat -> nat,
specification_of_addition add <-> specification_of_addition' add.
Proof.
intro add.
unfold specification_of_addition, specification_of_addition'.
Dana: OK. The *goals* window reads:
add : nat -> nat -> nat
============================
(forall m : nat, add 0 m = m) /\ (forall n' m : nat, add (S n') m = S (add n' m)) <->
(forall n' m : nat, add 0 m = m /\ add (S n') m = S (add n' m))
Pablito: Precisely. Now check out the lemma, once we apply it to fun m : nat => add 0 m = m and to fun n' m : nat => add (S n') m = S (add n' m)), i.e., to two terms that are what we want and that have the right type too:
Check (about_two_universal_quantifiers_and_conjunction
(fun m : nat => add 0 m = m)
(fun n' m : nat => add (S n') m = S (add n' m))).
Dana: OK. The *response* window reads:
about_two_universal_quantifiers_and_conjunction (fun m : nat => add 0 m = m)
(fun n' m : nat => add (S n') m = S (add n' m))
: (forall j : nat, add 0 j = j) /\ (forall i j : nat, add (S i) j = S (add i j)) <->
(forall i j : nat, add 0 j = j /\ add (S i) j = S (add i j))
Pablito: Yes. And that is exactly what we wanted to prove:
exact (about_two_universal_quantifiers_and_conjunction
(fun m : nat => add 0 m = m)
(fun n' m : nat => add (S n') m = S (add n' m))).
Qed.
Pablito: So the lifted specification and the dropped specification of addition are equivalent.
Mimer: Bravo.
Anton: By that book the equivalence of my dropped version of the lemma about a number being even or odd and your lifted version should be a corollary of Exercise 02. Lemmesee:
Proposition the_two_specifications_of_even_or_odd_are_equivalent :
forall n : nat,
(exists q : nat,
n = 2 * q
\/
n = S (2 * q))
<->
((exists q : nat,
n = 2 * q)
\/
(exists q : nat,
n = S (2 * q))).
Alfrothul: Let me help you here:
Proof.
intro n.
Anton: Thank you. Thank you very much.
Alfrothul: I was just getting started. By the book above, we should apply about_the_existential_quantifier_and_disjunction to, well, fun q : nat => n = 2 * q and fun q : nat => n = S (2 * q), no? Let’s see:
Check (about_the_existential_quantifier_and_disjunction
(fun q : nat => n = 2 * q)
(fun q : nat => n = S (2 * q))).
Anton: The *response* window looks right:
about_the_existential_quantifier_and_disjunction (fun q : nat => n = 2 * q) (fun q : nat => n = S (2 * q))
: (exists n0 : nat, n = 2 * n0 \/ n = S (2 * n0)) <->
(exists n0 : nat, n = 2 * n0) \/ (exists n0 : nat, n = S (2 * n0))
Alfrothul: Let’s try then:
exact (about_the_existential_quantifier_and_disjunction
(fun q : nat => n = 2 * q)
(fun q : nat => n = S (2 * q))).
Anton: Yes, that does it:
Qed.
Prove the following proposition:
Proposition factoring_and_distributing_a_forall_in_a_conclusion :
forall (P : nat -> Prop)
(Q : Prop),
(Q -> forall n : nat, P n)
<->
(forall n : nat,
Q -> P n).
Prove the following propositions:
Proposition interplay_between_quantifiers_and_implication :
forall (P : nat -> Prop)
(Q : Prop),
(exists n : nat, P n -> Q) ->
(forall n : nat, P n) -> Q.
Proposition interplay_between_exists_and_forall_in_a_premise :
forall (V : Type)
(P : Prop)
(Q : V -> Prop),
((exists v : V,
Q v) ->
P)
<->
(forall v : V,
Q v ->
P).
Prove the following proposition:
Proposition interplay_between_implication_and_quantifiers :
forall (P : nat -> Prop)
(Q : Prop),
((exists n : nat, P n) -> Q) ->
forall n : nat, P n -> Q.
Alfrothul: Remember specifications that are vacuous?
Dana: Yup. There are conditions that no function can satisfy.
Alfrothul: Indeed. And that is something we can formalize, look:
Theorem no_functions_satisfy_a_vacuous_specification :
forall specification : (Type -> Type) -> Prop,
(forall f : Type -> Type,
specification f ->
(exists v : Type,
f v <> f v)) ->
not (exists f : Type -> Type,
specification f).
Bong-sun: Let me see. OK, yes, a specification has type (Type -> Type) -> Prop since it states a property of a function.
Alfrothul: Right. And the premise of the implication is that the specification is vacuous, since the very definition of a function is that it maps the same input to the same output.
Dana: And the conclusion of the implication is that there is no function that satisfies the specification.
Anton: Er... And we prove that how?
Alfrothul: We start by inlining the definition of negation, look:
Proof.
unfold not.
Pablito (obligingly): The *goals* window now reads:
============================
forall specification : (Type -> Type) -> Prop,
(forall f : Type -> Type, specification f -> exists v : Type, f v = f v -> False) ->
(exists f : Type -> Type, specification f) -> False
Alfrothul: And then it’s business as usual, exploiting the fact that an existentially quantified statement is represented as a pair:
intros s V_s [f S_f].
Pablito (obligingly): The *goals* window now reads:
s : (Type -> Type) -> Prop
V_s : forall f : Type -> Type, s f -> exists v : Type, f v = f v -> False
f : Type -> Type
S_f : s f
============================
False
Alfrothul: Now look at the result of applying V_s to f and S_f:
Check (V_s f S_f).
Pablito (obligingly): The *response* window now reads:
V_s f S_f
: exists v : Type, f v = f v -> False
Anton: Ah! Since existentially quantified statements are represented as pairs, we can destructure this one:
destruct (V_s f S_f) as [v H_v].
Pablito (obligingly): The *goals* window now reads:
s : (Type -> Type) -> Prop
V_s : forall f : Type -> Type, s f -> exists v : Type, f v = f v -> False
f : Type -> Type
S_f : s f
v : Type
H_v : f v = f v -> False
============================
False
Alfrothul: Right. And since Leibniz equality is reflexive, the proof follows:
exact (H_v (eq_refl (f v))).
Qed.
Halcyon: Yay!
Bong-sun: Actually...
Dana: Yes, Bong-sun?
Bong-sun: Why isn’t the theorem stated to the effect that for all functions, the specification does not hold, look:
Theorem no_functions_satisfy_a_vacuous_specification_alt :
forall specification : (Type -> Type) -> Prop,
(forall f : Type -> Type,
specification f ->
(exists v : Type,
f v <> f v)) ->
forall f : Type -> Type,
not (specification f).
Pablito: May I?
Bong-sun: Please, Pablito, please.
Pablito: First we inline the definition of negation, and then it’s business as usual, look:
unfold not.
intros s V_s f S_f.
Halcyon (obligingly): The *goals* window now reads:
s : (Type -> Type) -> Prop
V_s : forall f : Type -> Type, s f -> exists v : Type, f v = f v -> False
f : Type -> Type
S_f : s f
============================
False
Pablito: See? It’s the same *goals* window, and so the rest is the proof is the same too:
destruct (V_s f S_f) as [v H_v].
exact (H_v (eq_refl (f v))).
Qed.
Halcyon: Yay!
Bong-sun: Hum.
Mimer: Yes, Bong-sun?
Bong-sun: That kind of begs for another exercise, doesn’t it?
Mimer (amused): It probably does.
The fourth wall: May I?
Alfrothul, Anton, Bong-sun, Dana, Halcyon, and Pablito: Please, fourth wall, please.
Prove the following proposition:
Proposition not_exists_and_forall_not :
forall (A : Type)
(P : A -> Prop),
(not (exists a : A, P a)) <-> (forall a : A, not (P a)).
Bong-sun: Hum.
Mimer: Yes, Bong-sun?
Bong-sun: That’s not quite what we need here. May I?
Mimer: Please, Bong-sun, please.
Prove the following proposition:
Proposition not_exists_and_forall_not_for_functions :
forall (F : Type -> Type)
(P : (Type -> Type) -> Prop),
(not (exists f : Type -> Type, P f)) <-> (forall f : Type -> Type, not (P f)).
Bong-sun: Ah, that’s better.
Anton: Er... It is better why?
Bong-sun: Because now we can prove no_functions_satisfy_a_vacuous_specification_alt as a corollary of no_functions_satisfy_a_vacuous_specification.
Loki: Check out the resource file.
Added the postlude about vacuous specifications and the subsequent exercises as a spinoff of a late email exchange with Avery Snow [21 Mar 2024]
Extracted this chapter from a chapter about miscellanies [21 Mar 2024]