Using MathJax with Alectryon

This example shows how to combine Alectryon with MathJax. We'll do a pretty-printed version of the proof that \(\sum_{i = 0}^n i = \frac{n \cdot (n + 1)}{2}\).

First, we start with a definition of sum:

Require Import NArith ArithRing.

Fixpoint nsum max f :=
  match max with
  | O => f 0
  | S max' => f max + nsum max' f
  end.

Then, we add notations to print LaTeX code (this is only one way to do it; another way would be to parse Coq's output to reconstruct LaTeX):

Notation "'\ccNat{}'" := nat.
Notation "'\ccSucc{' n '}'" := (S n).
Infix "\times" := mult
  (at level 30).
Notation "'\ccNsum{' x '}{' max '}{' f '}'" :=
  (nsum max (fun x => f))
    (format "'\ccNsum{' x '}{' max '}{' f '}'").
Notation "\ccNot{ x }" := (not x)
  (at level 100).
Infix "\wedge" := and
  (at level 190, right associativity).
Notation "A \Rightarrow{} B" := (∀ (_ : A), B)
  (at level 200, right associativity).
Notation "'\ccForall{' x .. y '}{' P '}'" := (∀ x, .. (∀ y, P) ..)
  (at level 200, x binder, y binder, right associativity,
   format "'\ccForall{' x .. y '}{' P '}'").

Then, we add MathJax definitions for each of these custom macros (look at the page source to see them):

Then we set up MathJax to render the proofs properly (look at the page source to see the relevant script):

And finally we write the actual proofs:

Lemma Gauss: ∀ n,
    2 * (nsum n (fun i => i)) = n * (n + 1).
\ccForall{n : \ccNat{}}{2 \times \ccNsum{i}{n}{i} =
                        n \times (n + 1)}
  induction n; cbn [nsum].
2 \times 0 = 0 \times (0 + 1)
n:\ccNat{}
IHn:2 \times \ccNsum{i}{n}{i} = n \times (n + 1)
2 \times (\ccSucc{ n} + \ccNsum{i}{n}{i}) =
\ccSucc{ n} \times (\ccSucc{ n} + 1)
  - (* n ← 0 *)
2 \times 0 = 0 \times (0 + 1)
    reflexivity.
  - (* n ← S _ *)
n:\ccNat{}
IHn:2 \times \ccNsum{i}{n}{i} = n \times (n + 1)
2 \times (\ccSucc{ n} + \ccNsum{i}{n}{i}) =
\ccSucc{ n} \times (\ccSucc{ n} + 1)
    rewrite Mult.mult_plus_distr_l.
n:\ccNat{}
IHn:2 \times \ccNsum{i}{n}{i} = n \times (n + 1)
2 \times \ccSucc{ n} + 2 \times \ccNsum{i}{n}{i} =
\ccSucc{ n} \times (\ccSucc{ n} + 1)
    rewrite IHn.
n:\ccNat{}
IHn:2 \times \ccNsum{i}{n}{i} = n \times (n + 1)
2 \times \ccSucc{ n} + n \times (n + 1) =
\ccSucc{ n} \times (\ccSucc{ n} + 1)
    ring.
Qed.

Note that Alectryon loads MathJax with the defer attribute, so if you need to call MathJax.typeset() or MathJax.typesetPromise(), you'll want to do that from a deferred script or from a DOMContentLoaded event listener.