Getting a stronger induction principle in Coq

Question

Assume the following:

Inductive bin : Set := Z | O.

Fixpoint fib (n : nat) : list bin :=
  match n with
    | 0   => [Z]
    | S k => match k with
               | 0    => [O]
               | S k' => fib k' ++ fib k
             end
  end.

I would like to show:

Theorem fib_first : forall n,
    Nat.Even n -> n > 3 -> exists w, fib n = Z :: w.

However, by performing induction on n, I get a really useless inductive hypothesis fixing n, stating that IH : Nat.Even n -> n > 3 -> exists w : list bin, fib n = Z :: w.

What I would ideally have is the following: IH : forall n : nat, Nat.Even n -> n > 3 -> exists w : list bin, fib n = Z :: w. Naturally I cannot assume the original proposition, but it feels like I need to prove something stronger perhaps?

My idea for the inductive reasoning would be made possible by expanding F n = F n-2 . F n-1, we know F n-2 is even iff F n is even, and since neither of F n-2 or F n-1 is empty, we can show the substring is shorter, therefore sufficient for the inductive hypothesis - how does one express this in Coq?

Answer 1

The trick is to unfold the definition of Nat.Even and do induction on n / 2 instead of n:

Theorem fib_first : forall n,
  Nat.Even n -> exists w, fib n = Z :: w.
Proof.
intros n [m ->].
induction m as [|m IH].
- now exists nil.
- rewrite <- mult_n_Sm, plus_comm.
  generalize (2 * m) IH. clear m IH. simpl.
  intros n [w ->].
  simpl. eauto.
Qed.

Note that your n > 3 hypothesis is not actually needed.