When is the first input to `list_rec` not a constant function?

Question

The list_rec function has the type:

list_rec
 : forall (A : Type) (P : list A -> Set),
   P nil ->
   (forall (a : A) (l : list A), P l -> P (a :: l)%list) ->
   forall l : list A, P l

In all of the examples I've come up with, P is just a constant function that ignores the input list and returns the same type no matter what. For example, P might be fun _ : list A => nat or fun _ : list A => list B. What are some use cases for making the output of P dependent on the input? Why is the type of P list A -> Set instead of just Set?

Answer 1

We can, for example, use list_rec with a non-constant P function to implement a function that converts a list to a vector (a length-indexed list).

Require List Vector.
Import List.ListNotations Vector.VectorNotations.
Set Implicit Arguments.

Section VecExample.
Variable A : Set.
Definition P (xs : list A) : Set := Vector.t A (length xs).

Definition list_to_vector : forall xs : list A, Vector.t A (length xs) := 
  list_rec P [] (fun x _ vtail => x :: vtail).
End VecExample.

You can compare it with the standard definition of the Vector.of_list function, which does exactly the same (t means Vector.t in the following code), using explicit recursion instead of hiding it behind a recursion principle:

Fixpoint of_list {A} (l : list A) : t A (length l) :=
match l as l' return t A (length l') with
  |Datatypes.nil => []
  |(h :: tail)%list => (h :: (of_list tail))
end.

A simple test:

Eval compute in list_to_vector [1;2;3].
Eval compute in Vector.of_list [1;2;3].

Both function calls return the same result:

= [1; 2; 3]
     : Vector.t nat (length [1; 2; 3])

Answer 2

Try to prove s ++ [] = s.

[Hint: Define P as fun s => s ++ [] = s.]