在以下简单定理中，直接以证明功能的形式给出了证明。我想了解这两个术语是如何反映我的概念的两个术语，并将其结合成返回预期类型的最终证明功能。
Lemma simple : forall i, i <= S i.
Proof
fun i => (le_S i i) (le_n i).
似乎（le_s ii）构造函数返回了一个函数，然后将（le_n i）作为参数。有人可以解释在这里如何起作用的证明功能组合如何工作吗？
In the following simple theorem the proof is given directly in the form of a proof function. I'd like to understand how the two terms, parenthesized to reflect my concept, combine into a final proof function that returns the expected type.
Lemma simple : forall i, i <= S i.
Proof
fun i => (le_S i i) (le_n i).
It seems as if the (le_S i i) constructor term returned a function which then would accept (le_n i) as a parameter. Could someone be kind to explain how proof function combination works here?
发布评论
评论（2）
（LE_S II）是一个函数的值。它期望作为参数的另一个值，此处（le_n i），类型（i＆lt; = i），因为le_n的类型是forall n：nat，（n＆lt; = n）。（le_s ii）的值应用于此参数的是类型（i＆lt; = s I），正如您可以从le_s <的类型中看到的那样/代码>。引理中的forall在用于定义简单的最终值中说明了fun。(le_S i i)is a value that is a function. It expects as argument another value, here(le_n i), of type(i <= i), since the type ofle_nisforall n : nat, (n <= n). The value of(le_S i i)applied to this argument is of type(i <= S i), as you could see from the type ofle_S. Theforallin the lemma explains thefunin the final value used to definesimple.您可能需要阅读（）。
基本上，在COQ证明中，功能是以某种命题为论点的证据（以证人的形式）作为参数，并为新的派生主张提供证据（证人）。
如果您执行
检查LE_S。，您会得到le_s是一个功能，它需要两个NAT和见证人n＆lt; = m并产生一个见证n＆lt; = s M。在您中，示例
le_n i是i＆lt; = i的见证。请注意，
- ＆gt;符号对于通常的功能具有相同的含义，例如检查Nat.Add。与证明相同。
a - ＆gt; b在两种情况下都意味着a到类型b的功能。You might want to read (https://en.wikipedia.org/wiki/Curry–Howard_correspondence).
Basically in Coq proofs are functions which take evidence (in form of a witness) for some proposition as arguments and produce evidence (a witness) for a new derived proposition.
If you do
Check le_S.you getSo
le_Sis a function which takes two nats and a witness forn <= mand produces a witness forn <= S m.In you example
le_n iis a witness fori <= i.Please note that the
->symbol has the same meaning for usual functions likeCheck Nat.add.as for proofs.
a -> bin both cases means function from typeato typeb.