Introduction to the Rocq Prover

Authors:

Yannick Forster

Théo Winterhalter

Files:

Display all goals and responses

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. You are welcome to play with this file in Rocq directly, by clicking on "Source" in the bar above.

Getting started with propositional logic

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.

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(s) for conjunctions.

\begin{equation*} \cfrac{P \land Q}{P} \qquad \cfrac{P \land Q}{Q} \end{equation*}

Expressed with a context this can be stated as only one rule:

\begin{equation*} \cfrac{\Gamma \vdash P \land Q \quad \Gamma, P, Q \vdash R}{\Gamma \vdash R} \end{equation*}

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:

\begin{equation*} \cfrac{\Gamma \vdash P \quad \Gamma \vdash Q}{\Gamma \vdash P \land Q} \end{equation*}

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.

Here apply plays the role of the axiom rule of natural deduction.

\begin{equation*} \cfrac{P \in \Gamma}{\Gamma \vdash P} \end{equation*}

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 should again be reminiscent of natural deduction rules, this time for disjunction elimination:

\begin{equation*} \cfrac{\Gamma \vdash P \lor Q \quad \Gamma, P \vdash R \quad \Gamma, Q \vdash R}{\Gamma \vdash R} \end{equation*}

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.

We can once again see the connection with natural deduction rules: we have two introduction rules for disjunction that correspond to left and right respectively.

\begin{equation*} \cfrac{\Gamma \vdash P}{\Gamma \vdash P \lor Q} \qquad \cfrac{\Gamma \vdash Q}{\Gamma \vdash P \lor Q} \end{equation*}

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.

Looking at natural deduction again, it makes sense, on the top of the inference line we see no premises.

\begin{equation*} \cfrac{}{\Gamma \vdash \top} \end{equation*}

Now, let's look at False.

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.

The corresponding rule is as follows.

\begin{equation*} \cfrac{\Gamma \vdash \bot}{\Gamma \vdash A} \end{equation*}

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.

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.

The corresponding rules are:

\begin{equation*} \cfrac{\Gamma, P \vdash \bot}{\Gamma \vdash \neg P} \qquad \cfrac{\Gamma \vdash \neg P \quad \Gamma \vdash P}{\Gamma \vdash \bot} \end{equation*}

By the way, we have implicitly used the introduction and elimination rules for implication from the very beginning (including for negation since it is defined in terms of implications):

\begin{equation*} \cfrac{\Gamma, Q \vdash P}{\Gamma \vdash Q \Longrightarrow P} \qquad \cfrac {\Gamma \vdash Q \Longrightarrow P \quad \Gamma \vdash Q} {\Gamma \vdash P} \end{equation*}

They are invoked through intro and apply respectively.

Lemma impl_trans P Q R :
  (P -> Q) -> (Q -> R) -> (P -> R).P, Q, R: Type
(P -> Q) -> (Q -> R) -> P -> R
Proof.P, Q, R: Type
(P -> Q) -> (Q -> R) -> P -> R

The following is equivalent to intro hPQ. intro hQR. intro hP. Notice the s.

  intros hPQ hQR hP.P, Q, R: Type
hPQ: P -> Q
hQR: Q -> R
hP: P
R

We now use elimination twice in a row.

  apply hQR.P, Q, R: Type
hPQ: P -> Q
hQR: Q -> R
hP: P
Q
  apply hPQ.P, Q, R: Type
hPQ: P -> Q
hQR: Q -> R
hP: P
P
  apply hP.
Qed.

Finally, let's end this part of the lesson by having a look at logical equivalence: \(P \iff Q\). In Rocq, this is unsurprisingly defined as the conjunction of the two implications: P <-> Q is the same as (P -> Q) /\ (Q -> P).

We can for instance prove that equivalence is symmetric (it is in fact an equivalence relation… shocking.)

Lemma equiv_sym P Q :
  (P <-> Q) -> (Q <-> P).P, Q: Prop
P <-> Q -> Q <-> P
Proof.P, Q: Prop
P <-> Q -> Q <-> P
  intros h.P, Q: Prop
h: P <-> Q
Q <-> P
  destruct h as [hPQ hQP].P, Q: Prop
hPQ: P -> Q
hQP: Q -> P
Q <-> P
  split.P, Q: Prop
hPQ: P -> Q
hQP: Q -> P
Q -> P
P, Q: Prop
hPQ: P -> Q
hQP: Q -> P
P -> Q
  -P, Q: Prop
hPQ: P -> Q
hQP: Q -> P
Q -> P apply hQP.
  -P, Q: Prop
hPQ: P -> Q
hQP: Q -> P
P -> Q apply hPQ.
Qed.

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.

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.

(* Start with a reminder of Wednesday: natural deduction + equivalence *)

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.

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.

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.

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.

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.

Defining functions

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 duplicating 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.

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 and that branches are marked with => instead of ->. The end 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))

Now we have ihm : double m = m * 2 in the context, and double m in the goal. So we would like to replace it with m * 2. There is a tactic to do just that: rewrite!

    rewrite ihm.m: nat
ihm: double m = m * 2
S (S (m * 2)) = S (S (m * 2)) reflexivity.
Qed.

Quantifiers

When using Check, About, or simply hovering constants in VSRocq, you have probably seen the keyword forall appear. It corresponds to the universal quantifier, often written ∀ (and in fact you can tell to print it like this if you tell to use Unicode).

Adding quantifiers makes us leave the realm of propositional logic and entering the world of higher order logic.

Have a look at the lemma we just proved, and see how its statement begins with forall (n : nat). When we put n to the left of the colon (:), we have implicitly quantified over it, universally.

Check double_eq2.double_eq2
     : forall n : nat, double n = n * 2

To see what looks like in natural deduction, we extend the notion of context so that besides formulas, it is able to contain also elements of a certain type such as n : nat.

\begin{equation*} \cfrac{\Gamma, x : A \vdash P}{\Gamma \vdash \forall (x : A).\ P} \qquad \cfrac{\Gamma, Q \vdash P}{\Gamma \vdash Q \Longrightarrow P} \end{equation*}

This is just like the context we see in goals. Notice the parallel with the introduction rule for implication we have seen previously. This introduction rule is materialised in Rocq as the tactic intro, exactly like for implication. See how it works below.

Lemma n_mul_0 : forall (n : nat), n * 0 = 0.forall n : nat, n * 0 = 0
Proof.forall n : nat, n * 0 = 0

As before, intro takes a name. We could pick n but we don't have to. Let's pick k for a change.

  intro k.k: nat
k * 0 = 0

Nothing prevents me from reusing k as a variable name. Don't do it if you find it confusing.

  induction k as [| k ih].0 * 0 = 0
k: nat
ih: k * 0 = 0
S k * 0 = 0
  -0 * 0 = 0 reflexivity.
  -k: nat
ih: k * 0 = 0
S k * 0 = 0 simpl.k: nat
ih: k * 0 = 0
k * 0 = 0 assumption.
Qed.

Of course, the universal quantifier also has an elimination rule, which we put side by side with the one for implication again, because there is a parallel to be made.

\begin{equation*} \cfrac {\Gamma \vdash \forall (x : A). P \quad \Gamma \vdash u : A} {\Gamma \vdash P[ x := u ]} \qquad \cfrac {\Gamma \vdash Q \Longrightarrow P \quad \Gamma \vdash Q} {\Gamma \vdash P} \end{equation*}

It is much more complicated than everything we have seen before for two reasons:

At the top we wrote \(u : A\) to the right of the turnstile (\(\vdash\)) insteaf of a proposition. This is because the element \(u\) of type \(A\) itself matters.
At the bottom we wrote \(P[ x := u ]\) to indicate that in the end we prove \(P\), but since \(P\) is allowed to mention \(x\) (think of forall (n : nat), n * 0 = 0 again), we need to replace it with the value \(u\).

If it's too hard, don't scratch your head too much and instead look at a concrete example where we use n_mul_0 using apply (again a parallel with implication).

Lemma dummy :
  forall (a b c : nat), (a + b * b + c * a) * 0 = 0.forall a b c : nat, (a + b * b + c * a) * 0 = 0
Proof.forall a b c : nat, (a + b * b + c * a) * 0 = 0
  intros a b c.a, b, c: nat
(a + b * b + c * a) * 0 = 0

This is just an instance of n * 0 = 0 where we replace n with a bigger expression. Fortunately, we don't even to specify it, Rocq will infer that information for us.

  apply n_mul_0.
Qed.

Another way to look at it, is to split it into steps using the specialize tactic.

Lemma spec :
  (forall n, n + n = 2 * n) ->
  (forall k r, (k + r) + (k + r) = 2 * (k + r)).(forall n : nat, n + n = 2 * n) ->
forall k r : nat, k + r + (k + r) = 2 * (k + r)
Proof.(forall n : nat, n + n = 2 * n) ->
forall k r : nat, k + r + (k + r) = 2 * (k + r)
  intros h k r.h: forall n : nat, n + n = 2 * n
k, r: nat
k + r + (k + r) = 2 * (k + r)
  specialize (h (k + r)).k, r: nat
h: k + r + (k + r) = 2 * (k + r)
k + r + (k + r) = 2 * (k + r)
  apply h.
Qed.

Let us now move on to the dual operator, the existential quantifier. First let us look at the natural deduction rules.

\begin{equation*} \cfrac {\Gamma \vdash u : A \quad \Gamma \vdash P[ x := u ]} {\Gamma \vdash \exists (x : A). P} \qquad \cfrac {\Gamma \vdash \exists (x : A). P \quad \Gamma, x : A, P \vdash Q} {\Gamma \vdash Q} \end{equation*}

In the elimination rule (on the right), remember that \(P\) can refer to \(x\), which is symbolised by having \(x\) appear before \(P\).

Let's look first at how to prove an existentially quantified statement. In Rocq they are written exists (x : A). P.

Lemma nat_desc n :
  n = 0 \/ (exists m, n = S m).n: nat
n = 0 \/ (exists m : nat, n = S m)
Proof.n: nat
n = 0 \/ (exists m : nat, n = S m)

We don't need full induction here.

  destruct n as [| m].0 = 0 \/ (exists m : nat, 0 = S m)
m: nat
S m = 0 \/ (exists m0 : nat, S m = S m0)
  -0 = 0 \/ (exists m : nat, 0 = S m) left.0 = 0 reflexivity.
  -m: nat
S m = 0 \/ (exists m0 : nat, S m = S m0) right.m: nat
exists m0 : nat, S m = S m0

Proving an existential can be done using the exists tactic, just like the quantifier itself!

    exists m.m: nat
S m = S m reflexivity.
Qed.

Using an existentially quantified assumption on the other hand is going to require the destruct tactic, a bit like a conjunction.

To see this, we are going to define two predicates on natural numbers corresponding to even- and oddness.

Definition even n := exists m, n = 2 * m.

Definition odd n := exists m, n = S (2 * m).

Lemma even_odd_S n :
  even n ->
  odd (S n).n: nat
even n -> odd (S n)
Proof.n: nat
even n -> odd (S n)
  intro hn.n: nat
hn: even n
odd (S n)
  destruct hn as [m e].n, m: nat
e: n = 2 * m
odd (S n)
  rewrite e.n, m: nat
e: n = 2 * m
odd (S (2 * m))
  exists m.n, m: nat
e: n = 2 * m
S (2 * m) = S (2 * m) reflexivity.
Qed.

To showcase more handy features. We're going to perform the introduction of the assumption at the same time as eliminating it. This is done by using so-called intropatterns: the tactic intros [n e] works essentially like intros h. destruct h as [n e]. while being much shorter.

Lemma even_odd_S_again n :
  even n ->
  odd (S n).n: nat
even n -> odd (S n)
Proof.n: nat
even n -> odd (S n)
  intros [m e].n, m: nat
e: n = 2 * m
odd (S n)
  exists m.n, m: nat
e: n = 2 * m
S n = S (2 * m)

For fun we're going to use rewrite from right to left.

  rewrite <- e.n, m: nat
e: n = 2 * m
S n = S n
  reflexivity.
Qed.

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

More to come on Wednesday… For now have look at exercises (at the top). It is expected that you can't solve all of them yet, since we haven't completed lesson 1. Also don't hesitate to refer to our cheatsheet when solving exercises.