The goal of this lecture note is to use the tactics learned so far to prove logical properties.
Given A and B of type Prop, their conjunction is noted:
A /\ B
To prove a conjunction, we use the tactic split, which creates two subgoals: one for A and one for B.
For example:
Lemma proving_a_conjunction :
forall A B : Prop,
A -> B -> A /\ B.
Proof.
intros A B H_A H_B.
split.
The *goals* window reads as follows:
2 subgoals, subgoal 1 (ID 8)
A, B : Prop
H_A : A
H_B : B
============================
A
subgoal 2 (ID 9) is:
B
In words:
(The part about (ID ...) is an internal notation.)
We then prove the first subgoal, and then the second:
exact H_A.
exact H_B.
To avoid cluttering the *goals* window, we can focus on the current subgoal
either by wrapping the proof steps of each subgoal between braces:
split.
{ exact H_A. }
{ exact H_B. }
or by itemizing each subproof (using -, --, ---, etc. or +, ++, +++, etc., or using *, **, ***, etc.):
split.
- exact H_A.
- exact H_B.
In simple cases, we can avoid splitting the proof and instead construct the conjunction directly using conj:
intros A B H_A H_B.
Check (conj H_A H_B).
exact (conj H_A H_B).
Conjunction is associative and by default it associates to the right, as illustrated by the following lemma and its proof:
Lemma proving_a_ternary_conjunction :
forall A B C : Prop,
A -> B -> C -> A /\ B /\ C.
Proof.
intros A B C.
intros H_A H_B H_C.
At that point the *goals* window reads:
A, B, C : Prop
H_A : A
H_B : B
H_C : C
============================
A /\ B /\ C
If we use the split tactic, tCPA selects A as the first subgoal to prove, with B /\ C as the second.
Alternatively, we can prove this goal in one step by constructing a nested conjunction that is associated to the right:
exact (conj H_A (conj H_B H_C)).
So if we need to prove a flat conjunction with many conjuncts, i.e., A /\ B /\ C /\ D, to keep the proof flat instead of drifting to the right, we can write:
split.
{ ...proof for A...}
split.
{ ...proof for B...}
split.
{ ...proof for C...}
...proof for D...
Anton: We are drifting to the right now?
Alfrothul: That is because /\ is binary and associates to the right, so A /\ B /\ C /\ D is parsed as A /\ (B /\ (C /\ D)).
Anton: Example?
Alfrothul: Of course:
Lemma example_for_Anton :
forall A B C D : Prop,
A /\ B /\ C /\ D.
Anton: And you are going to prove that?
Alfrothul: Not really, I’ll just admit the conjuncts with the admit tactic, and then we will see the shape of the proof.
Anton: Er... Sure.
Pablito: The admit tactic?
Alfrothul: We use the Admitted tactic to claim we proved the current proposition we are trying to prove, and we use the admit tactic to claim that we proved the current subgoal. OK?
Pablito: OK.
Alfrothul: Let’s get started:
Proof.
intros A B C D.
Pablito (helpfully): The *goals* buffer reads:
A, B, C, D : Prop
============================
A /\ B /\ C /\ D
Alfrothul: Here is how we would prove this proposition by focusing on each subgoals:
split.
- admit.
- split.
+ admit.
+ split.
* admit.
* admit.
Alfrothul: See how our proof is drifting to the right?
Anton: Let me check:
Restart.
intros A B C D.
split.
{ admit. }
{ split.
{ admit. }
{ split.
{ admit. }
{ admit. } } }
Anton: OK, I see.
Alfrothul: Whereas if we only use curly braces for the left conjunct and not for the right conjunct, the proof doesn’t drift to the right, look:
Restart.
intros A B C D.
split.
{ admit. }
split.
{ admit. }
split.
{ admit. }
admit.
Anton: Got it, thanks.
Loki: That’s really the idea of a programmer, isn’t it.
Mimer: How so?
Loki: Tail-call optimization.
Mimer: Harrumph.
Equivalence is noted with the infix operator <->, which is syntactic sugar for the conjunction of two implications. So concretely, given A and B of type Prop, the equivalence:
A <-> B
stands for the conjunction:
(A -> B) /\ (B -> A)
Halcyon (discreetly): Ahem.
An equivalence is therefore proved using the split tactic.
Given A and B of type Prop, their disjunction is noted:
A \/ B
To prove a disjunction, we use either the tactic left to select its left-hand side, or the tactic right to select its right-hand side.
For example:
Lemma proving_a_disjunction :
forall A B : Prop,
A -> B -> A \/ B.
Proof.
intros A B H_A H_B.
The *goals* window reads as follows:
A, B : Prop
H_A : A
H_B : B
============================
A \/ B
If we use the left tactic, then the *goals* window reads:
A, B : Prop
H_A : A
H_B : B
============================
A
If we use the right tactic, then the *goals* window reads:
A, B : Prop
H_A : A
H_B : B
============================
B
So there are two ways to create subgoals:
Prove that conjunction is commutative.
The first step is to formalize the statement:
Lemma conjunction_is_commutative :
forall A B : Prop,
A /\ B <-> B /\ A.
The proof is simple: declare A and B with the intro tactic, split the equivalence into two implications, and proceed from there:
Proof.
intros A B.
split.
- intros [H_A H_B].
exact (conj H_B H_A).
- intros [H_B H_A].
exact (conj H_A H_B).
Qed.
Since the proof for the two subgoals are identical, let us state an auxiliary lemma:
Lemma conjunction_is_commutative_aux :
forall A B : Prop,
A /\ B -> B /\ A.
Proof.
intros A B [H_A H_B].
exact (conj H_B H_A).
Qed.
Thus equipped, we can use this auxiliary lemma in each case of the proof:
Lemma conjunction_is_commutative_revisited :
forall A B : Prop,
A /\ B <-> B /\ A.
Proof.
intros A B.
split.
- exact (conjunction_is_commutative_aux A B).
- exact (conjunction_is_commutative_aux B A).
Qed.
Prove that conjunction is associative.
Prove that disjunction is commutative.
Prove that disjunction is associative.
Prove whether disjunction distributes over conjunction on the left and on the right.
Does conjunction distribute over disjunction on the left? And what about on the right?
What about the case where an implication lies on the left of an implication? The modus ponens rule of inference provides a simple example of this situation:
Proposition modus_ponens :
forall A B : Prop,
A -> (A -> B) -> B.
Proof.
intros A B.
intros H_A H_A_implies_B.
The *goals* window reads as follows:
A, B : Prop
H_A : A
H_A_implies_B : A -> B
============================
B
Applying H_A_implies_B to H_A yields a witness of B, as needed:
Check (H_A_implies_B H_A).
Indeed the *response* window then reads:
H_A_implies_B H_A
: B
And therefore writing:
exact (H_A_implies_B H_A).
completes the proof.
Alternatively, we can use the apply tactic to replace the goal B by A since A implies B:
apply H_A_implies_B.
The *goals* window then reads as follows:
A, B : Prop
H_A : A
H_A_implies_B : A -> B
============================
A
and so we are one step away from completing the proof.
Prove in as many ways as you can the following proposition, and justify each of these ways:
Proposition following :
forall A B : Prop,
(A -> B) -> A -> B.
Negating a proposition A is written as ~A, which is syntactic sugar for not A, which stands for A -> False.
The modus tollens rule of inference is stated as follows:
Proposition modus_tollens :
forall A B : Prop,
~B -> (A -> B) -> ~A.
Let us start by declaring A and B using the intros rule:
Proof.
intros A B.
The *goals* window then reads as follows:
A, B : Prop
============================
~ B -> (A -> B) -> ~ A
The notation ~ X is syntactic sugar for not X and not X being defined as X -> False, let us replace ~ B and ~ A by B -> False and A -> False by unfolding the definition of not, using the unfold tactic:
unfold not.
The *goals* window then reads as follows:
A, B : Prop
============================
(B -> False) -> (A -> B) -> A -> False
We can then name the three assumptions using the intros tactic:
intros H_B_implies_False H_A_implies_B H_A.
The *goals* window then reads as follows:
A, B : Prop
H_B_implies_False : B -> False
H_A_implies_B : A -> B
H_A : A
============================
False
Proof by using the apply tactic
We can use the apply tactic on H_B_implies_False since it says that B implies the current goal:
apply H_B_implies_False.
The *goals* window then reads as follows:
A, B : Prop
H_B_implies_False : B -> False
H_A_implies_B : A -> B
H_A : A
============================
B
We can use the apply tactic on H_A_implies_B since it says that A implies the current goal:
apply H_A_implies_B.
The *goals* window then reads as follows:
A, B : Prop
H_B_implies_False : B -> False
H_A_implies_B : A -> B
H_A : A
============================
A
This puts us one exact step away from completing the proof.
Proof by applying the assumptions
We can also apply H_A_implies_B to H_A to obtain B:
Check (H_A_implies_B H_A).
Indeed the *response* window then reads as follows:
H_A_implies_B H_A
: B
We can then apply H_B_implies_False to B:
Check (H_B_implies_False (H_A_implies_B H_A)).
Indeed the *response* window then reads as follows:
H_B_implies_False (H_A_implies_B H_A)
: False
This puts us one exact step away from completing the proof.
Proof as a corollary of the modus ponens rule of inference
Let us check the result of instantiating modus_ponens with A and B:
Check (modus_ponens A B).
The *response* window then reads as follows:
modus_ponens A B
: A -> (A -> B) -> B
Since we have a witness of A among the assumptions, let us check the result of instantiating modus_ponens with A, B, and this witness:
Check (modus_ponens A B H_A).
The *response* window then reads as follows:
modus_ponens A B H_A
: (A -> B) -> B
Since we have a witness of A -> among the assumptions, let us check the result of instantiating modus_ponens with A, B, H_A, and this witness:
modus_ponens A B H_A H_A_implies_B
: B
We can then apply H_B_implies_False to B:
Check (H_B_implies_False (modus_ponens A B H_A H_A_implies_B)).
Indeed the *response* window then reads as follows:
H_B_implies_False (modus_ponens A B H_A H_A_implies_B)
: False
This puts us one exact step away from completing the proof.
Alfrothul: Nice proofs.Anton: Yes. They neatly capture three distinct approaches.Mimer: And yet they are actually the same.Dana: You mean they prove the same proposition?Mimer: I mean that they are actually the same proof.Pablito: Come again?Mimer: All in due time.
Prove the following proposition:
Proposition implication_distributes_over_conjunction_on_the_left :
forall A B C : Prop,
(A -> B /\ C) <-> ((A -> B) /\ (A -> C)).
Pablito: Can I give it a shot?
Dana: Sure.
Pablito: Let’s get started:
Proof.
Dana: The *goals* window reads:
============================
forall A B C : Prop, (A -> B /\ C) <-> (A -> B) /\ (A -> C)
Pablito: Well, there is no choice here. Let’s use the intros tactic:
intros A B C.
Dana: The *goals* window reads:
A, B, C : Prop
============================
(A -> B /\ C) <-> (A -> B) /\ (A -> C)
Pablito: The goal is a bi-implication, and therefore a conjunction. So let’s use the split tactic:
split.
Dana: The whole *goals* window reads:
2 subgoals, subgoal 1 (ID 17)
A, B, C : Prop
============================
(A -> B /\ C) -> (A -> B) /\ (A -> C)
subgoal 2 (ID 18) is:
(A -> B) /\ (A -> C) -> A -> B /\ C
Pablito: Let’s focus on the first subgoal:
-
Dana: The *goals* window reads:
A, B, C : Prop
============================
(A -> B /\ C) -> (A -> B) /\ (A -> C)
Pablito: There is no choice here. Let’s use the intros tactic:
- intros H_A_implies_B_and_C.
Dana: The *goals* window reads:
A, B, C : Prop
H_A_implies_B_and_C : A -> B /\ C
============================
(A -> B) /\ (A -> C)
Pablito: There is still no choice here. Let’s use the split tactic:
split.
Dana: The whole *goals* window reads:
2 focused subgoals
(unfocused: 1), subgoal 1 (ID 21)
A, B, C : Prop
H_A_implies_B_and_C : A -> B /\ C
============================
A -> B
subgoal 2 (ID 22) is:
A -> C
Pablito: Ah, more subgoals. Well, let’s focus on the first one:
*
Dana: The *goals* window reads:
A, B, C : Prop
H_A_implies_B_and_C : A -> B /\ C
============================
A -> B
Pablito: So let’s use the intro tactic:
* intro H_A.
Dana: The *goals* window reads:
A, B, C : Prop
H_A_implies_B_and_C : A -> B /\ C
H_A : A
============================
B
Pablito: Now what.
Dana: Well, we can apply H_A_implies_B_and_C to H_A.
Pablito: Let me check:
Check (H_A_implies_B_and_C H_A).
Dana: The *response* window then reads:
H_A_implies_B_and_C H_A
: B /\ C
Pablito: OK?
Dana: We could destructure the resulting implication?
Pablito: You mean with the destruct tactic?
Dana: Yes, and name the resulting components ourselves with as [H_B H_C], or better with as [H_B _] since we don’t need the second one.
Pablito: Let me try:
destruct (H_A_implies_B_and_C H_A) as [H_B _].
Dana: Yes. The *goals* window then reads:
A, B, C : Prop
H_A_implies_B_and_C : A -> B /\ C
H_A : A
H_B : B
============================
B
Pablito: And we are one exact step away from solving this subgoal:
exact H_B.
Dana: Indeed. The *response* window then reads:
This subproof is complete, but there are some unfocused goals.
Focus next goal with bullet *.
Pablito: OK:
*
Dana: Right. The *goals* window now reads:
A, B, C : Prop
H_A_implies_B_and_C : A -> B /\ C
============================
A -> C
Pablito: Well, we should take essentially the same steps then: using the intro tactic to turn A into an assumption H_A and destructuring the result of applying H_A_implies_B_and_C to H_A.
Dana: Right. And this time we only need to name the right conjunct.
Pablito. Presto, and then the exact tactic:
* intro H_A.
destruct (H_A_implies_B_and_C H_A) as [_ H_C].
exact H_C.
Dana: Yup. The *response* window then reads:
This subproof is complete, but there are some unfocused goals.
Focus next goal with bullet -.
Pablito: Sure:
-
Dana: The *goals* window now reads:
A, B, C : Prop
============================
(A -> B) /\ (A -> C) -> A -> B /\ C
Pablito: OK. The intros tactic again:
- intros [H_A_implies_B H_A_implies_C] H_A.
Dana: And the *goals* window reads:
A, B, C : Prop
H_A_implies_B : A -> B
H_A_implies_C : A -> C
H_A : A
============================
B /\ C
Pablito: It looks like we could conjoin the applications of H_A_implies_B and of H_A_implies_C to H_A, could we not?
Dana: Show me.
Pablito: Let me check first:
Check (H_A_implies_B H_A).
Dana: The *response* window reads:
H_A_implies_B H_A
: B
Pablito: Let me check the conjunction:
Check (conj (H_A_implies_B H_A) (H_A_implies_C H_A)).
Dana: Indeed, Pablito. The *response* window now reads:
conj (H_A_implies_B H_A) (H_A_implies_C H_A)
: B /\ C
Pablito: All right:
exact (conj (H_A_implies_B H_A) (H_A_implies_C H_A)).
Dana: Congratulations, there are no more subgoals.
Pablito: Indeed:
Qed.
Halcyon: Yay!
Prove the following proposition:
Proposition implication_distributes_over_disjunction_on_the_right_and_with_a_twist :
forall A B C : Prop,
((A \/ B) -> C) <-> ((A -> C) /\ (B -> C)).
Alfrothul: Let’s get started:
Proof.
Anton: There is no choice here. Let’s use the intros tactic:
intros A B C.
Alfrothul: The *goals* window then reads:
A, B, C : Prop
============================
(A \/ B -> C) <-> (A -> C) /\ (B -> C)
Anton: Again, there is no choice here. Let’s use the split tactic, since bi-implication is syntactic sugar for a conjunction:
split.
Alfrothul: The whole *goals* window then reads:
2 subgoals, subgoal 1 (ID 16)
A, B, C : Prop
============================
(A \/ B -> C) -> (A -> C) /\ (B -> C)
subgoal 2 (ID 17) is:
(A -> C) /\ (B -> C) -> A \/ B -> C
Anton: It’s not really necessary, but let’s focus on the first subgoal, for clarity:
-
Alfrothul: The *goals* window then reads:
A, B, C : Prop
============================
(A \/ B -> C) -> (A -> C) /\ (B -> C)
Anton: Again, there is no choice here. Let’s use the intros tactic:
- intros H_A_or_B_implies_C.
Alfrothul: The *goals* window then reads:
A, B, C : Prop
H_A_or_B_implies_C : A \/ B -> C
============================
(A -> C) /\ (B -> C)
Anton: There is still no choice here. Let’s use the split tactic:
split.
Alfrothul: The whole *goals* window then reads:
2 focused subgoals
(unfocused: 1), subgoal 1 (ID 20)
A, B, C : Prop
H_A_or_B_implies_C : A \/ B -> C
============================
A -> C
subgoal 2 (ID 21) is:
B -> C
Anton: Ah, more subgoals. How about we trust the Force and focus on the first one:
+
Alfrothul: The *goals* window then reads:
A, B, C : Prop
H_A_or_B_implies_C : A \/ B -> C
============================
A -> C
Anton: Well, there is still no choice here. Let’s use the intro tactic:
+ intro H_A.
Alfrothul: The *goals* window then reads:
A, B, C : Prop
H_A_or_B_implies_C : A \/ B -> C
H_A : A
============================
C
Anton: Well, C is implied by one of the assumptions, so how about we use the apply tactic over this assumption:
apply H_A_or_B_implies_C.
Alfrothul: The *goals* window then reads:
A, B, C : Prop
H_A_or_B_implies_C : A \/ B -> C
H_A : A
============================
A \/ B
Anton: Since A is one of the assumptions, let’s select the left disjunct and use the left tactic:
left.
Alfrothul: The *goals* window then reads:
A, B, C : Prop
H_A_or_B_implies_C : A \/ B -> C
H_A : A
============================
A
Anton: Ah, we are one exact step away from the current subgoal:
exact H_A.
Alfrothul: The *response* window then reads:
This subproof is complete, but there are some unfocused goals.
Focus next goal with bullet +.
Anton: OK:
+
Alfrothul: The *goals* window then reads:
A, B, C : Prop
H_A_or_B_implies_C : A \/ B -> C
============================
B -> C
Anton: Ah, it’s the latest subgoal. Well, there is no choice here. Let’s use the intro tactic:
+ intro H_B.
Alfrothul: The *goals* window then reads:
A, B, C : Prop
H_A_or_B_implies_C : A \/ B -> C
H_B : B
============================
C
Anton: I see the pattern. We should use the apply tactic on H_A_or_B_implies_C, which will give us A \/ B as the new goal, then we can select the right disjunct since B is one of the assumptions, and then we are one exact step away from the then current subgoal. Let me try:
apply H_A_or_B_implies_C.
right.
exact H_B.
Alfrothul: Yay. The *response* window then reads:
This subproof is complete, but there are some unfocused goals.
Focus next goal with bullet -.
Anton: OK:
-
Alfrothul: The *goals* window then reads:
A, B, C : Prop
============================
(A -> C) /\ (B -> C) -> A \/ B -> C
Anton: Well, there is no choice here either. Let’s use the intros tactic:
- intros [H_A_implies_C H_B_implies_C] [H_A | H_B].
Alfrothul: The *goals* window then reads:
2 focused subgoals
(unfocused: 0), subgoal 1 (ID 40)
A, B, C : Prop
H_A_implies_C : A -> C
H_B_implies_C : B -> C
H_A : A
============================
C
subgoal 2 (ID 41) is:
C
Anton: I see. We need to focus on the first new subgoal, i.e., C. Then applying H_A_implies_C to H_A puts us one exact step away from proving C. And then we do the same for the other subgoal:
+ Check (H_A_implies_C H_A).
exact (H_A_implies_C H_A).
+ exact (H_B_implies_C H_B).
Alfrothul: Congratulations, there are no more subgoals.
Anton: Indeed:
Qed.
Halcyon: Yay!
Prove the contrapositive of an implication:
Proposition contrapositive_of_implication :
forall A B : Prop,
(A -> B) -> ~B -> ~A.
The proof starts as usual:
Proof.
intros A B.
intros H_A_implies_B H_not_B.
One would then be well inspired to check the following applications of the modus tollens rule:
Check (modus_tollens A B).
Check (modus_tollens A B H_not_B).
Check (modus_tollens A B H_not_B H_A_implies_B).
Reason about the contrapositive of the contrapositive of an implication:
Proposition contrapositive_of_contrapositive_of_implication :
forall A B : Prop,
(~B -> ~A) -> ~~A -> ~~B.
Dana: Could this proposition be an instance of contrapositive_of_implication?Na-bong (having fun): Why not.
Prove that a proposition implies its double negation:
Proposition double_negation :
forall A : Prop,
A -> ~~A.
Na-bong: Could this proposition be an instance of modus_ponens?Dana (having fun): Why not.
Added hints for Exercise 15, Exercise 16, and Exercise 17 [28 Jan 2024]
Added Exercise 12 [27 Jan 2024]
Created [25 Jan 2024]