An axiomatization of real numbers $\mathbb{R}$

This file provides a classical axiomatization of real numbers as a
discrete real archimedean field with in particular a theory of floor and
ceil.

    realType == type of real numbers                                       
       sup A == where A : set R with R : realType, the supremum of A when  
                it exists, 0 otherwise                                     
       inf A := - sup (- A)

The mixin corresponding to realType extends an archiFieldType with two
properties:

when sup A exists, it is an upper bound of A (lemma sup_upper_bound)
when sup A exists, there exists an element x in A such that
sup A - eps < x for any 0 < eps (lemma sup_adherent)

        Rint == the set of real numbers that can be written as z%:~R,      
                i.e., as an integer                                        
    Rtoint r == r when r is an integer, 0 otherwise                        
 floor_set x := [set y | Rtoint y /\ y <= x]                               
    Rfloor x == the floor of x as a real number                            
     floor x == the floor of x as an integer (type int)                    
    range1 x := [set y |x <= y < x + 1]                                    
     Rceil x == the ceil of x as a real number, i.e., - Rfloor (- x)       
      ceil x := - floor (- x)

From mathcomp Require Import all_ssreflect all_algebra.
From mathcomp Require Import mathcomp_extra boolp classical_sets set_interval.

Require Import Setoid.

Declare Scope real_scope.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Unset SsrOldRewriteGoalsOrder.

Import Order.TTheory Order.Syntax GRing.Theory Num.Def Num.Theory.

Delimit Scope real_scope with real.

Local Open Scope classical_set_scope.
Local Open Scope ring_scope.

Section subr_image .
Variable R : numDomainType.
Implicit Types (E : set R) (x : R).

Lemma has_ub_lbN E : has_ubound E <-> has_lbound (-%R @` E).

Proof.

Lemma has_lbound0 : has_lbound (@set0 R)

Proof.

Lemma has_ubound0 : has_ubound (@set0 R)

Proof.

Lemma ubound0 : ubound (@set0 R) = setT.

Proof.

Lemma lboundT : lbound [set: R] = set0.

Proof.

End subr_image.

Section has_bound_lemmas .
Variable R : realDomainType.
Implicit Types E : set R.
Implicit Types x : R.

Lemma has_ub_image_norm E : has_ubound (normr @` E) -> has_ubound E.

Proof.

Lemma has_inf_supN E : has_sup (-%R @` E) <-> has_inf E.

Proof.

Lemma has_supPn {E} : E !=set0 ->
~ has_sup E <-> (forall x, exists2 y, E y & x < y).

Proof.

End has_bound_lemmas.

Module Real .
Section Mixin .

Variable ( R : archiFieldType).

Record mixin_of : Type := Mixin {
   _ :
    forall E : set (Num.ArchimedeanField.sort R),
      has_sup E -> ubound E (supremum 0 E) ;
   _ :
    forall ( E : set (Num.ArchimedeanField.sort R)) ( eps : R), 0 < eps ->
      has_sup E -> exists2 e : R, E e & (supremum 0 E - eps) < e ;
}.

End Mixin.

Definition EtaMixin R sup_upper_bound sup_adherent :=
  let _ := @Mixin R sup_upper_bound sup_adherent in
  @Mixin (Num.ArchimedeanField.Pack (Num.ArchimedeanField.class R))
         sup_upper_bound sup_adherent.
Section ClassDef .

Record class_of ( R : Type) : Type := Class {
   base : Num.ArchimedeanField.class_of R;
   mixin_rcf : Num.real_closed_axiom (Num.NumDomain.Pack base);
   mixin : mixin_of (Num.ArchimedeanField.Pack base)
}.

Local Coercion base : class_of >-> Num.ArchimedeanField.class_of.
Local Coercion base_rcf R ( c : class_of R) : Num.RealClosedField.class_of R :=
  @Num.RealClosedField.Class _ c (@mixin_rcf _ c).

Structure type := Pack {sort; _ : class_of sort; _ : Type}.
Local Coercion sort : type >-> Sortclass.
Variables ( T : Type) ( cT : type).
Definition class := let: Pack _ c _ as cT' := cT return class_of cT' in c.
Definition clone c of phant_id class c := @Pack T c T.
Let xT := let: Pack T _ _ := cT in T.
Notation xclass := (class : class_of xT).

Definition rcf_axiom {R} ( cR : Num.RealClosedField.class_of R) :
   Num.real_closed_axiom (Num.NumDomain.Pack cR) :=
  match cR with Num.RealClosedField.Class _ ax => ax end.
Coercion rcf_axiom : Num.RealClosedField.class_of >-> Num.real_closed_axiom.

Definition pack b0 ( m0 : mixin_of (@Num.ArchimedeanField.Pack T b0)) :=
  fun bT b & phant_id (Num.ArchimedeanField.class bT) b =>
  fun ( bTr : rcfType) ( br : Num.RealClosedField.class_of bTr) &
      phant_id (Num.RealClosedField.class bTr) br =>
  fun cra & phant_id (@rcf_axiom bTr br) cra =>
  fun m & phant_id m0 m => Pack (@Class T b cra m) T.

Definition eqType := @Equality.Pack cT xclass.
Definition choiceType := @Choice.Pack cT xclass.
Definition porderType := @Order.POrder.Pack ring_display cT xclass.
Definition latticeType := @Order.Lattice.Pack ring_display cT xclass.
Definition distrLatticeType := @Order.DistrLattice.Pack ring_display cT xclass.
Definition orderType := @Order.Total.Pack ring_display cT xclass.
Definition zmodType := @GRing.Zmodule.Pack cT xclass.
Definition ringType := @GRing.Ring.Pack cT xclass.
Definition comRingType := @GRing.ComRing.Pack cT xclass.
Definition unitRingType := @GRing.UnitRing.Pack cT xclass.
Definition comUnitRingType := @GRing.ComUnitRing.Pack cT xclass.
Definition idomainType := @GRing.IntegralDomain.Pack cT xclass.
Definition numDomainType := @Num.NumDomain.Pack cT xclass.
Definition normedZmodType := NormedZmodType numDomainType cT xclass.
Definition fieldType := @GRing.Field.Pack cT xclass.
Definition realDomainType := @Num.RealDomain.Pack cT xclass.
Definition numFieldType := @Num.NumField.Pack cT xclass.
Definition realFieldType := @Num.RealField.Pack cT xclass.
Definition archimedeanFieldType := @Num.ArchimedeanField.Pack cT xclass.
Definition rcfType := @Num.RealClosedField.Pack cT xclass.
Definition join_rcfType := @Num.RealClosedField.Pack archimedeanFieldType xclass.

End ClassDef.

Module Exports .
Coercion base : class_of >-> Num.ArchimedeanField.class_of.
Coercion base_rcf : class_of >-> Num.RealClosedField.class_of.
Coercion mixin : class_of >-> mixin_of.
Coercion sort : type >-> Sortclass.
Bind Scope ring_scope with sort.
Coercion eqType : type >-> Equality.type.
Canonical eqType.
Coercion choiceType : type >-> Choice.type.
Canonical choiceType.
Coercion porderType : type >-> Order.POrder.type.
Canonical porderType.
Coercion latticeType : type >-> Order.Lattice.type.
Canonical latticeType.
Coercion distrLatticeType : type >-> Order.DistrLattice.type.
Canonical distrLatticeType.
Coercion orderType : type >-> Order.Total.type.
Canonical orderType.
Coercion zmodType : type >-> GRing.Zmodule.type.
Canonical zmodType.
Coercion ringType : type >-> GRing.Ring.type.
Canonical ringType.
Coercion comRingType : type >-> GRing.ComRing.type.
Canonical comRingType.
Coercion unitRingType : type >-> GRing.UnitRing.type.
Canonical unitRingType.
Coercion comUnitRingType : type >-> GRing.ComUnitRing.type.
Canonical comUnitRingType.
Coercion idomainType : type >-> GRing.IntegralDomain.type.
Canonical idomainType.
Coercion numDomainType : type >-> Num.NumDomain.type.
Canonical numDomainType.
Coercion normedZmodType : type >-> Num.NormedZmodule.type.
Canonical normedZmodType.
Coercion realDomainType : type >-> Num.RealDomain.type.
Canonical realDomainType.
Coercion fieldType : type >-> GRing.Field.type.
Canonical fieldType.
Coercion numFieldType : type >-> Num.NumField.type.
Canonical numFieldType.
Coercion realFieldType : type >-> Num.RealField.type.
Canonical realFieldType.
Coercion archimedeanFieldType : type >-> Num.ArchimedeanField.type.
Canonical archimedeanFieldType.
Coercion rcfType : type >-> Num.RealClosedField.type.
Canonical rcfType.
Canonical join_rcfType.

Notation realType := type.
Notation RealType T m := (@pack T _ m _ _ id _ _ id _ id _ id).
Notation RealMixin := EtaMixin.
Notation "[ 'realType' 'of' T 'for' cT ]" := (@clone T cT _ idfun)
  (at level 0, format "[ 'realType'  'of'  T  'for'  cT ]") : form_scope.
Notation "[ 'realType' 'of' T ]" := (@clone T _ _ id)
  (at level 0, format "[ 'realType'  'of'  T ]") : form_scope.

End Exports.
End Real.

Export Real.Exports.

Definition sup {R : realType} := @supremum _ R 0.
Definition inf {R : realType} ( E : set R) := - sup (-%R @` E).

Lemma sup_upper_bound {R : realType} ( E : set R):
  has_sup E -> ubound E (sup E).

Proof.

Lemma sup_adherent {R : realType} ( E : set R) ( eps : R) : 0 < eps ->
has_sup E -> exists2 e : R, E e & (sup E - eps) < e.

Proof.

Section IsInt .
Context {R : realFieldType}.

Definition Rint := [qualify a x : R | `[< exists z, x == z%:~R >]].
Fact Rint_key : pred_key Rint

Proof.

Canonical Rint_keyed := KeyedQualifier Rint_key.

Lemma Rint_def x : (x \is a Rint) = (`[< exists z, x == z%:~R >]).

Proof.

Lemma RintP x : reflect (exists z, x = z%:~R) (x \in Rint).

Proof.

Lemma RintC z : z%:~R \is a Rint.

Proof.

Lemma Rint0 : 0 \is a Rint.

Proof.

Lemma Rint1 : 1 \is a Rint.

Proof.

Hint Resolve Rint0 Rint1 RintC : core.

Lemma Rint_subring_closed : subring_closed Rint.

Proof.

Canonical Rint_opprPred := OpprPred Rint_subring_closed.
Canonical Rint_addrPred := AddrPred Rint_subring_closed.
Canonical Rint_mulrPred := MulrPred Rint_subring_closed.
Canonical Rint_zmodPred := ZmodPred Rint_subring_closed.
Canonical Rint_semiringPred := SemiringPred Rint_subring_closed.
Canonical Rint_smulrPred := SmulrPred Rint_subring_closed.
Canonical Rint_subringPred := SubringPred Rint_subring_closed.

Lemma Rint_ler_addr1 ( x y : R) : x \is a Rint -> y \is a Rint ->
(x + 1 <= y) = (x < y).

Proof.

Lemma Rint_ltr_addr1 ( x y : R) : x \is a Rint -> y \is a Rint ->
(x < y + 1) = (x <= y).

Proof.

End IsInt.

Section ToInt .
Context {R : realType}.

Implicit Types x y : R.

Definition Rtoint ( x : R) : int :=
  if insub x : {? x | x \is a Rint} is Some Px then
    xchoose (asboolP _ (tagged Px))
  else 0.

Lemma RtointK ( x : R): x \is a Rint -> (Rtoint x)%:~R = x.

Proof.

Lemma Rtointz ( z : int): Rtoint z%:~R = z.

Proof.

Lemma Rtointn ( n : nat): Rtoint n%:R = n%:~R.

Proof.

Lemma inj_Rtoint : {in Rint &, injective Rtoint}.

Proof.

Lemma RtointN x : x \is a Rint -> Rtoint (- x) = - Rtoint x.

Proof.

End ToInt.

Section RealDerivedOps .
Variable R : realType.

Implicit Types x y : R.
Definition floor_set x := [set y : R | (y \is a Rint) && (y <= x)].

Definition Rfloor x : R := sup (floor_set x).

Definition floor x : int := Rtoint (Rfloor x).

Definition range1 ( x : R) := [set y | x <= y < x + 1].

Definition Rceil x := - Rfloor (- x).

Definition ceil x := - floor (- x).

End RealDerivedOps.

Section RealLemmas .

Variables ( R : realType).

Implicit Types E : set R.
Implicit Types x : R.

Lemma sup_out E : ~ has_sup E -> sup E = 0

Proof.

Lemma sup0 : sup (@set0 R) = 0

Proof.

Lemma sup1 x : sup [set x] = x

Proof.

Lemma sup_ub {E} : has_ubound E -> ubound E (sup E).

Proof.

Lemma sup_ub_strict E : has_ubound E ->
~ E (sup E) -> E `<=` [set r | r < sup E].

Proof.

Lemma sup_total {E} x : has_sup E -> down E x \/ sup E <= x.

Proof.

Lemma sup_le_ub {E} x : E !=set0 -> (ubound E) x -> sup E <= x.

Proof.

Lemma sup_setU ( A B : set R) : has_sup B ->
(forall a b, A a -> B b -> a <= b) -> sup (A `|` B) = sup B.

Proof.

Lemma sup_gt ( S : set R) ( x : R) : S !=set0 ->
(x < sup S -> exists2 y, S y & x < y)%R.

Proof.

End RealLemmas.

Section sup_sum .
Context {R : realType}.

Lemma sup_sumE ( A B : set R) :
has_sup A -> has_sup B -> sup [set x + y | x in A & y in B] = sup A + sup B.

Proof.

Lemma inf_sumE ( A B : set R) :
has_inf A -> has_inf B -> inf [set x + y | x in A & y in B] = inf A + inf B.

Proof.

End sup_sum.

Section InfTheory .

Variables ( R : realType).

Implicit Types E : set R.
Implicit Types x : R.

Lemma inf_lower_bound E : has_inf E -> lbound E (inf E).

Proof.

Lemma inf_adherent E ( eps : R) : 0 < eps ->
has_inf E -> exists2 e, E e & e < inf E + eps.

Proof.

Lemma inf_out E : ~ has_inf E -> inf E = 0.

Proof.

Lemma inf0 : inf (@set0 R) = 0.

Proof.

Lemma inf1 x : inf [set x] = x.

Proof.

Lemma inf_lb E : has_lbound E -> lbound E (inf E).

Proof.

Lemma inf_lb_strict E : has_lbound E ->
~ E (inf E) -> E `<=` [set r | inf E < r].

Proof.

Lemma lb_le_inf E x : nonempty E -> (lbound E) x -> x <= inf E.

Proof.

Lemma has_infPn E : nonempty E ->
~ has_inf E <-> (forall x, exists2 y, E y & y < x).

Proof.

Lemma inf_setU ( A B : set R) : has_inf A ->
(forall a b, A a -> B b -> a <= b) -> inf (A `|` B) = inf A.

Proof.

Lemma inf_lt ( S : set R) ( x : R) : S !=set0 ->
(inf S < x -> exists2 y, S y & y < x)%R.

Proof.

End InfTheory.

Section FloorTheory .
Variable R : realType.

Implicit Types x y : R.

Lemma has_sup_floor_set x : has_sup (floor_set x).

Proof.

Lemma sup_in_floor_set x : (floor_set x) (sup (floor_set x)).

Proof.

Lemma isint_Rfloor x : Rfloor x \is a Rint.

Proof.

Lemma RfloorE x : Rfloor x = (floor x)%:~R.

Proof.

Lemma mem_rg1_Rfloor x : (range1 (Rfloor x)) x.

Proof.

Lemma Rfloor_le x : Rfloor x <= x.

Proof.

Lemma floor_le x : (floor x)%:~R <= x.

Proof.

Lemma lt_succ_Rfloor x : x < Rfloor x + 1.

Proof.

Lemma range1z_inj x ( m1 m2 : int) :
(range1 m1%:~R) x -> (range1 m2%:~R) x -> m1 = m2.

Proof.

Lemma range1rr x : (range1 x) x.

Proof.

Lemma range1zP ( m : int) x : Rfloor x = m%:~R <-> (range1 m%:~R) x.

Proof.

Lemma Rfloor_natz ( z : int) : Rfloor z%:~R = z%:~R :> R.

Proof.

Lemma Rfloor0 : Rfloor 0 = 0 :> R.

Proof.

Lemma Rfloor1 : Rfloor 1 = 1 :> R.

Proof.

Lemma le_Rfloor : {homo (@Rfloor R) : x y / x <= y}.

Proof.

Lemma Rfloor_ge_int x ( n : int) : (n%:~R <= x)= (n%:~R <= Rfloor x).

Proof.

Lemma Rfloor_lt_int x ( z : int) : (x < z%:~R) = (Rfloor x < z%:~R).

Proof.

Lemma Rfloor_le0 x : x <= 0 -> Rfloor x <= 0.

Proof.

Lemma Rfloor_lt0 x : x < 0 -> Rfloor x < 0.

Proof.

Lemma floor_natz n : floor (n%:R : R) = n%:~R :> int.

Proof.

Lemma floor0 : floor (0 : R) = 0.

Proof.

Lemma floor1 : floor (1 : R) = 1.

Proof.

Lemma floor_ge0 x : (0 <= floor x) = (0 <= x).

Proof.

Lemma floor_le0 x : x <= 0 -> floor x <= 0.

Proof.

Lemma floor_lt0 x : x < 0 -> floor x < 0.

Proof.

Lemma le_floor : {homo @floor R : x y / x <= y}.

Proof.

Lemma floor_neq0 x : (floor x != 0) = (x < 0) || (x >= 1).

Proof.

Lemma lt_succ_floor x : x < (floor x)%:~R + 1.

Proof.

Lemma floor_lt_int x ( z : int) : (x < z%:~R) = (floor x < z).

Proof.

Lemma floor_ge_int x ( z : int) : (z%:~R <= x) = (z <= floor x).

Proof.

Lemma ltr_add_invr ( y x : R) : y < x -> exists k, y + k.+1%:R^-1 < x.

Proof.

End FloorTheory.

Section CeilTheory .
Variable R : realType.

Implicit Types x y : R.

Lemma isint_Rceil x : Rceil x \is a Rint.

Proof.

Lemma Rceil0 : Rceil 0 = 0 :> R.

Proof.

Lemma Rceil_ge x : x <= Rceil x.

Proof.

Lemma le_Rceil : {homo (@Rceil R) : x y / x <= y}.

Proof.

Lemma Rceil_ge0 x : 0 <= x -> 0 <= Rceil x.

Proof.

Lemma RceilE x : Rceil x = (ceil x)%:~R.

Proof.

Lemma ceil_ge x : x <= (ceil x)%:~R.

Proof.

Lemma ceil_ge0 x : 0 <= x -> 0 <= ceil x.

Proof.

Lemma ceil_gt0 x : 0 < x -> 0 < ceil x.

Proof.

Lemma ceil_le0 x : x <= 0 -> ceil x <= 0.

Proof.

Lemma le_ceil : {homo @ceil R : x y / x <= y}.

Proof.

Lemma ceil_ge_int x ( z : int) : (x <= z%:~R) = (ceil x <= z).

Proof.

Lemma ceil_lt_int x ( z : int) : (z%:~R < x) = (z < ceil x).

Proof.

Lemma ceilN x : ceil (- x) = - floor x

Proof.

Lemma floorN x : floor (- x) = - ceil x

Proof.

End CeilTheory.

Section Sup .
Context {R : realType}.
Implicit Types A B : set R.

Lemma le_down A : A `<=` down A.

Proof.

Lemma downK A : down (down A) = down A.

Proof.

Lemma has_sup_down A : has_sup (down A) <-> has_sup A.

Proof.

Lemma le_sup A B : A `<=` down B -> nonempty A -> has_sup B ->
sup A <= sup B.

Proof.

Lemma le_inf A B : -%R @` B `<=` down (-%R @` A) -> nonempty B -> has_inf A ->
inf A <= inf B.

Proof.

Lemma sup_down A : sup (down A) = sup A.

Proof.

Lemma lt_sup_imfset {T : Type} ( F : T -> R) l :
  has_sup [set y | exists x, y = F x] ->
  l < sup [set y | exists x, y = F x] ->
  exists2 x, l < F x & F x <= sup [set y | exists x, y = F x].

Proof.

Lemma lt_inf_imfset {T : Type} ( F : T -> R) l :
  has_inf [set y | exists x, y = F x] ->
  inf [set y | exists x, y = F x] < l ->
  exists2 x, F x < l & inf [set y | exists x, y = F x] <= F x.

Proof.

End Sup.

Lemma int_lbound_has_minimum ( B : set int) i : B !=set0 -> lbound B i ->
exists j, B j /\ forall k, B k -> j <= k.

Proof.

Section rat_in_itvoo .

Let bound_div ( R : archiFieldType) ( x y : R) : nat :=
if y < 0 then 0%N else Num.bound (y / x).

Let archi_bound_divP ( R : archiFieldType) ( x y : R) :
0 < x -> y < x *+ bound_div x y.

Proof.

Lemma rat_in_itvoo ( R : realType) ( x y : R) :
x < y -> exists q, ratr q \in `]x, y[.

Proof.

End rat_in_itvoo.

Module mathcomp.analysis.reals

An axiomatization of real numbers R\mathbb{R}R

An axiomatization of real numbers $\mathbb{R}$