As an alternative induction principle of nat, nat_ind2 is defined like so:
Definition nat_ind2 :
forall (P : nat -> Prop),
P 0 ->
P 1 ->
(forall n : nat, P n -> P (S(S n))) ->
forall n : nat , P n :=
fun P => fun P0 => fun P1 => fun PSS =>
fix f (n:nat) := match n with
0 => P0
| 1 => P1
| S (S n') => PSS n' (f n')
end.
If my IDE isn't wrong, function f has the type nat -> nat. But I thought PSS requires something of the type P n in its second argument, so why is f typed like so?
Also, is there a way to define nat_ind2 as a Fixpoint? I tried this:
Fixpoint nat_ind (P : nat -> Prop) (P0 : P 0) (P1 : P 1)
(PSS : forall n : nat, P n -> P (S (S n))) (n : nat) :=
fix PK :=
match n with
| 0 => P0
| 1 => P1
| S (S k) => PSS k (PK k)
end.
But it doesn't work. The main difficulty I think is that PK can't be annotated to take the right type (P k). I'm pretty new to coq, so there's probably something I'm missing.
Edit: My IDE is probably wrong, the type of f should be forall n:nat, P n
With recent Coq (8.18) you can write:
Fixpoint nat_ind2 (P : nat -> Prop) (P0 : P 0) (P1 : P 1)
(PSS : forall n : nat, P n -> P (S (S n))) (n : nat) :=
match n with
| 0 => P0
| 1 => P1
| S (S k) => PSS k (nat_ind2 P P0 P1 PSS k)
end.
About nat_ind2.
which gives
nat_ind2 :
forall P : nat -> Prop,
P 0 ->
P 1 ->
(forall n : nat, P n -> P (S (S n))) -> forall n : nat, P n
I think this was not always possible - the consistency checker for fixpoints has been improved over time.
But there are reasons for using the more complicated design above with a local fixpoint: you can pass only the one changing argument and keep all others from the outer function. If functions are used for computation, this does make a performance / stack space difference, but for induction principles which are usually only used in opaque proofs, this doesn't make a difference and IMHO the simpler variant without a local fixpoint definition is preferable.