我在形式化以下形式的定义时遇到问题:定义一个整数,使某些属性成立.
假设我正式确定了该属性的定义:
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旨在适用于实际数学,这应该不难形式化.
coq ×1