coq - 为什么 Coq.Init.Logic 定义符号 "A -> B"？

Question

Coq 标准库文件 Coq.Init.Logic，可以找到 here , 包含语句
Notation "A -> B" := (forall (_ : A), B) : type_scope.
我不明白这怎么可能，因为符号 ->已经具有内在含义。是 ->被这个覆盖？

如果我输入 A -> B , Coq 怎么知道我的意思是 A -> B或 forall (x : A), B ?

是的，我知道这两个命题在逻辑上是等价的，但这不应该是一个定理而不是一个符号吗？

如您所知，我对 Coq 没有太多经验，但我想了解细节。

Answer 1

->符号实际上是由您在 Coq.Init.Logic 中找到的符号定义的。 !而forall是内置的，->是使用符号系统定义的。 Coq.Init.Logic模块会自动加载到 Coq 中，因为它是由 Coq.Init.Prelude 导出的，这就是为什么您可以立即访问它。

当你写 A -> B它使用符号来解释，即 forall (_:A), B ;这在语法上类似于 forall (x:A), B , 除了表达式 B不允许依赖 x .没有歧义 - 这是 A -> B 的唯一定义, 实际上如果你在没有前奏的情况下加载 Coq(例如，通过传递 -noinit 标志)A -> B不会解析。

Coq 的一个方面使 ->似乎内置的是符号是双向的 - 它适用于解析和打印。这就是为什么您会看到 ->在您的目标中以及当您使用 Check 时和 Search .这里有真正的歧义；在这种情况下，如果 forall (x:A), B有一个 B不依赖于 x , Coq 更喜欢使用符号而不是内置语法来打印它。如果您关闭符号打印 (Unset Printing Notation.)，您将看到 forall (_:A), B你曾经看到的任何地方A -> B .当然，如果你有一个真正依赖的函数类型，那么 Coq 需要使用 forall (x:A), B自从 B需要引用变量x .