Double induction in Coq

Question

Basically, I would like to prove that following result:

Lemma nat_ind_2 (P: nat -> Prop): P 0 -> P 1 -> (forall n, P n -> P (2+n)) ->
    forall n, P n.

that is the recurrence scheme of the so called double induction.

I tried to prove it applying induction two times, but I am not sure that I will get anywhere this way. Indeed, I got stuck at that point:

Proof.
  intros. elim n.
    exact H.
    intros. elim n0.
      exact H0.
      intros. apply (H1 n1).

Answer 1

Actually, there's a much simpler solution. A fix allows recursion (aka induction) on any subterm while nat_rect only allows recursion on the immediate subterm of a nat. nat_rect itself is defined with a fix, and nat_ind is just a special case of nat_rect.

Definition nat_rect_2 (P : nat -> Type) (f1 : P 0) (f2 : P 1)
  (f3 : forall n, P n -> P (S (S n))) : forall n, P n :=
  fix nat_rect_2 n :=
  match n with
  | 0 => f1
  | 1 => f2
  | S (S m) => f3 m (nat_rect_2 m)
  end.

Answer 2

@Rui's fix solution is quite general. Here is an alternative solution that uses the following observation: when proving this lemma mentally, you use somewhat stronger induction principle. For example if P holds for two consecutive numbers it becomes easy to make it hold for the next pair:

Lemma nat_ind_2 (P: nat -> Prop): P 0 -> P 1 -> (forall n, P n -> P (2+n)) ->
    forall n, P n.
Proof.
  intros P0 P1 H.
  assert (G: forall n, P n /\ P (S n)).
    induction n as [ | n [Pn PSn]]; auto.
    split; try apply H; auto.
  apply G.
Qed.

Here G proves something redundant, yet calling the induction tactic for it brings sufficient context for near-trivial proof.

Answer 3

I think well-founded induction is necessary for that.

Require Import Arith.

Theorem nat_rect_3 : forall P,
  (forall n1, (forall n2, n2 < n1 -> P n2) -> P n1) ->
  forall n, P n.
Proof.
intros P H1 n1.
apply Acc_rect with (R := lt).
  info_eauto.
  induction n1 as [| n1 H2].
    apply Acc_intro. intros n2 H3. Check lt_n_0. Check (lt_n_0 _). Check (lt_n_0 _ H3). destruct (lt_n_0 _ H3).
    destruct H2 as [H2]. apply Acc_intro. intros n2 H3. apply Acc_intro. intros n3 H4. apply H2. info_eauto with *.
Defined.

Theorem nat_rect_2 : forall P,
  P 0 ->
  P 1 ->
  (forall n, P n -> P (S (S n))) ->
  forall n, P n.
Proof.
intros ? H1 H2 H3.
induction n as [n H4] using nat_rect_3.
destruct n as [| [| n]].
info_eauto with *.
info_eauto with *.
info_eauto with *.
Defined.

Answer 4

A fun observation: Rui's answer is the fixpoint translation of NonNumeric's answer, which is the generalization of user1861759's answer for any n, not just n = 2.

In other words, these answers are all fine, and actually deeply related to one another, by the correspondence between terminating fixpoints and generalized induction.