问按属性定义的coq

EN

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

在Coq理论中，命题(即Props)及其证明具有非常特殊的地位。特别是，通常不可能写出提取存在证据的证人的选择操作符。这样做是为了使该理论与某些公理和原则相一致，例如证明无关性，即一个命题的所有证明都是平等的。如果您想要做到这一点，您需要添加这个选择运算符作为您的理论的附加公理，如在标准库。

然而，在某些特殊情况下，可以从抽象的存在证明中提取证人，而不必重复任何附加的公理。特别是，当所讨论的属性是可判定的时，可以对可数类型(如Z)执行此操作。例如，您可以使用斯皮尔库中的斯皮尔接口来获得您想要的结果(查找xchoose函数)。

尽管如此，我通常会建议不要这样做，因为这会导致不必要的复杂性。直接定义Good可能更容易，而无需诉诸存在性证明，然后单独证明Good具有所寻求的属性。

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来计算给定的x，然后分别证明该函数以特定的方式关联输入和输出。然后，通过证明y是内射的，可以说对于不同的xs，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是从自然数到整数的规范注入，NoDup是断言列表不包含重复元素的谓词，Forall是一个高阶谓词，断言给定谓词(在本例中，IsGood)持有列表中的所有元素。

最后，我建议不要在只涉及自然数的情况下使用Z。在您的示例中，您使用一个整数来讨论一个集合的基数，这个数字始终是一个自然数。