「list_rec」的第一個輸入何時不是一個常量函數？

的list_rec函數的類型：「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？

來源

2016-12-31 mushroom

我們可以，例如，使用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])

來源

2017-01-01 10:48:10

試着證明s ++ [] = s。

[提示：定義P作爲fun s => s ++ [] = s。]

來源

2017-01-01 09:20:54 ejgallego

「list_rec」的第一個輸入何時不是一個常量函數？

回答

相關問題