From 412edaf4c7b5fb219837a60946fddf930caeba63 Mon Sep 17 00:00:00 2001 From: Patrick Stevens Date: Fri, 10 Apr 2020 19:00:57 +0100 Subject: [PATCH] Lots of refactoring towards partially-ordered ring R (#109) --- Everything/Safe.agda | 7 +- Fields/CauchyCompletion/Addition.agda | 7 +- Fields/CauchyCompletion/Approximation.agda | 65 +- Fields/CauchyCompletion/Comparison.agda | 98 +- Fields/CauchyCompletion/Definition.agda | 8 + Fields/CauchyCompletion/Field.agda | 18 +- Fields/CauchyCompletion/Group.agda | 78 +- Fields/CauchyCompletion/Multiplication.agda | 41 +- .../PartiallyOrderedRing.agda | 160 +++ Fields/CauchyCompletion/Ring.agda | 45 +- Fields/CauchyCompletion/Setoid.agda | 40 - Fields/FieldOfFractions/Order.agda | 1134 +++++++++-------- LogicalFormulae.agda | 12 +- Numbers/Rationals/Definition.agda | 9 +- Numbers/Reals/Definition.agda | 12 +- RedBlackTree.agda | 42 - Rings/Orders/Total/Lemmas.agda | 3 + Sequences.agda | 3 + Sets/Cardinality/Infinite/Examples.agda | 11 +- 19 files changed, 1015 insertions(+), 778 deletions(-) create mode 100644 Fields/CauchyCompletion/PartiallyOrderedRing.agda delete mode 100644 RedBlackTree.agda diff --git a/Everything/Safe.agda b/Everything/Safe.agda index 014ed6d..abf4a1b 100644 --- a/Everything/Safe.agda +++ b/Everything/Safe.agda @@ -85,6 +85,7 @@ open import Rings.Divisible.Lemmas open import Rings.Associates.Lemmas open import Rings.InitialRing open import Rings.Homomorphisms.Lemmas +open import Rings.UniqueFactorisationDomains.Definition open import Setoids.Setoids open import Setoids.DirectSum @@ -125,9 +126,6 @@ open import Monoids.Definition open import Semirings.Definition open import Semirings.Solver -open import Fields.CauchyCompletion.Group -open import Fields.CauchyCompletion.Ring - open import Categories.Definition open import Categories.Functor.Definition open import Categories.Functor.Lemmas @@ -149,4 +147,7 @@ open import Modules.PolynomialModule open import Modules.Lemmas open import Modules.DirectSum +open import Fields.CauchyCompletion.Ring +open import Fields.CauchyCompletion.Comparison + module Everything.Safe where diff --git a/Fields/CauchyCompletion/Addition.agda b/Fields/CauchyCompletion/Addition.agda index f03c0ff..d7b25a5 100644 --- a/Fields/CauchyCompletion/Addition.agda +++ b/Fields/CauchyCompletion/Addition.agda @@ -32,9 +32,10 @@ open import Fields.CauchyCompletion.Definition order F open import Rings.Orders.Partial.Lemmas pRing open import Rings.Orders.Total.Lemmas order -lemm : (m : ℕ) (a b : Sequence A) → index (apply _+_ a b) m ≡ (index a m) + (index b m) -lemm zero a b = refl -lemm (succ m) a b = lemm m (Sequence.tail a) (Sequence.tail b) +private + lemm : (m : ℕ) (a b : Sequence A) → index (apply _+_ a b) m ≡ (index a m) + (index b m) + lemm zero a b = refl + lemm (succ m) a b = lemm m (Sequence.tail a) (Sequence.tail b) _+C_ : CauchyCompletion → CauchyCompletion → CauchyCompletion CauchyCompletion.elts (record { elts = a ; converges = convA } +C record { elts = b ; converges = convB }) = apply _+_ a b diff --git a/Fields/CauchyCompletion/Approximation.agda b/Fields/CauchyCompletion/Approximation.agda index acd2801..f7d7f95 100644 --- a/Fields/CauchyCompletion/Approximation.agda +++ b/Fields/CauchyCompletion/Approximation.agda @@ -40,20 +40,26 @@ open import Fields.CauchyCompletion.Comparison order F charNot2 abstract chain : {a b : A} (c : CauchyCompletion) → (a r