Can I tell Coq to do induction from n to n+2?

Question

I'm trying to see if it's possible to prove evenb n = true <-> exists k, n = double k from https://softwarefoundations.cis.upenn.edu/lf-current/Logic.html without involving odd numbers at all. I tried something like the following:

Theorem evenb_double_k : forall n,
  evenb n = true -> exists k, n = double k.
Proof.
  intros n H. induction n as [|n' IHn'].
  - exists 0. reflexivity.
  - (* stuck *)

But apparently induction works one natural number at a time, and exists k : nat, S n' = double k is clearly not provable.

n' : nat
H : evenb (S n') = true
IHn' : evenb n' = true -> exists k : nat, n' = double k
______________________________________(1/1)
exists k : nat, S n' = double k

Is there a way to have induction go from n to n+2?

Answer 1

Yes, absolutely! Let's use the induction principle from this answer.

From Coq Require Import Arith.

Lemma pair_induction (P : nat -> Prop) :
  P 0 -> P 1 ->
  (forall n, P n -> P (S n) -> P (S (S n))) ->
  forall n, P n.
Proof.
  intros H0 H1 Hstep n.
  enough (P n /\ P (S n)) by easy.
  induction n; intuition.
Qed.

Now we can use the new principle like so (I switched the non-standard functions with their stdlib counterparts so that everything compiles):

Theorem evenb_double_k : forall n,
  Nat.even n = true -> exists k, n = Nat.double k.
Proof.
  intros n Ev.
  induction n as [| |n IHn _] using pair_induction.
  (* the rest of the proof has been removed to not spoil the fun *)
Qed.