在下面的简单定理中，证明直接以证明函数的形式给出。我想了解这两个用括号括起来以反映我的概念的术语如何组合成一个返回预期类型的最终证明函数。
Lemma simple : forall i, i <= S i.
Proof
fun i => (le_S i i) (le_n i).
似乎(le_S i i) 构造函数项返回了一个函数，该函数随后将接受(le_n i) 作为参数。有人可以解释一下证明函数组合是如何工作的吗？
【问题讨论】：
标签： coq
(le_S i i) 是一个函数值。它期望另一个值作为参数，这里是(le_n i)，类型为(i <= i)，因为le_n 的类型是forall n : nat, (n <= n)。应用于此参数的(le_S i i) 的值是(i <= S i) 类型，从le_S 的类型中可以看出。引理中的forall 解释了用于定义simple 的最终值中的fun。
【讨论】：
le_S i i 是一个函数。你能简单解释一下吗。
le_S 的类型，您会看到它是 forall n m : nat, (n <= m) -> (n <= S m)。一旦为n 和m 传递了两个参数i 和i，您将获得一个可以传递(le_n i) 的函数值。
您可能想阅读 (https://en.wikipedia.org/wiki/Curry–Howard_correspondence)。
基本上，在 Coq 中，证明是一些函数，它们将某个命题的证据（以证人的形式）作为论据，并为新的派生命题产生证据（证人）。
如果你这样做Check le_S.，你会得到
le_S
: forall n m : nat, n <= m -> n <= S m
所以le_S 是一个函数，它接受两个nat 和n <= m 的见证，并为n <= S m 生成见证。
在您的示例中，le_n i 是i <= i 的见证人。
请注意->symbol 与Check Nat.add. 等常用函数的含义相同
Nat.add
: nat -> nat -> nat
至于证明。 a -> b 在这两种情况下都表示从a 类型到b 类型的函数。
【讨论】：