Literate programming with Alectryon (reST input)

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

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

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

Coq fragments are introduced with .. coq:::

Lemma le_l : forall y x, S x <= y -> x <= y.forall y x : nat, S x <= y -> x <= y
  induction y; inversion 1; subst.y: nat
IHy: forall x : nat, S x <= y -> x <= y
H: S y <= S y
y <= S y
y: nat
IHy: forall x : nat, S x <= y -> x <= y
x: nat
H: S x <= S y
H1: S x <= y
x <= S y
  all: info_eauto.(* info eauto: *)
simple apply le_S.
simple apply le_n.
(* info eauto: *)
simple apply le_S.
simple apply IHy.
exact H1.
Qed.

Goal forall x y z, x <= y <= z -> x <= z.forall x y z : nat, x <= y <= z -> x <= z

They can be nested into other reST directives, such as tables:

Coq commands
Coq command	Description
intros x y. `x, y`: nat forall z : nat, x <= y <= z -> x <= z	Move the variables `x` and `y` into the context.
revert x; induction y. forall x z : nat, x <= 0 <= z -> x <= z `y`: nat `IHy`: forall x z : nat, x <= y <= z -> x <= z forall x z : nat, x <= S y <= z -> x <= z	Perform induction on `y`, generalizing `x`.
all: intros x z (Hl & Hr). `x, z`: nat `Hl`: x <= 0 `Hr`: 0 <= z x <= z `y`: nat `IHy`: forall x z : nat, x <= y <= z -> x <= z `x, z`: nat `Hl`: x <= S y `Hr`: S y <= z x <= z	Move conjunction into the context, splitting it into `Hl` and `Hr`.
- `x, z`: nat `Hl`: x <= 0 `Hr`: 0 <= z x <= z inversion Hl; assumption.	Solve base case; `inversion` changes `x <= 0` into `x = 0`.
- `y`: nat `IHy`: forall x z : nat, x <= y <= z -> x <= z `x, z`: nat `Hl`: x <= S y `Hr`: S y <= z x <= z inversion Hl; subst; try congruence. `y`: nat `IHy`: forall x z : nat, x <= y <= z -> x <= z `x, z`: nat `Hl`: x <= S y `Hr`: S y <= z `H0`: x <= y x <= z apply IHy; split; info_eauto using le_l. (* info eauto: ) exact H0. ( info eauto: *) simple apply le_l. exact Hr.	Solve inductive case using the `le_l` lemma.

Directive options

The .. coq:: directive supports :class: and :name: attributes. Adding :name: makes the block a referenceable target, and :class: attaches CSS classes:

Definition test := "Hello, World!".

Link to first Coq fragment. Another link.