实数( Coq )

Question

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

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

我们可以找到以下公理

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

没有提到库，但是在为什么实数在Coq中公理化？中可以找到相同的描述：

我想知道Coq是把实数定义为Cauchy序列还是Dedekind割集，所以我检查了Coq.Reals.Raxioms和.这两个人都没有。实数是公理化的，以及它们的运算(作为参数和公理)。为什么会这样呢？而且，实数严格依赖于子集的概念，因为它们的一个定义性质是，每个上有界子集都有一个最小的上界。公理完整性将这些子集编码为道具。“

然而，每当我看到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

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

• 构造实数，用Cauchy序列定义，完全不使用公理；
• 经典实数，是一组商的构造性结果，它使用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中的reals的公理化定义，我提供了一个构造性的定义。

Require Import Coq.Reals.Abstract.ConstructiveReals.

如果假设上面有三个公理，这将成为经典reals的接口。

Answer 2

这些描述已经过时了。过去，实数的R类型是公理化的，以及它的基本性质。但现在(自从2019?)它是用更基本的公理来定义的，或多或少就像传统数学中的那样。