coq - 使用列表删除功能

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}".

我很确定删除函数的定义中与假设有关。我不知道如何处理它，有什么帮助吗？

Answer 1

remove 在包含以下内容的上下文中定义:

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

函数removes将此作为第一个参数(您可以通过执行Printremove看到。)

这个假设是一个函数，决定列表中类型元素的相等性。在你的情况下，你必须提供一个函数来决定 var 的相等性(这似乎是 nat，所以标准库中也可能有这样的函数) .

如果您不知道“{p} + {q}”表示法，可以在这里查找: http://coq.inria.fr/library/Coq.Init.Specif.html#sumbool