RealRocq's Axiomatic Real Numbers

Axiomatizing the set R

Traditionally, real numbers are represented by Cauchy Sequences or Dedekind Cuts. These representations are mathematically rigorous and expressible in Rocq, and implemented in libraries like the Rocq Repository at Nijmegen (CoRN). However, these representations are difficult both to express and to compute with.

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

Module OurR.

Parameter R : Set.

Delimit Scope R_scope with R.
Local Open Scope R_scope.

We'll start by declaring two real numbers - the important ones.

Parameter R₀ : R.
Parameter R₁ : R.

Along with methods for obtaining (some of) the others

Parameter Rplus : R → R → R.
Parameter Rmult : R → R → R.
Parameter Ropp : R → R.
Parameter Rinv : R → R.

Infix "+" := Rplus : R_scope.
Infix "×" := Rmult : R_scope.
Notation "- x" := (Ropp x) : R_scope.
Notation "/ x" := (Rinv x) : R_scope.

Other basic operations are given in terms of our declared ones

Definition Rminus (r₁ r₂:R) : R := r₁ + - r₂.
Definition Rdiv (r₁ r₂:R) : R := r₁ × / r₂.

Infix "-" := Rminus : R_scope.
Infix "/" := Rdiv : R_scope.

We'd like to be able to convert natural numbers to Rs, thereby allowing ourselves to write numbers like 0, 1, 2, 3...

Fixpoint INR (n : nat) : R :=
  match n with
  | O ⇒ R₀
  | 1 ⇒ R₁
  | S n' ⇒ R₁ + INR n'
  end.

The standard library defines a coercion from Z to R which is slightly more useful but also more difficult to parse.

A coercion tells Rocq to try applying a given function whenever types mismatch. For instance, Rplus 4 5 will currently give a type error.

Fail Check (4 + 5).

Coercion INR : nat >-> R.

Check 4 + 5.

The Field Equations

We can now proceed to the core of the real number library : The axioms

Axiom R1_neq_R₀ : INR 1 ≠ INR 0.

Addition

Axiom Rplus_comm : ∀ r₁ r₂ : R, r₁ + r₂ = r₂ + r₁.

Axiom Rplus_assoc : ∀ r₁ r₂ r₃ : R, r₁ + r₂ + r₃ = r₁ + (r₂ + r₃ ).

Axiom Rplus_opp_r : ∀ r : R, r + - r = 0.

Axiom Rplus_0_l : ∀ r : R, 0 + r = r.

Of course, not everything needs to be an axiom: We've left some things out.

Lemma Rplus_0_r : ∀ r : R, r + 0 = r.
Proof.
  (* WORKED IN CLASS *)
  intros r.
  rewrite Rplus_comm.
  apply Rplus_0_l.
Qed.

Lemma Rplus_opp_l : ∀ r, -r + r = 0.
Proof.
  (* WORKED IN CLASS *)
  intros r.
  rewrite Rplus_comm.
  apply Rplus_opp_r.
Qed.

Lemma Ropp_0 : -0 = 0.
Proof.
  rewrite <- (Rplus_0_l (-0)).
  rewrite Rplus_opp_r.
  reflexivity.
Qed.

Lemma Rplus_cancel_l : ∀ r₁ r₂ r₃, r₁ + r₂ = r₁ + r₃ → r₂ = r₃.
Proof.
  intros r₁ r₂ r₃ H.
  rewrite <- Rplus_0_l.
  rewrite <- (Rplus_opp_l r₁).
  rewrite Rplus_assoc.
  rewrite <- H.
  rewrite <- Rplus_assoc.
  rewrite Rplus_opp_l.
  rewrite Rplus_0_l.
  reflexivity.
Qed.

Lemma R0_unique : ∀ r₁ r₂, r₁ + r₂ = r₁ → r₂ = 0.
Proof.
  intros r₁ r₂ H.
  rewrite <- Rplus_0_r in H.
  eapply Rplus_cancel_l.
  apply H.
Qed.

Multiplicative axioms

Axiom Rmult_comm : ∀ r₁ r₂:R, r₁ × r₂ = r₂ × r₁.

Axiom Rmult_assoc : ∀ r₁ r₂ r₃:R, r₁ × r₂ × r₃ = r₁ × (r₂ × r₃ ).

Axiom Rinv_l : ∀ r:R, r ≠ 0 → / r × r = 1.

Axiom Rmult_1_l : ∀ r:R, 1 × r = r.

Axiom Rmult_plus_distr_l : ∀ r₁ r₂ r₃:R, r₁ × (r₂ + r₃ ) = r₁ × r₂ + r₁ × r₃.

Lemma Rmult_0_r : ∀ r, r × 0 = 0.
Proof.
  (* WORKED IN CLASS *)
  intros r.
  apply (R0_unique (r × 0)).
  rewrite <- Rmult_plus_distr_l.
  rewrite Rplus_0_l.
  reflexivity.
Qed.

Lemma Rmult_plus_distr_r : ∀ r₁ r₂ r₃:R, (r₁ + r₂ ) × r₃ = r₁ × r₃ + r₂ × r₃.
Proof.
  (* WORKED IN CLASS *)
  intros r₁ r₂ r₃.
  rewrite Rmult_comm.
  rewrite Rmult_plus_distr_l.
  rewrite 2 (Rmult_comm r₃).
  reflexivity.
Qed.

Lemma Rinv_r : ∀ r:R, r ≠ 0 → r × / r = 1.
Proof.
  (* WORKED IN CLASS *)
  intros. rewrite Rmult_comm.
  apply Rinv_l.
  assumption.
Qed.

The Ring and Field tactics

Once we have some set of basic lemmas, we can tell Rocq that R forms an algebraic ring and field.

Export Ring.
Export Field.

Lemma R_Ring_Theory : ring_theory R₀ R₁ Rplus Rmult Rminus Ropp eq.
Proof.
  constructor.
  (* addition *)
  (* left identity *) apply Rplus_0_l.
  (* commutativity *) apply Rplus_comm.
  (* associativity *) intros; rewrite Rplus_assoc; easy.
  (* multiplication *)
  (* left identity *) apply Rmult_1_l.
  (* commutativity *) apply Rmult_comm.
  (* associativity *) intros; rewrite Rmult_assoc; easy.
  (* distributivity *) apply Rmult_plus_distr_r.
  (* sub = opp *) reflexivity.
  (* additive inverse *) apply Rplus_opp_r.
Defined.

Add Ring RRing : R_Ring_Theory.

Lemma R_Field_Theory : field_theory R₀ R₁ Rplus Rmult Rminus Ropp Rdiv Rinv eq.
Proof.
  constructor.
  (* ring axioms *) apply R_Ring_Theory.
  (* 0 <> 1 *) apply R1_neq_R₀.
  (* div = inv *) reflexivity.
  (* multiplicative inverse *) apply Rinv_l.
Defined.

Add Field RField : R_Field_Theory.

Let's look at what these tactics can do

Example ring_test1 : ∀ (x : R), x + x = 2 × x. Proof. intros. simpl. ring. Qed.
Example ring_test2 : ∀ (x y z: R), x × y + z = z + y × x. Proof. intros. ring. Qed.

Example field_test1 : ∀ (x y : R), x ≠ 0 → x × y / x = y.
Proof. intros. Fail ring. field. assumption. Qed.

Ordering

We also impose the standard ordering on real numbers, again by means of axioms

Parameter Rlt : R → R → Prop.

Infix "<" := Rlt : R_scope.

Definition Rgt (r₁ r₂:R) : Prop := r₂ < r₁.
Definition Rle (r₁ r₂:R) : Prop := r₁ < r₂ ∨ r₁ = r₂.
Definition Rge (r₁ r₂:R) : Prop := Rgt r₁ r₂ ∨ r₁ = r₂.

Infix "≤" := Rle : R_scope.
Infix "≥" := Rge : R_scope.
Infix ">" := Rgt : R_scope.

Axiom total_order_T : ∀ r₁ r₂ : R, {r₁ < r₂ } + {r₁ = r₂ } + {r₁ > r₂ }.

Axiom Rlt_asym : ∀ r₁ r₂ : R, r₁ < r₂ → ¬ r₂ < r₁.

Axiom Rlt_trans : ∀ r₁ r₂ r₃ : R, r₁ < r₂ → r₂ < r₃ → r₁ < r₃.

Axiom Rplus_lt_compat_l : ∀ r r₁ r₂ : R, r₁ < r₂ → r + r₁ < r + r₂.

Axiom Rmult_lt_compat_l : ∀ r r₁ r₂ : R, 0 < r → r₁ < r₂ → r × r₁ < r × r₂.

Completeness

Of course, not every field corresponds to the real numbers: Even the rational numbers (a strict subset of the reals) form a field. The last thing we need to "complete" the real numbers is the completeness axiom. This states that every bounded set of real numbers has a least upper bound, which itself is a real number.

As usual, we will express sets as functions of type R → Prop, indicating whether the given real number is a member of the set.

Definition is_upper_bound (E:R → Prop) (m:R) := ∀ x:R, E x → x ≤ m.

Definition bound (E:R → Prop) := ∃ m : R , is_upper_bound E m.

Definition is_lub (E:R → Prop) (m:R) :=
is_upper_bound E m ∧ (∀ b:R, is_upper_bound E b → m ≤ b ).

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

Defining irrational numbers

Let's see an example of the completeness axiom in practice. We'll only need one new lemma, which we can prove, but it's harder than you think.

Lemma Rlt_0_1 : 0 < 1. Admitted.

We want to define the square root of 2. The square root of 2 is the least upper bound of the predicate x × x < 2 (or x × x ≤ 2). Let's use the completeness axiom to show that such a least upper bound exists.

Definition lt_sqrt2 (x : R) := x × x < 2.

First we need to show that this predicate has an upper bound. One reasonable upper bound is 2 (though 3/2 and 5 would also work).

Lemma upper_bound_2_sqrt_2 : is_upper_bound lt_sqrt2 2.
Proof.
  unfold is_upper_bound, lt_sqrt2; simpl.
  intros x H.
  left.
  destruct (total_order_T x 1) as [[L | E] | G].
  - rewrite <- (Rplus_0_r x).
    eapply Rlt_trans.
    apply Rplus_lt_compat_l.
    apply Rlt_0_1.
    rewrite Rplus_comm.
    apply Rplus_lt_compat_l.
    assumption.
  - rewrite E.
    rewrite <- (Rplus_0_r 1).
    apply Rplus_lt_compat_l.
    apply Rlt_0_1.
  - assert (x × 1 < x × x).
    apply Rmult_lt_compat_l.
    eapply Rlt_trans.
    apply Rlt_0_1.
    apply G.
    apply G.
    rewrite Rmult_comm, Rmult_1_l in H₀.
    eapply Rlt_trans.
    apply H₀.
    apply H.
Qed.

Lemma bound_sqrt2 : bound lt_sqrt2.
Proof. ∃ 2. apply upper_bound_2_sqrt_2. Qed.

We also need to show that some number satisfies this predicate: 0, 1 and -1 are all reasonable candidates.

Lemma ex_lt_sqrt2 : ∃ x , lt_sqrt2 x.
Proof.
  ∃ 1. unfold lt_sqrt2.
  rewrite Rmult_1_l.
  rewrite <- (Rplus_0_r 1); simpl.
  apply Rplus_lt_compat_l.
  apply Rlt_0_1.
Qed.

We can now plug these proofs into our completeness axiom/function, getting out a real number that is the least upper bound of lt_sqrt2 -- that is, the square root of 2.

Definition sqrt2 := completeness lt_sqrt2 bound_sqrt2 ex_lt_sqrt2.

In subsequent chapters we will make use of real numbers like √2, π and e, which are defined in the Rocq real number library using the completeness axiom.

End OurR.

Let's take a look at our upper bound proof using Rocq's own real numbers and definitions. Here we will benefit from Rocq's automation tactics.

Export Reals.
Export Psatz.

Open Scope R_scope.

Definition lt_sqrt2 (x : R) := x × x < 2.

Lemma upper_bound_2_sqrt_2 : is_upper_bound lt_sqrt2 2.
Proof.
  unfold is_upper_bound, lt_sqrt2; simpl.
  intros x H.
  destruct (total_order_T x 1) as [[L | E] | G]; try lra.
  assert (x × 1 ≤ x × x).
  { apply Rmult_le_compat_l; lra. }
  lra.
Qed.

lra stands for Linear Real Arithmetic and is broadly useful in proving real number (in)equalities

Notation "√ x" := (sqrt x) (at level 1).

Lemma pow2_sqrt : ∀ x:R, 0 ≤ x → (√ x ) ^ 2 = x.
Proof. intros; simpl; rewrite Rmult_1_r, sqrt_def; auto. Qed.

Lemma pow2_sqrt2 : (√ 2) ^ 2 = 2.
Proof. apply pow2_sqrt; lra. Qed.

Lemma pown_sqrt : ∀ (x : R) (n : nat),
0 ≤ x → √ x ^ (S (S n)) = (x × √ x ^ n)%R.
Proof.
intros. simpl. rewrite <- Rmult_assoc. rewrite sqrt_sqrt; auto.
Qed.

Lemma sqrt_neq_0_compat : ∀ r : R, 0 < r → (√ r)%R ≠ 0.
Proof. intros. specialize (sqrt_lt_R₀ r). lra. Qed.

Lemma sqrt_inv : ∀ (r : R), 0 < r → √ (/ r ) = (/ √ r)%R.
Proof.
  intros.
  replace (/r)%R with (1/r)%R by lra.
  rewrite sqrt_div_alt, sqrt_1 by lra.
  lra.
Qed.

Lemma sqrt2_inv : √ (/ 2) = (/ √ 2)%R.
Proof.
apply sqrt_inv; lra.
Qed.

(* 2026-09-08 13:38 *)