Coq 中的实数

Question

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

Coq's standard library takes a very different approach to the real numbers: An axiomatic approach.

并且可以找到以下公理：

Axiom
  completeness :
    ∀E:R → Prop,
      bound E → (∃x : R, E x) → { m:R | is_lub E m }.

没有提到该库，但在中可以找到相同的描述：

I was wondering whether Coq defined the real numbers as Cauchy sequences or Dedekind cuts, so I checked Coq.Reals.Raxioms and... none of these two. The real numbers are axiomatized, along with their operations (as Parameters and Axioms). Why is it so?

Also, the real numbers tightly rely on the notion of subset, since one of their defining properties is that is every upper bounded subset has a least upper bound. The Axiom completeness encodes those subsets as Props."

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

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

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

Answer 1

这些描述已经过时了。它曾经是实数类型 R 及其基本属性被公理化的情况。但是现在（自 2019?），它是根据更基本的公理来定义的，或多或少就像人们在传统数学中所做的那样。

Answer 2

你提到的描述确实过时了，因为自从我问了你链接的问题后，我以更标准的方式重写了定义 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 个公理，这将成为经典实数的接口。

Coq 中的实数

Real numbers in Coq

coq

real-number