Когда первый вход в `list_rec` не является постоянной функцией?

Question

list_rec функция имеет вид:

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 

Во всех примерах, которые я придумал, P только постоянная функция, которая игнорирует список ввода и возвращает тот же тип, независимо от того, что. Например, P может быть fun _ : list A => nat или fun _ : list A => list B. Каковы некоторые варианты использования вывода P в зависимости от ввода? Почему тип Plist A -> Set вместо Set?

Answer 1

Мы можем, например, использовать list_rec с непостоянной P функции реализовать функцию, которая преобразует список в вектор (длина индексированные список) ,

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. 

Вы можете сравнить его со стандартным определением функции Vector.of_list, которая делает точно то же самое (t означает Vector.t в следующем коде), с использованием явной рекурсии вместо того, чтобы скрыть это за принцип рекурсии:

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. 

простой тест:

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

Обе функции возвращают вызовы и тот же результат:

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

Answer 2

Попробуйте доказать s ++ [] = s.

[Подсказка: Определить P, как fun s => s ++ [] = s.]