An example using Coqdoc

This is a hybrid rendering mode: coqdoc is used to render literate comments, and Alectryon is used to render code, responses, and goals. It's a bit as if coqdoc was just a markup language, without anything specific to Coq. Cons:

There's a dependency on coqdoc
It doesn't use a standard markup language like reST, markdown, etc.
You can't switch back and forth between a code view and a prose view: all prose editing happens in comments.
Annotations can't be applied to whole blocks, so if you want to unfold all sentences in a block you have to say on every sentence, for example.

Some code

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)
  -true = true <-> Even 0 split.true = true -> Even 0
Even 0 -> true = true
    all: constructor.
  -n:nat
IHn:even n = true <-> Even n
even (S n) = true <-> Even (S n) apply IHn.In environment
n : nat
IHn : even n = true <-> Even n
H : even n = true -> Even n
Unable to unify "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))
    +IHn:even 0 = true <-> Even 0
even 1 = true <-> Even 1 split; inversion 1.
    +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:

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