使用列表刪除功能

Question

我試圖使用Coq standard library中的列表刪除功能，但它要求一個奇怪的打字，我不知道如何解決。

我執行的功能是使自由變量列表中一個lambda項如下：

Fixpoint fv (t : trm) : vars := 
    match t with 
    | Var v => [v] 
    | App t1 t2 => (fv t1) ++ (fv t2) 
    | Abs x t' => remove x (fv t') 
    end. 

，它給我下面的錯誤：

Error: In environment 
fv : trm -> vars 
t : trm 
x : nat 
t' : trm 
The term "x" has type "nat" while it is expected to have type 
"forall x0 y : ?171, {x0 = y} + {x0 <> y}". 

我很確定，在remove函數的定義中，這個hyphotesis事情有點關係。我不知道如何處理它，有什麼幫助？

Hypothesis eq_dec : forall x y : A, {x = y}+{x <> y}. 

該函數刪除藉此作爲第一個參數（其可以看到通過執行Print remove.）

這一假說是決定元件的平等的函數：

Answer 1

remove在含有上下文中定義的類型在你的列表中。在你的情況下，你將不得不提供一個函數來決定var（這似乎是nat，所以標準庫中也可能有這樣一個函數）的相等性。

如果你不知道「{P} + {Q}」符號，你可以看看它在這裏： http://coq.inria.fr/library/Coq.Init.Specif.html#sumbool