有趣的关键字在Coq中做了什么？

Question

我正在努力理解Coq中关键词'fun'的含义.

有所有类型和功能forallb:

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 ...您的代码中还有另一个有趣的特性.代码中该函数的结果类型必须是proposition(Prop),而不是boolean.表达式test x = true必须是那种类型,因此我们得出结论,=在coq中表示关于相等性的命题,而不是布尔二进制操作(==在Haskell中已知;我们不会从您的示例中看到这一点,但也许coq的符号相似).

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

而all X P在此代码,就像是哈斯克尔类型构造(当然,参数化的家庭类型构造),但依赖一个,类型[X] -> *(Haskell中的符号).all_nil并且all_cons就像这种新类型的数据构造函数.