The goal of this chapter is to continue exploring situations where an existential declaration also occurs among the assumptions rather than only in the goal.
In tCPA, existential declarations that occur among the assumptions are represented as pairs – the name of the witness and the assumption that depends on this witness.
Here is a simple example:
Lemma selective_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 business as usual:
exists n.
Henceforth we can either
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 05 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 06.
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 06 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: Bra-vo.
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 06. 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 deconstruct 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.
Created [07 Mar 2025]