如何阅读 ex_intro 的定义？
How do I read the definition of ex_intro?
我正在阅读 Mike Nahas's introductory Coq tutorial，上面写着：
The arguments to "ex_intro" are:
- the predicate
- the witness
- a proof of the predicated called with the witness
我看了the definition:
Inductive ex (A:Type) (P:A -> Prop) : Prop :=
ex_intro : forall x:A, P x -> ex (A:=A) P.
我在解析它时遇到问题。表达式 forall x:A, P x -> ex (A:=A) P 的哪些部分对应于这三个参数（谓词、见证和证明）？
要理解 Mike 的意思，最好启动 Coq 解释器并查询 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 个参数：
- 您要量化的事物的类型，
A；
- 谓词
P : A -> Prop;
- 证人
x : A；和
-
P x 的证明，断言 x 是有效证人。
如果将所有这些结合起来，您将得到 exists x : A, P x 的证明。例如，@ex_intro nat (fun n => n = 3) 3 eq_refl 是 exists n, n = 3.
的证明
因此，ex_intro 的实际类型与您在定义中阅读的类型之间的区别在于，前者包括 header 中给出的所有参数——在此案例，A 和 P。
是的，那些归纳类型定义可能很难阅读。
第一部分是：
Inductive ex (A:Type) (P:A -> Prop) : Prop :=
这是与类型本身相关联的内容。所以任何时候你看到一个 ex，它都会有一个 A 和一个 P，而 ex 将是 Prop 类型。暂时跳过 A，让我们关注谓词 P。因此，如果我们使用 "there exists a natural number which is prime" 作为示例，P 可能是 is_prime，其中 is_prime 以 nat（自然数）作为参数并且可以如果 nat 是质数，则存在它的证明。
在此示例中，A 将是 nat。在教程中，A 没有被提及，因为 Coq 总能推断出它。给定谓词，Coq 可以通过查看谓词参数的类型来获得 A 的类型。
总而言之，在我们的示例中，类型为 ex nat is_prime。这表示存在一个质数 nat，但没有说明是哪个 nat。当我们构建一个 ex nat is_prime 时，我们需要说明是哪个 - 我们将需要一个 "witness"。这将我们引向构造函数定义：
ex_intro : forall x:A, P x -> ex (A:=A) P.
构造函数名为 ex_intro。这里的棘手之处在于构造函数具有该类型的所有参数。因此，在我们到达 ex_intro 之后列出的那些之前，我们必须包括类型的那些：A 和 P.
这些参数之后是 ex_intro 之后列出的参数：x，它是 witness，P x，它是谓词对 witness 持有的证明。使用我们的示例，x 可能是 2 而 P x 将是 (is_prime 2) 的证明。
构造函数需要为其构造的类型ex指定参数。这就是箭头 (->) 之后发生的事情。这些不必与调用构造函数时使用的参数匹配，但它们通常会匹配。为实现这一点，参数 A 是 而不是 被推断 - 它被显式传递。 (A:=A) 表示 ex 中的参数 A 应该等于调用构造函数中的 A 。同样，ex 的参数 P 从对构造函数的调用中设置为 P。
因此，如果我们有 proof_that_2_is_prime，类型为 (prime 2)，我们可以调用 ex_intro is_prime 2 proof_that_2_is_prime，它的类型为 ex nat is_prime。这是我们证明存在一个自然数是质数的证明。
直接回答你的问题：表达式forall x:A, P x -> ex (A:=A)中，x:A是witness，P x是witness为真的证明。表达式不包含谓词，因为它是必须传递给构造函数的类型参数的一部分 ex_intro。本教程的参数列表不包括 A，因为是由 Coq 推断的。
我希望你能理解为什么我认为这个讨论对于我的教程来说太详细了！谢谢提问。
我正在阅读 Mike Nahas's introductory Coq tutorial，上面写着：
The arguments to "ex_intro" are:
- the predicate
- the witness
- a proof of the predicated called with the witness
我看了the definition:
Inductive ex (A:Type) (P:A -> Prop) : Prop :=
ex_intro : forall x:A, P x -> ex (A:=A) P.
我在解析它时遇到问题。表达式 forall x:A, P x -> ex (A:=A) P 的哪些部分对应于这三个参数（谓词、见证和证明）？
要理解 Mike 的意思，最好启动 Coq 解释器并查询 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 个参数：
- 您要量化的事物的类型，
A； - 谓词
P : A -> Prop; - 证人
x : A；和 -
P x的证明，断言x是有效证人。
如果将所有这些结合起来，您将得到 exists x : A, P x 的证明。例如，@ex_intro nat (fun n => n = 3) 3 eq_refl 是 exists n, n = 3.
因此，ex_intro 的实际类型与您在定义中阅读的类型之间的区别在于，前者包括 header 中给出的所有参数——在此案例，A 和 P。
是的，那些归纳类型定义可能很难阅读。
第一部分是：
Inductive ex (A:Type) (P:A -> Prop) : Prop :=
这是与类型本身相关联的内容。所以任何时候你看到一个 ex，它都会有一个 A 和一个 P，而 ex 将是 Prop 类型。暂时跳过 A，让我们关注谓词 P。因此，如果我们使用 "there exists a natural number which is prime" 作为示例，P 可能是 is_prime，其中 is_prime 以 nat（自然数）作为参数并且可以如果 nat 是质数，则存在它的证明。
在此示例中，A 将是 nat。在教程中，A 没有被提及，因为 Coq 总能推断出它。给定谓词，Coq 可以通过查看谓词参数的类型来获得 A 的类型。
总而言之，在我们的示例中，类型为 ex nat is_prime。这表示存在一个质数 nat，但没有说明是哪个 nat。当我们构建一个 ex nat is_prime 时，我们需要说明是哪个 - 我们将需要一个 "witness"。这将我们引向构造函数定义：
ex_intro : forall x:A, P x -> ex (A:=A) P.
构造函数名为 ex_intro。这里的棘手之处在于构造函数具有该类型的所有参数。因此，在我们到达 ex_intro 之后列出的那些之前，我们必须包括类型的那些：A 和 P.
这些参数之后是 ex_intro 之后列出的参数：x，它是 witness，P x，它是谓词对 witness 持有的证明。使用我们的示例，x 可能是 2 而 P x 将是 (is_prime 2) 的证明。
构造函数需要为其构造的类型ex指定参数。这就是箭头 (->) 之后发生的事情。这些不必与调用构造函数时使用的参数匹配，但它们通常会匹配。为实现这一点，参数 A 是 而不是 被推断 - 它被显式传递。 (A:=A) 表示 ex 中的参数 A 应该等于调用构造函数中的 A 。同样，ex 的参数 P 从对构造函数的调用中设置为 P。
因此，如果我们有 proof_that_2_is_prime，类型为 (prime 2)，我们可以调用 ex_intro is_prime 2 proof_that_2_is_prime，它的类型为 ex nat is_prime。这是我们证明存在一个自然数是质数的证明。
直接回答你的问题：表达式forall x:A, P x -> ex (A:=A)中，x:A是witness，P x是witness为真的证明。表达式不包含谓词，因为它是必须传递给构造函数的类型参数的一部分 ex_intro。本教程的参数列表不包括 A，因为是由 Coq 推断的。
我希望你能理解为什么我认为这个讨论对于我的教程来说太详细了！谢谢提问。