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?

Lemma even_Even :
  forall n, even n = true <-> Even n. (* .fold *)
Proof. (* .fold *)
  induction n.
  all: cbn.
  - (* n ← 0 *)
    split.
    all: constructor.
  - (* n ← S _ *)
    Fail apply IHn. (* .fails .no-goals *) (* stuck! *)

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

destruct n.
+ (* n ← 1 *)
  split; inversion 1.
+ (* n ← S (S _) *)

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)). (* .fold *)
Proof. (* .fold *)
  induction n; cbn.
  - (* n ← 0 *)
    repeat split; cbn.
    all: try constructor.
    all: inversion 1.
  - (* n ← S _ *)
    destruct IHn as ((Hne & HnE) & (HSne & HSnE)).
    repeat split; cbn.
    all: eauto using EvenS.
    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. (* .fold *)
Proof. (* .fold *)
  destruct n as [ | [ | n ] ]; cbn.
  - (* n ← 0 *)
    repeat constructor.
  - (* n ← 1 *)
    split; inversion 1.
  - (* n ← S (S _) *)
    split.
    + constructor; apply even_Even_fp; assumption.
    + inversion 1; apply even_Even_fp; assumption.
Qed.

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