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.

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.P_imp_P is defined

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.and_comm is defined

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.or_comm is defined

Lemma truetrue : True.True
  split.
Qed.truetrue is defined

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.anything_goes is defined

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

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.imp_trans is defined

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.to_not_not is defined

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.distr is defined

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.contrad is defined

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.lem_pl is defined

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.lem_dns is defined

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.dn_functorial is defined

Let us switch to Booleans again.

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.andb_orb_distr is defined

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.de_morgan is defined

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.calc_12_3 is defined

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.n_plus_0 is defined

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.double_eq is defined

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.plus_S is defined

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.plus_comm is defined

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.plus_assoc is defined

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 => min n m
  end.min is defined
min is recursively defined (guarded on 1st argument)

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.

  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
min n m = min m n apply ih.
Qed.min_comm is defined

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.

Section Advanced.

  Context (P Q R : Prop).P is declared
Q is declared
R is declared

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.P_iff_P is defined

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.or_imp is defined

  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.Russel is defined

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.forall_False is defined

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.forall_False' is defined

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.False_forall is defined

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.theLEM is defined

Double Negation Shift

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

Peirce's law

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

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.lem_dns_general is defined

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.lem_pl_general is defined

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.dns_lem is defined

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.pl_lem is defined

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.forall_or is defined

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.classical_or_contra_r is defined

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.classical_impl is defined

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.contrapositive is defined

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.twice is defined

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.mult_distr is defined

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.mult_distr_lia is defined