coq - Coq arrow -> 在 Coq 定理中是什么意思？

Question

我正在尝试理解 Coq 定理:

Theorem thm0 : UseCl Pos (PredVP (UsePN john_PN) walk_V) ->
               UseCl Pos (PredVP (UsePN john_PN) walk_V).
intro H.
exact H.
Qed.

来自 https://github.com/GU-CLASP/FraCoq/blob/master/Tutorial.org

箭头符号 -> 是什么意思？据我了解，Coq 使用两个箭头 https://softwarefoundations.cis.upenn.edu/lf-current/Basics.html : 1) 用于定义类型构造函数的双箭头和 2) 用于定义新类型的单箭头 ->。但是这个定理是语句，不是类型定义。为什么会有这个箭头？如何将此陈述理解为 Coq 定理？

Answer 1

双箭头 (=>) 在 Coq 中用于标记模式匹配分支。例如，我们可以这样定义 bool 否定:

Definition negb (b : bool) : bool :=
  match b with
  | true  => false
  | false => true
  end.

单箭头(->)用来表达两个看似无关的概念:

1. 函数类型。例如，nat -> bool 是从自然数到 bool 值的函数类型。

2. 逻辑蕴涵。这是您在定理陈述中看到的用法。语句 A -> B 表示只要 A 成立，B 就成立。

然而，实际上，这种区别只是表面上的:在 Coq 中，蕴涵证明和函数实际上是一回事!对于 Coq，蕴涵式证明 A -> B 在精确意义上是一个函数，它采用断言 A 为真的证明并返回断言为真的证明B。如果这听起来令人困惑，请不要担心:大多数时候你可以假装箭头的两种用法指的是不同的东西，这不会伤害你。软件基础一书有一个 chapter更详细地讨论了这些问题。