Exercise session 1 — Solutions

Authors:

Yannick Forster

Théo Winterhalter

Files:

Display all goals and responses

Try to 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.

We will begin with the exercises you have seen already.

Lemma P_imp_P (P : Prop) : P -> P.P: Prop
P -> P
Proof.P: Prop
P -> P
  intro h.P: Prop
h: P
P
  apply h.
Qed.

Lemma and_comm (P Q : Prop) : P /\ Q -> Q /\ P.P, Q: Prop
P /\ Q -> Q /\ P
Proof.P, Q: Prop
P /\ Q -> Q /\ P
  intro h.P, Q: Prop
h: P /\ Q
Q /\ P
  destruct h as [hP hQ].P, Q: Prop
hP: P
hQ: Q
Q /\ P
  split.P, Q: Prop
hP: P
hQ: Q
Q
P, Q: Prop
hP: P
hQ: Q
P
  -P, Q: Prop
hP: P
hQ: Q
Q apply hQ.
  -P, Q: Prop
hP: P
hQ: Q
P apply hP.
Qed.

Lemma or_comm (P Q : Prop) : P \/ Q -> Q \/ P.P, Q: Prop
P \/ Q -> Q \/ P
Proof.P, Q: Prop
P \/ Q -> Q \/ P
  intro h.P, Q: Prop
h: P \/ Q
Q \/ P
  destruct h as [hP | hQ].P, Q: Prop
hP: P
Q \/ P
P, Q: Prop
hQ: Q
Q \/ P
  -P, Q: Prop
hP: P
Q \/ P right.P, Q: Prop
hP: P
P
    apply hP.
  -P, Q: Prop
hQ: Q
Q \/ P left.P, Q: Prop
hQ: Q
Q
    apply hQ.
Qed.

Lemma truetrue : True.True
  split.
Qed.

Lemma anything_goes (P : Prop) : False -> P.P: Prop
False -> P
Proof.P: Prop
False -> P
  intro h.P: Prop
h: False
P
  destruct h.
Qed.

Lemma nofalse : ~ False.~ False
Proof.~ False
  intro h.h: False
False
  apply h.
Qed.

Now some new exercises about propositional logic.

Lemma imp_trans (P Q R : Prop) : (P -> Q) -> (Q -> R) -> (P -> R).P, Q, R: Prop
(P -> Q) -> (Q -> R) -> P -> R
Proof.P, Q, R: Prop
(P -> Q) -> (Q -> R) -> P -> R
  intro hPQ.P, Q, R: Prop
hPQ: P -> Q
(Q -> R) -> P -> R intro hQR.P, Q, R: Prop
hPQ: P -> Q
hQR: Q -> R
P -> R intro hP.P, Q, R: Prop
hPQ: P -> Q
hQR: Q -> R
hP: P
R
  apply hQR.P, Q, R: Prop
hPQ: P -> Q
hQR: Q -> R
hP: P
Q apply hPQ.P, Q, R: Prop
hPQ: P -> Q
hQR: Q -> R
hP: P
P apply hP.
Qed.

Lemma to_not_not (P : Prop) : P -> ~~ P.P: Prop
P -> ~ ~ P
Proof.P: Prop
P -> ~ ~ P
  intro hP.P: Prop
hP: P
~ ~ P intro hnP.P: Prop
hP: P
hnP: ~ P
False apply hnP.P: Prop
hP: P
hnP: ~ P
P 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 : Prop) : (P \/ Q) /\ R -> (P /\ R) \/ (Q /\ R).P, Q, R: Prop
(P \/ Q) /\ R -> P /\ R \/ Q /\ R
Proof.P, Q, R: Prop
(P \/ Q) /\ R -> P /\ R \/ Q /\ R
  intro h.P, Q, R: Prop
h: (P \/ Q) /\ R
P /\ R \/ Q /\ R destruct h as [hPQ hR].P, Q, R: Prop
hPQ: P \/ Q
hR: R
P /\ R \/ Q /\ R
  destruct hPQ as [hP | hQ].P, Q, R: Prop
hP: P
hR: R
P /\ R \/ Q /\ R
P, Q, R: Prop
hQ: Q
hR: R
P /\ R \/ Q /\ R
  -P, Q, R: Prop
hP: P
hR: R
P /\ R \/ Q /\ R left.P, Q, R: Prop
hP: P
hR: R
P /\ R split.P, Q, R: Prop
hP: P
hR: R
P
P, Q, R: Prop
hP: P
hR: R
R
    +P, Q, R: Prop
hP: P
hR: R
P apply hP.
    +P, Q, R: Prop
hP: P
hR: R
R apply hR.
  -P, Q, R: Prop
hQ: Q
hR: R
P /\ R \/ Q /\ R right.P, Q, R: Prop
hQ: Q
hR: R
Q /\ R split.P, Q, R: Prop
hQ: Q
hR: R
Q
P, Q, R: Prop
hQ: Q
hR: R
R
    +P, Q, R: Prop
hQ: Q
hR: R
Q apply hQ.
    +P, Q, R: Prop
hQ: Q
hR: R
R apply hR.
Qed.

Lemma contrad (P : Prop) : P /\ ~ P -> False.P: Prop
P /\ ~ P -> False
Proof.P: Prop
P /\ ~ P -> False
  intro h.P: Prop
h: P /\ ~ P
False destruct h as [hP hnP].P: Prop
hP: P
hnP: ~ P
False
  apply hnP.P: Prop
hP: P
hnP: ~ P
P apply hP.
Qed.

Lemma lem_pl (P Q : Prop) : P \/ ~ P -> ((P -> Q) -> P) -> P.P, Q: Prop
P \/ ~ P -> ((P -> Q) -> P) -> P
Proof.P, Q: Prop
P \/ ~ P -> ((P -> Q) -> P) -> P
  intro lem.P, Q: Prop
lem: P \/ ~ P
((P -> Q) -> P) -> P
  intro h.P, Q: Prop
lem: P \/ ~ P
h: (P -> Q) -> P
P destruct lem as [hP | hnP].P, Q: Prop
hP: P
h: (P -> Q) -> P
P
P, Q: Prop
hnP: ~ P
h: (P -> Q) -> P
P
  -P, Q: Prop
hP: P
h: (P -> Q) -> P
P apply hP.
  -P, Q: Prop
hnP: ~ P
h: (P -> Q) -> P
P apply h.P, Q: Prop
hnP: ~ P
h: (P -> Q) -> P
P -> Q intro hP.P, Q: Prop
hnP: ~ P
h: (P -> Q) -> P
hP: P
Q
    exfalso.P, Q: Prop
hnP: ~ P
h: (P -> Q) -> P
hP: P
False apply hnP.P, Q: Prop
hnP: ~ P
h: (P -> Q) -> P
hP: P
P apply hP.
Qed.

Lemma lem_dns (P : Prop) : P \/ ~ P -> ~~ P -> P.P: Prop
P \/ ~ P -> ~ ~ P -> P
Proof.P: Prop
P \/ ~ P -> ~ ~ P -> P
  intro lem.P: Prop
lem: P \/ ~ P
~ ~ P -> P intro hnnP.P: Prop
lem: P \/ ~ P
hnnP: ~ ~ P
P
  destruct lem as [hP | hnP].P: Prop
hP: P
hnnP: ~ ~ P
P
P: Prop
hnP: ~ P
hnnP: ~ ~ P
P
  -P: Prop
hP: P
hnnP: ~ ~ P
P assumption.
  -P: Prop
hnP: ~ P
hnnP: ~ ~ P
P exfalso.P: Prop
hnP: ~ P
hnnP: ~ ~ P
False apply hnnP.P: Prop
hnP: ~ P
hnnP: ~ ~ P
~ P apply hnP.
Qed.

To introduce several variables at once, you can use the intros tactic.

Lemma dn_functorial P Q : (P -> Q) -> ~~ P -> ~~ Q.P, Q: Prop
(P -> Q) -> ~ ~ P -> ~ ~ Q
Proof.P, Q: Prop
(P -> Q) -> ~ ~ P -> ~ ~ Q
  intros hPQ hnnP.P, Q: Prop
hPQ: P -> Q
hnnP: ~ ~ P
~ ~ Q
  intro hnQ.P, Q: Prop
hPQ: P -> Q
hnnP: ~ ~ P
hnQ: ~ Q
False apply hnnP.P, Q: Prop
hPQ: P -> Q
hnnP: ~ ~ P
hnQ: ~ Q
~ P intro hP.P, Q: Prop
hPQ: P -> Q
hnnP: ~ ~ P
hnQ: ~ Q
hP: P
False
  apply hnQ.P, Q: Prop
hPQ: P -> Q
hnnP: ~ ~ P
hnQ: ~ Q
hP: P
Q apply hPQ.P, Q: Prop
hPQ: P -> Q
hnnP: ~ ~ P
hnQ: ~ Q
hP: P
P apply hP.
Qed.

Let us switch to Booleans again.

andb is conjunction, orb is disjunction, negb is negation. Both andb and ordb look at the first Boolean before simplifying.

Lemma andb_orb_distr (b1 b2 b3 : bool) :
  andb b1 (orb b2 b3) = orb (andb b1 b2) (andb b1 b3).b1, b2, b3: bool
(b1 && (b2 || b3))%bool = (b1 && b2 || b1 && b3)%bool
Proof.b1, b2, b3: bool
(b1 && (b2 || b3))%bool = (b1 && b2 || b1 && b3)%bool
  destruct b1.b2, b3: bool
(true && (b2 || b3))%bool = (true && b2 || true && b3)%bool
b2, b3: bool
(false && (b2 || b3))%bool = (false && b2 || false && b3)%bool
  -b2, b3: bool
(true && (b2 || b3))%bool = (true && b2 || true && b3)%bool simpl.b2, b3: bool
(b2 || b3)%bool = (b2 || b3)%bool reflexivity.
  -b2, b3: bool
(false && (b2 || b3))%bool = (false && b2 || false && b3)%bool simpl.b2, b3: bool
false = false reflexivity.
Qed.

Lemma de_morgan (b1 b2 : bool) :
  negb (andb b1 b2) = orb (negb b1) (negb b2).b1, b2: bool
negb (b1 && b2) = (negb b1 || negb b2)%bool
Proof.b1, b2: bool
negb (b1 && b2) = (negb b1 || negb b2)%bool
  destruct b1.b2: bool
negb (true && b2) = (negb true || negb b2)%bool
b2: bool
negb (false && b2) = (negb false || negb b2)%bool
  -b2: bool
negb (true && b2) = (negb true || negb b2)%bool simpl.b2: bool
negb b2 = negb b2 reflexivity.
  -b2: bool
negb (false && b2) = (negb false || negb b2)%bool simpl.b2: bool
true = true reflexivity.
Qed.

Let us switch to natural numbers.

Lemma calc_12_3 : 12 + 3 = 15.12 + 3 = 15
Proof.12 + 3 = 15
  simpl.15 = 15 reflexivity.
Qed.

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 hypotheses!

Lemma n_plus_0 (n : nat) : n + 0 = n.n: nat
n + 0 = n
Proof.n: nat
n + 0 = n
  induction n.0 + 0 = 0
n: nat
IHn: n + 0 = n
S n + 0 = S n
  -0 + 0 = 0 simpl.0 = 0 reflexivity.
  -n: nat
IHn: n + 0 = n
S n + 0 = S n simpl.n: nat
IHn: n + 0 = n
S (n + 0) = S n f_equal.n: nat
IHn: n + 0 = n
n + 0 = n assumption.
Qed.

Lemma double_eq (n : nat) : n + n = 2 * n.n: nat
n + n = 2 * n
Proof.n: nat
n + n = 2 * n
  simpl.n: nat
n + n = n + (n + 0) f_equal.n: nat
n = n + 0 rewrite n_plus_0.n: nat
n = n reflexivity.
Qed.

Lemma plus_S (n m : nat) : n + S m = S n + m.n, m: nat
n + S m = S n + m
Proof.n, m: nat
n + S m = S n + m
  induction n as [| n ih].m: nat
0 + S m = 1 + m
n, m: nat
ih: n + S m = S n + m
S n + S m = S (S n) + m
  -m: nat
0 + S m = 1 + m simpl.m: nat
S m = S m reflexivity.
  -n, m: nat
ih: n + S m = S n + m
S n + S m = S (S n) + m simpl.n, m: nat
ih: n + S m = S n + m
S (n + S m) = S (S (n + m)) f_equal.n, m: nat
ih: n + S m = S n + m
n + S m = S (n + m) apply ih.
Qed.

Lemma plus_comm (n m : nat) : n + m = m + n.n, m: nat
n + m = m + n
Proof.n, m: nat
n + m = m + n
  induction n.m: nat
0 + m = m + 0
n, m: nat
IHn: n + m = m + n
S n + m = m + S n
  -m: nat
0 + m = m + 0 simpl.m: nat
m = m + 0
    rewrite n_plus_0.m: nat
m = m
    reflexivity.
  -n, m: nat
IHn: n + m = m + n
S n + m = m + S n simpl.n, m: nat
IHn: n + m = m + n
S (n + m) = m + S n
    rewrite plus_S.n, m: nat
IHn: n + m = m + n
S (n + m) = S m + n simpl.n, m: nat
IHn: n + m = m + n
S (n + m) = S (m + n) f_equal.n, m: nat
IHn: n + m = m + n
n + m = m + n
    assumption.
Qed.

Show associativity of additon.

Lemma plus_assoc (k n m : nat) : k + n + m = k + (n + m).k, n, m: nat
k + n + m = k + (n + m)
Proof.k, n, m: nat
k + n + m = k + (n + m)
  induction k.n, m: nat
0 + n + m = 0 + (n + m)
k, n, m: nat
IHk: k + n + m = k + (n + m)
S k + n + m = S k + (n + m)
  -n, m: nat
0 + n + m = 0 + (n + m) simpl.n, m: nat
n + m = n + m reflexivity.
  -k, n, m: nat
IHk: k + n + m = k + (n + m)
S k + n + m = S k + (n + m) simpl.k, n, m: nat
IHk: k + n + m = k + (n + m)
S (k + n + m) = S (k + (n + m)) f_equal.k, n, m: nat
IHk: k + n + m = k + (n + m)
k + n + m = k + (n + m) assumption.
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.

Fill in the cases for the following function.

Fixpoint min (n m : nat) :=
  match n, m with
  | 0, _ => 0
  | _, 0 => 0
  | S n, S m => S (min n m)
  end.

Lemma min_comm : forall n m, min n m = min m n.forall n m : nat, min n m = min m n
Proof.forall n m : nat, min n m = min m n
  intro n.n: nat
forall m : nat, min n m = min m n

Hint: start the induction before introducing m. You can also use induction ... in.

  induction n as [| ? ih].forall m : nat, min 0 m = min m 0
n: nat
ih: forall m : nat, min n m = min m n
forall m : nat, min (S n) m = min m (S n)
  -forall m : nat, min 0 m = min m 0 intro m.m: nat
min 0 m = min m 0 destruct m.min 0 0 = min 0 0
m: nat
min 0 (S m) = min (S m) 0
    +min 0 0 = min 0 0 simpl.0 = 0 reflexivity.
    +m: nat
min 0 (S m) = min (S m) 0 simpl.m: nat
0 = 0 reflexivity.
  -n: nat
ih: forall m : nat, min n m = min m n
forall m : nat, min (S n) m = min m (S n) intro m.n: nat
ih: forall m : nat, min n m = min m n
m: nat
min (S n) m = min m (S n) destruct m.n: nat
ih: forall m : nat, min n m = min m n
min (S n) 0 = min 0 (S n)
n: nat
ih: forall m : nat, min n m = min m n
m: nat
min (S n) (S m) = min (S m) (S n)
    +n: nat
ih: forall m : nat, min n m = min m n
min (S n) 0 = min 0 (S n) simpl.n: nat
ih: forall m : nat, min n m = min m n
0 = 0 reflexivity.
    +n: nat
ih: forall m : nat, min n m = min m n
m: nat
min (S n) (S m) = min (S m) (S n) simpl.n: nat
ih: forall m : nat, min n m = min m n
m: nat
S (min n m) = S (min m n) f_equal.n: nat
ih: forall m : nat, min n m = min m n
m: nat
min n m = min m n apply ih.
Qed.

ADVANCED EXERCISES

If you have already used Rocq before or you are done with the exercises, give the advanced exercises a try. They hopefully teach you thinks you have not seen before.

If they are too hard, don't worry too much about it for the exam.

Section Advanced.

  Context (P Q R : Prop).

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.

  Lemma P_iff_P : P <-> P.P, Q, R: Prop
P <-> P
  Proof.P, Q, R: Prop
P <-> P
    split.P, Q, R: Prop
P -> P
P, Q, R: Prop
P -> P
    -P, Q, R: Prop
P -> P intro.P, Q, R: Prop
H: P
P assumption.
    -P, Q, R: Prop
P -> P intro.P, Q, R: Prop
H: P
P assumption.
  Qed.

And here is a new tactic that is going to be useful: assert.

When you write assert (h : P) you are telling Rocq 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.P, Q, R: Prop
(Q -> P) /\ (R -> P) -> Q \/ R -> ~ ~ P
  Proof.P, Q, R: Prop
(Q -> P) /\ (R -> P) -> Q \/ R -> ~ ~ P
    intros h1 h2.P, Q, R: Prop
h1: (Q -> P) /\ (R -> P)
h2: Q \/ R
~ ~ P
    assert (hP : P).P, Q, R: Prop
h1: (Q -> P) /\ (R -> P)
h2: Q \/ R
P
P, Q, R: Prop
h1: (Q -> P) /\ (R -> P)
h2: Q \/ R
hP: P
~ ~ P
    {P, Q, R: Prop
h1: (Q -> P) /\ (R -> P)
h2: Q \/ R
P destruct h1 as [hQP hRP].P, Q, R: Prop
hQP: Q -> P
hRP: R -> P
h2: Q \/ R
P
      destruct h2 as [hQ | hR].P, Q, R: Prop
hQP: Q -> P
hRP: R -> P
hQ: Q
P
P, Q, R: Prop
hQP: Q -> P
hRP: R -> P
hR: R
P
      -P, Q, R: Prop
hQP: Q -> P
hRP: R -> P
hQ: Q
P apply hQP.P, Q, R: Prop
hQP: Q -> P
hRP: R -> P
hQ: Q
Q apply hQ.
      -P, Q, R: Prop
hQP: Q -> P
hRP: R -> P
hR: R
P apply hRP.P, Q, R: Prop
hQP: Q -> P
hRP: R -> P
hR: R
R apply hR.
    }P, Q, R: Prop
h1: (Q -> P) /\ (R -> P)
h2: Q \/ R
hP: P
~ ~ P
    apply to_not_not.P, Q, R: Prop
h1: (Q -> P) /\ (R -> P)
h2: Q \/ R
hP: P
P apply hP.
  Qed.

  Lemma Russel : ~ (P <-> ~ P).P, Q, R: Prop
~ (P <-> ~ P)
  Proof.P, Q, R: Prop
~ (P <-> ~ P)
    intro h.P, Q, R: Prop
h: P <-> ~ P
False destruct h as [h1 h2].P, Q, R: Prop
h1: P -> ~ P
h2: ~ P -> P
False
    assert (hP : P).P, Q, R: Prop
h1: P -> ~ P
h2: ~ P -> P
P
P, Q, R: Prop
h1: P -> ~ P
h2: ~ P -> P
hP: P
False
    {P, Q, R: Prop
h1: P -> ~ P
h2: ~ P -> P
P apply h2.P, Q, R: Prop
h1: P -> ~ P
h2: ~ P -> P
~ P intro hP.P, Q, R: Prop
h1: P -> ~ P
h2: ~ P -> P
hP: P
False apply h1.P, Q, R: Prop
h1: P -> ~ P
h2: ~ P -> P
hP: P
P
P, Q, R: Prop
h1: P -> ~ P
h2: ~ P -> P
hP: P
P
      -P, Q, R: Prop
h1: P -> ~ P
h2: ~ P -> P
hP: P
P apply hP.
      -P, Q, R: Prop
h1: P -> ~ P
h2: ~ P -> P
hP: P
P apply hP.
    }P, Q, R: Prop
h1: P -> ~ P
h2: ~ P -> P
hP: P
False
    assert (hnP : ~ P).P, Q, R: Prop
h1: P -> ~ P
h2: ~ P -> P
hP: P
~ P
P, Q, R: Prop
h1: P -> ~ P
h2: ~ P -> P
hP: P
hnP: ~ P
False
    {P, Q, R: Prop
h1: P -> ~ P
h2: ~ P -> P
hP: P
~ P apply h1.P, Q, R: Prop
h1: P -> ~ P
h2: ~ P -> P
hP: P
P apply hP. }P, Q, R: Prop
h1: P -> ~ P
h2: ~ P -> P
hP: P
hnP: ~ P
False
    apply hnP.P, Q, R: Prop
h1: P -> ~ P
h2: ~ P -> P
hP: P
hnP: ~ P
P apply hP.
  Qed.

End Advanced.

For even more advanced stuff we are going to use quantifiers on propositions too. Its 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 : (forall (P : Prop), P) -> False.(forall P : Prop, P) -> False
Proof.(forall P : Prop, P) -> False
  intro h.h: forall P : Prop, P
False
  specialize (h False).h: False
False
  assumption.
Qed.

Note that it would work with apply directly in this case.

Lemma forall_False' : (forall (P : Prop), P) -> False.(forall P : Prop, P) -> False
Proof.(forall P : Prop, P) -> False
  intro h.h: forall P : Prop, P
False
  apply h.
Qed.

Prove the converse now.

Lemma False_forall : False -> (forall (P : Prop), P).False -> forall P : Prop, P
Proof.False -> forall P : Prop, P
  intro h.h: False
forall P : Prop, P
  destruct h.
Qed.

Rocq is, at its basis, as system that has nothing but elimination and introduction rules for disjunctions:

\begin{equation*} \frac{P}{P \vee Q} \end{equation*}

\begin{equation*} \frac{Q}{P \vee Q} \end{equation*}

\begin{equation*} \frac{P \vee Q \qquad P \Longrightarrow R \qquad Q \Longrightarrow R}{R} \end{equation*}

In particular, these rules do not allow proving

\begin{equation*} P \vee \neg P \end{equation*}

In other words, Rocq implements intuitionistic logic. This allows

assuming classical laws of reasoning like the law of excluded middle and doing classical math

not assuming the law of excluded middle, thus being able to have interesting proofs of the form A -> LEM for a statement A.

We will prove A <-> LEM for two statements now:

Law of Excluded Middle

Definition theLEM := forall P, P \/ ~ P.

Double Negation Shift

Definition theDNS := forall P, ~~ P -> P.

Peirce's law

Definition thePL := forall P Q : Prop, ((P -> Q) -> P) -> P.

We can now prove the other direction from before.

Lemma lem_dns_general : theLEM -> theDNS.theLEM -> theDNS
Proof.theLEM -> theDNS

You can use unfold to replace a name by its definition.

  unfold theLEM, theDNS.(forall P : Prop, P \/ ~ P) -> forall P : Prop, ~ ~ P -> P
  intros lem P h.lem: forall P : Prop, P \/ ~ P
P: Prop
h: ~ ~ P
P
  destruct (lem P) as [hP | hnP].lem: forall P : Prop, P \/ ~ P
P: Prop
h: ~ ~ P
hP: P
P
lem: forall P : Prop, P \/ ~ P
P: Prop
h: ~ ~ P
hnP: ~ P
P
  -lem: forall P : Prop, P \/ ~ P
P: Prop
h: ~ ~ P
hP: P
P assumption.
  -lem: forall P : Prop, P \/ ~ P
P: Prop
h: ~ ~ P
hnP: ~ P
P contradiction.
Qed.

Lemma lem_pl_general : theLEM -> thePL.theLEM -> thePL
Proof.theLEM -> thePL
  unfold theLEM, thePL.(forall P : Prop, P \/ ~ P) -> forall P Q : Prop, ((P -> Q) -> P) -> P
  intros lem P Q h.lem: forall P : Prop, P \/ ~ P
P, Q: Prop
h: (P -> Q) -> P
P
  destruct (lem P) as [hP | hnP].lem: forall P : Prop, P \/ ~ P
P, Q: Prop
h: (P -> Q) -> P
hP: P
P
lem: forall P : Prop, P \/ ~ P
P, Q: Prop
h: (P -> Q) -> P
hnP: ~ P
P
  -lem: forall P : Prop, P \/ ~ P
P, Q: Prop
h: (P -> Q) -> P
hP: P
P assumption.
  -lem: forall P : Prop, P \/ ~ P
P, Q: Prop
h: (P -> Q) -> P
hnP: ~ P
P apply h.lem: forall P : Prop, P \/ ~ P
P, Q: Prop
h: (P -> Q) -> P
hnP: ~ P
P -> Q contradiction.
Qed.

Lemma dns_lem : theDNS -> theLEM.theDNS -> theLEM
Proof.theDNS -> theLEM
  unfold theDNS, theLEM.(forall P : Prop, ~ ~ P -> P) -> forall P : Prop, P \/ ~ P
  intros dns P.dns: forall P : Prop, ~ ~ P -> P
P: Prop
P \/ ~ P
  apply dns.dns: forall P : Prop, ~ ~ P -> P
P: Prop
~ ~ (P \/ ~ P) intros hn.dns: forall P : Prop, ~ ~ P -> P
P: Prop
hn: ~ (P \/ ~ P)
False
  assert (hnP : ~ P).dns: forall P : Prop, ~ ~ P -> P
P: Prop
hn: ~ (P \/ ~ P)
~ P
dns: forall P : Prop, ~ ~ P -> P
P: Prop
hn: ~ (P \/ ~ P)
hnP: ~ P
False
  {dns: forall P : Prop, ~ ~ P -> P
P: Prop
hn: ~ (P \/ ~ P)
~ P intros hP.dns: forall P : Prop, ~ ~ P -> P
P: Prop
hn: ~ (P \/ ~ P)
hP: P
False apply hn.dns: forall P : Prop, ~ ~ P -> P
P: Prop
hn: ~ (P \/ ~ P)
hP: P
P \/ ~ P left.dns: forall P : Prop, ~ ~ P -> P
P: Prop
hn: ~ (P \/ ~ P)
hP: P
P assumption. }dns: forall P : Prop, ~ ~ P -> P
P: Prop
hn: ~ (P \/ ~ P)
hnP: ~ P
False
  apply hn.dns: forall P : Prop, ~ ~ P -> P
P: Prop
hn: ~ (P \/ ~ P)
hnP: ~ P
P \/ ~ P right.dns: forall P : Prop, ~ ~ P -> P
P: Prop
hn: ~ (P \/ ~ P)
hnP: ~ P
~ P assumption.
Qed.

Lemma pl_lem : thePL -> theLEM.thePL -> theLEM
Proof.thePL -> theLEM
  unfold thePL.(forall P Q : Prop, ((P -> Q) -> P) -> P) -> theLEM
  intro pl.pl: forall P Q : Prop, ((P -> Q) -> P) -> P
theLEM apply dns_lem.pl: forall P Q : Prop, ((P -> Q) -> P) -> P
theDNS
  unfold theDNS.pl: forall P Q : Prop, ((P -> Q) -> P) -> P
forall P : Prop, ~ ~ P -> P intro P.pl: forall P Q : Prop, ((P -> Q) -> P) -> P
P: Prop
~ ~ P -> P
  specialize (pl P).P: Prop
pl: forall Q : Prop, ((P -> Q) -> P) -> P
~ ~ P -> P specialize (pl False).P: Prop
pl: ((P -> False) -> P) -> P
~ ~ P -> P
  intro hnnP.P: Prop
pl: ((P -> False) -> P) -> P
hnnP: ~ ~ P
P
  apply pl.P: Prop
pl: ((P -> False) -> P) -> P
hnnP: ~ ~ P
(P -> False) -> P intro hnP.P: Prop
pl: ((P -> False) -> P) -> P
hnnP: ~ ~ P
hnP: P -> False
P contradiction.
Qed.

Advanced advanced exercise

Come up with more natural statements equivalent to LEM.

Come up with a statement S such that LEM -> S, you cannot prove S -> LEM, but S is also not provable without any assumptions in Rocq.

Found one? Great! Now find a statement S' such that S -> S', you cannot prove S' -> S, but S' is also not provable without any assumptions in Rocq.

Can you come up with a hierarchy S_i of such statements such that S_0 is the strongest and they get subsequently weaker?

Can you come up with a hierarchy S_i of such statements such that S_0 is the weakest and they get subsequently stronger?

🗣️ Talk to us if you want to know more about the solution.

An example of commuting forall and \/.

Lemma forall_or :
  forall P Q,
    (Q \/ ~ Q) ->
    (forall (x : nat), P x \/ Q) ->
    (forall x, P x) \/ Q.forall (P : nat -> Prop) (Q : Prop),
Q \/ ~ Q -> (forall x : nat, P x \/ Q) -> (forall x : nat, P x) \/ Q
Proof.forall (P : nat -> Prop) (Q : Prop),
Q \/ ~ Q -> (forall x : nat, P x \/ Q) -> (forall x : nat, P x) \/ Q
  intros P Q lemQ h.P: nat -> Prop
Q: Prop
lemQ: Q \/ ~ Q
h: forall x : nat, P x \/ Q
(forall x : nat, P x) \/ Q
  destruct lemQ as [hQ | hnQ].P: nat -> Prop
Q: Prop
hQ: Q
h: forall x : nat, P x \/ Q
(forall x : nat, P x) \/ Q
P: nat -> Prop
Q: Prop
hnQ: ~ Q
h: forall x : nat, P x \/ Q
(forall x : nat, P x) \/ Q
  -P: nat -> Prop
Q: Prop
hQ: Q
h: forall x : nat, P x \/ Q
(forall x : nat, P x) \/ Q right.P: nat -> Prop
Q: Prop
hQ: Q
h: forall x : nat, P x \/ Q
Q assumption.
  -P: nat -> Prop
Q: Prop
hnQ: ~ Q
h: forall x : nat, P x \/ Q
(forall x : nat, P x) \/ Q left.P: nat -> Prop
Q: Prop
hnQ: ~ Q
h: forall x : nat, P x \/ Q
forall x : nat, P x intro x.P: nat -> Prop
Q: Prop
hnQ: ~ Q
h: forall x : nat, P x \/ Q
x: nat
P x
    specialize (h x).P: nat -> Prop
Q: Prop
hnQ: ~ Q
x: nat
h: P x \/ Q
P x destruct h as [hPx | hQ].P: nat -> Prop
Q: Prop
hnQ: ~ Q
x: nat
hPx: P x
P x
P: nat -> Prop
Q: Prop
hnQ: ~ Q
x: nat
hQ: Q
P x
    +P: nat -> Prop
Q: Prop
hnQ: ~ Q
x: nat
hPx: P x
P x assumption.
    +P: nat -> Prop
Q: Prop
hnQ: ~ Q
x: nat
hQ: Q
P x exfalso.P: nat -> Prop
Q: Prop
hnQ: ~ Q
x: nat
hQ: Q
False apply hnQ.P: nat -> Prop
Q: Prop
hnQ: ~ Q
x: nat
hQ: Q
Q assumption.
Qed.

More classical reasoning

Lemma classical_or_contra_r :
  theLEM ->
  forall (P Q : Prop),
    (~ Q -> P) ->
    P \/ Q.theLEM -> forall P Q : Prop, (~ Q -> P) -> P \/ Q
Proof.theLEM -> forall P Q : Prop, (~ Q -> P) -> P \/ Q
  intros lem P Q h.lem: theLEM
P, Q: Prop
h: ~ Q -> P
P \/ Q
  specialize (lem Q).Q: Prop
lem: Q \/ ~ Q
P: Prop
h: ~ Q -> P
P \/ Q destruct lem as [hQ | hnQ].Q: Prop
hQ: Q
P: Prop
h: ~ Q -> P
P \/ Q
Q: Prop
hnQ: ~ Q
P: Prop
h: ~ Q -> P
P \/ Q
  -Q: Prop
hQ: Q
P: Prop
h: ~ Q -> P
P \/ Q right.Q: Prop
hQ: Q
P: Prop
h: ~ Q -> P
Q assumption.
  -Q: Prop
hnQ: ~ Q
P: Prop
h: ~ Q -> P
P \/ Q left.Q: Prop
hnQ: ~ Q
P: Prop
h: ~ Q -> P
P apply h.Q: Prop
hnQ: ~ Q
P: Prop
h: ~ Q -> P
~ Q assumption.
Qed.

For the following do you need LEM for both directions?

Lemma classical_impl :
  theLEM ->
  forall (P Q : Prop),
    (P -> Q) <-> (~ P \/ Q).theLEM -> forall P Q : Prop, (P -> Q) <-> ~ P \/ Q
Proof.theLEM -> forall P Q : Prop, (P -> Q) <-> ~ P \/ Q
  intros lem P Q.lem: theLEM
P, Q: Prop
(P -> Q) <-> ~ P \/ Q
  split.lem: theLEM
P, Q: Prop
(P -> Q) -> ~ P \/ Q
lem: theLEM
P, Q: Prop
~ P \/ Q -> P -> Q
  -lem: theLEM
P, Q: Prop
(P -> Q) -> ~ P \/ Q intro h.lem: theLEM
P, Q: Prop
h: P -> Q
~ P \/ Q specialize (lem P).P: Prop
lem: P \/ ~ P
Q: Prop
h: P -> Q
~ P \/ Q destruct lem.P: Prop
H: P
Q: Prop
h: P -> Q
~ P \/ Q
P: Prop
H: ~ P
Q: Prop
h: P -> Q
~ P \/ Q
    +P: Prop
H: P
Q: Prop
h: P -> Q
~ P \/ Q right.P: Prop
H: P
Q: Prop
h: P -> Q
Q apply h.P: Prop
H: P
Q: Prop
h: P -> Q
P assumption.
    +P: Prop
H: ~ P
Q: Prop
h: P -> Q
~ P \/ Q left.P: Prop
H: ~ P
Q: Prop
h: P -> Q
~ P assumption.
  -lem: theLEM
P, Q: Prop
~ P \/ Q -> P -> Q intros h hP.lem: theLEM
P, Q: Prop
h: ~ P \/ Q
hP: P
Q destruct h as [hnP | hQ].lem: theLEM
P, Q: Prop
hnP: ~ P
hP: P
Q
lem: theLEM
P, Q: Prop
hQ: Q
hP: P
Q
    +lem: theLEM
P, Q: Prop
hnP: ~ P
hP: P
Q exfalso.lem: theLEM
P, Q: Prop
hnP: ~ P
hP: P
False apply hnP.lem: theLEM
P, Q: Prop
hnP: ~ P
hP: P
P apply hP.
    +lem: theLEM
P, Q: Prop
hQ: Q
hP: P
Q assumption.
Qed.

Lemma contrapositive :
  theLEM ->
  forall (P Q : Prop),
    (~ Q -> ~ P) ->
    P -> Q.theLEM -> forall P Q : Prop, (~ Q -> ~ P) -> P -> Q
Proof.theLEM -> forall P Q : Prop, (~ Q -> ~ P) -> P -> Q
  intros lem P Q h hP.lem: theLEM
P, Q: Prop
h: ~ Q -> ~ P
hP: P
Q
  specialize (lem Q).Q: Prop
lem: Q \/ ~ Q
P: Prop
h: ~ Q -> ~ P
hP: P
Q destruct lem as [hQ | hnQ].Q: Prop
hQ: Q
P: Prop
h: ~ Q -> ~ P
hP: P
Q
Q: Prop
hnQ: ~ Q
P: Prop
h: ~ Q -> ~ P
hP: P
Q
  -Q: Prop
hQ: Q
P: Prop
h: ~ Q -> ~ P
hP: P
Q assumption.
  -Q: Prop
hnQ: ~ Q
P: Prop
h: ~ Q -> ~ P
hP: P
Q exfalso.Q: Prop
hnQ: ~ Q
P: Prop
h: ~ Q -> ~ P
hP: P
False
    apply h.Q: Prop
hnQ: ~ Q
P: Prop
h: ~ Q -> ~ P
hP: P
~ Q
Q: Prop
hnQ: ~ Q
P: Prop
h: ~ Q -> ~ P
hP: P
P

Notice we get two goals! Because h : ~ Q -> P -> False.

    +Q: Prop
hnQ: ~ Q
P: Prop
h: ~ Q -> ~ P
hP: P
~ Q assumption.
    +Q: Prop
hnQ: ~ Q
P: Prop
h: ~ Q -> ~ P
hP: P
P 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 ->
  forall (P Q : Prop),
    ((P -> Q) -> Q) ->
    ((Q -> P) -> P).theLEM -> forall P Q : Prop, ((P -> Q) -> Q) -> (Q -> P) -> P
Proof.theLEM -> forall P Q : Prop, ((P -> Q) -> Q) -> (Q -> P) -> P
  intros lem P Q h h'.lem: theLEM
P, Q: Prop
h: (P -> Q) -> Q
h': Q -> P
P
  specialize (lem P) as lemP.lem: theLEM
P, Q: Prop
h: (P -> Q) -> Q
h': Q -> P
lemP: P \/ ~ P
P
  destruct lemP as [hP | hnP].lem: theLEM
P, Q: Prop
h: (P -> Q) -> Q
h': Q -> P
hP: P
P
lem: theLEM
P, Q: Prop
h: (P -> Q) -> Q
h': Q -> P
hnP: ~ P
P
  -lem: theLEM
P, Q: Prop
h: (P -> Q) -> Q
h': Q -> P
hP: P
P assumption.
  -lem: theLEM
P, Q: Prop
h: (P -> Q) -> Q
h': Q -> P
hnP: ~ P
P specialize (lem Q) as lemQ.lem: theLEM
P, Q: Prop
h: (P -> Q) -> Q
h': Q -> P
hnP: ~ P
lemQ: Q \/ ~ Q
P
    destruct lemQ as [hQ | hnQ].lem: theLEM
P, Q: Prop
h: (P -> Q) -> Q
h': Q -> P
hnP: ~ P
hQ: Q
P
lem: theLEM
P, Q: Prop
h: (P -> Q) -> Q
h': Q -> P
hnP: ~ P
hnQ: ~ Q
P
    +lem: theLEM
P, Q: Prop
h: (P -> Q) -> Q
h': Q -> P
hnP: ~ P
hQ: Q
P apply h'.lem: theLEM
P, Q: Prop
h: (P -> Q) -> Q
h': Q -> P
hnP: ~ P
hQ: Q
Q assumption.
    +lem: theLEM
P, Q: Prop
h: (P -> Q) -> Q
h': Q -> P
hnP: ~ P
hnQ: ~ Q
P exfalso.lem: theLEM
P, Q: Prop
h: (P -> Q) -> Q
h': Q -> P
hnP: ~ P
hnQ: ~ Q
False apply hnQ.lem: theLEM
P, Q: Prop
h: (P -> Q) -> Q
h': Q -> P
hnP: ~ P
hnQ: ~ Q
Q apply h.lem: theLEM
P, Q: Prop
h: (P -> Q) -> Q
h': Q -> P
hnP: ~ P
hnQ: ~ Q
P -> Q
      intro hP.lem: theLEM
P, Q: Prop
h: (P -> Q) -> Q
h': Q -> P
hnP: ~ P
hnQ: ~ Q
hP: P
Q exfalso.lem: theLEM
P, Q: Prop
h: (P -> Q) -> Q
h': Q -> P
hnP: ~ P
hnQ: ~ Q
hP: P
False apply hnP.lem: theLEM
P, Q: Prop
h: (P -> Q) -> Q
h': Q -> P
hnP: ~ P
hnQ: ~ Q
hP: P
P apply hP.
Qed.

More natural numbers

Lemma mult_distr :
  forall n m k,
    k * (n + m) = k * n + k * m.forall n m k : nat, k * (n + m) = k * n + k * m
Proof.forall n m k : nat, k * (n + m) = k * n + k * m
  intros n m k.n, m, k: nat
k * (n + m) = k * n + k * m
  induction k as [| k ihk] in n, m |- *.n, m: nat
0 * (n + m) = 0 * n + 0 * m
n, m, k: nat
ihk: forall n m : nat, k * (n + m) = k * n + k * m
S k * (n + m) = S k * n + S k * m
  -n, m: nat
0 * (n + m) = 0 * n + 0 * m simpl.n, m: nat
0 = 0 reflexivity.
  -n, m, k: nat
ihk: forall n m : nat, k * (n + m) = k * n + k * m
S k * (n + m) = S k * n + S k * m simpl.n, m, k: nat
ihk: forall n m : nat, k * (n + m) = k * n + k * m
n + m + k * (n + m) = n + k * n + (m + k * m)
    rewrite ihk.n, m, k: nat
ihk: forall n m : nat, k * (n + m) = k * n + k * m
n + m + (k * n + k * m) = n + k * n + (m + k * m)
    rewrite <- plus_assoc.n, m, k: nat
ihk: forall n m : nat, k * (n + m) = k * n + k * m
n + m + k * n + k * m = n + k * n + (m + k * m)
    symmetry.n, m, k: nat
ihk: forall n m : nat, k * (n + m) = k * n + k * m
n + k * n + (m + k * m) = n + m + k * n + k * m rewrite <- plus_assoc.n, m, k: nat
ihk: forall n m : nat, k * (n + m) = k * n + k * m
n + k * n + m + k * m = n + m + k * n + k * m
    f_equal.n, m, k: nat
ihk: forall n m : nat, k * (n + m) = k * n + k * m
n + k * n + m = n + m + k * n symmetry.n, m, k: nat
ihk: forall n m : nat, k * (n + m) = k * n + k * m
n + m + k * n = n + k * n + m
    rewrite plus_comm.n, m, k: nat
ihk: forall n m : nat, k * (n + m) = k * n + k * m
k * n + (n + m) = n + k * n + m rewrite <- plus_assoc.n, m, k: nat
ihk: forall n m : nat, k * (n + m) = k * n + k * m
k * n + n + m = n + k * n + m f_equal.n, m, k: nat
ihk: forall n m : nat, k * (n + m) = k * n + k * m
k * n + n = n + k * n
    rewrite plus_comm.n, m, k: nat
ihk: forall n m : nat, k * (n + m) = k * n + k * m
n + k * n = n + k * n reflexivity.
Qed.

If you thought this kind of proof is extremely annoying, rest assured, most would agree and in practice you don't have to do them by hand. We torture you so you understand better how things work.

In practice Rocq users will use the lia tactic to solve a lot of integer arithmetic problems.

From Stdlib Require Import Lia.

Lemma mult_distr_lia :
  forall n m k,
    k * (n + m) = k * n + k * m.forall n m k : nat, k * (n + m) = k * n + k * m
Proof.forall n m k : nat, k * (n + m) = k * n + k * m
  lia.

See? Much better. 😊

Qed.