How to read this blog

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

even_Even_fp:forall n0 : nat, even n0 = true <-> Even n0
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
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))
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))
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
H:true = true
Even 0
even_Even_fp:forall n : nat, even n = true <-> Even n
H:Even 0
true = true
all: constructor.
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
false = true -> Even 1
even_Even_fp:forall n : nat, even n = true <-> Even n
Even 1 -> false = true
all: inversion 1.
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 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
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
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:

= "Hello, world!" : string
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:

forall n : nat, 2 * sum n = n * (n + 1)
forall n : nat, 2 * sum n = n * (n + 1)
n:nat
2 * sum n = n * (n + 1)
2 * sum 0 = 0 * (0 + 1)
n:nat
IHn:2 * sum n = n * (n + 1)
2 * sum (S n) = S n * (S n + 1)
2 * sum 0 = 0 * (0 + 1)
reflexivity.
n:nat
IHn:2 * sum n = n * (n + 1)
2 * sum (S n) = S n * (S n + 1)
n:nat
IHn:2 * sum n = n * (n + 1)
2 * (S n + sum n) = S n * (S n + 1)
n:nat
IHn:2 * sum n = n * (n + 1)
2 * S n + 2 * sum n = S n * (S n + 1)
n:nat
IHn:2 * sum n = n * (n + 1)
2 * S n + n * (n + 1) = S n * (S n + 1)
n:nat
IHn:2 * sum n = n * (n + 1)
2 * (1 + n) + n * (n + 1) = (1 + n) * (1 + n + 1)
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)
n:nat
IHn:2 * sum n = n * (n + 1)
1 + 1 + (n + n) + (n * n + n) = 1 + n + (n + n * n) + (1 + n)
n:nat
IHn:2 * sum n = n * (n + 1)
1 + 1 + n + n + n * n + n = 1 + n + n + n * n + 1 + n
n:nat
IHn:2 * sum n = n * (n + 1)
2 + n + n + n * n + n = 1 + n + n + n * n + 1 + n
n:nat
IHn:2 * sum n = n * (n + 1)
2 + n + n + n * n + n = 1 + 1 + n + n + n * n + n
n:nat
IHn:2 * sum n = n * (n + 1)
2 + n + n + n * n + n = 2 + n + n + n * n + n
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!