按属性定义的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的理论中,命题(即Props)及其证明具有非常特殊的地位.特别是,通常不可能编写提取存在证据的证人的选择运算符.这样做是为了使理论与某些公理和原则相容,例如证明不相关,即证明给定命题的所有证明彼此相等.如果您希望能够这样做,您需要将此选择运算符添加为理论的附加公理,就像在标准库中一样.

然而,在某些特定的情况下,是可以提取见证了一个抽象的存在,证明没有重复到任何额外的公理.特别是,Z当有问题的属性是可判定的时,可以对可数类型(例如)执行此操作.例如,您可以使用Ssreflect库中的choiceType接口来获得您想要的内容(查找函数).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计算y给定类型的函数x,然后单独证明该函数以特定方式关联输入和输出.然后,你可以说通过证明y是不同的s是不同的s是不同的.xy_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只能涉及自然数字的东西.在您的示例中,您使用整数来讨论集合的基数,并且此数字始终是自然数.