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.
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.
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#).