Why do Coq recursion principles pass along both the substructure and the result of the recursive call?

Question

After examining a few different recursion principles generated for different recursive data types, I noticed that in the recursive case, substructures are passed along with the result of the recursive call on the substructure.

For example, doing Print list_rect gives:

list_rect =
fun (A : Type) (P : list A -> Type) (f : P nil)
  (f0 : forall (a : A) (l : list A), P l -> P (a :: l)%list) =>
fix F (l : list A) : P l :=
  match l as l0 return (P l0) with
  | nil => f
  | (y :: l0)%list => f0 y l0 (F l0)
  end
     : forall (A : Type) (P : list A -> Type),
       P nil ->
       (forall (a : A) (l : list A), P l -> P (a :: l)%list) ->
       forall l : list A, P l

In the pattern match, the cons case looks like (y :: l0)%list => f0 y l0 (F l0). Why does f0 take both l0 and the result of recursively calling F on l0? What are situations when you need access to the tail of the list when you've already computed the result of calling F on it?

Answer 1

As soon as you need the induction hypothesis, you need the tail of the list because it appears in its type: to write P l, l needs to be in scope.

Now if you weren't bothered about types, a good reason to have both the tail of the list and the recursive call is efficiency: computing the tail is linear in the size of the list but grabbing it on the way is constant time. The prototypical example of this type of issue is the definition of the predecessor function for unary natural numbers when you only have access to the iterator and not the recursor.