Search code examples
coqreal-number

Real numbers in Coq

In https://www.cs.umd.edu/~rrand/vqc/Real.html#lab1 one can read:

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

and one can find the following axiom:

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

The library is not mentioned but in Why are the real numbers axiomatized in Coq? one can find the same description :

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."

Nevertheless, whenever I look at https://coq.inria.fr/library/Coq.Reals.Raxioms.html I do not see any axiomatic approach, in particular we have the following lemma:

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

Where can I find such an axiomatic approach of the real numbers in Coq?

Solution

  • The description you mention is outdated indeed, because since I asked the question you linked, I rewrote the axioms defining Coq's standard library real numbers in a more standard way. The real numbers are now divided into 2 layers

    • constructive real numbers, that are defined in terms of Cauchy sequences and that use no axioms at all;
    • classical real numbers, that are a quotient set of constructive reals, and that do use 3 axioms to prove the least upper bound theorem that you mention.

    Coq easily gives you the axioms underlying any term by the Print Assumptions command:

    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

    As you can see these 3 axioms are purely logical, they do not speak about real numbers at all. They just assume a fragment of classical logic.

    If you want an axiomatic definition of the reals in Coq, I provided one for the constructive reals

    Require Import Coq.Reals.Abstract.ConstructiveReals.

    And this becomes an interface for classical reals if you assume the 3 axioms above.