(** * 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 (* .unfold *) 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.