From 9b80058157916c793a9a2d3823797482bf0efa14 Mon Sep 17 00:00:00 2001 From: Patrick Stevens Date: Thu, 16 Apr 2020 13:41:51 +0100 Subject: [PATCH] Lots of speedups (#116) --- Everything/Safe.agda | 9 +- Fields/CauchyCompletion/Addition.agda | 31 ++- Fields/CauchyCompletion/Approximation.agda | 4 +- Fields/CauchyCompletion/Archimedean.agda | 28 ++ Fields/CauchyCompletion/Comparison.agda | 47 +++- Fields/CauchyCompletion/Definition.agda | 8 +- Fields/CauchyCompletion/Field.agda | 22 +- Fields/CauchyCompletion/Group.agda | 16 +- Fields/CauchyCompletion/Multiplication.agda | 227 ++++++++-------- .../PartiallyOrderedRing.agda | 247 ++++++++++++------ Fields/CauchyCompletion/Ring.agda | 6 +- Fields/CauchyCompletion/Setoid.agda | 13 +- Fields/FieldOfFractions/Archimedean.agda | 68 +++++ Fields/FieldOfFractions/Group.agda | 1 - Fields/FieldOfFractions/Order.agda | 38 ++- .../Orders/LeastUpperBounds/Definition.agda | 2 +- Fields/Orders/LeastUpperBounds/Examples.agda | 3 +- Fields/Orders/Lemmas.agda | 5 +- Fields/Orders/Limits/Definition.agda | 4 +- Fields/Orders/Limits/Lemmas.agda | 4 +- Fields/Orders/Partial/Definition.agda | 2 +- Fields/Orders/Total/Archimedean.agda | 65 +++++ Fields/Orders/Total/Definition.agda | 2 +- Fields/Orders/Total/Lemmas.agda | 5 +- Groups/Cyclic/Definition.agda | 5 +- Groups/FreeProduct/Addition.agda | 15 +- Groups/Homomorphisms/Definition.agda | 3 + Groups/Homomorphisms/Lemmas.agda | 6 + Groups/Homomorphisms/Lemmas2.agda | 1 - Groups/Orders/Archimedean.agda | 20 ++ Groups/Orders/Partial/Definition.agda | 17 ++ Lists/Definition.agda | 9 +- LogicalFormulae.agda | 4 + Numbers/ClassicalReals/Examples.agda | 25 +- Numbers/ClassicalReals/RealField.agda | 2 +- Numbers/ClassicalReals/RealField/Lemmas.agda | 2 +- Numbers/Integers/Definition.agda | 3 + Numbers/Integers/Order.agda | 2 +- .../Integers/RingStructure/Archimedean.agda | 30 +++ Numbers/Intervals/Arithmetic.agda | 2 +- Numbers/Intervals/Definition.agda | 2 +- Numbers/Naturals/Addition.agda | 1 + Numbers/Naturals/Multiplication.agda | 1 + Numbers/Rationals/Definition.agda | 3 +- Numbers/Rationals/Lemmas.agda | 3 +- Numbers/Reals/Definition.agda | 2 +- Orders/Total/Lemmas.agda | 1 - Rings/Homomorphisms/Lemmas.agda | 1 - Rings/InitialRing.agda | 4 +- Rings/Orders/Partial/Bounded.agda | 2 +- Rings/Orders/Partial/Definition.agda | 6 +- Rings/Orders/Partial/Lemmas.agda | 16 +- Rings/Orders/Total/AbsoluteValue.agda | 217 +++++++++++++++ Rings/Orders/Total/BaseExpansion.agda | 17 +- Rings/Orders/Total/Bounded.agda | 3 +- Rings/Orders/Total/Cauchy.agda | 16 +- Rings/Orders/Total/Definition.agda | 3 +- Rings/Orders/Total/Lemmas.agda | 199 +------------- Semirings/Solver.agda | 5 +- Setoids/Orders/Orders.agda | 19 ++ .../Partial/Definition.agda} | 22 +- Setoids/Orders/Total/Definition.agda | 33 +++ Setoids/Orders/Total/Lemmas.agda | 67 +++++ 63 files changed, 1082 insertions(+), 564 deletions(-) create mode 100644 Fields/CauchyCompletion/Archimedean.agda create mode 100644 Fields/FieldOfFractions/Archimedean.agda create mode 100644 Fields/Orders/Total/Archimedean.agda create mode 100644 Groups/Orders/Archimedean.agda create mode 100644 Groups/Orders/Partial/Definition.agda create mode 100644 Numbers/Integers/RingStructure/Archimedean.agda create mode 100644 Rings/Orders/Total/AbsoluteValue.agda create mode 100644 Setoids/Orders/Orders.agda rename Setoids/{Orders.agda => Orders/Partial/Definition.agda} (57%) create mode 100644 Setoids/Orders/Total/Definition.agda create mode 100644 Setoids/Orders/Total/Lemmas.agda diff --git a/Everything/Safe.agda b/Everything/Safe.agda index 86c8b4d..7887c60 100644 --- a/Everything/Safe.agda +++ b/Everything/Safe.agda @@ -16,6 +16,7 @@ open import Numbers.Modulo.Group open import Numbers.Integers.Integers open import Numbers.Integers.RingStructure.EuclideanDomain +open import Numbers.Integers.RingStructure.Archimedean open import Numbers.ClassicalReals.Examples open import Numbers.ClassicalReals.RealField.Lemmas @@ -52,12 +53,15 @@ open import Groups.LectureNotes.Lecture1 open import Fields.Fields open import Fields.Orders.Partial.Definition open import Fields.Orders.Total.Definition +open import Fields.Orders.Total.Archimedean open import Fields.Orders.LeastUpperBounds.Examples open import Fields.Orders.Lemmas open import Fields.Orders.Limits.Definition open import Fields.FieldOfFractions.Field open import Fields.FieldOfFractions.Lemmas open import Fields.FieldOfFractions.Order +open import Fields.FieldOfFractions.Order +--open import Fields.FieldOfFractions.Archimedean open import Rings.Definition open import Rings.Lemmas @@ -100,7 +104,7 @@ open import Rings.Orders.Total.BaseExpansion open import Setoids.Setoids open import Setoids.DirectSum open import Setoids.Lists -open import Setoids.Orders +open import Setoids.Orders.Total.Lemmas open import Setoids.Functions.Definition open import Setoids.Functions.Extension open import Setoids.Algebra.Lemmas @@ -159,8 +163,7 @@ open import Modules.PolynomialModule open import Modules.Lemmas open import Modules.DirectSum -open import Fields.CauchyCompletion.Ring -open import Fields.CauchyCompletion.Comparison +open import Fields.CauchyCompletion.Archimedean open import Fields.Orders.Limits.Lemmas open import ProjectEuler.Problem1 diff --git a/Fields/CauchyCompletion/Addition.agda b/Fields/CauchyCompletion/Addition.agda index 1e8ca63..b955606 100644 --- a/Fields/CauchyCompletion/Addition.agda +++ b/Fields/CauchyCompletion/Addition.agda @@ -9,7 +9,8 @@ open import Groups.Lemmas open import Fields.Fields open import Sets.EquivalenceRelations open import Sequences -open import Setoids.Orders +open import Setoids.Orders.Partial.Definition +open import Setoids.Orders.Total.Definition open import Functions open import LogicalFormulae open import Numbers.Naturals.Semiring @@ -31,7 +32,9 @@ open import Fields.Lemmas F open import Fields.CauchyCompletion.Definition order F open import Rings.Orders.Partial.Lemmas pRing open import Fields.Orders.Total.Lemmas {F = F} (record { oRing = order }) +open import Rings.Orders.Total.AbsoluteValue order open import Rings.Orders.Total.Lemmas order +open import Rings.Orders.Total.Cauchy order open import Rings.InitialRing R private @@ -39,19 +42,23 @@ private lemm zero a b = refl lemm (succ m) a b = lemm m (Sequence.tail a) (Sequence.tail b) +private + additionConverges : (a b : CauchyCompletion) → cauchy (apply _+_ (CauchyCompletion.elts a) (CauchyCompletion.elts b)) + additionConverges record { elts = a ; converges = convA } record { elts = b ; converges = convB } ε 0