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)?

Bouleversement

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

Syreetasyria

Answer 2

Indeed, the Coq.Real library is a bit weak in the sense that it is totally specified as axioms, and at some (brief) points in the past it was even inconsistent.

So the definition of le is a bit "ad hoc" in the sense that from the point of view of the system it carries zero computational meaning, being just a constant and a few axioms. You could well add the axiom "x < x" and Coq could do nothing to detect it.

It is worth pointing to some alternative constructions of the Reals for Coq:

My favourite classical construction is the one done in the four Color theorem by Georges Gonthier and B. Werner: http://research.microsoft.com/en-us/downloads/5464e7b1-bd58-4f7c-bfe1-5d3b32d42e6d/

It only uses the excluded middle axiom (mainly to compare real numbers) so the confidence in its consistency is very high.

The best known axiom-free characterization of the reals is the C-CORN project, http://corn.cs.ru.nl/ but we aware that constructive analysis significantly differs from the usual one.

Appointive