How is "less than" defined for real numbers in Coq?

Question

I am just wondering how is the "less than" relationship defined for real numbers.

I understand that for natural numbers (nat), < can be defined recursively in terms of one number being the (1+) successor S of another number. I heard that many things about real numbers are axiomatic in Coq and do not compute.

But I am wondering whether there is a minimum set of axioms for real numbers in Coq based upon which other properties/relations can be derived. (e.g. Coq.Reals.RIneq has it that Rplus_0_r : forall r, r + 0 = r. is an axiom, among others)

In particular, I am interested in whether the relationships such as < or <= can be defined on top of the equality relationship. For example, I can imagine that in conventional math, given two numbers r1 r2:

r1 < r2 <=> exists s, s > 0 /\ r1 + s = r2.

But does this hold in the constructive logic of Coq? And can I use this to at least do some reasoning about inequalities (instead of rewriting axioms all the time)?

Answer 1

Coq.Reals.RIneq has it that Rplus_0_r : forall r, r + 0 = r. is an axiom, among others

Nitpick: Rplus_0_r is not an axiom but Rplus_0_l is. You can get a list of them in the module Coq.Reals.Raxioms and a list of the parameters used in Coq.Reals.Rdefinitions.

As you can see "greater than (or equal)" and "less than or equal" are all defined in terms of "less than" which is postulated rather than introduced using the proposition you suggest.

It looks like Rlt could indeed be defined in the fashion you suggest: the two propositions are provably equivalent as shown below.

Require Import Reals.
Require Import Psatz.
Open Scope R_scope.

Goal forall (r1 r2 : R), r1 < r2 <-> exists s, s > 0 /\ r1 + s = r2.
Proof.
intros r1 r2; split.
 - intros H; exists (r2 - r1); split; [lra | ring].
 - intros [s [s_pos eq]]; lra.
Qed.

However you would still need to define what it means to be "strictly positive" for the s > 0 bit to make sense and it's not at all clear that you'd have fewer axioms in the end (e.g. the notion of being strictly positive should be closed under addition, multiplication, etc.).