From 4b8f6993d0c628bc22e16af1513b32022b2641b2 Mon Sep 17 00:00:00 2001
From: Patrick Stevens <patrick+github@patrickstevens.co.uk>
Date: Tue, 19 May 2020 07:44:42 +0100
Subject: [PATCH] Tidy up a bit (#127)

---
 Fields/CauchyCompletion/BaseExpansion.agda    |  15 ++-
 .../CauchyCompletion/EquivalentMonotone.agda  |  12 +-
 Fields/CauchyCompletion/Field.agda            |   2 +-
 Fields/CauchyCompletion/NearlyTotalOrder.agda | 117 ++++++++++++++++++
 4 files changed, 134 insertions(+), 12 deletions(-)
 create mode 100644 Fields/CauchyCompletion/NearlyTotalOrder.agda

diff --git a/Fields/CauchyCompletion/BaseExpansion.agda b/Fields/CauchyCompletion/BaseExpansion.agda
index d222bfd..58715c0 100644
--- a/Fields/CauchyCompletion/BaseExpansion.agda
+++ b/Fields/CauchyCompletion/BaseExpansion.agda
@@ -10,8 +10,9 @@ open import Groups.Lemmas
 open import Fields.Fields
 open import Sets.EquivalenceRelations
 open import Sequences
-open import Setoids.Orders
-open import Functions
+open import Setoids.Orders.Partial.Definition
+open import Setoids.Orders.Total.Definition
+open import Functions.Definition
 open import LogicalFormulae
 open import Numbers.Naturals.Semiring
 open import Numbers.Naturals.Order
@@ -37,6 +38,7 @@ open import Fields.Orders.Limits.Lemmas {F = F} (record { oRing = order })
 open import Fields.Lemmas F
 open import Fields.Orders.Lemmas {F = F} record { oRing = order }
 open import Rings.Orders.Total.Lemmas order
+open import Rings.Orders.Total.AbsoluteValue order
 open import Rings.Orders.Partial.Lemmas pRing
 open import Fields.CauchyCompletion.Definition order F
 open import Fields.CauchyCompletion.Setoid order F
@@ -48,6 +50,7 @@ open import Rings.Orders.Partial.Bounded pRing
 open import Rings.Orders.Total.Bounded order
 open import Rings.Orders.Total.Cauchy order
 
+-- TODO this is not necessarily true :( the bounded sequence could oscillate between 1 and -1
 cauchyTimesBoundedIsCauchy : {s : Sequence A} → cauchy s → {t : Sequence A} → Bounded t → cauchy (apply _*_ s t)
 cauchyTimesBoundedIsCauchy {s} cau {t} (K , bounded) e 0<e with allInvertible K (boundNonzero (K , bounded))
 ... | 1/K , prK with cau (1/K * e) (orderRespectsMultiplication (reciprocalPositive K 1/K (boundGreaterThanZero (K , bounded)) (transitive *Commutative prK)) 0<e)
@@ -97,11 +100,11 @@ private
 
   digitExpansionBoundedLemma : {n : ℕ} → .(0<n : 0 <N n) → (seq : Sequence (ℤn n 0<n)) → (m : ℕ) → index (digitExpansionSeq _ seq) m < fromN n
   digitExpansionBoundedLemma {n} 0<n seq zero with Sequence.head seq
-  ... | record { x = x ; xLess = xLess } = fromNPreservesOrder nontrivial {x} {n} ((squash<N xLess))
+  ... | record { x = x ; xLess = xLess } = fromNPreservesOrder (0<1 nontrivial) {x} {n} ((squash<N xLess))
   digitExpansionBoundedLemma 0<n seq (succ m) = digitExpansionBoundedLemma 0<n (Sequence.tail seq) m
 
   digitExpansionBoundedLemma2 : {n : ℕ} → .(0<n : 0 <N n) → (seq : Sequence (ℤn n 0<n)) → (m : ℕ) → inverse (fromN n) < index (digitExpansionSeq 0<n seq) m
-  digitExpansionBoundedLemma2 {n} 0<n seq zero = <WellDefined identLeft (transitive (symmetric +Associative) (transitive (+WellDefined reflexive invRight) identRight)) (orderRespectsAddition {_} {fromN (ℤn.x (Sequence.head seq)) + fromN n} (<WellDefined reflexive (fromNPreserves+ (ℤn.x (Sequence.head seq)) n) (fromNPreservesOrder nontrivial {0} {ℤn.x (Sequence.head seq) +N n} (canAddToOneSideOfInequality' _ (squash<N 0<n)))) (inverse (fromN n)))
+  digitExpansionBoundedLemma2 {n} 0<n seq zero = <WellDefined identLeft (transitive (symmetric +Associative) (transitive (+WellDefined reflexive invRight) identRight)) (orderRespectsAddition {_} {fromN (ℤn.x (Sequence.head seq)) + fromN n} (<WellDefined reflexive (fromNPreserves+ (ℤn.x (Sequence.head seq)) n) (fromNPreservesOrder (0<1 nontrivial) {0} {ℤn.x (Sequence.head seq) +N n} (canAddToOneSideOfInequality' _ (squash<N 0<n)))) (inverse (fromN n)))
   digitExpansionBoundedLemma2 0<n seq (succ m) = digitExpansionBoundedLemma2 0<n (Sequence.tail seq) m
 
   digitExpansionBounded : {n : ℕ} → .(0<n : 0 <N n) → (seq : Sequence (ℤn n 0<n)) → Bounded (digitExpansionSeq 0<n seq)
@@ -110,11 +113,11 @@ private
 private
   1/nPositive : (n : ℕ) → 0R < underlying (allInvertible (fromN (succ n)) (charNotN n))
   1/nPositive n with allInvertible (fromN (succ n)) (charNotN n)
-  ... | a , b = reciprocalPositive (fromN (succ n)) a (fromNPreservesOrder nontrivial (succIsPositive n)) (transitive *Commutative b)
+  ... | a , b = reciprocalPositive (fromN (succ n)) a (fromNPreservesOrder (0<1 nontrivial) (succIsPositive n)) (transitive *Commutative b)
 
   1/n<1 : (n : ℕ) → (0 <N n) → underlying (allInvertible (fromN (succ n)) (charNotN n)) < 1R
   1/n<1 n 1<n with allInvertible (fromN (succ n)) (charNotN n)
-  ... | a , b = reciprocal<1 (fromN (succ n)) a (<WellDefined identRight reflexive (fromNPreservesOrder nontrivial {1} {succ n} (succPreservesInequality 1<n))) (transitive *Commutative b)
+  ... | a , b = reciprocal<1 (fromN (succ n)) a (<WellDefined identRight reflexive (fromNPreservesOrder (0<1 nontrivial) {1} {succ n} (succPreservesInequality 1<n))) (transitive *Commutative b)
 
 -- Construct the real that is the given base-n expansion between 0 and 1.
 ofBaseExpansion : {n : ℕ} → .(1<n : 1 <N n) → (fromN n ∼ 0R → False) → Sequence (ℤn n (0<n 1<n)) → CauchyCompletion
diff --git a/Fields/CauchyCompletion/EquivalentMonotone.agda b/Fields/CauchyCompletion/EquivalentMonotone.agda
index 1ceeadc..3624810 100644
--- a/Fields/CauchyCompletion/EquivalentMonotone.agda
+++ b/Fields/CauchyCompletion/EquivalentMonotone.agda
@@ -4,24 +4,26 @@ open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
 open import Setoids.Setoids
 open import Rings.Definition
 open import Rings.Lemmas
-open import Rings.Orders.Definition
+open import Rings.Orders.Partial.Definition
+open import Rings.Orders.Total.Definition
 open import Groups.Definition
 open import Groups.Groups
 open import Fields.Fields
 open import Sets.EquivalenceRelations
 open import Sequences
-open import Setoids.Orders
-open import Functions
+open import Setoids.Orders.Partial.Definition
+open import Setoids.Orders.Total.Definition
+open import Functions.Definition
 open import LogicalFormulae
 open import Numbers.Naturals.Naturals
 
-module Fields.CauchyCompletion.EquivalentMonotone {m n o : _} {A : Set m} {S : Setoid {m} {n} A} {_+_ : A → A → A} {_*_ : A → A → A} {_<_ : Rel {m} {o} A} {pOrder : SetoidPartialOrder S _<_} {tOrder : SetoidTotalOrder {_<_ = _<_} pOrder} {R : Ring S _+_ _*_} (order : OrderedRing R tOrder) (F : Field R) (charNot2 : Setoid._∼_ S ((Ring.1R R) + (Ring.1R R)) (Ring.0R R) → False) where
+module Fields.CauchyCompletion.EquivalentMonotone {m n o : _} {A : Set m} {S : Setoid {m} {n} A} {_+_ : A → A → A} {_*_ : A → A → A} {_<_ : Rel {m} {o} A} {pOrder : SetoidPartialOrder S _<_} {tOrder : SetoidTotalOrder {_<_ = _<_} pOrder} {R : Ring S _+_ _*_} (order : TotallyOrderedRing R tOrder) (F : Field R) (charNot2 : Setoid._∼_ S ((Ring.1R R) + (Ring.1R R)) (Ring.0R R) → False) where
 
 open Setoid S
 open SetoidTotalOrder tOrder
 open SetoidPartialOrder pOrder
 open Equivalence eq
-open OrderedRing order
+open TotallyOrderedRing order
 open Field F
 open Group (Ring.additiveGroup R)
 open Ring R
diff --git a/Fields/CauchyCompletion/Field.agda b/Fields/CauchyCompletion/Field.agda
index 68df635..a810d6b 100644
--- a/Fields/CauchyCompletion/Field.agda
+++ b/Fields/CauchyCompletion/Field.agda
@@ -13,7 +13,7 @@ open import Sets.EquivalenceRelations
 open import Sequences
 open import Setoids.Orders.Partial.Definition
 open import Setoids.Orders.Total.Definition
-open import Functions
+open import Functions.Definition
 open import LogicalFormulae
 open import Numbers.Naturals.Semiring
 open import Numbers.Naturals.Order
diff --git a/Fields/CauchyCompletion/NearlyTotalOrder.agda b/Fields/CauchyCompletion/NearlyTotalOrder.agda
new file mode 100644
index 0000000..43c6a81
--- /dev/null
+++ b/Fields/CauchyCompletion/NearlyTotalOrder.agda
@@ -0,0 +1,117 @@
+{-# OPTIONS --safe --warning=error --without-K --guardedness #-}
+
+open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
+open import Setoids.Setoids
+open import Rings.Definition
+open import Rings.Orders.Partial.Definition
+open import Rings.Orders.Total.Definition
+open import Groups.Definition
+open import Groups.Lemmas
+open import Fields.Fields
+open import Sets.EquivalenceRelations
+open import Sequences
+open import Setoids.Orders.Partial.Definition
+open import Setoids.Orders.Total.Definition
+open import Functions.Definition
+open import LogicalFormulae
+open import Numbers.Naturals.Semiring
+open import Numbers.Naturals.Order
+open import Numbers.Naturals.Order.Lemmas
+open import Semirings.Definition
+
+module Fields.CauchyCompletion.NearlyTotalOrder {m n o : _} {A : Set m} {S : Setoid {m} {n} A} {_+_ : A → A → A} {_*_ : A → A → A} {_<_ : Rel {m} {o} A} {pOrder : SetoidPartialOrder S _<_} {R : Ring S _+_ _*_} {pRing : PartiallyOrderedRing R pOrder} (order : TotallyOrderedRing pRing) (F : Field R) where
+
+open Setoid S
+open SetoidTotalOrder (TotallyOrderedRing.total order)
+open SetoidPartialOrder pOrder
+open Equivalence eq
+open PartiallyOrderedRing pRing
+open Ring R
+open Group additiveGroup
+open Field F
+open import Fields.Orders.Lemmas {F = F} {pRing} (record { oRing = order })
+open import Setoids.Orders.Partial.Sequences pOrder
+
+open import Rings.InitialRing R
+open import Rings.Orders.Partial.Lemmas pRing
+open import Rings.Orders.Total.Lemmas order
+open import Rings.Orders.Total.Cauchy order
+open import Rings.Orders.Total.AbsoluteValue order
+open import Fields.Lemmas F
+open import Fields.CauchyCompletion.Definition order F
+open import Fields.CauchyCompletion.Setoid order F
+open import Fields.CauchyCompletion.Group order F
+open import Fields.CauchyCompletion.Addition order F
+open import Fields.CauchyCompletion.Approximation order F
+open import Fields.CauchyCompletion.Comparison order F
+open import Fields.CauchyCompletion.PartiallyOrderedRing order F
+open import Fields.Orders.Total.Lemmas {F = F} (record { oRing = order })
+
+makeIncreasingLemma : (a : A) (s : Sequence A) → Sequence A
+Sequence.head (makeIncreasingLemma a s) with totality a (Sequence.head s)
+... | inl (inl x) = Sequence.head s
+... | inl (inr x) = a
+... | inr x = a
+Sequence.tail (makeIncreasingLemma a s) = makeIncreasingLemma (Sequence.head (makeIncreasingLemma a s)) (Sequence.tail s)
+
+makeIncreasingLemmaIsIncreasing : (a : A) (s : Sequence A) → WeaklyIncreasing (makeIncreasingLemma a s)
+makeIncreasingLemmaIsIncreasing a s zero with totality a (Sequence.head s)
+makeIncreasingLemmaIsIncreasing a s zero | inl (inl x) with totality (Sequence.head s) (Sequence.head (Sequence.tail s))
+makeIncreasingLemmaIsIncreasing a s zero | inl (inl x) | inl (inl y) = inl y
+makeIncreasingLemmaIsIncreasing a s zero | inl (inl x) | inl (inr y) = inr reflexive
+makeIncreasingLemmaIsIncreasing a s zero | inl (inl x) | inr y = inr reflexive
+makeIncreasingLemmaIsIncreasing a s zero | inl (inr x) with totality a (Sequence.head (Sequence.tail s))
+... | inl (inl y) = inl y
+... | inl (inr y) = inr reflexive
+... | inr y = inr reflexive
+makeIncreasingLemmaIsIncreasing a s zero | inr x with totality a (Sequence.head (Sequence.tail s))
+... | inl (inl y) = inl y
+... | inl (inr y) = inr reflexive
+... | inr y = inr reflexive
+makeIncreasingLemmaIsIncreasing a s (succ m) = makeIncreasingLemmaIsIncreasing (Sequence.head (makeIncreasingLemma a s)) (Sequence.tail s) m
+
+makeIncreasing : Sequence A → Sequence A
+Sequence.head (makeIncreasing x) = Sequence.head x
+Sequence.tail (makeIncreasing x) = makeIncreasingLemma (Sequence.head x) (Sequence.tail x)
+
+makeIncreasingIsIncreasing : (a : Sequence A) → WeaklyIncreasing (makeIncreasing a)
+makeIncreasingIsIncreasing a zero with totality (Sequence.head a) (Sequence.head (Sequence.tail a))
+... | inl (inl x) = inl x
+... | inl (inr x) = inr reflexive
+... | inr x = inr reflexive
+makeIncreasingIsIncreasing a (succ m) = makeIncreasingLemmaIsIncreasing _ _ m
+
+approximateIncreasingSeqRaw : CauchyCompletion → Sequence A
+approximateIncreasingSeqRaw a = funcToSequence f
+  where
+    f : ℕ → A
+    f n with allInvertible (fromN (succ n)) λ n=0 → irreflexive (<WellDefined reflexive n=0 (fromNPreservesOrder (0<1 nontrivial) (succIsPositive n)))
+    ... | 1/n , prN = underlying (approximateBelow a 1/n (reciprocalPositive' (fromN (succ n)) 1/n (fromNPreservesOrder (0<1 nontrivial) (succIsPositive n)) prN))
+
+approximateIncreasingSeq : CauchyCompletion → Sequence A
+approximateIncreasingSeq a = makeIncreasing (approximateIncreasingSeqRaw a)
+
+approximateIncreasingConverges : (a : CauchyCompletion) → cauchy (approximateIncreasingSeq a)
+approximateIncreasingConverges a e 0<e = {!!}
+
+approximateIncreasingIncreases : (a : CauchyCompletion) → WeaklyIncreasing (approximateIncreasingSeq a)
+approximateIncreasingIncreases a = makeIncreasingIsIncreasing (approximateIncreasingSeqRaw a)
+
+approximateIncreasing : CauchyCompletion → CauchyCompletion
+approximateIncreasing a = record { elts = approximateIncreasingSeq a ; converges = approximateIncreasingConverges a }
+
+approximateIncreasingEqual : (a : CauchyCompletion) → Setoid._∼_ cauchyCompletionSetoid (approximateIncreasing a) a
+approximateIncreasingEqual a e 0<e = {!!}
+
+decideSign : (a : CauchyCompletion) → (Setoid._∼_ cauchyCompletionSetoid a (injection 0R) → False) → (a <Cr 0R) || (0R r<C a)
+decideSign a a!=0 = {!!}
+  where
+
+private
+  lemma : (a b : CauchyCompletion) → Setoid._∼_ cauchyCompletionSetoid ((b +C (-C a)) +C a) b
+  lemma a b = Equivalence.transitive (Setoid.eq cauchyCompletionSetoid) {record { converges = CauchyCompletion.converges ((b +C (-C a)) +C a) }} {record { converges = CauchyCompletion.converges (b +C ((-C a) +C a)) }} {record { converges = CauchyCompletion.converges b }} (Group.+Associative' CGroup {record { converges = CauchyCompletion.converges b }} {record { converges = CauchyCompletion.converges (-C a) }} { record { converges = CauchyCompletion.converges a }}) (Equivalence.transitive (Setoid.eq cauchyCompletionSetoid) {record {converges = CauchyCompletion.converges (b +C ((-C a) +C a))}} {record { converges = CauchyCompletion.converges (b +C (injection 0R))}} {record {converges = CauchyCompletion.converges b}} (Group.+WellDefinedRight CGroup {record {converges = CauchyCompletion.converges b}} {record {converges = CauchyCompletion.converges ((-C a) +C a)}} {record { converges = CauchyCompletion.converges (injection 0R)}} (Group.invLeft CGroup {record { converges = CauchyCompletion.converges a }})) (Group.identRight CGroup {record { converges = CauchyCompletion.converges b }}))
+
+nearlyTotal : (a b : CauchyCompletion) → (Setoid._∼_ cauchyCompletionSetoid a b → False) → (a <C b) || (b <C a)
+nearlyTotal a b a!=b with decideSign (b +C (-C a)) λ bad → a!=b (Equivalence.symmetric (Setoid.eq cauchyCompletionSetoid) {record { converges = CauchyCompletion.converges b }} {record { converges = CauchyCompletion.converges a  }} (transferToRight CGroup {record { converges = CauchyCompletion.converges b }} {record { converges = CauchyCompletion.converges a }} bad))
+... | inl x = inr (<CWellDefined (lemma a b) (Group.identLeft CGroup {record { converges = CauchyCompletion.converges a }}) (PartiallyOrderedRing.orderRespectsAddition CpOrderedRing (<CRelaxR x) a))
+... | inr x = inl (<CWellDefined (Group.identLeft CGroup {record { converges = CauchyCompletion.converges a }}) (lemma a b) (PartiallyOrderedRing.orderRespectsAddition CpOrderedRing (<CRelaxL x) a))