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 n0 : nat,
even n0 = true <-> Even n0
n:nat
even n = true <-> Even n
Proof.
even_Even_fp:forall n0 : nat,
even n0 = true <-> Even n0
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 n0 : nat,
even n0 = true <-> Even n0
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 n0 : nat,
even n0 = true <-> Even n0
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 n0 : nat,
even n0 = true <-> Even n0
n:nat
even n = true <-> Even (S (S n))
    split.
even_Even_fp:forall n0 : nat,
even n0 = true <-> Even n0
n:nat
even n = true -> Even (S (S n))
even_Even_fp:forall n0 : nat,
even n0 = true <-> Even n0
n:nat
Even (S (S n)) -> even n = true
    all: (constructor || inversion 1).
even_Even_fp:forall n0 : nat,
even n0 = true <-> Even n0
n:nat
H:even n = true
Even n
even_Even_fp:forall n1 : nat,
even n1 = true <-> Even n1
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 n0 : nat,
even n0 = true <-> Even n0
n:nat
H:even n = true
even n = true
even_Even_fp:forall n1 : nat,
even n1 = true <-> Even n1
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
Search (_ + _ = _ -> _ = _).
plus_reg_l: forall n m p : nat, p + n = p + m -> n = m
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 Mult.mult_plus_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 !Mult.mult_plus_distr_l, !Mult.mult_plus_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.

I plan to write about the system that powers this blog in the future. For now, happy hacking!