我如何阅读ex_intro的定义？ [英] How do I read the definition of ex_intro?

问题描述

我正在阅读迈克·纳哈斯（Mike Nahas）介绍性的Coq教程，其中说：

ex_intro的参数是：

The arguments to "ex_intro" are:

• 谓词


• 见证人


• 证据谓词与证人通话

我看着定义：

Inductive ex (A:Type) (P:A -> Prop) : Prop :=
  ex_intro : forall x:A, P x -> ex (A:=A) P.

，我在解析它时遇到了麻烦。 表达式的哪一部分？ ex（A：= A）P 对应于这三个参数（谓词，见证和证明）？

and I'm having trouble parsing it. Which parts of the expression forall x:A, P x -> ex (A:=A) P correspond to those three arguments (predicate, witness, and proof)?

推荐答案

要了解Mike的意思，最好启动Coq解释器并查询 ex_intro 的类型：

To understand what Mike meant, it's better to launch the Coq interpreter and query for the type of ex_intro:

Check ex_intro.

然后您应该看到：

ex_intro
     : forall (A : Type) (P : A -> Prop) (x : A), P x -> exists x, P x

这表示 ex_intro 不仅需要3个参数，还需要4个参数：

This says that ex_intro takes not only 3, but 4 arguments:

• 您要量化的事物的类型， A ;


• 谓词 P：A->道具;


• 证人 x：A ;


• P x 的证明，声称 x 是有效的

• the type of the thing you're quantifying over, A;
• the predicate P : A -> Prop;
• the witness x : A; and
• a proof of P x, asserting that x is a valid witness.

如果将所有这些内容结合起来，将得到 exists x的证明x：A，P x 。例如， @ex_intro nat（fun n => n = 3）3 eq_refl 就是存在n，n = 3 。

If you combine all of those things, you get a proof of exists x : A, P x. For example, @ex_intro nat (fun n => n = 3) 3 eq_refl is a proof of exists n, n = 3.

因此， ex_intro 的实际类型与您在定义是前者包括标头中给出的所有参数-在这种情况下， A 和 P 。

Thus, the difference between the actual type of ex_intro and the one you read on the definition is that the former includes all of the parameters that are given in the header -- in this case, A and P.

这篇关于我如何阅读ex_intro的定义？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！