Literate programming with Alectryon (Coq input)

Alectryon supports literate programs and documents (combinations of code and prose) written in Coq and reStructuredText. Here is an example, written in Coq. It can be converted to reST, HTML, or LaTeX using the following commands:

alectryon literate_coq.v
    # Coq+reST → HTML;  produces ‘literate_coq.html’
alectryon --html-dialect=html5 literate_coq.v \
  -o literate_coq.5.html
    # Coq+reST → HTML5; produces ‘literate_coq.5.html’
$ DOCUTILSCONFIG=literate.docutils.conf alectryon \
  literate_coq.v --backend latex
    # Coq+reST → LaTeX; produces ‘literate_coq.tex’
$ DOCUTILSCONFIG=literate.docutils.conf alectryon \
  literate_coq.v --backend latex --latex-dialect lualatex \
  -o literate_coq.lua.tex
    # Coq+reST → LuaLaTeX; produces ‘literate_coq.lua.tex’
alectryon literate_coq.v --backend rst
    # Coq+reST → reST;  produces ‘literate_coq.v.rst’

$ cd ..; python -m alectryon.literate --from coq --to rst \
    recipes/literate_coq.v > recipes/literate_coq.min.rst
  # Minimal Coq → reST; produces ‘literate_coq.min.rst’
$ cd ..; python -m alectryon.literate --from coq --to rst - \
    < recipes/literate_coq.v > recipes/literate_coq.min.stdin.rst
  # Minimal Coq → reST; produces ‘literate_coq.min.stdin.rst’

Here's an inductive specification of evenness:

Inductive Even : nat -> Prop :=
| EvenO : Even O
| EvenS : forall n, Even n -> Even (S (S n)).

… and a corresponding decision procedure:

Fixpoint even (n: nat): bool :=
  match n with
  | 0 => true
  | 1 => false
  | S (S n) => even n
  end.

(* Ensure that we never unfold [even (S n)] *)
Arguments even : simpl nomatch.

Can we prove it correct?

Lemma even_Even :
  forall n, even n = true <-> Even n.forall n : nat, even n = true <-> Even n
Proof.forall n : nat, even n = true <-> Even n
  induction n.even 0 = true <-> Even 0
n: nat
IHn: even n = true <-> Even n
even (S n) = true <-> Even (S n)
  all: cbn.true = true <-> Even 0
n: nat
IHn: even n = true <-> Even n
even (S n) = true <-> Even (S n)
  - (* n ← 0 *)true = true <-> Even 0
    split.true = true -> Even 0
Even 0 -> true = true
    all: constructor.
  - (* n ← S _ *)n: nat
IHn: even n = true <-> Even n
even (S n) = true <-> Even (S n)
    apply IHn. (* stuck! *)In environment
n : nat
IHn : even n = true <-> Even n
Unable to unify "even n = true <-> Even n" with
 "even (S n) = true <-> Even (S n)".

The induction hypothesis doesn't apply — maybe we need to destruct n?

    destruct n.IHn: even 0 = true <-> Even 0
even 1 = true <-> Even 1
n: nat
IHn: even (S n) = true <-> Even (S n)
even (S (S n)) = true <-> Even (S (S n))
    + (* n ← 1 *)IHn: even 0 = true <-> Even 0
even 1 = true <-> Even 1
      split; inversion 1.
    + (* n ← S (S _) *)n: nat
IHn: even (S n) = true <-> Even (S n)
even (S (S n)) = true <-> Even (S (S n))

Stuck again!

Abort.

Strengthening the spec

The usual approach is to strengthen the spec to work around the weakness of the inductive principle.

Lemma even_Even :
  forall n, (even n = true <-> Even n) /\
       (even (S n) = true <-> Even (S n)).forall n : nat,
(even n = true <-> Even n) /\
(even (S n) = true <-> Even (S n))
Proof.forall n : nat,
(even n = true <-> Even n) /\
(even (S n) = true <-> Even (S n))
  induction n; cbn.(true = true <-> Even 0) /\ (false = true <-> Even 1)
n: nat
IHn: (even n = true <-> Even n) /\
(even (S n) = true <-> Even (S n))
(even (S n) = true <-> Even (S n)) /\
(even n = true <-> Even (S (S n)))
  - (* n ← 0 *)(true = true <-> Even 0) /\ (false = true <-> Even 1)
    repeat split; cbn.true = true -> Even 0
false = true -> Even 1
Even 1 -> false = true
    all: try constructor.false = true -> Even 1
Even 1 -> false = true
    all: inversion 1.
  - (* n ← S _ *)n: nat
IHn: (even n = true <-> Even n) /\
(even (S n) = true <-> Even (S n))
(even (S n) = true <-> Even (S n)) /\
(even n = true <-> Even (S (S n)))
    destruct IHn as ((Hne & HnE) & (HSne & HSnE)).n: nat
Hne: even n = true -> Even n
HnE: Even n -> even n = true
HSne: even (S n) = true -> Even (S n)
HSnE: Even (S n) -> even (S n) = true
(even (S n) = true <-> Even (S n)) /\
(even n = true <-> Even (S (S n)))
    repeat split; cbn.n: nat
Hne: even n = true -> Even n
HnE: Even n -> even n = true
HSne: even (S n) = true -> Even (S n)
HSnE: Even (S n) -> even (S n) = true
even (S n) = true -> Even (S n)
n: nat
Hne: even n = true -> Even n
HnE: Even n -> even n = true
HSne: even (S n) = true -> Even (S n)
HSnE: Even (S n) -> even (S n) = true
Even (S n) -> even (S n) = true
n: nat
Hne: even n = true -> Even n
HnE: Even n -> even n = true
HSne: even (S n) = true -> Even (S n)
HSnE: Even (S n) -> even (S n) = true
even n = true -> Even (S (S n))
n: nat
Hne: even n = true -> Even n
HnE: Even n -> even n = true
HSne: even (S n) = true -> Even (S n)
HSnE: Even (S n) -> even (S n) = true
Even (S (S n)) -> even n = true
    all: eauto using EvenS.n: nat
Hne: even n = true -> Even n
HnE: Even n -> even n = true
HSne: even (S n) = true -> Even (S n)
HSnE: Even (S n) -> even (S n) = true
Even (S (S n)) -> even n = true
    inversion 1; eauto.
Qed.

Writing a fixpoint

But writing a fixpoint (either with the Fixpoint command or with the fix tactic) is much nicer:

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 ] ]; 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
    repeat constructor.
  - (* n ← 1 *)even_Even_fp: forall n : nat, even n = true <-> Even n
false = true <-> Even 1
    split; 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
    +even_Even_fp: forall n : nat, even n = true <-> Even n
n: nat
even n = true -> Even (S (S n)) constructor; apply even_Even_fp; assumption.
    +even_Even_fp: forall n : nat, even n = true <-> Even n
n: nat
Even (S (S n)) -> even n = true inversion 1; apply even_Even_fp; assumption.
Qed.

Alectryon defines a :coqid: role to link to definitions in Coqdoc-generated documentation; for example:

Note that the standard library already contains a boolean predicate for even (called Coq.Init.Nat.even, or even for short), as well as an inductive one (called Nat.Even in module Coq.Arith.PeanoNat).

If you have your own documentation, you can use a custom role to point to your own URL:

With this definition, for example, you can write Nat.Even instead of Nat.Even.