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

Question

可在此处找到的Coq标准库文件Coq.Init.Logic 包含该语句

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.这里有一种真实的含糊之处; 在这种情况下,如果a forall (x:A), B具有B不依赖的x,Coq更喜欢使用符号而不是内置语法来打印它.如果你关闭符号打印(Unset Printing Notation.),你会看到forall (_:A), B你曾经看过的任何地方A -> B.当然,如果你有一个具有真实依赖关系的函数类型,那么Coq需要使用,forall (x:A), B因为B需要引用变量x.