coq - coq中的属性定义

Question

我在形式化以下形式的定义时遇到了麻烦:定义一个整数，使某些属性成立。

假设我正式定义了属性:

Definition IsGood (x : Z) : Prop := ...

现在我需要一个表格的定义:

Definition Good : Z := ...

假设我证明了具有该属性的整数存在并且是唯一的:

Lemma Lemma_GoodExistsUnique : exists! (x : Z), IsGood x.

有没有一种简单的方法来定义 Good使用 IsGood和 Lemma_GoodExistsUnique ?

由于该属性是在整数上定义的，因此似乎不需要额外的公理。无论如何，我看不出添加诸如选择公理之类的东西如何有助于定义。

此外，我在将以下形式的定义形式化时遇到了麻烦(我怀疑这与我上面描述的问题有关，但如果不是这种情况，请指出):对于每个 x , 存在 y ，以及这些 y因不同而不同 x .例如，如何定义有 N使用 IsGood 区分好的整数:

Definition ThereAreNGoodIntegers (N : Z) (IsGood : Z -> Prop) := ...?

在现实世界的数学中，这样的定义不时出现，因此如果 Coq 旨在适用于实际数学，这应该不难形式化。

Answer 1

对您的第一个问题的简短回答是:一般来说，这是不可能的，但在您的特定情况下，是的。

在 Coq 的理论中，命题(即 Prop s)及其证明具有非常特殊的地位。特别是，通常不可能编写提取存在证明的见证的选择运算符。这样做是为了使理论与某些公理和原则兼容，例如证明无关性，即给定命题的所有证明彼此相等。如果您希望能够做到这一点，您需要将此选择运算符作为附加公理添加到您的理论中，如 standard library 中所示。 .

但是，在某些特定情况下，可以从抽象存在证明中提取证人，而无需重复任何其他公理。特别是，当所讨论的属性是可判定的时，可以对可数类型(例如 Z )执行此操作。例如，您可以使用 choiceType Ssreflect中的界面库以获得您想要的(查找 xchoose 函数)。

话虽如此，我通常建议不要以这种方式做事，因为它会导致不必要的复杂性。定义 Good 可能更容易。直接，不借助存在性证明，再单独证明Good拥有所寻求的属性(property)。

Definition Good : Z := (* ... *)
Definition IsGood (z : Z) : Prop := (* ... *)

Lemma GoodIsGood : IsGood Good.
Proof. (* ... *) Qed.

Lemma GoodUnique : forall z : Z, IsGood z -> z = Good.

如果你绝对想定义 Good有了存在证明，你也可以改变 Lemma_GoodExistsUnique的证明在 Type 中使用连接词而不是 Prop ，因为它允许您使用 proj1_sig 直接提取见证。功能:

Lemma Lemma_GoodExistsUnique : {z : Z | Good z /\ forall z', Good z' -> z' = z}.
Proof. (* ... *) Qed.

至于你的第二个问题，是的，和第一点有点关系。再一次，我建议你写下一个函数 y_from_x类型为 Z -> Z这将计算 y给定 x ，然后分别证明该函数以特定方式关联输入和输出。那么，你可以说 y s因不同而不同 x s 通过证明 y_from_x是内射的。

另一方面，我不确定您的最后一个示例与第二个问题有何关系。如果我理解您想要正确执行的操作，您可以编写类似的内容

Definition ThereAreNGoodIntegers (N : Z) (IsGood : Z -> Prop) :=
  exists zs : list Z,
    Z.of_nat (length zs) = N
    /\ NoDup zs
    /\ Forall IsGood zs.

在这里， Z.of_nat : nat -> Z是从自然数到整数的规范注入(inject)， NoDup是断言列表不包含重复元素的谓词， Forall是一个高阶谓词，断言给定谓词(在本例中为 IsGood )包含列表的所有元素。

最后一点，我建议不要使用 Z对于只能涉及自然数的事物。在您的示例中，您使用整数来谈论集合的基数，并且该数字始终是自然数。