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