Coq定理中的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中使用双箭头(=>)标记模式匹配分支.例如，我们可以像这样定义布尔否定：

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

单箭头(->)用于表示两个看似无关的概念：

1. 功能类型例如，nat -> bool是从自然数到布尔函数的类型。
2. 逻辑含义。这就是你在定理陈述中看到的用法。A -> B语句意味着，每当A存在时，B就保持不变。

然而，在现实中，这种区分只是表面的:在Coq中，对含义和功能的证明实际上是一回事！对于Coq来说，隐含A -> B的证明在某种意义上是一个函数，它接受一个断言A真理的证明，并返回一个断言B真理的证明。如果这听起来令人困惑，请不要担心:你可以在大多数情况下假装箭头的两种用法指的是不同的东西，这不会伤害你。软件基金会的书有一个第二章，可以更详细地讨论这些问题。