lambda - fun 关键字在 Coq 中的作用是什么？

Question

我正在努力理解 Coq 中关键字“fun”的含义。

allb 有类型 all 和函数:

Inductive all (X : Type) (P : X -> Prop) : list X -> Prop :=
  | all_nil : all X P []
  | all_cons : forall (x:X) (l: list X) , P x -> all X P l -> all X P (x::l).

Fixpoint forallb {X : Type} (test : X -> bool) (l : list X) : bool :=
 match l with
| [] => true
| x :: l' => andb (test x) (forallb test l')
end.

和定理:

Theorem all_spec: forall (X:Type) (test : X -> bool) (l: list X),
    forallb test l = true <-> all X (fun x => test x = true) l.

我理解左侧部分，但对<->右侧的乐趣感到困惑。

Answer 1

它是不是就像一个lambda，即不在这里 fun x => ...就像 \x -> ...在 haskell ？

还有另一个有趣的特点 fun ...在你的代码中。代码中该函数的结果类型必须是命题 ( Prop )，而不是 bool 值。表达式test x = true一定是这种类型，所以我们得出结论 = in coq 表示关于相等的命题，而不是 bool 二元运算(在 Haskell 中称为 ==；我们没有从您的示例中看到这一点，但也许 coq 的表示法是相似的)。

所以，虽然这个想法fun ...只是一个lambda，从Haskell的角度来看有点不寻常，因为这里它引入了一个在类型级别上操作的函数(结果类型是 Prop )，而不是值级别(仅后者必须是可能的——或者至少是通常的用法——对于 Haskell 中的 \ x-> ... )。公鸡的Prop与 * 处于同一水平在 Haskell 中，不是吗？

和all X P这段代码就像 Haskell 中的类型构造函数(好吧，类型构造函数的参数化系列)，但它是一个依赖类型，类型为 [X] -> * (用 haskell 的符号表示)。 all_nil和all_cons就像这种新类型的数据构造函数。