From 82b81b4bab767adb98a5244fe51c46e69ff9874e Mon Sep 17 00:00:00 2001
From: Patrick Stevens <smaug451@gmail.com>
Date: Mon, 4 Nov 2019 07:34:59 +0000
Subject: [PATCH] Elevate the real numbers to actually existing (#65)

---
 Everything/WithK.agda              |  4 ++-
 Fields/FieldOfFractions/Field.agda | 19 ++++++++-------
 Numbers/Rationals/Definition.agda  |  3 +++
 Numbers/Reals.agda                 | 39 ------------------------------
 Numbers/Reals/Definition.agda      | 39 ++++++++++++++++++++++++++++++
 5 files changed, 55 insertions(+), 49 deletions(-)
 delete mode 100644 Numbers/Reals.agda
 create mode 100644 Numbers/Reals/Definition.agda

diff --git a/Everything/WithK.agda b/Everything/WithK.agda
index bc7f5e1..169c2c0 100644
--- a/Everything/WithK.agda
+++ b/Everything/WithK.agda
@@ -1,4 +1,4 @@
-{-# OPTIONS --warning=error --safe #-}
+{-# OPTIONS --warning=error --safe --guardedness #-}
 
 -- This file contains everything that is --safe, but uses K.
 
@@ -7,6 +7,8 @@ open import Numbers.Primes.IntegerFactorisation
 open import Numbers.Rationals.Definition
 open import Numbers.Rationals.Lemmas
 
+open import Numbers.Reals.Definition
+
 open import Logic.PropositionalLogic
 open import Logic.PropositionalLogicExamples
 open import Logic.PropositionalAxiomsTautology
diff --git a/Fields/FieldOfFractions/Field.agda b/Fields/FieldOfFractions/Field.agda
index 52cff91..b5b5ec6 100644
--- a/Fields/FieldOfFractions/Field.agda
+++ b/Fields/FieldOfFractions/Field.agda
@@ -24,15 +24,16 @@ open import Fields.FieldOfFractions.Ring I
 fieldOfFractions : Field fieldOfFractionsRing
 Field.allInvertible fieldOfFractions (fst ,, (b , _)) prA = (b ,, (fst , ans)) , need
   where
-    open Setoid S
-    open Equivalence eq
-    need : ((b * fst) * Ring.1R R) ∼ ((fst * b) * Ring.1R R)
-    need = Ring.*WellDefined R (Ring.*Commutative R) reflexive
-    ans : fst ∼ Ring.0R R → False
-    ans pr = prA need'
-      where
-        need' : (fst * Ring.1R R) ∼ (b * Ring.0R R)
-        need' = transitive (Ring.*WellDefined R pr reflexive) (transitive (transitive (Ring.*Commutative R) (Ring.timesZero R)) (symmetric (Ring.timesZero R)))
+    abstract
+      open Setoid S
+      open Equivalence eq
+      need : ((b * fst) * Ring.1R R) ∼ ((fst * b) * Ring.1R R)
+      need = Ring.*WellDefined R (Ring.*Commutative R) reflexive
+      ans : fst ∼ Ring.0R R → False
+      ans pr = prA need'
+        where
+          need' : (fst * Ring.1R R) ∼ (b * Ring.0R R)
+          need' = transitive (Ring.*WellDefined R pr reflexive) (transitive (transitive (Ring.*Commutative R) (Ring.timesZero R)) (symmetric (Ring.timesZero R)))
 Field.nontrivial fieldOfFractions pr = IntegralDomain.nontrivial I (symmetric (transitive (symmetric (Ring.timesZero R)) (transitive (Ring.*Commutative R) (transitive pr (Ring.identIsIdent R)))))
   where
     open Setoid S
diff --git a/Numbers/Rationals/Definition.agda b/Numbers/Rationals/Definition.agda
index 4c62da1..b76fbdc 100644
--- a/Numbers/Rationals/Definition.agda
+++ b/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 ()
diff --git a/Numbers/Reals.agda b/Numbers/Reals.agda
deleted file mode 100644
index 42f15fc..0000000
--- a/Numbers/Reals.agda
+++ /dev/null
@@ -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 = {!!}
diff --git a/Numbers/Reals/Definition.agda b/Numbers/Reals/Definition.agda
new file mode 100644
index 0000000..8633d0c
--- /dev/null
+++ b/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