# How to read this blog

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 n0n:nateven n = true <-> Even n
Proof.even_Even_fp:forall n0 : nat,
even n0 = true <-> Even n0n:nateven n = true <-> Even n
destruct n as [ | [ | n ] ].even_Even_fp:forall n : nat,
even n = true <-> Even neven 0 = true <-> Even 0even_Even_fp:forall n : nat,
even n = true <-> Even neven 1 = true <-> Even 1even_Even_fp:forall n0 : nat,
even n0 = true <-> Even n0n:nateven (S (S n)) = true <-> Even (S (S n))
all: cbn.even_Even_fp:forall n : nat,
even n = true <-> Even ntrue = true <-> Even 0even_Even_fp:forall n : nat,
even n = true <-> Even nfalse = true <-> Even 1even_Even_fp:forall n0 : nat,
even n0 = true <-> Even n0n:nateven n = true <-> Even (S (S n))
- (* n ← 0 *)even_Even_fp:forall n : nat,
even n = true <-> Even ntrue = true <-> Even 0
split; intros.even_Even_fp:forall n : nat,
even n = true <-> Even nH:true = trueEven 0even_Even_fp:forall n : nat,
even n = true <-> Even nH:Even 0true = true
all: constructor.
- (* n ← 1 *)even_Even_fp:forall n : nat,
even n = true <-> Even nfalse = true <-> Even 1
split.even_Even_fp:forall n : nat,
even n = true <-> Even nfalse = true -> Even 1even_Even_fp:forall n : nat,
even n = true <-> Even nEven 1 -> false = true
all: inversion 1.
- (* n ← S (S _) *)even_Even_fp:forall n0 : nat,
even n0 = true <-> Even n0n:nateven n = true <-> Even (S (S n))
split.even_Even_fp:forall n0 : nat,
even n0 = true <-> Even n0n:nateven n = true -> Even (S (S n))even_Even_fp:forall n0 : nat,
even n0 = true <-> Even n0n:natEven (S (S n)) -> even n = true
all: (constructor || inversion 1).even_Even_fp:forall n0 : nat,
even n0 = true <-> Even n0n:natH:even n = trueEven neven_Even_fp:forall n1 : nat,
even n1 = true <-> Even n1n:natH:Even (S (S n))n0:natH1:Even nH0:n0 = neven n = true
all: apply even_Even_fp.even_Even_fp:forall n0 : nat,
even n0 = true <-> Even n0n:natH:even n = trueeven n = trueeven_Even_fp:forall n1 : nat,
even n1 = true <-> Even n1n:natH:Even (S (S n))n0:natH1:Even nH0:n0 = nEven 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 = mNat.add_sub_eq_r:
forall n m p : nat, m + p = n -> n - p = mNat.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:nat2 * sum n = n * (n + 1)
induction n.2 * sum 0 = 0 * (0 + 1)n:natIHn: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:natIHn:2 * sum n = n * (n + 1)2 * sum (S n) = S n * (S n + 1)
cbn [sum].n:natIHn:2 * sum n = n * (n + 1)2 * (S n + sum n) = S n * (S n + 1)
rewrite Mult.mult_plus_distr_l.n:natIHn:2 * sum n = n * (n + 1)2 * S n + 2 * sum n = S n * (S n + 1)
rewrite IHn.n:natIHn:2 * sum n = n * (n + 1)2 * S n + n * (n + 1) = S n * (S n + 1)
change (S n) with (1 + n).n:natIHn: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:natIHn: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:natIHn: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:natIHn: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:natIHn: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:natIHn: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:natIHn: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!