Coq 中的实数

Question

在https://www.cs.umd.edu/~rrand/vqc/Real.html#lab1中可以阅读：

\n

\n

Coq 的标准库对实数采用了一种非常不同的方法：公理化方法。

\n

\n

并且可以找到以下公理：

\n

Axiom\n  completeness :\n    \xe2\x88\x80E:R \xe2\x86\x92 Prop,\n      bound E \xe2\x86\x92 (\xe2\x88\x83x : R, E x) \xe2\x86\x92 { m:R | is_lub E m }.\n

\n

但在《为什么实数在 Coq 中公理化？》中没有提到该库。人们可以找到相同的描述：

\n

\n

我想知道 Coq 是否将实数定义为柯西序列或 Dedekind 切割，所以我检查了 Coq.Reals.Raxioms ......这两个都不是。实数及其运算（作为参数和公理）被公理化。为什么会这样呢？

\n

\n

\n

此外，实数紧密依赖于子集的概念，因为它们的定义属性之一是每个上界子集都有一个最小上限。Axiom 完整性将这些子集编码为 Props。”

\n

\n

尽管如此，每当我查看https://coq.inria.fr/library/Coq.Reals.Raxioms.html时，我都没有看到任何公理化方法，特别是我们有以下引理：

\n

Lemma completeness :\n    forall E:R -> Prop,\n      bound E -> (exists x : R, E x) -> { m:R | is_lub E m }.\n

\n

我在哪里可以找到 Coq 中实数的这种公理化方法？

\n

Answer 1

你提到的描述确实已经过时了，因为自从我问了你链接的问题以来，我以更标准的方式重写了定义 Coq 标准库实数的公理。实数现在分为 2 层

• 构造实数，根据柯西序列定义并且根本不使用公理；
• 经典实数，它们是构造实数的商集，并且确实使用 3 个公理来证明您提到的最小上限定理。

Coq 通过以下命令轻松为您提供任何术语背后的公理Print Assumptions：

Require Import Raxioms.
Print Assumptions completeness.

Axioms:
ClassicalDedekindReals.sig_not_dec : forall P : Prop, {~ ~ P} + {~ P}
ClassicalDedekindReals.sig_forall_dec
  : forall P : nat -> Prop,
    (forall n : nat, {P n} + {~ P n}) -> {n : nat | ~ P n} + {forall n : nat, P n}
FunctionalExtensionality.functional_extensionality_dep
  : forall (A : Type) (B : A -> Type) (f g : forall x : A, B x),
    (forall x : A, f x = g x) -> f = g

正如你所看到的，这 3 个公理纯粹是逻辑性的，它们根本不涉及实数。他们只是假设古典逻辑的一个片段。

如果你想要 Coq 中实数的公理化定义，我为构造性实数提供了一个定义

Require Import Coq.Reals.Abstract.ConstructiveReals.

如果你假设上面的 3 个公理，这将成为经典实数的接口。