Understanding nat_ind2 in Logical Foundations

Question

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

Answer 1

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.