MPRI PRFA — Proof Assistants

Introduction to the Rocq Prover

This course teaches you how to use one proof assistant (Rocq), with the goal to

be able to use Rocq in other courses,
use Rocq in an internship,
learn other proof assistants or become an expert user of Rocq via self study,
ultimately use or study proof assistants as part of a PhD.

In particular, we believe that taking this course will allow you to learn other proof assistants, e.g. Agda, Isabelle, or Lean, via self study, very quickly. Note that the MPRI HOTT course teaches Agda in more detail, relying on you having learnt about proof assistants in this course.

You should have installed Rocq before attending, but in case you haven't, please consult our page about installing Rocq.

In this first lecture, we will introduce fundamentals of Rocq and proof assistants in general:

propositional logic
proofs by case analysis
proofs by induction

Note that this document is being interpreted from Rocq files by Alectryon. Bubbles () indicate interactive fragments: hover for details, click to reveal contents. Use Ctrl+↑ and Ctrl+↓ to navigate, Ctrl+🖱️ to focus. On macOS, use ⌘ instead of Ctrl.

Let's get started with proving a first simple fact about propositional logic: If P holds, then P holds, i.e., an implication.

Implications are written -> in Rocq.

To prove a fact, one writes Lemma name : statement. Lemmas can be parameterized, our first lemma is parametric in an arbitrary proposition P. We denote this by writing (P : Prop).

Lemma P_imp_P (P : Prop) : P -> P.P: Prop
P -> P
Proof.P: Prop
P -> P

If you interpret this script live, you will see the so-called goal: P -> P. Verbally: P implies P.

To prove it, we can assume we have a proof of P, we call it h.

  intro h.P: Prop
h: P
P

The command intro is called a tactic.

The goal is now P, but notice we have some extra assumption h : P. To use an assumption, one can use the apply tactic:

  apply h.

Proof finished! All that's left to do is to type Qed.

Qed.P_imp_P is defined

Try to see what happens if one types Qed before the proof is finished.

We now have a new fact that can be used in other proofs: P_imp_P which is a proof of P -> P.

You can check this fact using the Check command.

Check P_imp_P.P_imp_P
     : forall P : Prop, P -> P

We can also write conjunction (/\) and disjunction (\/)

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

We have an implication so we use intro.

  intro h.P, Q: Prop
h: P /\ Q
Q /\ P

We now have h : P /\ Q as assumption and we need to prove Q /\ P.

First we need to have a look at P /\ Q, we would like to turn it into two different hyoptheses: one for P and one for Q. If you have taken a course in logic, you would have said that we need to apply the elimination rule for conjunctions. We can use elimination rules in general using the destruct tactic to decompose an hypothesis into all possible proofs of it. In the case of P /\ Q, there is just one:

  destruct h as [hP hQ].P, Q: Prop
hP: P
hQ: Q
Q /\ P

The as clause above is used to give a name to the resulting hypotheses. Here we name hP : P and hQ : Q.

To prove a conjunction we can use the split tactic to get two goals:

  split.P, Q: Prop
hP: P
hQ: Q
Q
P, Q: Prop
hP: P
hQ: Q
P

In logical terms, this corresponds to applying the introduction rule for conjuctions.

Notice we now have two goals, P and Q. We use bullets to focus on the goals one by one.

  -P, Q: Prop
hP: P
hQ: Q
Q

Now proving Q is easy.

    apply hQ.
  -P, Q: Prop
hP: P
hQ: Q
P apply hP.
Qed.and_comm is defined

Let us look at a slightly different example: disjunction.

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

Now we first need to do a case analysis on whether P or Q holds. This is done using the destruct tactic again, doing a case analysis on all possible proofs of P \/ Q. There are two:

  destruct h as [hP | hQ].P, Q: Prop
hP: P
Q \/ P
P, Q: Prop
hQ: Q
Q \/ P

Notice how we used a pipe to separate the two cases.

  -P, Q: Prop
hP: P
Q \/ P

Now we have P and we want to prove Q \/ P. We can use the tactic right to say we want to prove the right case.

    right.P, Q: Prop
hP: P
P
    apply hP.
  -P, Q: Prop
hQ: Q
Q \/ P

Unsurprisingly, the dual tactic is called left.

    left.P, Q: Prop
hQ: Q
Q
    apply hQ.
Qed.or_comm is defined

We also have the usual ⊤ and ⊥ which in Rocq are called True and False.

Lemma truetrue : True.True
Proof.True

To prove it, you can also use split! It's like the nullary conjunction. split will work with all logical constructions that only have one introduction rule.

  split.
Qed.truetrue is defined

Lemma falsefalse : False.False
Proof.False

Of course, one cannot prove False without assumptions. So we give up:

Abort.

Rocq will now not add falsefalse to the environment, and thus the Check command will fail:

Fail Check falsefalse.The command has indeed failed with message:
The reference falsefalse was not found in the current environment.

However, False implies anything: ex falso quodlibet.

Lemma anything_goes P : False -> P.P: Type
False -> P
Proof.P: Type
False -> P
  intro bot.P: Type
bot: False
P

The exfalso tactic concludes anything as long as you can prove False.

  exfalso.P: Type
bot: False
False
  apply bot.
Qed.anything_goes is defined

Let's do the proof again, with an alternative approach.

Lemma anything_goes_again P : False -> P.P: Type
False -> P
Proof.P: Type
False -> P

Namely, we can do case analysis on all possible proofs of False directly — of which there are none.

  intro bot.P: Type
bot: False
P
  destruct bot.
Qed.anything_goes_again is defined

Let us have a look at negation now. ~ P is a notation for the negation of P. In fact it is defined as P -> False, so we can use intro to prove a negation.

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

Case analysis and induction

Let us consider the type of Booleans, with elements true and false. We also refer to the negb function from the standard library which sends true to false and vice versa.

Lemma negb_true :
  negb true = false.negb true = false
Proof.negb true = false

Here we have computation, so we can ask Rocq to simplify things.

  simpl.false = false

Equality is then proven with the following tactic which solves goals of the form x = x.

  reflexivity.
Qed.negb_true is defined

We show that boolean negation is involutive.

Lemma negb_invol (b : bool) :
  negb (negb b) = b.b: bool
negb (negb b) = b
Proof.b: bool
negb (negb b) = b

Similar to how destruct can be used to do case analysis on hypotheses, it can be used to do case analysis on booleans. There are two cases:

  destruct b.negb (negb true) = true
negb (negb false) = false
  -negb (negb true) = true simpl.true = true reflexivity.
  -negb (negb false) = false simpl.false = false reflexivity.
Qed.negb_invol is defined

We now turn to boolean conjunction.

Lemma andb_comm b1 b2 :
  andb b1 b2 = andb b2 b1.b1, b2: bool
(b1 && b2)%bool = (b2 && b1)%bool
Proof.b1, b2: bool
(b1 && b2)%bool = (b2 && b1)%bool
  destruct b1.b2: bool
(true && b2)%bool = (b2 && true)%bool
b2: bool
(false && b2)%bool = (b2 && false)%bool
  -b2: bool
(true && b2)%bool = (b2 && true)%bool simpl.b2: bool
b2 = (b2 && true)%bool destruct b2.true = (true && true)%bool
false = (false && true)%bool
    +true = (true && true)%bool simpl.true = true reflexivity.
    +false = (false && true)%bool simpl.false = false reflexivity.
  -b2: bool
(false && b2)%bool = (b2 && false)%bool simpl.b2: bool
false = (b2 && false)%bool destruct b2.false = (true && false)%bool
false = (false && false)%bool
    +false = (true && false)%bool simpl.false = false reflexivity.
    +false = (false && false)%bool simpl.false = false reflexivity.
Qed.andb_comm is defined

Lemma andb_comm' b1 b2 :
  andb b1 b2 = andb b2 b1.b1, b2: bool
(b1 && b2)%bool = (b2 && b1)%bool
Proof.b1, b2: bool
(b1 && b2)%bool = (b2 && b1)%bool

We can also ask Rocq to do two case analyses at the same time.

  destruct b1, b2.(true && true)%bool = (true && true)%bool
(true && false)%bool = (false && true)%bool
(false && true)%bool = (true && false)%bool
(false && false)%bool = (false && false)%bool
  -(true && true)%bool = (true && true)%bool

No need to use simpl every time, reflexivity does it on its own.

    reflexivity.
  -(true && false)%bool = (false && true)%bool reflexivity.
  -(false && true)%bool = (true && false)%bool reflexivity.
  -(false && false)%bool = (false && false)%bool reflexivity.
Qed.andb_comm' is defined

Let us switch to natural numbers.

Lemma calc_12_3 : 12 + 3 = 15.12 + 3 = 15
Proof.12 + 3 = 15

Here we have computation again, so we can ask Rocq to simplify things.

  simpl.15 = 15

Now we have to prove 15 = 15, the is true by reflexivity of equality.

  reflexivity.
Qed.calc_12_3 is defined

Lemma double_eq n : n + n = 2 * n.n: nat
n + n = 2 * n
Proof.n: nat
n + n = 2 * n

Functions in Rocq have computation rules.

  simpl.n: nat
n + n = n + (n + 0)

The + 0 at the end might seem surprising. This has to do with the definition of multiplication:

0 * m := 0

(n + 1) * m := m + n * m

So 2 * m = m + 1 * m = m + (m + (0 * m)) = m + (m + 0).

Note that n + 0 also does not simplify by computation, because the defining rules are:

0 + m := m

(n + 1) + m := (n + m) + 1

However, we can prove that n + 0 = n. We do so with a lemma first.

Abort.

Lemma plus_zero n : n = n + 0.n: nat
n = n + 0
Proof.n: nat
n = n + 0

Case analysis is no longer sufficient to prove such a result, instead we're going to perform induction on natural numbers. We do so with the following tactic.

  induction n.0 = 0 + 0
n: nat
IHn: n = n + 0
S n = S n + 0

We have two cases to prove, the case n = 0 and the case n + 1. In Rocq, the successor of n is written S n, like in Peano arithmetic.

  -0 = 0 + 0

Now, 0 + 0 computes to 0:

    simpl.0 = 0 reflexivity.
  -n: nat
IHn: n = n + 0
S n = S n + 0 simpl.n: nat
IHn: n = n + 0
S n = S (n + 0)

We have S on both sides. We can use the f_equal tactic to prove that f x = f y if x = y.

    f_equal.n: nat
IHn: n = n + 0
n = n + 0

Here we can apply our induction hypothesis. Since we did not chose its name, we can use a different tactic that finds a matching hypothesis on its own:

    assumption.
Qed.plus_zero is defined

The lemma we wanted to prove earlier is now easy, we just have to make use of plus_zero we just proved.

Lemma double_eq n : 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 apply plus_zero.
Qed.double_eq is defined

Defining functions

One last thing: in Rocq you can also write your own definitions and they can be recursive. In models a recursive function corresponds to a fixed point so such functions are introduced with the keyword Fixpoint. It corresponds roughly to OCaml's let rec syntax, but compared to OCaml, functions must be total (defined on all inputs) so in particular, they must be terminating.

Here, we define a function double which doubles its argument by dupplicating all occurrences of S in it. For instance, double (S (S 0)) will compute to S (S (double (S 0))) and then to S (S (S (S (double 0)))) which is S (S (S (S 0))). In other words double 2 = 4.

Fixpoint double (n : nat) :=
  match n with
  | 0 => 0
  | S n => S (S (double n))
  end.double is defined
double is recursively defined (guarded on 1st argument)

Note that the definition contains the match construct which performs pattern matching, or case analysis. If you know OCaml then it is the same syntax with the exception that a match block has to end with the keyword end. This makes it easier to parse for both humans and machines, in particular when several match are nested.

We can now prove by a simple induction that double n is the same as n * 2.

Lemma double_eq2 n : double n = n * 2.n: nat
double n = n * 2
Proof.n: nat
double n = n * 2
  induction n as [ | m IHm].double 0 = 0 * 2
m: nat
IHm: double m = m * 2
double (S m) = S m * 2

This time we decided to give names to the extra hypotheses produced by the induction tactic. As with destruct before, there is a pipe (|) separating the two cases (0 and S m). In the first case, there is no induction hypothesis so we do not need to introduce any name. In the successor case, we need to provide a name for the induction hypothesis IHm but also for the natural number that appears below S, here we chose m.

  -double 0 = 0 * 2 simpl.0 = 0 reflexivity.
  -m: nat
IHm: double m = m * 2
double (S m) = S m * 2 simpl.m: nat
IHm: double m = m * 2
S (S (double m)) = S (S (m * 2)) rewrite IHm.m: nat
IHm: double m = m * 2
S (S (m * 2)) = S (S (m * 2)) reflexivity.
Qed.double_eq2 is defined

This concludes our first lesson. Try to do the exercises and ask for help if needed.

Go back to the course homepage.