How to read this blog – SYSTEMF @ EPFL

Many of the pages in this blog have Coq proofs embedded in them, like this:

Fixpoint even_Even_fp (n: nat):
  even n = true <-> Even n.even_Even_fp: forall n : nat, even n = true <-> Even n
n: nat
even n = true <-> Even n
Proof.even_Even_fp: forall n : nat, even n = true <-> Even n
n: nat
even n = true <-> Even n
  destruct n as [ | [ | n ] ].even_Even_fp: forall n : nat, even n = true <-> Even n
even 0 = true <-> Even 0
even_Even_fp: forall n : nat, even n = true <-> Even n
even 1 = true <-> Even 1
even_Even_fp: forall n : nat, even n = true <-> Even n
n: nat
even (S (S n)) = true <-> Even (S (S n))
  all: cbn.even_Even_fp: forall n : nat, even n = true <-> Even n
true = true <-> Even 0
even_Even_fp: forall n : nat, even n = true <-> Even n
false = true <-> Even 1
even_Even_fp: forall n : nat, even n = true <-> Even n
n: nat
even n = true <-> Even (S (S n))
  - (* n ← 0 *)even_Even_fp: forall n : nat, even n = true <-> Even n
true = true <-> Even 0
    split; intros.even_Even_fp: forall n : nat, even n = true <-> Even n
H: true = true
Even 0
even_Even_fp: forall n : nat, even n = true <-> Even n
H: Even 0
true = true
    all: constructor.
  - (* n ← 1 *)even_Even_fp: forall n : nat, even n = true <-> Even n
false = true <-> Even 1
    split.even_Even_fp: forall n : nat, even n = true <-> Even n
false = true -> Even 1
even_Even_fp: forall n : nat, even n = true <-> Even n
Even 1 -> false = true
    all: inversion 1.
  - (* n ← S (S _) *)even_Even_fp: forall n : nat, even n = true <-> Even n
n: nat
even n = true <-> Even (S (S n))
    split.even_Even_fp: forall n : nat, even n = true <-> Even n
n: nat
even n = true -> Even (S (S n))
even_Even_fp: forall n : nat, even n = true <-> Even n
n: nat
Even (S (S n)) -> even n = true
    all: (constructor || inversion 1).even_Even_fp: forall n : nat, even n = true <-> Even n
n: nat
H: even n = true
Even n
even_Even_fp: forall n : nat, even n = true <-> Even n
n: nat
H: Even (S (S n))
n0: nat
H1: Even n
H0: n0 = n
even n = true
    all: apply even_Even_fp.even_Even_fp: forall n : nat, even n = true <-> Even n
n: nat
H: even n = true
even n = true
even_Even_fp: forall n : nat, even n = true <-> Even n
n: nat
H: Even (S (S n))
n0: nat
H1: Even n
H0: n0 = n
Even n
    all: assumption.
Qed.

Coq is a Proof Assistant that makes heavy use of tactics to create proofs. As a result, Coq proofs are usually not so readable without seeing the intermediate goals that Coq normally displays.

On this website, you'll notice small bubbles (like this ) next to some of the code. These bubbles indicate Coq fragments (sentences) that you can interact with. Try hovering over the sentences below:

Compute (rot13 "Uryyb, jbeyq!").= "Hello, world!"%string
: string
Search (_ + _ = _ -> _ = _).Nat.add_sub_eq_r:
  forall n m p : nat, m + p = n -> n - p = m
Nat.add_sub_eq_l:
  forall n m p : nat, m + p = n -> n - m = p

Clicking on a sentence will inline Coq's output and make it persistently visible. This is convenient when comparing steps of a proof. Try it on the unnecessarily long sequence of proof steps below:

Lemma Gauss:
  forall n, 2 * (sum n) = n * (n + 1).forall n : nat, 2 * sum n = n * (n + 1)
Proof.forall n : nat, 2 * sum n = n * (n + 1)
  intros.n: nat
2 * sum n = n * (n + 1)
  induction n.2 * sum 0 = 0 * (0 + 1)
n: nat
IHn: 2 * sum n = n * (n + 1)
2 * sum (S n) = S n * (S n + 1)
  - (* n ← 0 *)2 * sum 0 = 0 * (0 + 1) reflexivity.
  - (* n ← S _ *)n: nat
IHn: 2 * sum n = n * (n + 1)
2 * sum (S n) = S n * (S n + 1)
    cbn [sum].n: nat
IHn: 2 * sum n = n * (n + 1)
2 * (S n + sum n) = S n * (S n + 1)
    rewrite Nat.mul_add_distr_l.n: nat
IHn: 2 * sum n = n * (n + 1)
2 * S n + 2 * sum n = S n * (S n + 1)
    rewrite IHn.n: nat
IHn: 2 * sum n = n * (n + 1)
2 * S n + n * (n + 1) = S n * (S n + 1)
    change (S n) with (1 + n).n: nat
IHn: 2 * sum n = n * (n + 1)
2 * (1 + n) + n * (n + 1) = (1 + n) * (1 + n + 1)
    rewrite !Nat.mul_add_distr_l, !Nat.mul_add_distr_r.n: nat
IHn: 2 * sum n = n * (n + 1)
2 * 1 + 2 * n + (n * n + n * 1) =
1 * 1 + n * 1 + (1 * n + n * n) + (1 * 1 + n * 1)
    cbn [Nat.mul]; rewrite !Nat.mul_1_r, !Nat.add_0_r.n: nat
IHn: 2 * sum n = n * (n + 1)
1 + 1 + (n + n) + (n * n + n) =
1 + n + (n + n * n) + (1 + n)
    rewrite !Nat.add_assoc.n: nat
IHn: 2 * sum n = n * (n + 1)
1 + 1 + n + n + n * n + n = 1 + n + n + n * n + 1 + n
    change (1 + 1) with 2.n: nat
IHn: 2 * sum n = n * (n + 1)
2 + n + n + n * n + n = 1 + n + n + n * n + 1 + n
    rewrite !(Nat.add_comm _ 1), !Nat.add_assoc.n: nat
IHn: 2 * sum n = n * (n + 1)
2 + n + n + n * n + n = 1 + 1 + n + n + n * n + n
    change (1 + 1) with 2.n: nat
IHn: 2 * sum n = n * (n + 1)
2 + n + n + n * n + n = 2 + n + n + n * n + n
    Show Existentials.Existential 1 =
?Goal :
  [n : nat  IHn : 2 * sum n = n * (n + 1)
  |- 2 + n + n + n * n + n = 2 + n + n + n * n + n]
    reflexivity.
Qed.

One final way to interact with the proofs is using the keyboard, in a style similar to Proof General or CoqIDE. Try pressing Ctrl+↓ and Ctrl+↑; you will be taken back to the beginning of this article and shown goals and responses at each step. You can also click on a sentence while holding Ctrl (or Cmd on macOS) to focus on a given goal.