(*|
===================================================================
 Forget about strengthening induction hypotheses: write fixpoints!
===================================================================

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?

.. coq:: unfold
|*)

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
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``?

.. coq:: unfold
|*)

    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.

.. coq:: unfold
|*)

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 :coq:`Fixpoint` command or with the `fix` tactic) is much nicer:

.. coq:: unfold
|*)

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.

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