PRFA.tp1c
Exercise session 1
Try and solve the following exercises by using the tactics shown in class:
intro, apply, destruct, split, left, right, exfalso, simpl, reflexivity,
f_equal, induction, assumption.
Lemmas currently end with the keyword Admitted which means the lemma is
accepted and can be used without a proof.
Replace Admitted with Qed once you have completed the proofs.
There are more exercises than what can be done in the exercise session during
the lecture.
Proving is like programming: You will have to practice at home.
It is fine not to do all the exercises, but you should feel like you *could*
do the exercises. We will help you with this assessment at the start of every
lecture.
Please send us this file with your (partial) solutions by email before the
next lecture:
yannick.forster@inria.fr, theo.winterhalter@inria.fr
We will begin with the exercises you have seen already.
Section TP1.
Context (P Q R : Prop).
Lemma P_imp_P : P → P.
Proof.
intro h.
apply h.
Qed.
Lemma and_comm : P ∧ Q → Q ∧ P.
Proof.
intro h.
destruct h as [hP hQ].
split.
- apply hQ.
- apply hP.
Qed.
Lemma or_comm : P ∨ Q → Q ∨ P.
Proof.
intro h.
destruct h as [hP | hQ].
- right.
apply hP.
- left.
apply hQ.
Qed.
Lemma truetrue : True.
Proof.
split.
Qed.
Lemma anything_goes : False → P.
Proof.
intro h.
destruct h.
Qed.
Lemma nofalse : ¬ False.
Proof.
intro h.
apply h.
Qed.
Now some new exercises about propositional logic
Lemma imp_trans : (P → Q) → (Q → R) → (P → R).
Proof.
intro hPQ. intro hQR. intro hP.
apply hQR. apply hPQ. apply hP.
Qed.
Lemma to_not_not : P → ~~ P.
Proof.
intro hP. intro hnP. apply hnP. apply hP.
Qed.
For this one, note that if you already separated a case distinction
with dashes (-) then you can use + at the next level.
The following level is marked with *.
Lemma distr : (P ∨ Q) ∧ R → (P ∧ R) ∨ (Q ∧ R).
Proof.
intro h. destruct h as [hPQ hR].
destruct hPQ as [hP | hQ].
- left. split.
+ apply hP.
+ apply hR.
- right. split.
+ apply hQ.
+ apply hR.
Qed.
Lemma contrad : P ∧ ¬ P → False.
Proof.
intro h. destruct h as [hP hnP].
apply hnP. apply hP.
Qed.
Classical logic
In Coq, excluded middle (P \/ ~ P) is not provable, we say that its logic
is intuitionistic, as opposed to classical.
It is possible to reason classically in Coq by taking excluded middle as
an axiom.
The law of excluded middle (LEM) is equivalent to other principles:
Pierce's law (PL): ((P -> Q) -> P) -> P
Double negation shift (DNS): ~~ P -> P
Show that LEM implies the other two. For that we are going to use
definitions to avoid repeating the principles all the time.
We will show the other direction later.
Definition LEM := P ∨ ¬ P.
Definition PL := ((P → Q) → P) → P.
Definition DNS := ~~ P → P.
Lemma lem_pl : LEM → PL.
Proof.
(* You can unfold definitions with the unfold tactic. *)
unfold LEM, PL.
intro lem.
intro h. destruct lem as [hP | hnP].
- apply hP.
- apply h. intro hP.
exfalso. apply hnP. apply hP.
Qed.
Lemma lem_dns : LEM → DNS.
Proof.
unfold LEM, DNS.
intro lem. intro hnnP.
destruct lem as [hP | hnP].
- assumption.
- exfalso. apply hnnP. apply hnP.
Qed.
To introduce several variables at once, you can use the intros tactic
Lemma dn_functorial : (P → Q) → ~~ P → ~~ Q.
Proof.
intros hPQ hnnP.
intro hnQ. apply hnnP. intro hP.
apply hnQ. apply hPQ. apply hP.
Qed.
Let us switch to booleans again
Context (b1 b2 b3 : bool).
Lemma andb_orb_distr :
andb b1 (orb b2 b3) = orb (andb b1 b2) (andb b1 b3).
Proof.
destruct b1.
- simpl. reflexivity.
- simpl. reflexivity.
Qed.
Lemma de_morgan :
negb (andb b1 b2) = orb (negb b1) (negb b2).
Proof.
destruct b1.
- simpl. reflexivity.
- simpl. reflexivity.
Qed.
Let us switch to natural numbers.
Let us make a lemma out of the n + 0 = n property.
You can then apply this lemma by using apply n_plus_0 like for hyoptheses!
Lemma n_plus_0 : n + 0 = n.
Proof.
induction n.
- simpl. reflexivity.
- simpl. f_equal. assumption.
Qed.
Lemma double_eq : n + n = 2 × n.
Proof.
simpl. f_equal. rewrite n_plus_0. reflexivity.
Qed.
End TP1.
We now start using quantifiers for natural numbers.
We write forall n m, n + m = m + n to mean that for all natural numbers
n and m, n + m is equal to m + n.
Let's show it, by first showing that n + S m = S n + m.
Lemma plus_S : ∀ n m, n + S m = S n + m.
Proof.
(* forall works a bit like -> so we can use intro as well *)
intro n. (* We now have n : nat as hypothesis *)
induction n.
- intro m. simpl. reflexivity.
- intro m. simpl. f_equal. apply IHn.
Qed.
Lemma plus_comm : ∀ n m, n + m = m + n.
Proof.
intro n. induction n.
- intro m. simpl.
(* We now face a similar situation as before.
We can apply the lemma n_plus_0 now. Indeed now that we left the
section, it has been generalised.
See for yourself.
*)
About n_plus_0.
Fail apply n_plus_0.
(* Wait! It doesn't work because it proves m + 0 = m but we need m = m + 0!
We will use the rewrite tactic instead.
rewrite n_plus_0 will turn m + 0 into m in the goal.
*)
rewrite n_plus_0.
reflexivity.
- intro m. simpl.
rewrite plus_S. simpl. f_equal.
apply IHn.
Qed.
Show associativity of additon
Lemma plus_assoc : ∀ k n m, k + n + m = k + (n + m).
Proof.
intro k. induction k.
- intros n m. simpl. reflexivity.
- intros n m. simpl. f_equal. apply IHk.
Qed.
We can also show commutativity of multiplication.
Try to come up with the lemmas yourself.
Note that you can also use rewrite in the opposite direction by using
rewrite <- n_plus_0
for instance.
You can also use rewrite with hypotheses you have.
If you ever find yourself with x = y to prove, when you think you can
prove y = x, you can also use the symmetry tactic.
Lemma mult_0 : ∀ n, n × 0 = 0.
Proof.
intro n. induction n.
- simpl. reflexivity.
- simpl. assumption.
Qed.
Lemma mult_S : ∀ n m, n × S m = n + n × m.
Proof.
intro n. induction n.
- intro m. simpl. reflexivity.
- intro m. simpl. f_equal.
rewrite IHn.
rewrite plus_comm. rewrite plus_assoc.
f_equal. rewrite plus_comm.
reflexivity.
Qed.
Lemma mult_comm : ∀ n m, n × m = m × n.
Proof.
intros n m.
induction n.
- simpl. rewrite mult_0. reflexivity.
- simpl. rewrite mult_S. rewrite IHn. reflexivity.
Qed.
Fill in the cases for the following function.
We use a placeholder REPLACE_ME that you need to replace.
Definition REPLACE_ME := 123.
Fixpoint min (n m : nat) :=
match n, m with
| 0, _ ⇒ 0
| _, 0 ⇒ 0
| S n, S m ⇒ min n m
end.
Lemma min_comm : ∀ n m, min n m = min m n.
Proof.
intro n.
(* Hint: start the induction before introducing m *)
induction n.
- intro m. destruct m.
+ simpl. reflexivity.
+ simpl. reflexivity.
- intro m. destruct m.
+ simpl. reflexivity.
+ simpl. apply IHn.
Qed.
Fixpoint min (n m : nat) :=
match n, m with
| 0, _ ⇒ 0
| _, 0 ⇒ 0
| S n, S m ⇒ min n m
end.
Lemma min_comm : ∀ n m, min n m = min m n.
Proof.
intro n.
(* Hint: start the induction before introducing m *)
induction n.
- intro m. destruct m.
+ simpl. reflexivity.
+ simpl. reflexivity.
- intro m. destruct m.
+ simpl. reflexivity.
+ simpl. apply IHn.
Qed.
ADVANCED EXERCISES
If you have already used Coq before or you are done with the exercises,
give the advanced exercises a try.
They hopefully teach you thinks you have not seen before.
We introduce a new notation P <-> Q meaning P is equivalent to Q.
It is essentially a notation for P -> Q /\ Q -> P so you can use the
tactics split and destruct to prove it and use it.
Here is a trivial example to understand it.
And here is a new tactic that is going to be useful: assert
When you write assert (h : P) you are telling Coq that you want to prove P
and that then you are going to use this as an hypothesis named h.
This is sometimes called forward reasoning.
See how it works below.
Lemma or_imp : (Q → P) ∧ (R → P) → Q ∨ R → ~~ P.
Proof.
intros h1 h2.
assert (hP : P).
{ destruct h1 as [hQP hRP].
destruct h2 as [hQ | hR].
- apply hQP. apply hQ.
- apply hRP. apply hR.
}
apply to_not_not. apply hP.
Qed.
Lemma Russel : ¬ (P ↔ ¬ P).
Proof.
intro h. destruct h as [h1 h2].
assert (hP : P).
{ apply h2. intro hP. apply h1.
- apply hP.
- apply hP.
}
assert (hnP : ¬ P).
{ apply h1. apply hP. }
apply hnP. apply hP.
Qed.
End Advanced.
For even more advanced stuff we are going to use quantifiers
on propositions too. It's basically the same as with natural numbers.
If you have some hypothesis of the form
h : forall x, P x
then know that you can use
specialize (h y) to obtain h : P y.
See the following example.
Lemma forall_False : (∀ (P : Prop), P) → False.
Proof.
intro h.
specialize (h False).
assumption.
Qed.
Note that it would work with apply directly in this case.
Prove the converse now
Let us go back to LEM, PL and DNS, their proper definitions use quantifiers
of course.
Definition theLEM := ∀ P, P ∨ ¬ P.
Definition theDNS := ∀ P, ~~ P → P.
Definition thePL := ∀ P Q, ((P → Q) → P) → P.
We can now prove the other direction from before.
Lemma dns_lem : theDNS → theLEM.
Proof.
unfold theDNS, theLEM.
intro dns. intro P.
apply dns. intro h.
assert (hnP : ¬ P).
{ intro hP. apply h. left. assumption. }
apply h. right. assumption.
Qed.
Lemma pl_lem : thePL → theLEM.
Proof.
unfold thePL.
intro pl. apply dns_lem.
unfold theDNS. intro P.
specialize (pl P). specialize (pl False).
intro hnnP.
apply pl. intro hnP.
exfalso. apply hnnP. intro hP. apply hnP. assumption.
Qed.
An example of commuting forall and \/
Lemma forall_or :
∀ P Q,
(Q ∨ ¬ Q) →
(∀ (x : nat), P x ∨ Q) →
(∀ x, P x) ∨ Q.
Proof.
intros P Q lemQ h.
destruct lemQ as [hQ | hnQ].
- right. assumption.
- left. intro x.
specialize (h x). destruct h as [hPx | hQ].
+ assumption.
+ exfalso. apply hnQ. assumption.
Qed.
More classical reasoning.
Lemma classical_or_contra_r :
theLEM →
∀ (P Q : Prop),
(¬ Q → P) →
P ∨ Q.
Proof.
intros lem P Q h.
specialize (lem Q). destruct lem as [hQ | hnQ].
- right. assumption.
- left. apply h. assumption.
Qed.
(* For the following do you need LEM for both directions? *)
Lemma classical_impl :
theLEM →
∀ (P Q : Prop),
(P → Q) ↔ (¬ P ∨ Q).
Proof.
intros lem P Q.
split.
- intro h. specialize (lem P). destruct lem.
+ right. apply h. assumption.
+ left. assumption.
- intros h hP. destruct h as [hnP | hQ].
+ exfalso. apply hnP. apply hP.
+ assumption.
Qed.
Lemma contrapositive :
theLEM →
∀ (P Q : Prop),
(¬ Q → ¬ P) →
P → Q.
Proof.
intros lem P Q h hP.
specialize (lem Q). destruct lem as [hQ | hnQ].
- assumption.
- exfalso.
apply h. (* Notice we get two goals! Because h : ~ Q -> P -> False *)
+ assumption.
+ assumption.
Qed.
Note: if you want to use specialize on a hyothesis twice, you
can use specialize (h x) as hx to create a new hypothesis instead of
replacing h.
Lemma twice :
theLEM →
∀ (P Q : Prop),
((P → Q) → Q) →
((Q → P) → P).
Proof.
intros lem P Q h h'.
specialize (lem P) as lemP.
destruct lemP as [hP | hnP].
- assumption.
- specialize (lem Q) as lemQ.
destruct lemQ as [hQ | hnQ].
+ apply h'. assumption.
+ exfalso. apply hnQ. apply h.
intro hP. exfalso. apply hnP. apply hP.
Qed.
More natural numbers.
Sometimes you will need to generalise a goal before calling the induction
tactic. To that end you can use the revert tactic that works as the opposite
of intro.
For instance if you have goal
n, m, k : nat
something
then you can type
revert m.
and obtain goal
n, k : nat
forall m, something
something
forall m, something
Lemma mult_distr :
∀ n m k,
k × (n + m) = k × n + k × m.
Proof.
intros n m k.
revert n m.
induction k.
- intros n m. simpl. reflexivity.
- intros n m. simpl.
rewrite IHk.
rewrite <- plus_assoc.
symmetry. rewrite <- plus_assoc.
f_equal. symmetry.
rewrite plus_comm. rewrite <- plus_assoc. f_equal.
rewrite plus_comm. reflexivity.
Qed.
Of course, proofs like this are not written in practice.
We show you what is going on under the hood to explain how things work.
In practice Coq users will use the lia tactic to solve a lot of integer
arithmetic problems.