Elevate the real numbers to actually existing (#65)

Numbers/Rationals/Definition.agda

@@ -85,3 +85,6 @@ negateQWellDefined a b a=b = inverseWellDefined (Ring.additiveGroup ℚRing) {a}
 
 ℚOrdered : TotallyOrderedRing ℚPOrdered
 ℚOrdered = fieldOfFractionsOrderedRing
+
+ℚcharNot2 : ((Ring.1R ℚRing) +Q (Ring.1R ℚRing)) =Q (Ring.0R ℚRing) → False
+ℚcharNot2 ()

Numbers/Reals.agda

@@ -1,39 +0,0 @@
-{-# OPTIONS --safe --warning=error #-}
-
-open import Fields.Fields
-open import Functions
-open import Orders
-open import LogicalFormulae
-open import Numbers.Rationals
-open import Numbers.RationalsLemmas
-open import Numbers.Naturals
-open import Setoids.Setoids
-open import Setoids.Orders
-
-open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
-
-module Numbers.Reals where
-  record ℝ : Set where
-    field
-      f : ℕ → ℚ
-      converges : {ε : ℚ} → Sg ℕ (λ x → {y : ℕ} → x <N y → (absQ ((f x) -Q (f y))) <Q ε)
-
-  _+R_ : ℝ → ℝ → ℝ
-  ℝ.f (record { f = a ; converges = conA } +R record { f = b ; converges = conB }) n = (a n) +Q (b n)
-  ℝ.converges (record { f = a ; converges = conA } +R record { f = b ; converges = conB }) {e} = {!absQ (a x +Q b x)!}
-
-  negateR : ℝ → ℝ
-  ℝ.f (negateR record { f = f ; converges = converges }) n = negateQ (f n)
-  ℝ.converges (negateR record { f = f ; converges = converges }) {e} with converges {e}
-  ... | n , pr = n , λ {y} x<y → SetoidPartialOrder.wellDefined ℚPartialOrder {absQ ((f n) -Q (f y))} {absQ ((negateQ (f n)) -Q (negateQ (f y)))} {e} {e} {!!} {!reflQ e!} (pr {y} x<y)
-
-  _-R_ : ℝ → ℝ → ℝ
-  a -R b = a +R (negateR b)
-
-  _*R_ : ℝ → ℝ → ℝ
-  ℝ.f (record { f = a ; converges = conA } *R record { f = b ; converges = conB }) n = (a n) *Q (b n)
-  ℝ.converges (record { f = a ; converges = conA } *R record { f = b ; converges = conB}) {e} = {!!}
-
-  realsSetoid : Setoid ℝ
-  (realsSetoid Setoid.∼ record { f = a ; converges = convA }) record { f = b ; converges = convB } = {!!}
-  Setoid.eq realsSetoid = {!!}

Numbers/Reals/Definition.agda

@@ -0,0 +1,39 @@
+{-# OPTIONS --warning=error --safe --guardedness #-}
+
+open import Setoids.Orders
+open import LogicalFormulae
+open import Rings.Definition
+open import Numbers.Rationals.Definition
+
+module Numbers.Reals.Definition where
+
+open import Fields.CauchyCompletion.Definition ℚOrdered ℚField
+open import Fields.CauchyCompletion.Setoid ℚOrdered ℚField ℚcharNot2
+open import Fields.CauchyCompletion.Addition ℚOrdered ℚField ℚcharNot2
+open import Fields.CauchyCompletion.Multiplication ℚOrdered ℚField ℚcharNot2
+open import Fields.CauchyCompletion.Ring ℚOrdered ℚField ℚcharNot2
+open import Fields.CauchyCompletion.Comparison ℚOrdered ℚField ℚcharNot2
+
+ℝ : Set
+ℝ = CauchyCompletion
+
+_+R_ : ℝ → ℝ → ℝ
+_+R_ = _+C_
+
+_*R_ : ℝ → ℝ → ℝ
+_*R_ = _*C_
+
+ℝRing : Ring cauchyCompletionSetoid _+R_ _*R_
+ℝRing = CRing
+
+injectionR : ℚ → ℝ
+injectionR = injection
+
+0R : ℝ
+0R = injection 0Q
+
+_<R_ : ℝ → ℝ → Set
+_<R_ = _<C_
+
+ℝPartialOrder : SetoidPartialOrder cauchyCompletionSetoid _<C_
+ℝPartialOrder = <COrder