patrick/agdaproofs
1
0
Fork 0
mirror of https://github.com/Smaug123/agdaproofs synced 2025-10-08 05:18:40 +00:00
Code Issues Packages Projects Releases Wiki Activity

Minor perf improvements? (#60)

Browse Source
This commit is contained in:
Patrick Stevens
2019-11-02 08:57:15 +00:00
committed by GitHub
parent a66080b8ae
commit 55995ea801
7 changed files with 695 additions and 676 deletions
Download Patch File Download Diff File Expand all files Collapse all files

300
Fields/CauchyCompletion/Approximation.agda
View File

@@ -37,160 +37,162 @@ open import Fields.CauchyCompletion.Addition order F charNot2
open import Fields.CauchyCompletion.Setoid order F charNot2
open import Fields.CauchyCompletion.Comparison order F charNot2
chain : {a b : A} (c : CauchyCompletion) → (a r<C c) → (c <Cr b) → a < b
chain {a} {b} c (betweenAC , (0<betweenAC ,, (Nac , prAC))) (betweenCB , (0<betweenCB ,, (Nb , prBC))) = SetoidPartialOrder.transitive pOrder (SetoidPartialOrder.transitive pOrder (<WellDefined identLeft (Equivalence.reflexive eq) (orderRespectsAddition 0<betweenAC a)) (<WellDefined groupIsAbelian (Equivalence.reflexive eq) (SetoidPartialOrder.transitive pOrder (prAC (succ Nac +N Nb) (le Nb (applyEquality succ (Semiring.commutative ℕSemiring Nb Nac)))) (<WellDefined identLeft (Equivalence.reflexive eq) (orderRespectsAddition 0<betweenCB (index (Sequence.tail (CauchyCompletion.elts c)) (Nac +N Nb))))))) (prBC (succ Nac +N Nb) (le Nac refl))
abstract
approxLemma : (a : CauchyCompletion) (e e/2 : A) → (0G < e) → (e/2 + e/2 ∼ e) → (m N : ℕ) → abs ((index (CauchyCompletion.elts a) m) + inverse (index (CauchyCompletion.elts a) N)) < e/2 → (e/2 + index (CauchyCompletion.elts a) m) < (index (CauchyCompletion.elts a) N + e)
approxLemma a e e/2 0<e prE/2 m N ans with SetoidTotalOrder.totality tOrder 0R ((index (CauchyCompletion.elts a) m) + inverse (index (CauchyCompletion.elts a) N))
approxLemma a e e/2 0<e prE/2 m N ans | inl (inl x) with <WellDefined (Equivalence.transitive eq (Equivalence.transitive eq (Equivalence.symmetric eq +Associative) (+WellDefined (Equivalence.reflexive eq) (invLeft))) identRight) groupIsAbelian (orderRespectsAddition ans (index (CauchyCompletion.elts a) N))
... | bl = <WellDefined groupIsAbelian (Equivalence.transitive eq (Equivalence.symmetric eq +Associative) (+WellDefined (Equivalence.reflexive eq) prE/2)) (orderRespectsAddition bl e/2)
approxLemma a e e/2 0<e prE/2 m N ans | inl (inr x) with <WellDefined (Equivalence.transitive eq (Equivalence.transitive eq (Equivalence.symmetric eq +Associative) (+WellDefined (Equivalence.reflexive eq) (invLeft))) identRight) (identLeft) (orderRespectsAddition x (index (CauchyCompletion.elts a) N))
... | bl = <WellDefined groupIsAbelian (Equivalence.reflexive eq) (ringAddInequalities bl (halfLess e/2 e 0<e prE/2))
approxLemma a e e/2 0<e prE/2 m N ans | inr x with transferToRight additiveGroup (Equivalence.symmetric eq x)
... | bl = <WellDefined (+WellDefined (Equivalence.reflexive eq) (Equivalence.symmetric eq bl)) groupIsAbelian (orderRespectsAddition (halfLess e/2 e 0<e prE/2) (index (CauchyCompletion.elts a) N))
chain : {a b : A} (c : CauchyCompletion) → (a r<C c) → (c <Cr b) → a < b
chain {a} {b} c (betweenAC , (0<betweenAC ,, (Nac , prAC))) (betweenCB , (0<betweenCB ,, (Nb , prBC))) = SetoidPartialOrder.transitive pOrder (SetoidPartialOrder.transitive pOrder (<WellDefined identLeft (Equivalence.reflexive eq) (orderRespectsAddition 0<betweenAC a)) (<WellDefined groupIsAbelian (Equivalence.reflexive eq) (SetoidPartialOrder.transitive pOrder (prAC (succ Nac +N Nb) (le Nb (applyEquality succ (Semiring.commutative ℕSemiring Nb Nac)))) (<WellDefined identLeft (Equivalence.reflexive eq) (orderRespectsAddition 0<betweenCB (index (Sequence.tail (CauchyCompletion.elts c)) (Nac +N Nb))))))) (prBC (succ Nac +N Nb) (le Nac refl))
approximateAboveCrude : (a : CauchyCompletion) → Sg A (λ b → (a <Cr b))
approximateAboveCrude a with CauchyCompletion.converges a 1R (0<1 (charNot2ImpliesNontrivial charNot2))
... | N , conv = ((((index (CauchyCompletion.elts a) (succ N)) + 1R) + 1R) + 1R) , (1R , (0<1 (charNot2ImpliesNontrivial charNot2) ,, (N , ans)))
where
ans : (m : ℕ) → (N <N m) → (1R + index (CauchyCompletion.elts a) m) < (((index (CauchyCompletion.elts a) (succ N) + 1R) + 1R) + 1R)
ans m N<m with conv {m} {succ N} N<m (le 0 refl)
... | bl with totality 0G (index (CauchyCompletion.elts a) m + inverse (index (CauchyCompletion.elts a) (succ N)))
ans m N<m | bl | inl (inl 0<am-aN) with <WellDefined (Equivalence.transitive eq (Equivalence.transitive eq (Equivalence.symmetric eq +Associative) (+WellDefined (Equivalence.reflexive eq) (invLeft))) identRight) (Equivalence.reflexive eq) (orderRespectsAddition bl (index (CauchyCompletion.elts a) (succ N)))
... | am<1+an = <WellDefined (Equivalence.transitive eq (+WellDefined (Equivalence.reflexive eq) identLeft) groupIsAbelian) (Equivalence.transitive eq (+WellDefined groupIsAbelian (Equivalence.reflexive eq)) +Associative) (ringAddInequalities am<1+an (orderRespectsAddition (0<1 (charNot2ImpliesNontrivial charNot2)) 1R))
ans m N<m | bl | inl (inr am-aN<0) with <WellDefined (Equivalence.transitive eq (Equivalence.transitive eq (Equivalence.symmetric eq +Associative) (+WellDefined (Equivalence.reflexive eq) invLeft)) identRight) identLeft (orderRespectsAddition am-aN<0 (index (CauchyCompletion.elts a) (succ N)))
... | am<aN = <WellDefined groupIsAbelian (Equivalence.reflexive eq) (orderRespectsAddition (SetoidPartialOrder.transitive pOrder am<aN (<WellDefined (Equivalence.reflexive eq) (+Associative) (<WellDefined identLeft groupIsAbelian (orderRespectsAddition (<WellDefined identLeft (Equivalence.reflexive eq) (ringAddInequalities (0<1 (charNot2ImpliesNontrivial charNot2)) (0<1 (charNot2ImpliesNontrivial charNot2)))) (index (CauchyCompletion.elts a) (succ N)))))) 1R)
ans m N<m | bl | inr 0=am-aN = <WellDefined (Equivalence.transitive eq (+WellDefined identLeft (Equivalence.reflexive eq)) identLeft) (Equivalence.transitive eq groupIsAbelian (Equivalence.transitive eq (+WellDefined (Equivalence.transitive eq groupIsAbelian (+WellDefined (transferToRight additiveGroup (Equivalence.symmetric eq 0=am-aN)) (Equivalence.reflexive eq))) (Equivalence.reflexive eq)) +Associative)) (orderRespectsAddition (ringAddInequalities (0<1 (charNot2ImpliesNontrivial charNot2)) (0<1 (charNot2ImpliesNontrivial charNot2))) (1R + (index (CauchyCompletion.elts a) m)))
approxLemma : (a : CauchyCompletion) (e e/2 : A) → (0G < e) → (e/2 + e/2 ∼ e) → (m N : ℕ) → abs ((index (CauchyCompletion.elts a) m) + inverse (index (CauchyCompletion.elts a) N)) < e/2 → (e/2 + index (CauchyCompletion.elts a) m) < (index (CauchyCompletion.elts a) N + e)
approxLemma a e e/2 0<e prE/2 m N ans with SetoidTotalOrder.totality tOrder 0R ((index (CauchyCompletion.elts a) m) + inverse (index (CauchyCompletion.elts a) N))
approxLemma a e e/2 0<e prE/2 m N ans | inl (inl x) with <WellDefined (Equivalence.transitive eq (Equivalence.transitive eq (Equivalence.symmetric eq +Associative) (+WellDefined (Equivalence.reflexive eq) (invLeft))) identRight) groupIsAbelian (orderRespectsAddition ans (index (CauchyCompletion.elts a) N))
... | bl = <WellDefined groupIsAbelian (Equivalence.transitive eq (Equivalence.symmetric eq +Associative) (+WellDefined (Equivalence.reflexive eq) prE/2)) (orderRespectsAddition bl e/2)
approxLemma a e e/2 0<e prE/2 m N ans | inl (inr x) with <WellDefined (Equivalence.transitive eq (Equivalence.transitive eq (Equivalence.symmetric eq +Associative) (+WellDefined (Equivalence.reflexive eq) (invLeft))) identRight) (identLeft) (orderRespectsAddition x (index (CauchyCompletion.elts a) N))
... | bl = <WellDefined groupIsAbelian (Equivalence.reflexive eq) (ringAddInequalities bl (halfLess e/2 e 0<e prE/2))
approxLemma a e e/2 0<e prE/2 m N ans | inr x with transferToRight additiveGroup (Equivalence.symmetric eq x)
... | bl = <WellDefined (+WellDefined (Equivalence.reflexive eq) (Equivalence.symmetric eq bl)) groupIsAbelian (orderRespectsAddition (halfLess e/2 e 0<e prE/2) (index (CauchyCompletion.elts a) N))
rationalApproximatelyAbove : (a : CauchyCompletion) → (e : A) → (0G < e) → A
rationalApproximatelyAbove a e 0<e with halve charNot2 e
... | e/2 , prE/2 with halvePositive e/2 (<WellDefined (Equivalence.reflexive eq) (Equivalence.symmetric eq prE/2) 0<e)
... | 0<e/2 with halve charNot2 e/2
... | e/4 , prE/4 with halvePositive e/4 (<WellDefined (Equivalence.reflexive eq) (Equivalence.symmetric eq prE/4) 0<e/2)
... | 0<e/4 with CauchyCompletion.converges a e/4 0<e/4
... | N , cauchyBeyondN = index (CauchyCompletion.elts a) (succ N) + e/2
approximateAboveCrude : (a : CauchyCompletion) → Sg A (λ b → (a <Cr b))
approximateAboveCrude a with CauchyCompletion.converges a 1R (0<1 (charNot2ImpliesNontrivial charNot2))
... | N , conv = ((((index (CauchyCompletion.elts a) (succ N)) + 1R) + 1R) + 1R) , (1R , (0<1 (charNot2ImpliesNontrivial charNot2) ,, (N , ans)))
where
ans : (m : ℕ) → (N <N m) → (1R + index (CauchyCompletion.elts a) m) < (((index (CauchyCompletion.elts a) (succ N) + 1R) + 1R) + 1R)
ans m N<m with conv {m} {succ N} N<m (le 0 refl)
... | bl with totality 0G (index (CauchyCompletion.elts a) m + inverse (index (CauchyCompletion.elts a) (succ N)))
ans m N<m | bl | inl (inl 0<am-aN) with <WellDefined (Equivalence.transitive eq (Equivalence.transitive eq (Equivalence.symmetric eq +Associative) (+WellDefined (Equivalence.reflexive eq) (invLeft))) identRight) (Equivalence.reflexive eq) (orderRespectsAddition bl (index (CauchyCompletion.elts a) (succ N)))
... | am<1+an = <WellDefined (Equivalence.transitive eq (+WellDefined (Equivalence.reflexive eq) identLeft) groupIsAbelian) (Equivalence.transitive eq (+WellDefined groupIsAbelian (Equivalence.reflexive eq)) +Associative) (ringAddInequalities am<1+an (orderRespectsAddition (0<1 (charNot2ImpliesNontrivial charNot2)) 1R))
ans m N<m | bl | inl (inr am-aN<0) with <WellDefined (Equivalence.transitive eq (Equivalence.transitive eq (Equivalence.symmetric eq +Associative) (+WellDefined (Equivalence.reflexive eq) invLeft)) identRight) identLeft (orderRespectsAddition am-aN<0 (index (CauchyCompletion.elts a) (succ N)))
... | am<aN = <WellDefined groupIsAbelian (Equivalence.reflexive eq) (orderRespectsAddition (SetoidPartialOrder.transitive pOrder am<aN (<WellDefined (Equivalence.reflexive eq) (+Associative) (<WellDefined identLeft groupIsAbelian (orderRespectsAddition (<WellDefined identLeft (Equivalence.reflexive eq) (ringAddInequalities (0<1 (charNot2ImpliesNontrivial charNot2)) (0<1 (charNot2ImpliesNontrivial charNot2)))) (index (CauchyCompletion.elts a) (succ N)))))) 1R)
ans m N<m | bl | inr 0=am-aN = <WellDefined (Equivalence.transitive eq (+WellDefined identLeft (Equivalence.reflexive eq)) identLeft) (Equivalence.transitive eq groupIsAbelian (Equivalence.transitive eq (+WellDefined (Equivalence.transitive eq groupIsAbelian (+WellDefined (transferToRight additiveGroup (Equivalence.symmetric eq 0=am-aN)) (Equivalence.reflexive eq))) (Equivalence.reflexive eq)) +Associative)) (orderRespectsAddition (ringAddInequalities (0<1 (charNot2ImpliesNontrivial charNot2)) (0<1 (charNot2ImpliesNontrivial charNot2))) (1R + (index (CauchyCompletion.elts a) m)))
rationalApproximatelyAboveIsAbove : (a : CauchyCompletion) (e : A) → (0<e : 0G < e) → a <Cr (rationalApproximatelyAbove a e 0<e)
rationalApproximatelyAboveIsAbove a e 0<e with halve charNot2 e
... | e/2 , prE/2 with halvePositive e/2 (<WellDefined (Equivalence.reflexive eq) (Equivalence.symmetric eq prE/2) 0<e)
... | 0<e/2 with halve charNot2 e/2
... | e/4 , prE/4 with halvePositive e/4 (<WellDefined (Equivalence.reflexive eq) (Equivalence.symmetric eq prE/4) 0<e/2)
... | 0<e/4 with CauchyCompletion.converges a e/4 0<e/4
... | N , cauchyBeyondN with halve charNot2 e/4
... | e/8 , prE/8 with halvePositive e/8 (<WellDefined (Equivalence.reflexive eq) (Equivalence.symmetric eq prE/8) 0<e/4)
... | 0<e/8 with CauchyCompletion.converges a e/8 0<e/8
... | N2 , cauchyBeyondN2 = e/8 , (0<e/8 ,, ((N +N N2) , ans2))
where
ans2 : (m : ℕ) → N +N N2 <N m → (e/8 + index (CauchyCompletion.elts a) m) < (index (CauchyCompletion.elts a) (succ N) + e/2) -- TODO not sure this is actually true
ans2 m <m with cauchyBeyondN {m} {succ N} (inequalityShrinkLeft <m) (le 0 refl)
... | absam-aN<e/4 with totality 0R ((index (CauchyCompletion.elts a) m) + inverse (index (CauchyCompletion.elts a) (succ N)))
ans2 m <m | am-aN<e/4 | inl (inl 0<am-aN) = SetoidPartialOrder.transitive pOrder (<WellDefined groupIsAbelian (Equivalence.transitive eq groupIsAbelian +Associative) (orderRespectsAddition (<WellDefined (Equivalence.transitive eq (Equivalence.transitive eq (Equivalence.symmetric eq +Associative) (+WellDefined (Equivalence.reflexive eq) invLeft)) identRight) (Equivalence.reflexive eq) (orderRespectsAddition am-aN<e/4 (index (CauchyCompletion.elts a) (succ N)))) e/8)) (<WellDefined (Equivalence.reflexive eq) groupIsAbelian (orderRespectsAddition (<WellDefined (Equivalence.reflexive eq) prE/4 (orderRespectsAddition (halfLess e/8 e/4 0<e/4 prE/8) e/4)) (index (CauchyCompletion.elts a) (succ N))))
ans2 m <m | -[am-aN]<e/4 | inl (inr am-aN<0) with <WellDefined (Equivalence.transitive eq +Associative (Equivalence.transitive eq (+WellDefined invLeft (Equivalence.reflexive eq)) identLeft)) (Equivalence.reflexive eq) (orderRespectsAddition (<WellDefined (Equivalence.reflexive eq) (invTwice additiveGroup _) (ringSwapNegatives' -[am-aN]<e/4)) (e/4 + e/8))
... | e/8<am-aN+e/4+e/8 = SetoidPartialOrder.transitive pOrder (orderRespectsAddition e/8<am-aN+e/4+e/8 (index (CauchyCompletion.elts a) m)) (<WellDefined (Equivalence.reflexive eq) groupIsAbelian (ringAddInequalities (<WellDefined (Equivalence.reflexive eq) identLeft (ringAddInequalities am-aN<0 (<WellDefined groupIsAbelian prE/4 (orderRespectsAddition (halfLess e/8 e/4 0<e/4 prE/8) e/4)))) am<aN))
where
am<aN : (index (CauchyCompletion.elts a) m) < (index (CauchyCompletion.elts a) (succ N))
am<aN = <WellDefined (Equivalence.transitive eq (Equivalence.transitive eq (Equivalence.symmetric eq +Associative) (+WellDefined (Equivalence.reflexive eq) groupIsAbelian)) (Equivalence.transitive eq (+WellDefined (Equivalence.reflexive eq) invRight) identRight)) identLeft (orderRespectsAddition am-aN<0 (index (CauchyCompletion.elts a) (succ N)))
ans2 m <m | absam-aN<e/4 | inr 0=am-aN = <WellDefined (Equivalence.reflexive eq) (Equivalence.transitive eq groupIsAbelian (+WellDefined (transferToRight additiveGroup (Equivalence.symmetric eq 0=am-aN)) (Equivalence.reflexive eq))) (orderRespectsAddition {b = e/2} (SetoidPartialOrder.transitive pOrder (halfLess e/8 e/4 0<e/4 prE/8) (halfLess e/4 e/2 0<e/2 prE/4)) (index (CauchyCompletion.elts a) m))
rationalApproximatelyAbove : (a : CauchyCompletion) → (e : A) → (0G < e) → A
rationalApproximatelyAbove a e 0<e with halve charNot2 e
... | e/2 , prE/2 with halvePositive e/2 (<WellDefined (Equivalence.reflexive eq) (Equivalence.symmetric eq prE/2) 0<e)
... | 0<e/2 with halve charNot2 e/2
... | e/4 , prE/4 with halvePositive e/4 (<WellDefined (Equivalence.reflexive eq) (Equivalence.symmetric eq prE/4) 0<e/2)
... | 0<e/4 with CauchyCompletion.converges a e/4 0<e/4
... | N , cauchyBeyondN = index (CauchyCompletion.elts a) (succ N) + e/2
rationalApproximatelyAboveIsNear : (a : CauchyCompletion) (e : A) → (0<e : 0G < e) → (injection (rationalApproximatelyAbove a e 0<e) +C (-C a)) <C (injection e)
rationalApproximatelyAboveIsNear a e 0<e with halve charNot2 e
... | e/2 , prE/2 with halvePositive e/2 (<WellDefined (Equivalence.reflexive eq) (Equivalence.symmetric eq prE/2) 0<e)
... | 0<e/2 with halve charNot2 e/2
... | e/4 , prE/4 with halvePositive e/4 (<WellDefined (Equivalence.reflexive eq) (Equivalence.symmetric eq prE/4) 0<e/2)
... | 0<e/4 with CauchyCompletion.converges a e/4 0<e/4
... | N , cauchyBeyondN with halve charNot2 e/4
... | e/8 , prE/8 with halvePositive e/8 (<WellDefined (Equivalence.reflexive eq) (Equivalence.symmetric eq prE/8) 0<e/4)
... | 0<e/8 with CauchyCompletion.converges a e/8 0<e/8
... | N8 , cauchyBeyondN8 with halve charNot2 e/8
... | e/16 , prE/16 with halvePositive e/16 (<WellDefined (Equivalence.reflexive eq) (Equivalence.symmetric eq prE/16) 0<e/8)
... | 0<e/16 = ((e/2 + e/4) + e/8) , ((e/8 , (0<e/8 ,, ((N +N N8) , ans))) ,, (e/16 , (0<e/16 ,, (0 , t'))))
where
t' : (m : ℕ) → (0 <N m) → (((e/2 + e/4) + e/8) + e/16) < index (constSequence e) m
t' m 0<m rewrite indexAndConst e m = <WellDefined (Equivalence.reflexive eq) prE/2 (<WellDefined (Equivalence.reflexive eq) (+WellDefined (Equivalence.reflexive eq) prE/4) (<WellDefined +Associative (Equivalence.symmetric eq +Associative) (<WellDefined groupIsAbelian groupIsAbelian (orderRespectsAddition (<WellDefined (Equivalence.reflexive eq) prE/8 (<WellDefined groupIsAbelian groupIsAbelian (orderRespectsAddition (halfLess e/16 e/8 0<e/8 prE/16) e/8))) (e/2 + e/4)))))
ans : (m : ℕ) → (N +N N8) <N m → (e/8 + index (apply _+_ (constSequence (index (CauchyCompletion.elts a) (succ N) + e/2)) (map inverse (CauchyCompletion.elts a))) m) < ((e/2 + e/4) + e/8)
ans m N<m rewrite indexAndApply (constSequence (index (CauchyCompletion.elts a) (succ N) + e/2)) (map inverse (CauchyCompletion.elts a)) _+_ {m} | indexAndConst (index (CauchyCompletion.elts a) (succ N) + e/2) m | equalityCommutative (mapAndIndex (CauchyCompletion.elts a) inverse m) = <WellDefined groupIsAbelian (+WellDefined groupIsAbelian (Equivalence.reflexive eq)) (orderRespectsAddition (<WellDefined (Equivalence.transitive eq groupIsAbelian (Equivalence.reflexive eq)) (Equivalence.reflexive eq) q) e/8)
where
am = index (CauchyCompletion.elts a) m
aN = index (CauchyCompletion.elts a) (succ N)
t : abs (am + inverse aN) < e/4
t = cauchyBeyondN {m} {succ N} (inequalityShrinkLeft N<m) (le 0 refl)
r : ((inverse am) + aN) < e/4
r with t
... | f with totality 0G (am + inverse aN)
r | am-aN<e/4 | inl (inl 0<am-aN) = SetoidPartialOrder.transitive pOrder (<WellDefined (Equivalence.transitive eq (invContravariant additiveGroup) (Equivalence.transitive eq groupIsAbelian (+WellDefined (Equivalence.reflexive eq) (invTwice additiveGroup _)))) (Equivalence.reflexive eq) (lemm2' _ 0<am-aN)) 0<e/4
r | f | inl (inr x) = <WellDefined (Equivalence.transitive eq (invContravariant additiveGroup) (Equivalence.transitive eq groupIsAbelian (+WellDefined (Equivalence.reflexive eq) (invTwice additiveGroup _)))) (Equivalence.reflexive eq) f
r | am-aN<e/4 | inr 0=am-aN = <WellDefined (Equivalence.transitive eq (Equivalence.symmetric eq 0=am-aN) (Equivalence.transitive eq (Equivalence.transitive eq (Equivalence.transitive eq (Equivalence.transitive eq (Equivalence.symmetric eq (invIdentity additiveGroup)) (inverseWellDefined additiveGroup 0=am-aN)) (inverseWellDefined additiveGroup groupIsAbelian)) (invContravariant additiveGroup)) (+WellDefined (Equivalence.reflexive eq) (invTwice additiveGroup _)))) (Equivalence.reflexive eq) am-aN<e/4
q : ((inverse (index (CauchyCompletion.elts a) m)) + (index (CauchyCompletion.elts a) (succ N) + e/2)) < (e/4 + e/2)
q = <WellDefined (Equivalence.symmetric eq +Associative) (Equivalence.reflexive eq) (orderRespectsAddition r e/2)
rationalApproximatelyAboveIsAbove : (a : CauchyCompletion) (e : A) → (0<e : 0G < e) → a <Cr (rationalApproximatelyAbove a e 0<e)
rationalApproximatelyAboveIsAbove a e 0<e with halve charNot2 e
... | e/2 , prE/2 with halvePositive e/2 (<WellDefined (Equivalence.reflexive eq) (Equivalence.symmetric eq prE/2) 0<e)
... | 0<e/2 with halve charNot2 e/2
... | e/4 , prE/4 with halvePositive e/4 (<WellDefined (Equivalence.reflexive eq) (Equivalence.symmetric eq prE/4) 0<e/2)
... | 0<e/4 with CauchyCompletion.converges a e/4 0<e/4
... | N , cauchyBeyondN with halve charNot2 e/4
... | e/8 , prE/8 with halvePositive e/8 (<WellDefined (Equivalence.reflexive eq) (Equivalence.symmetric eq prE/8) 0<e/4)
... | 0<e/8 with CauchyCompletion.converges a e/8 0<e/8
... | N2 , cauchyBeyondN2 = e/8 , (0<e/8 ,, ((N +N N2) , ans2))
where
ans2 : (m : ℕ) → N +N N2 <N m → (e/8 + index (CauchyCompletion.elts a) m) < (index (CauchyCompletion.elts a) (succ N) + e/2)
ans2 m <m with cauchyBeyondN {m} {succ N} (inequalityShrinkLeft <m) (le 0 refl)
... | absam-aN<e/4 with totality 0R ((index (CauchyCompletion.elts a) m) + inverse (index (CauchyCompletion.elts a) (succ N)))
ans2 m <m | am-aN<e/4 | inl (inl 0<am-aN) = SetoidPartialOrder.transitive pOrder (<WellDefined groupIsAbelian (Equivalence.transitive eq groupIsAbelian +Associative) (orderRespectsAddition (<WellDefined (Equivalence.transitive eq (Equivalence.transitive eq (Equivalence.symmetric eq +Associative) (+WellDefined (Equivalence.reflexive eq) invLeft)) identRight) (Equivalence.reflexive eq) (orderRespectsAddition am-aN<e/4 (index (CauchyCompletion.elts a) (succ N)))) e/8)) (<WellDefined (Equivalence.reflexive eq) groupIsAbelian (orderRespectsAddition (<WellDefined (Equivalence.reflexive eq) prE/4 (orderRespectsAddition (halfLess e/8 e/4 0<e/4 prE/8) e/4)) (index (CauchyCompletion.elts a) (succ N))))
ans2 m <m | -[am-aN]<e/4 | inl (inr am-aN<0) with <WellDefined (Equivalence.transitive eq +Associative (Equivalence.transitive eq (+WellDefined invLeft (Equivalence.reflexive eq)) identLeft)) (Equivalence.reflexive eq) (orderRespectsAddition (<WellDefined (Equivalence.reflexive eq) (invTwice additiveGroup _) (ringSwapNegatives' -[am-aN]<e/4)) (e/4 + e/8))
... | e/8<am-aN+e/4+e/8 = SetoidPartialOrder.transitive pOrder (orderRespectsAddition e/8<am-aN+e/4+e/8 (index (CauchyCompletion.elts a) m)) (<WellDefined (Equivalence.reflexive eq) groupIsAbelian (ringAddInequalities (<WellDefined (Equivalence.reflexive eq) identLeft (ringAddInequalities am-aN<0 (<WellDefined groupIsAbelian prE/4 (orderRespectsAddition (halfLess e/8 e/4 0<e/4 prE/8) e/4)))) am<aN))
where
am<aN : (index (CauchyCompletion.elts a) m) < (index (CauchyCompletion.elts a) (succ N))
am<aN = <WellDefined (Equivalence.transitive eq (Equivalence.transitive eq (Equivalence.symmetric eq +Associative) (+WellDefined (Equivalence.reflexive eq) groupIsAbelian)) (Equivalence.transitive eq (+WellDefined (Equivalence.reflexive eq) invRight) identRight)) identLeft (orderRespectsAddition am-aN<0 (index (CauchyCompletion.elts a) (succ N)))
ans2 m <m | absam-aN<e/4 | inr 0=am-aN = <WellDefined (Equivalence.reflexive eq) (Equivalence.transitive eq groupIsAbelian (+WellDefined (transferToRight additiveGroup (Equivalence.symmetric eq 0=am-aN)) (Equivalence.reflexive eq))) (orderRespectsAddition {b = e/2} (SetoidPartialOrder.transitive pOrder (halfLess e/8 e/4 0<e/4 prE/8) (halfLess e/4 e/2 0<e/2 prE/4)) (index (CauchyCompletion.elts a) m))
approximateAbove : (a : CauchyCompletion) → (ε : A) → (0G < ε) → Sg A (λ b → (a <Cr b) && (injection b +C (-C a)) <C (injection ε))
approximateAbove a e 0<e = rationalApproximatelyAbove a e 0<e , (rationalApproximatelyAboveIsAbove a e 0<e ,, rationalApproximatelyAboveIsNear a e 0<e)
rationalApproximatelyAboveIsNear : (a : CauchyCompletion) (e : A) → (0<e : 0G < e) → (injection (rationalApproximatelyAbove a e 0<e) +C (-C a)) <C (injection e)
rationalApproximatelyAboveIsNear a e 0<e with halve charNot2 e
... | e/2 , prE/2 with halvePositive e/2 (<WellDefined (Equivalence.reflexive eq) (Equivalence.symmetric eq prE/2) 0<e)
... | 0<e/2 with halve charNot2 e/2
... | e/4 , prE/4 with halvePositive e/4 (<WellDefined (Equivalence.reflexive eq) (Equivalence.symmetric eq prE/4) 0<e/2)
... | 0<e/4 with CauchyCompletion.converges a e/4 0<e/4
... | N , cauchyBeyondN with halve charNot2 e/4
... | e/8 , prE/8 with halvePositive e/8 (<WellDefined (Equivalence.reflexive eq) (Equivalence.symmetric eq prE/8) 0<e/4)
... | 0<e/8 with CauchyCompletion.converges a e/8 0<e/8
... | N8 , cauchyBeyondN8 with halve charNot2 e/8
... | e/16 , prE/16 with halvePositive e/16 (<WellDefined (Equivalence.reflexive eq) (Equivalence.symmetric eq prE/16) 0<e/8)
... | 0<e/16 = ((e/2 + e/4) + e/8) , ((e/8 , (0<e/8 ,, ((N +N N8) , ans))) ,, (e/16 , (0<e/16 ,, (0 , t'))))
where
t' : (m : ℕ) → (0 <N m) → (((e/2 + e/4) + e/8) + e/16) < index (constSequence e) m
t' m 0<m rewrite indexAndConst e m = <WellDefined (Equivalence.reflexive eq) prE/2 (<WellDefined (Equivalence.reflexive eq) (+WellDefined (Equivalence.reflexive eq) prE/4) (<WellDefined +Associative (Equivalence.symmetric eq +Associative) (<WellDefined groupIsAbelian groupIsAbelian (orderRespectsAddition (<WellDefined (Equivalence.reflexive eq) prE/8 (<WellDefined groupIsAbelian groupIsAbelian (orderRespectsAddition (halfLess e/16 e/8 0<e/8 prE/16) e/8))) (e/2 + e/4)))))
ans : (m : ℕ) → (N +N N8) <N m → (e/8 + index (apply _+_ (constSequence (index (CauchyCompletion.elts a) (succ N) + e/2)) (map inverse (CauchyCompletion.elts a))) m) < ((e/2 + e/4) + e/8)
ans m N<m rewrite indexAndApply (constSequence (index (CauchyCompletion.elts a) (succ N) + e/2)) (map inverse (CauchyCompletion.elts a)) _+_ {m} | indexAndConst (index (CauchyCompletion.elts a) (succ N) + e/2) m | equalityCommutative (mapAndIndex (CauchyCompletion.elts a) inverse m) = <WellDefined groupIsAbelian (+WellDefined groupIsAbelian (Equivalence.reflexive eq)) (orderRespectsAddition (<WellDefined (Equivalence.transitive eq groupIsAbelian (Equivalence.reflexive eq)) (Equivalence.reflexive eq) q) e/8)
where
am = index (CauchyCompletion.elts a) m
aN = index (CauchyCompletion.elts a) (succ N)
t : abs (am + inverse aN) < e/4
t = cauchyBeyondN {m} {succ N} (inequalityShrinkLeft N<m) (le 0 refl)
r : ((inverse am) + aN) < e/4
r with t
... | f with totality 0G (am + inverse aN)
r | am-aN<e/4 | inl (inl 0<am-aN) = SetoidPartialOrder.transitive pOrder (<WellDefined (Equivalence.transitive eq (invContravariant additiveGroup) (Equivalence.transitive eq groupIsAbelian (+WellDefined (Equivalence.reflexive eq) (invTwice additiveGroup _)))) (Equivalence.reflexive eq) (lemm2' _ 0<am-aN)) 0<e/4
r | f | inl (inr x) = <WellDefined (Equivalence.transitive eq (invContravariant additiveGroup) (Equivalence.transitive eq groupIsAbelian (+WellDefined (Equivalence.reflexive eq) (invTwice additiveGroup _)))) (Equivalence.reflexive eq) f
r | am-aN<e/4 | inr 0=am-aN = <WellDefined (Equivalence.transitive eq (Equivalence.symmetric eq 0=am-aN) (Equivalence.transitive eq (Equivalence.transitive eq (Equivalence.transitive eq (Equivalence.transitive eq (Equivalence.symmetric eq (invIdentity additiveGroup)) (inverseWellDefined additiveGroup 0=am-aN)) (inverseWellDefined additiveGroup groupIsAbelian)) (invContravariant additiveGroup)) (+WellDefined (Equivalence.reflexive eq) (invTwice additiveGroup _)))) (Equivalence.reflexive eq) am-aN<e/4
q : ((inverse (index (CauchyCompletion.elts a) m)) + (index (CauchyCompletion.elts a) (succ N) + e/2)) < (e/4 + e/2)
q = <WellDefined (Equivalence.symmetric eq +Associative) (Equivalence.reflexive eq) (orderRespectsAddition r e/2)
approximateBelow : (a : CauchyCompletion) → (ε : A) → (0G < ε) → Sg A (λ b → (b r<C a) && (a +C (-C injection b)) <C (injection ε))
approximateBelow a e 0<e with approximateAbove (-C a) e 0<e
... | x , ((deltaXAnd-A , (0<deltaXA ,, (NdeltaXA , prDeltaXA))) ,, (rationalNear , ((bound , (0<bound ,, (N , prBound))) ,, (bound2 , (0<bound2 ,, (N2 , prBound2)))))) = inverse x , ((deltaXAnd-A , (0<deltaXA ,, (NdeltaXA , λ m N<m → <WellDefined (Equivalence.transitive eq groupIsAbelian (Equivalence.transitive eq (Equivalence.symmetric eq +Associative) (+WellDefined (Equivalence.reflexive eq) (Equivalence.transitive eq groupIsAbelian (Equivalence.transitive eq (Equivalence.symmetric eq +Associative) (Equivalence.transitive eq (+WellDefined (Equivalence.reflexive eq) (cancel {m} (CauchyCompletion.elts a))) identRight)))))) (Equivalence.transitive eq +Associative (Equivalence.transitive eq (+WellDefined invRight (Equivalence.reflexive eq)) identLeft)) (orderRespectsAddition (prDeltaXA m N<m) (inverse x + (index (CauchyCompletion.elts a) m)))))) ,, (rationalNear , ((bound , (0<bound ,, (N , pr1))) ,, (bound2 , (0<bound2 ,, (N2 , prBound2))))))
where
cancel : {m : ℕ} (a : Sequence A) → (index (map inverse a) m) + (index a m) ∼ 0G
cancel {m} a rewrite equalityCommutative (mapAndIndex a inverse m) = invLeft
pr1 : (m : ℕ) → (N <N m) → (bound + index (apply _+_ (CauchyCompletion.elts a) (map inverse (constSequence (inverse x)))) m) < rationalNear
pr1 m N<m with prBound m N<m
... | bl rewrite indexAndApply (CauchyCompletion.elts a) (map inverse (constSequence (inverse x))) _+_ {m} | equalityCommutative (mapAndIndex (constSequence (inverse x)) inverse m) | indexAndConst x m | indexAndApply (constSequence x) (map inverse (map inverse (CauchyCompletion.elts a))) _+_ {m} | indexAndConst x m | equalityCommutative (mapAndIndex (map inverse (CauchyCompletion.elts a)) inverse m) | equalityCommutative (mapAndIndex (CauchyCompletion.elts a) inverse m) | indexAndConst (inverse x) m = <WellDefined (+WellDefined (Equivalence.reflexive eq) (Equivalence.transitive eq groupIsAbelian (+WellDefined (invTwice additiveGroup _) (Equivalence.symmetric eq (invTwice additiveGroup _))))) (Equivalence.reflexive eq) bl
approximateAbove : (a : CauchyCompletion) → (ε : A) → (0G < ε) → Sg A (λ b → (a <Cr b) && (injection b +C (-C a)) <C (injection ε))
approximateAbove a e 0<e = rationalApproximatelyAbove a e 0<e , (rationalApproximatelyAboveIsAbove a e 0<e ,, rationalApproximatelyAboveIsNear a e 0<e)
boundModulus : (a : CauchyCompletion) → Sg A (λ b → Sg ℕ (λ N → (m : ℕ) → (N <N m) → (abs (index (CauchyCompletion.elts a) m)) < b))
boundModulus a with approximateBelow a 1R (0<1 (charNot2ImpliesNontrivial charNot2))
... | below , (below<a ,, a-below<e) with approximateAbove a 1R (0<1 (charNot2ImpliesNontrivial charNot2))
... | above , (a<above ,, above-a<e) with SetoidTotalOrder.totality tOrder 0R below
boundModulus a | below , (below<a ,, a-below<e) | above , (a<above ,, above-a<e) | inl (inl 0<below) with SetoidTotalOrder.totality tOrder 0R above
boundModulus a | below , ((belowBound , (0<belowBound ,, (Nbelow , prBelow))) ,, a-below<e) | above , ((bound , (0<bound ,, (N , ans))) ,, above-a<e) | inl (inl 0<below) | inl (inl 0<above) = above , ((N +N Nbelow) , λ m N<m → SetoidPartialOrder.transitive pOrder (res m N<m) (ans m (inequalityShrinkLeft N<m)))
where
res : (m : ℕ) → ((N +N Nbelow) <N m) → (abs (index (CauchyCompletion.elts a) m)) < (bound + index (CauchyCompletion.elts a) m)
res m N<m with SetoidTotalOrder.totality tOrder 0R (index (CauchyCompletion.elts a) m)
res m N<m | inl (inl _) = <WellDefined identLeft (Equivalence.reflexive eq) (orderRespectsAddition 0<bound (index (CauchyCompletion.elts a) m))
res m N<m | inl (inr am<0) = exFalso (irreflexive (SetoidPartialOrder.transitive pOrder 0<below (SetoidPartialOrder.transitive pOrder (SetoidPartialOrder.transitive pOrder (<WellDefined identLeft groupIsAbelian (orderRespectsAddition 0<belowBound below)) (prBelow m (inequalityShrinkRight N<m))) am<0)))
res m N<m | inr 0=am = <WellDefined 0=am (Equivalence.transitive eq (Equivalence.symmetric eq identRight) (+WellDefined (Equivalence.reflexive eq) 0=am)) 0<bound
boundModulus a | below , (below<a ,, a-below<e) | above , (a<above ,, above-a<e) | inl (inl 0<below) | inl (inr above<0) = exFalso (irreflexive (SetoidPartialOrder.transitive pOrder 0<below (SetoidPartialOrder.transitive pOrder (chain a below<a a<above) above<0)))
boundModulus a | below , (below<a ,, a-below<e) | above , (a<above ,, above-a<e) | inl (inl 0<below) | inr 0=above = exFalso (irreflexive (SetoidPartialOrder.transitive pOrder 0<below (<WellDefined (Equivalence.reflexive eq) (Equivalence.symmetric eq 0=above) (chain a below<a a<above))))
boundModulus a | below , (below<a ,, a-below<e) | above , (a<above ,, above-a<e) | inl (inr below<0) with SetoidTotalOrder.totality tOrder 0R above
boundModulus a | below , (below<a ,, a-below<e) | above , (a<above ,, above-a<e) | inl (inr below<0) | inl (inl 0<above) with SetoidTotalOrder.totality tOrder (inverse below) above
boundModulus a | below , ((boundBelow , (0<boundBelow ,, (N , prBoundBelow))) ,, a-below<e) | above , ((boundAbove , (0<boundAbove ,, (Nabove , prBoundAbove))) ,, above-a<e) | inl (inr below<0) | inl (inl 0<above) | inl (inl -bel<ab) = above , ((N +N Nabove) , ans)
where
ans : (m : ℕ) → (N +N Nabove <N m) → abs (index (CauchyCompletion.elts a) m) < above
ans m N<m with SetoidTotalOrder.totality tOrder 0G (index (CauchyCompletion.elts a) m)
ans m N<m | inl (inl 0<am) = SetoidPartialOrder.transitive pOrder (<WellDefined identLeft (Equivalence.reflexive eq) (orderRespectsAddition 0<boundAbove (index (CauchyCompletion.elts a) m))) (prBoundAbove m (inequalityShrinkRight N<m))
ans m N<m | inl (inr am<0) = SetoidPartialOrder.transitive pOrder (ringSwapNegatives' (prBoundBelow m (inequalityShrinkLeft N<m))) (SetoidPartialOrder.transitive pOrder (ringSwapNegatives' (<WellDefined identLeft groupIsAbelian (orderRespectsAddition 0<boundBelow below))) -bel<ab)
ans m N<m | inr 0=am = <WellDefined 0=am (Equivalence.reflexive eq) 0<above
boundModulus a | below , ((boundBelow , (0<boundBelow ,, (N , prBoundBelow))) ,, a-below<e) | above , ((boundAbove , (0<boundAbove ,, (Nabove , prBoundAbove))) ,, above-a<e) | inl (inr below<0) | inl (inl 0<above) | inl (inr ab<-bel) = inverse below , ((N +N Nabove) , ans)
where
ans : (m : ℕ) → (N +N Nabove <N m) → abs (index (CauchyCompletion.elts a) m) < (inverse below)
ans m N<m with SetoidTotalOrder.totality tOrder 0G (index (CauchyCompletion.elts a) m)
ans m N<m | inl (inl 0<am) = SetoidPartialOrder.transitive pOrder (SetoidPartialOrder.transitive pOrder (<WellDefined identLeft (Equivalence.reflexive eq) (orderRespectsAddition 0<boundAbove (index (CauchyCompletion.elts a) m))) (prBoundAbove m (inequalityShrinkRight N<m))) ab<-bel
ans m N<m | inl (inr am<0) = ringSwapNegatives' (SetoidPartialOrder.transitive pOrder (<WellDefined identLeft groupIsAbelian (orderRespectsAddition 0<boundBelow below)) (prBoundBelow m (inequalityShrinkLeft N<m)))
ans m N<m | inr 0=am = <WellDefined 0=am (Equivalence.reflexive eq) (lemm2 below below<0)
boundModulus a | below , ((boundBelow , (0<boundBelow ,, (N , prBoundBelow))) ,, a-below<e) | above , ((boundAbove , (0<boundAbove ,, (Nabove , prBoundAbove))) ,, above-a<e) | inl (inr below<0) | inl (inl 0<above) | inr -bel=ab = above , ((N +N Nabove) , ans)
where
ans : (m : ℕ) → (N +N Nabove <N m) → abs (index (CauchyCompletion.elts a) m) < above
ans m N<m with SetoidTotalOrder.totality tOrder 0G (index (CauchyCompletion.elts a) m)
ans m N<m | inl (inl 0<am) = SetoidPartialOrder.transitive pOrder (<WellDefined identLeft (Equivalence.reflexive eq) (orderRespectsAddition 0<boundAbove (index (CauchyCompletion.elts a) m))) (prBoundAbove m (inequalityShrinkRight N<m))
ans m N<m | inl (inr am<0) = <WellDefined (Equivalence.reflexive eq) (-bel=ab) (ringSwapNegatives' (SetoidPartialOrder.transitive pOrder (<WellDefined identLeft groupIsAbelian (orderRespectsAddition 0<boundBelow below)) (prBoundBelow m (inequalityShrinkLeft N<m))))
ans m N<m | inr 0=am = <WellDefined 0=am (Equivalence.reflexive eq) 0<above
boundModulus a | below , ((boundBelow , (0<boundBelow ,, (N , prBoundBelow))) ,, a-below<e) | above , ((boundAbove , (0<boundAbove ,, (Nabove , prBoundAbove))) ,, above-a<e) | inl (inr below<0) | inl (inr above<0) = inverse below , ((N +N Nabove) , ans)
where
ans : (m : ℕ) → ((N +N Nabove) <N m) → abs (index (CauchyCompletion.elts a) m) < inverse below
ans m N<m with SetoidTotalOrder.totality tOrder 0R (index (CauchyCompletion.elts a) m)
ans m N<m | inl (inl 0<am) = exFalso (irreflexive {0G} (SetoidPartialOrder.transitive pOrder 0<am (SetoidPartialOrder.transitive pOrder (SetoidPartialOrder.transitive pOrder (<WellDefined identLeft (Equivalence.reflexive eq) (orderRespectsAddition 0<boundAbove (index (CauchyCompletion.elts a) m))) (prBoundAbove m (inequalityShrinkRight N<m))) above<0)))
ans m N<m | inl (inr am<0) = ringSwapNegatives' (SetoidPartialOrder.transitive pOrder (<WellDefined identLeft groupIsAbelian (orderRespectsAddition 0<boundBelow below)) (prBoundBelow m (inequalityShrinkLeft N<m)))
ans m N<m | inr 0=am = exFalso (irreflexive {0G} (<WellDefined (Equivalence.symmetric eq 0=am) (Equivalence.reflexive eq) (SetoidPartialOrder.transitive pOrder (SetoidPartialOrder.transitive pOrder (<WellDefined identLeft (Equivalence.reflexive eq) (orderRespectsAddition 0<boundAbove (index (CauchyCompletion.elts a) m))) (prBoundAbove m (inequalityShrinkRight N<m))) above<0)))
boundModulus a | below , ((boundBelow , (0<boundBelow ,, (N , prBoundBelow))) ,, a-below<e) | above , ((boundAbove , (0<boundAbove ,, (Nabove , prBoundAbove))) ,, above-a<e) | inl (inr below<0) | inr 0=above = inverse below , ((N +N Nabove) , ans)
where
ans : (m : ℕ) → ((N +N Nabove) <N m) → abs (index (CauchyCompletion.elts a) m) < inverse below
ans m N<m with SetoidTotalOrder.totality tOrder 0R (index (CauchyCompletion.elts a) m)
ans m N<m | inl (inl 0<am) = exFalso (irreflexive {0G} (<WellDefined (Equivalence.reflexive eq) (Equivalence.symmetric eq 0=above) (SetoidPartialOrder.transitive pOrder 0<am (SetoidPartialOrder.transitive pOrder (<WellDefined identLeft (Equivalence.reflexive eq) (orderRespectsAddition 0<boundAbove (index (CauchyCompletion.elts a) m))) (prBoundAbove m (inequalityShrinkRight N<m))))))
ans m N<m | inl (inr am<0) = ringSwapNegatives' (SetoidPartialOrder.transitive pOrder (<WellDefined identLeft groupIsAbelian (orderRespectsAddition 0<boundBelow below)) (prBoundBelow m (inequalityShrinkLeft N<m)))
ans m N<m | inr 0=am = <WellDefined 0=am (Equivalence.reflexive eq) (lemm2 _ below<0)
boundModulus a | below , ((boundBelow , ((boundBelowDiff ,, (Nb , ansBelow)))) ,, a-below<e) | above , ((bound , (0<bound ,, (N , ans))) ,, above-a<e) | inr 0=below = above , ((N +N Nb) , λ m N<m → SetoidPartialOrder.transitive pOrder (res m N<m) (ans m (inequalityShrinkLeft N<m)))
where
res : (m : ℕ) → (N +N Nb) <N m → (abs (index (CauchyCompletion.elts a) m)) < (bound + index (CauchyCompletion.elts a) m)
res m N<m with SetoidTotalOrder.totality tOrder 0R (index (CauchyCompletion.elts a) m)
res m N<m | inl (inl 0<am) = <WellDefined identLeft (Equivalence.reflexive eq) (orderRespectsAddition 0<bound (index (CauchyCompletion.elts a) m))
res m N<m | inl (inr am<0) = exFalso (irreflexive (<WellDefined (Equivalence.symmetric eq 0=below) (Equivalence.reflexive eq) (SetoidPartialOrder.transitive pOrder (SetoidPartialOrder.transitive pOrder (<WellDefined identLeft groupIsAbelian (orderRespectsAddition boundBelowDiff below)) (ansBelow m (inequalityShrinkRight N<m))) am<0)))
res m N<m | inr 0=am = <WellDefined 0=am (Equivalence.transitive eq (Equivalence.symmetric eq identRight) (+WellDefined (Equivalence.reflexive eq) 0=am)) 0<bound
approximateBelow : (a : CauchyCompletion) → (ε : A) → (0G < ε) → Sg A (λ b → (b r<C a) && (a +C (-C injection b)) <C (injection ε))
approximateBelow a e 0<e with approximateAbove (-C a) e 0<e
... | x , ((deltaXAnd-A , (0<deltaXA ,, (NdeltaXA , prDeltaXA))) ,, (rationalNear , ((bound , (0<bound ,, (N , prBound))) ,, (bound2 , (0<bound2 ,, (N2 , prBound2)))))) = inverse x , ((deltaXAnd-A , (0<deltaXA ,, (NdeltaXA , λ m N<m → <WellDefined (Equivalence.transitive eq groupIsAbelian (Equivalence.transitive eq (Equivalence.symmetric eq +Associative) (+WellDefined (Equivalence.reflexive eq) (Equivalence.transitive eq groupIsAbelian (Equivalence.transitive eq (Equivalence.symmetric eq +Associative) (Equivalence.transitive eq (+WellDefined (Equivalence.reflexive eq) (cancel {m} (CauchyCompletion.elts a))) identRight)))))) (Equivalence.transitive eq +Associative (Equivalence.transitive eq (+WellDefined invRight (Equivalence.reflexive eq)) identLeft)) (orderRespectsAddition (prDeltaXA m N<m) (inverse x + (index (CauchyCompletion.elts a) m)))))) ,, (rationalNear , ((bound , (0<bound ,, (N , pr1))) ,, (bound2 , (0<bound2 ,, (N2 , prBound2))))))
where
cancel : {m : ℕ} (a : Sequence A) → (index (map inverse a) m) + (index a m) ∼ 0G
cancel {m} a rewrite equalityCommutative (mapAndIndex a inverse m) = invLeft
pr1 : (m : ℕ) → (N <N m) → (bound + index (apply _+_ (CauchyCompletion.elts a) (map inverse (constSequence (inverse x)))) m) < rationalNear
pr1 m N<m with prBound m N<m
... | bl rewrite indexAndApply (CauchyCompletion.elts a) (map inverse (constSequence (inverse x))) _+_ {m} | equalityCommutative (mapAndIndex (constSequence (inverse x)) inverse m) | indexAndConst x m | indexAndApply (constSequence x) (map inverse (map inverse (CauchyCompletion.elts a))) _+_ {m} | indexAndConst x m | equalityCommutative (mapAndIndex (map inverse (CauchyCompletion.elts a)) inverse m) | equalityCommutative (mapAndIndex (CauchyCompletion.elts a) inverse m) | indexAndConst (inverse x) m = <WellDefined (+WellDefined (Equivalence.reflexive eq) (Equivalence.transitive eq groupIsAbelian (+WellDefined (invTwice additiveGroup _) (Equivalence.symmetric eq (invTwice additiveGroup _))))) (Equivalence.reflexive eq) bl
boundModulus : (a : CauchyCompletion) → Sg A (λ b → Sg ℕ (λ N → (m : ℕ) → (N <N m) → (abs (index (CauchyCompletion.elts a) m)) < b))
boundModulus a with approximateBelow a 1R (0<1 (charNot2ImpliesNontrivial charNot2))
... | below , (below<a ,, a-below<e) with approximateAbove a 1R (0<1 (charNot2ImpliesNontrivial charNot2))
... | above , (a<above ,, above-a<e) with SetoidTotalOrder.totality tOrder 0R below
boundModulus a | below , (below<a ,, a-below<e) | above , (a<above ,, above-a<e) | inl (inl 0<below) with SetoidTotalOrder.totality tOrder 0R above
boundModulus a | below , ((belowBound , (0<belowBound ,, (Nbelow , prBelow))) ,, a-below<e) | above , ((bound , (0<bound ,, (N , ans))) ,, above-a<e) | inl (inl 0<below) | inl (inl 0<above) = above , ((N +N Nbelow) , λ m N<m → SetoidPartialOrder.transitive pOrder (res m N<m) (ans m (inequalityShrinkLeft N<m)))
where
res : (m : ℕ) → ((N +N Nbelow) <N m) → (abs (index (CauchyCompletion.elts a) m)) < (bound + index (CauchyCompletion.elts a) m)
res m N<m with SetoidTotalOrder.totality tOrder 0R (index (CauchyCompletion.elts a) m)
res m N<m | inl (inl _) = <WellDefined identLeft (Equivalence.reflexive eq) (orderRespectsAddition 0<bound (index (CauchyCompletion.elts a) m))
res m N<m | inl (inr am<0) = exFalso (irreflexive (SetoidPartialOrder.transitive pOrder 0<below (SetoidPartialOrder.transitive pOrder (SetoidPartialOrder.transitive pOrder (<WellDefined identLeft groupIsAbelian (orderRespectsAddition 0<belowBound below)) (prBelow m (inequalityShrinkRight N<m))) am<0)))
res m N<m | inr 0=am = <WellDefined 0=am (Equivalence.transitive eq (Equivalence.symmetric eq identRight) (+WellDefined (Equivalence.reflexive eq) 0=am)) 0<bound
boundModulus a | below , (below<a ,, a-below<e) | above , (a<above ,, above-a<e) | inl (inl 0<below) | inl (inr above<0) = exFalso (irreflexive (SetoidPartialOrder.transitive pOrder 0<below (SetoidPartialOrder.transitive pOrder (chain a below<a a<above) above<0)))
boundModulus a | below , (below<a ,, a-below<e) | above , (a<above ,, above-a<e) | inl (inl 0<below) | inr 0=above = exFalso (irreflexive (SetoidPartialOrder.transitive pOrder 0<below (<WellDefined (Equivalence.reflexive eq) (Equivalence.symmetric eq 0=above) (chain a below<a a<above))))
boundModulus a | below , (below<a ,, a-below<e) | above , (a<above ,, above-a<e) | inl (inr below<0) with SetoidTotalOrder.totality tOrder 0R above
boundModulus a | below , (below<a ,, a-below<e) | above , (a<above ,, above-a<e) | inl (inr below<0) | inl (inl 0<above) with SetoidTotalOrder.totality tOrder (inverse below) above
boundModulus a | below , ((boundBelow , (0<boundBelow ,, (N , prBoundBelow))) ,, a-below<e) | above , ((boundAbove , (0<boundAbove ,, (Nabove , prBoundAbove))) ,, above-a<e) | inl (inr below<0) | inl (inl 0<above) | inl (inl -bel<ab) = above , ((N +N Nabove) , ans)
where
ans : (m : ℕ) → (N +N Nabove <N m) → abs (index (CauchyCompletion.elts a) m) < above
ans m N<m with SetoidTotalOrder.totality tOrder 0G (index (CauchyCompletion.elts a) m)
ans m N<m | inl (inl 0<am) = SetoidPartialOrder.transitive pOrder (<WellDefined identLeft (Equivalence.reflexive eq) (orderRespectsAddition 0<boundAbove (index (CauchyCompletion.elts a) m))) (prBoundAbove m (inequalityShrinkRight N<m))
ans m N<m | inl (inr am<0) = SetoidPartialOrder.transitive pOrder (ringSwapNegatives' (prBoundBelow m (inequalityShrinkLeft N<m))) (SetoidPartialOrder.transitive pOrder (ringSwapNegatives' (<WellDefined identLeft groupIsAbelian (orderRespectsAddition 0<boundBelow below))) -bel<ab)
ans m N<m | inr 0=am = <WellDefined 0=am (Equivalence.reflexive eq) 0<above
boundModulus a | below , ((boundBelow , (0<boundBelow ,, (N , prBoundBelow))) ,, a-below<e) | above , ((boundAbove , (0<boundAbove ,, (Nabove , prBoundAbove))) ,, above-a<e) | inl (inr below<0) | inl (inl 0<above) | inl (inr ab<-bel) = inverse below , ((N +N Nabove) , ans)
where
ans : (m : ℕ) → (N +N Nabove <N m) → abs (index (CauchyCompletion.elts a) m) < (inverse below)
ans m N<m with SetoidTotalOrder.totality tOrder 0G (index (CauchyCompletion.elts a) m)
ans m N<m | inl (inl 0<am) = SetoidPartialOrder.transitive pOrder (SetoidPartialOrder.transitive pOrder (<WellDefined identLeft (Equivalence.reflexive eq) (orderRespectsAddition 0<boundAbove (index (CauchyCompletion.elts a) m))) (prBoundAbove m (inequalityShrinkRight N<m))) ab<-bel
ans m N<m | inl (inr am<0) = ringSwapNegatives' (SetoidPartialOrder.transitive pOrder (<WellDefined identLeft groupIsAbelian (orderRespectsAddition 0<boundBelow below)) (prBoundBelow m (inequalityShrinkLeft N<m)))
ans m N<m | inr 0=am = <WellDefined 0=am (Equivalence.reflexive eq) (lemm2 below below<0)
boundModulus a | below , ((boundBelow , (0<boundBelow ,, (N , prBoundBelow))) ,, a-below<e) | above , ((boundAbove , (0<boundAbove ,, (Nabove , prBoundAbove))) ,, above-a<e) | inl (inr below<0) | inl (inl 0<above) | inr -bel=ab = above , ((N +N Nabove) , ans)
where
ans : (m : ℕ) → (N +N Nabove <N m) → abs (index (CauchyCompletion.elts a) m) < above
ans m N<m with SetoidTotalOrder.totality tOrder 0G (index (CauchyCompletion.elts a) m)
ans m N<m | inl (inl 0<am) = SetoidPartialOrder.transitive pOrder (<WellDefined identLeft (Equivalence.reflexive eq) (orderRespectsAddition 0<boundAbove (index (CauchyCompletion.elts a) m))) (prBoundAbove m (inequalityShrinkRight N<m))
ans m N<m | inl (inr am<0) = <WellDefined (Equivalence.reflexive eq) (-bel=ab) (ringSwapNegatives' (SetoidPartialOrder.transitive pOrder (<WellDefined identLeft groupIsAbelian (orderRespectsAddition 0<boundBelow below)) (prBoundBelow m (inequalityShrinkLeft N<m))))
ans m N<m | inr 0=am = <WellDefined 0=am (Equivalence.reflexive eq) 0<above
boundModulus a | below , ((boundBelow , (0<boundBelow ,, (N , prBoundBelow))) ,, a-below<e) | above , ((boundAbove , (0<boundAbove ,, (Nabove , prBoundAbove))) ,, above-a<e) | inl (inr below<0) | inl (inr above<0) = inverse below , ((N +N Nabove) , ans)
where
ans : (m : ℕ) → ((N +N Nabove) <N m) → abs (index (CauchyCompletion.elts a) m) < inverse below
ans m N<m with SetoidTotalOrder.totality tOrder 0R (index (CauchyCompletion.elts a) m)
ans m N<m | inl (inl 0<am) = exFalso (irreflexive {0G} (SetoidPartialOrder.transitive pOrder 0<am (SetoidPartialOrder.transitive pOrder (SetoidPartialOrder.transitive pOrder (<WellDefined identLeft (Equivalence.reflexive eq) (orderRespectsAddition 0<boundAbove (index (CauchyCompletion.elts a) m))) (prBoundAbove m (inequalityShrinkRight N<m))) above<0)))
ans m N<m | inl (inr am<0) = ringSwapNegatives' (SetoidPartialOrder.transitive pOrder (<WellDefined identLeft groupIsAbelian (orderRespectsAddition 0<boundBelow below)) (prBoundBelow m (inequalityShrinkLeft N<m)))
ans m N<m | inr 0=am = exFalso (irreflexive {0G} (<WellDefined (Equivalence.symmetric eq 0=am) (Equivalence.reflexive eq) (SetoidPartialOrder.transitive pOrder (SetoidPartialOrder.transitive pOrder (<WellDefined identLeft (Equivalence.reflexive eq) (orderRespectsAddition 0<boundAbove (index (CauchyCompletion.elts a) m))) (prBoundAbove m (inequalityShrinkRight N<m))) above<0)))
boundModulus a | below , ((boundBelow , (0<boundBelow ,, (N , prBoundBelow))) ,, a-below<e) | above , ((boundAbove , (0<boundAbove ,, (Nabove , prBoundAbove))) ,, above-a<e) | inl (inr below<0) | inr 0=above = inverse below , ((N +N Nabove) , ans)
where
ans : (m : ℕ) → ((N +N Nabove) <N m) → abs (index (CauchyCompletion.elts a) m) < inverse below
ans m N<m with SetoidTotalOrder.totality tOrder 0R (index (CauchyCompletion.elts a) m)
ans m N<m | inl (inl 0<am) = exFalso (irreflexive {0G} (<WellDefined (Equivalence.reflexive eq) (Equivalence.symmetric eq 0=above) (SetoidPartialOrder.transitive pOrder 0<am (SetoidPartialOrder.transitive pOrder (<WellDefined identLeft (Equivalence.reflexive eq) (orderRespectsAddition 0<boundAbove (index (CauchyCompletion.elts a) m))) (prBoundAbove m (inequalityShrinkRight N<m))))))
ans m N<m | inl (inr am<0) = ringSwapNegatives' (SetoidPartialOrder.transitive pOrder (<WellDefined identLeft groupIsAbelian (orderRespectsAddition 0<boundBelow below)) (prBoundBelow m (inequalityShrinkLeft N<m)))
ans m N<m | inr 0=am = <WellDefined 0=am (Equivalence.reflexive eq) (lemm2 _ below<0)
boundModulus a | below , ((boundBelow , ((boundBelowDiff ,, (Nb , ansBelow)))) ,, a-below<e) | above , ((bound , (0<bound ,, (N , ans))) ,, above-a<e) | inr 0=below = above , ((N +N Nb) , λ m N<m → SetoidPartialOrder.transitive pOrder (res m N<m) (ans m (inequalityShrinkLeft N<m)))
where
res : (m : ℕ) → (N +N Nb) <N m → (abs (index (CauchyCompletion.elts a) m)) < (bound + index (CauchyCompletion.elts a) m)
res m N<m with SetoidTotalOrder.totality tOrder 0R (index (CauchyCompletion.elts a) m)
res m N<m | inl (inl 0<am) = <WellDefined identLeft (Equivalence.reflexive eq) (orderRespectsAddition 0<bound (index (CauchyCompletion.elts a) m))
res m N<m | inl (inr am<0) = exFalso (irreflexive (<WellDefined (Equivalence.symmetric eq 0=below) (Equivalence.reflexive eq) (SetoidPartialOrder.transitive pOrder (SetoidPartialOrder.transitive pOrder (<WellDefined identLeft groupIsAbelian (orderRespectsAddition boundBelowDiff below)) (ansBelow m (inequalityShrinkRight N<m))) am<0)))
res m N<m | inr 0=am = <WellDefined 0=am (Equivalence.transitive eq (Equivalence.symmetric eq identRight) (+WellDefined (Equivalence.reflexive eq) 0=am)) 0<bound

237
Fields/CauchyCompletion/Multiplication.agda
View File

@@ -50,48 +50,52 @@ CauchyCompletion.converges (record { elts = a ; converges = aConv } *C record {
where
boundBoth : A
boundBoth = aBound + bBound
ab<bb : aBound < boundBoth
ab<bb = <WellDefined identLeft groupIsAbelian (orderRespectsAddition {0R} {bBound} (greaterThanAbsImpliesGreaterThan0 (prBBound (succ Nb) (le 0 refl))) aBound)
bb<bb : bBound < boundBoth
bb<bb = <WellDefined identLeft (Equivalence.reflexive eq) (orderRespectsAddition {0R} {aBound} (greaterThanAbsImpliesGreaterThan0 (prABound (succ Na) (le 0 refl))) bBound)
0<boundBoth : 0R < boundBoth
0<boundBoth = <WellDefined identLeft (Equivalence.reflexive eq) (ringAddInequalities (greaterThanAbsImpliesGreaterThan0 (prABound (succ Na) (le 0 refl))) (greaterThanAbsImpliesGreaterThan0 (prBBound (succ Nb) (le 0 refl))))
1/boundBoothAndPr : Sg A λ i → i * (aBound + bBound) ∼ 1R
1/boundBoothAndPr = allInvertible boundBoth λ pr → irreflexive (<WellDefined (Equivalence.reflexive eq) pr 0<boundBoth)
1/boundBooth : A
1/boundBooth with 1/boundBoothAndPr
... | a , _ = a
1/boundBoothPr : 1/boundBooth * (aBound + bBound) ∼ 1R
1/boundBoothPr with 1/boundBoothAndPr
... | _ , pr = pr
0<1/boundBooth : 0G < 1/boundBooth
0<1/boundBooth = inversePositiveIsPositive 1/boundBoothPr 0<boundBoth
miniEAndPr : Sg A (λ i → (i + i) ∼ (e * 1/boundBooth))
miniEAndPr = halve charNot2 (e * 1/boundBooth)
miniE : A
miniE with miniEAndPr
... | a , _ = a
miniEPr : (miniE + miniE) ∼ (e * 1/boundBooth)
miniEPr with miniEAndPr
... | _ , pr = pr
0<miniE : 0R < miniE
0<miniE = halvePositive miniE (<WellDefined (Equivalence.reflexive eq) (Equivalence.symmetric eq miniEPr) (orderRespectsMultiplication 0<e 0<1/boundBooth))
reallyNAAndPr : Sg ℕ (λ N → {m n : ℕ} → N <N m → N <N n → abs (index a m + inverse (index a n)) < miniE)
reallyNAAndPr = aConv miniE 0<miniE
reallyNa : ℕ
reallyNa with reallyNAAndPr
... | a , _ = a
reallyNaPr : {m n : ℕ} → reallyNa <N m → reallyNa <N n → abs (index a m + inverse (index a n)) < miniE
reallyNaPr with reallyNAAndPr
... | _ , pr = pr
reallyNBAndPr : Sg ℕ (λ N → {m n : ℕ} → N <N m → N <N n → abs (index b m + inverse (index b n)) < miniE)
reallyNBAndPr = bConv miniE 0<miniE
reallyNb : ℕ
reallyNb with reallyNBAndPr
... | a , _ = a
reallyNbPr : {m n : ℕ} → reallyNb <N m → reallyNb <N n → abs (index b m + inverse (index b n)) < miniE
reallyNbPr with reallyNBAndPr
... | _ , pr = pr
abstract
ab<bb : aBound < boundBoth
ab<bb = <WellDefined identLeft groupIsAbelian (orderRespectsAddition {0R} {bBound} (greaterThanAbsImpliesGreaterThan0 (prBBound (succ Nb) (le 0 refl))) aBound)
bb<bb : bBound < boundBoth
bb<bb = <WellDefined identLeft (Equivalence.reflexive eq) (orderRespectsAddition {0R} {aBound} (greaterThanAbsImpliesGreaterThan0 (prABound (succ Na) (le 0 refl))) bBound)
0<boundBoth : 0R < boundBoth
0<boundBoth = <WellDefined identLeft (Equivalence.reflexive eq) (ringAddInequalities (greaterThanAbsImpliesGreaterThan0 (prABound (succ Na) (le 0 refl))) (greaterThanAbsImpliesGreaterThan0 (prBBound (succ Nb) (le 0 refl))))
abstract
1/boundBoothAndPr : Sg A λ i → i * (aBound + bBound) ∼ 1R
1/boundBoothAndPr = allInvertible boundBoth λ pr → irreflexive (<WellDefined (Equivalence.reflexive eq) pr 0<boundBoth)
1/boundBooth : A
1/boundBooth with 1/boundBoothAndPr
... | a , _ = a
1/boundBoothPr : 1/boundBooth * (aBound + bBound) ∼ 1R
1/boundBoothPr with 1/boundBoothAndPr
... | _ , pr = pr
0<1/boundBooth : 0G < 1/boundBooth
0<1/boundBooth = inversePositiveIsPositive 1/boundBoothPr 0<boundBoth
abstract
miniEAndPr : Sg A (λ i → (i + i) ∼ (e * 1/boundBooth))
miniEAndPr = halve charNot2 (e * 1/boundBooth)
miniE : A
miniE with miniEAndPr
... | a , _ = a
miniEPr : (miniE + miniE) ∼ (e * 1/boundBooth)
miniEPr with miniEAndPr
... | _ , pr = pr
0<miniE : 0R < miniE
0<miniE = halvePositive miniE (<WellDefined (Equivalence.reflexive eq) (Equivalence.symmetric eq miniEPr) (orderRespectsMultiplication 0<e 0<1/boundBooth))
abstract
reallyNAAndPr : Sg ℕ (λ N → {m n : ℕ} → N <N m → N <N n → abs (index a m + inverse (index a n)) < miniE)
reallyNAAndPr = aConv miniE 0<miniE
reallyNa : ℕ
reallyNa with reallyNAAndPr
... | a , _ = a
reallyNaPr : {m n : ℕ} → reallyNa <N m → reallyNa <N n → abs (index a m + inverse (index a n)) < miniE
reallyNaPr with reallyNAAndPr
... | _ , pr = pr
reallyNBAndPr : Sg ℕ (λ N → {m n : ℕ} → N <N m → N <N n → abs (index b m + inverse (index b n)) < miniE)
reallyNBAndPr = bConv miniE 0<miniE
reallyNb : ℕ
reallyNb with reallyNBAndPr
... | a , _ = a
reallyNbPr : {m n : ℕ} → reallyNb <N m → reallyNb <N n → abs (index b m + inverse (index b n)) < miniE
reallyNbPr with reallyNBAndPr
... | _ , pr = pr
N : ℕ
N = (Na +N (Nb +N (reallyNa +N reallyNb)))
ans : {m : ℕ} {n : ℕ} → N <N m → N <N n → abs (index (apply _*_ a b) m + inverse (index (apply _*_ a b) n)) < e
@@ -101,8 +105,9 @@ CauchyCompletion.converges (record { elts = a ; converges = aConv } *C record {
Na<m = inequalityShrinkLeft N<m
Nb<n : Nb <N n
Nb<n = inequalityShrinkLeft (inequalityShrinkRight {Na} N<n)
sum : {m n : ℕ} → (reallyNa +N reallyNb) <N m → (reallyNa +N reallyNb) <N n → (boundBoth * ((abs (index b m + inverse (index b n))) + (abs (index a m + inverse (index a n))))) < e
sum {m} {n} <m <n = <WellDefined *Commutative (Equivalence.transitive eq (*WellDefined miniEPr (Equivalence.reflexive eq)) (Equivalence.transitive eq (Equivalence.symmetric eq *Associative) (Equivalence.transitive eq (Equivalence.transitive eq (*WellDefined (Equivalence.reflexive eq) 1/boundBoothPr) *Commutative) (identIsIdent)))) (ringCanMultiplyByPositive {c = boundBoth} 0<boundBoth (ringAddInequalities (reallyNbPr {m} {n} (inequalityShrinkRight <m) (inequalityShrinkRight <n)) (reallyNaPr {m} {n} (inequalityShrinkLeft <m) (inequalityShrinkLeft <n))))
abstract
sum : {m n : ℕ} → (reallyNa +N reallyNb) <N m → (reallyNa +N reallyNb) <N n → (boundBoth * ((abs (index b m + inverse (index b n))) + (abs (index a m + inverse (index a n))))) < e
sum {m} {n} <m <n = <WellDefined *Commutative (Equivalence.transitive eq (*WellDefined miniEPr (Equivalence.reflexive eq)) (Equivalence.transitive eq (Equivalence.symmetric eq *Associative) (Equivalence.transitive eq (Equivalence.transitive eq (*WellDefined (Equivalence.reflexive eq) 1/boundBoothPr) *Commutative) (identIsIdent)))) (ringCanMultiplyByPositive {c = boundBoth} 0<boundBoth (ringAddInequalities (reallyNbPr {m} {n} (inequalityShrinkRight <m) (inequalityShrinkRight <n)) (reallyNaPr {m} {n} (inequalityShrinkLeft <m) (inequalityShrinkLeft <n))))
q : ((boundBoth * (abs (index b m + inverse (index b n)))) + (boundBoth * (abs (index a m + inverse (index a n))))) < e
q = <WellDefined *DistributesOver+ (Equivalence.reflexive eq) (sum {m} {n} (inequalityShrinkRight {Nb} (inequalityShrinkRight {Na} N<m)) (inequalityShrinkRight {Nb} (inequalityShrinkRight {Na} N<n)))
p : ((abs (index a m) * abs (index b m + inverse (index b n))) + (abs (index b n) * abs (index a m + inverse (index a n)))) < e
@@ -152,85 +157,81 @@ CauchyCompletion.converges (record { elts = a ; converges = aConv } *C record {
ans : {m : ℕ} → 0 <N m → abs (index (apply _+_ (CauchyCompletion.elts (a *C b)) (map inverse (CauchyCompletion.elts (b *C a)))) m) < ε
ans {m} 0<m rewrite indexAndApply (apply _*_ (CauchyCompletion.elts a) (CauchyCompletion.elts b)) (map inverse (apply _*_ (CauchyCompletion.elts b) (CauchyCompletion.elts a))) _+_ {m} | indexAndApply (CauchyCompletion.elts a) (CauchyCompletion.elts b) _*_ {m} | equalityCommutative (mapAndIndex (apply _*_ (CauchyCompletion.elts b) (CauchyCompletion.elts a)) inverse m) | indexAndApply (CauchyCompletion.elts b) (CauchyCompletion.elts a) _*_ {m} = <WellDefined (Equivalence.symmetric eq (Equivalence.transitive eq (absWellDefined _ _ foo) (identityOfIndiscernablesRight _∼_ (Equivalence.reflexive eq) (absZero order)))) (Equivalence.reflexive eq) 0<e
absBoundedImpliesBounded : {a b : A} → abs a < b → a < b
absBoundedImpliesBounded {a} {b} a<b with SetoidTotalOrder.totality tOrder 0G a
absBoundedImpliesBounded {a} {b} a<b | inl (inl x) = a<b
absBoundedImpliesBounded {a} {b} a<b | inl (inr x) = SetoidPartialOrder.transitive pOrder x (SetoidPartialOrder.transitive pOrder (lemm2 a x) a<b)
absBoundedImpliesBounded {a} {b} a<b | inr x = a<b
abstract
multiplicationWellDefinedLeft' : (0!=1 : 0R ∼ 1R → False) (a b c : CauchyCompletion) → Setoid._∼_ cauchyCompletionSetoid a b → Setoid._∼_ cauchyCompletionSetoid (a *C c) (b *C c)
multiplicationWellDefinedLeft' 0!=1 a b c a=b ε 0<e = N , ans
where
cBoundAndPr : Sg A (λ b → Sg ℕ (λ N → (m : ℕ) → (N <N m) → (abs (index (CauchyCompletion.elts c) m)) < b))
cBoundAndPr = boundModulus c
cBound : A
cBound with cBoundAndPr
... | a , _ = a
cBoundN : ℕ
cBoundN with cBoundAndPr
... | _ , (N , _) = N
cBoundPr : (m : ℕ) → (cBoundN <N m) → (abs (index (CauchyCompletion.elts c) m)) < cBound
cBoundPr with cBoundAndPr
... | _ , (_ , pr) = pr
0<cBound : 0G < cBound
0<cBound with totality 0G cBound
0<cBound | inl (inl 0<cBound) = 0<cBound
0<cBound | inl (inr cBound<0) = exFalso (absNonnegative (SetoidPartialOrder.transitive pOrder (cBoundPr (succ cBoundN) (le 0 refl)) cBound<0))
0<cBound | inr 0=cBound = exFalso (absNonnegative (<WellDefined (Equivalence.reflexive eq) (Equivalence.symmetric eq 0=cBound) (cBoundPr (succ cBoundN) (le 0 refl))))
e/c : A
e/c with allInvertible cBound (λ pr → irreflexive (<WellDefined (Equivalence.reflexive eq) pr 0<cBound))
... | (1/c , _) = ε * 1/c
e/cPr : e/c * cBound ∼ ε
e/cPr with allInvertible cBound (λ pr → irreflexive (<WellDefined (Equivalence.reflexive eq) pr 0<cBound))
... | (1/c , pr) = Equivalence.transitive eq (Equivalence.transitive eq (Equivalence.transitive eq (Equivalence.symmetric eq *Associative) (*WellDefined (Equivalence.reflexive eq) pr)) *Commutative) (identIsIdent)
0<e/c : 0G < e/c
0<e/c = ringCanCancelPositive {0G} {e/c} 0<cBound (<WellDefined (Equivalence.symmetric eq (Equivalence.transitive eq *Commutative timesZero)) (Equivalence.symmetric eq e/cPr) 0<e)
abBound : ℕ
abBound with a=b e/c 0<e/c
... | Na=b , _ = Na=b
abPr : {m : ℕ} → (abBound <N m) → abs (index (apply _+_ (CauchyCompletion.elts a) (map inverse (CauchyCompletion.elts b))) m) < e/c
abPr with a=b e/c 0<e/c
... | Na=b , pr = pr
N : ℕ
N = abBound +N cBoundN
cBounded : (m : ℕ) → (N <N m) → abs (index (CauchyCompletion.elts c) m) < cBound
cBounded m N<m = cBoundPr m (inequalityShrinkRight N<m)
a-bSmall : (m : ℕ) → N <N m → abs ((index (CauchyCompletion.elts a) m) + inverse (index (CauchyCompletion.elts b) m)) < e/c
a-bSmall m N<m with abPr {m} (inequalityShrinkLeft N<m)
... | f rewrite indexAndApply (CauchyCompletion.elts a) (map inverse (CauchyCompletion.elts b)) _+_ {m} | equalityCommutative (mapAndIndex (CauchyCompletion.elts b) inverse m) = f
ans : {m : ℕ} → N <N m → abs (index (apply _+_ (apply _*_ (CauchyCompletion.elts a) (CauchyCompletion.elts c)) (map inverse (apply _*_ (CauchyCompletion.elts b) (CauchyCompletion.elts c)))) m) < ε
ans {m} N<m rewrite indexAndApply (apply _*_ (CauchyCompletion.elts a) (CauchyCompletion.elts c)) (map inverse (apply _*_ (CauchyCompletion.elts b) (CauchyCompletion.elts c))) _+_ {m} | equalityCommutative (mapAndIndex (apply _*_ (CauchyCompletion.elts b) (CauchyCompletion.elts c)) inverse m) | indexAndApply (CauchyCompletion.elts b) (CauchyCompletion.elts c) _*_ {m} | indexAndApply (CauchyCompletion.elts a) (CauchyCompletion.elts c) _*_ {m} = <WellDefined (absWellDefined _ _ (+WellDefined (Equivalence.reflexive eq) (ringMinusExtracts' R))) (Equivalence.reflexive eq) (<WellDefined (absWellDefined ((index (CauchyCompletion.elts a) m + inverse (index (CauchyCompletion.elts b) m)) * index (CauchyCompletion.elts c) m) _ (Equivalence.transitive eq (Equivalence.transitive eq *Commutative *DistributesOver+) (+WellDefined *Commutative *Commutative))) (Equivalence.reflexive eq) (<WellDefined (Equivalence.symmetric eq (absRespectsTimes _ _)) (Equivalence.reflexive eq) (<WellDefined (Equivalence.reflexive eq) e/cPr (ans' (index (CauchyCompletion.elts a) m) (index (CauchyCompletion.elts b) m) (index (CauchyCompletion.elts c) m) (a-bSmall m N<m) (cBounded m N<m)))))
where
ans' : (a b c : A) → abs (a + inverse b) < e/c → abs c < cBound → (abs (a + inverse b) * abs c) < (e/c * cBound)
ans' a b c a-b<e/c c<bound with SetoidTotalOrder.totality tOrder 0R c
ans' a b c a-b<e/c c<bound | inl (inl 0<c) with totality 0G (a + inverse b)
ans' a b c a-b<e/c c<bound | inl (inl 0<c) | inl (inl 0<a-b) = ringMultiplyPositives 0<a-b 0<c a-b<e/c c<bound
ans' a b c a-b<e/c c<bound | inl (inl 0<c) | inl (inr a-b<0) = ringMultiplyPositives (lemm2 (a + inverse b) a-b<0) 0<c a-b<e/c c<bound
ans' a b c a-b<e/c c<bound | inl (inl 0<c) | inr 0=a-b = <WellDefined (Equivalence.symmetric eq (Equivalence.transitive eq (*WellDefined (Equivalence.symmetric eq 0=a-b) (Equivalence.reflexive eq)) (Equivalence.transitive eq *Commutative timesZero))) (Equivalence.reflexive eq) (orderRespectsMultiplication 0<e/c 0<cBound)
ans' a b c a-b<e/c c<bound | inl (inr c<0) with totality 0G (a + inverse b)
ans' a b c a-b<e/c c<bound | inl (inr c<0) | inl (inl 0<a-b) = ringMultiplyPositives 0<a-b (lemm2 c c<0) a-b<e/c c<bound
ans' a b c a-b<e/c c<bound | inl (inr c<0) | inl (inr a-b<0) = ringMultiplyPositives (lemm2 (a + inverse b) a-b<0) (lemm2 c c<0) a-b<e/c c<bound
ans' a b c a-b<e/c c<bound | inl (inr c<0) | inr 0=a-b = <WellDefined (Equivalence.symmetric eq (Equivalence.transitive eq (*WellDefined (Equivalence.symmetric eq 0=a-b) (Equivalence.reflexive eq)) (Equivalence.transitive eq *Commutative timesZero))) (Equivalence.reflexive eq) (orderRespectsMultiplication 0<e/c 0<cBound)
ans' a b c a-b<e/c c<bound | inr 0=c = <WellDefined (Equivalence.symmetric eq (Equivalence.transitive eq (*WellDefined (Equivalence.reflexive eq) (Equivalence.symmetric eq 0=c)) timesZero)) (Equivalence.reflexive eq) (orderRespectsMultiplication 0<e/c 0<cBound)
multiplicationWellDefinedLeft' : (0!=1 : 0R ∼ 1R → False) (a b c : CauchyCompletion) → Setoid._∼_ cauchyCompletionSetoid a b → Setoid._∼_ cauchyCompletionSetoid (a *C c) (b *C c)
multiplicationWellDefinedLeft' 0!=1 a b c a=b ε 0<e = N , ans
where
cBoundAndPr : Sg A (λ b → Sg ℕ (λ N → (m : ℕ) → (N <N m) → (abs (index (CauchyCompletion.elts c) m)) < b))
cBoundAndPr = boundModulus c
cBound : A
cBound with cBoundAndPr
... | a , _ = a
cBoundN : ℕ
cBoundN with cBoundAndPr
... | _ , (N , _) = N
cBoundPr : (m : ℕ) → (cBoundN <N m) → (abs (index (CauchyCompletion.elts c) m)) < cBound
cBoundPr with cBoundAndPr
... | _ , (_ , pr) = pr
0<cBound : 0G < cBound
0<cBound with totality 0G cBound
0<cBound | inl (inl 0<cBound) = 0<cBound
0<cBound | inl (inr cBound<0) = exFalso (absNonnegative (SetoidPartialOrder.transitive pOrder (cBoundPr (succ cBoundN) (le 0 refl)) cBound<0))
0<cBound | inr 0=cBound = exFalso (absNonnegative (<WellDefined (Equivalence.reflexive eq) (Equivalence.symmetric eq 0=cBound) (cBoundPr (succ cBoundN) (le 0 refl))))
e/c : A
e/c with allInvertible cBound (λ pr → irreflexive (<WellDefined (Equivalence.reflexive eq) pr 0<cBound))
... | (1/c , _) = ε * 1/c
e/cPr : e/c * cBound ∼ ε
e/cPr with allInvertible cBound (λ pr → irreflexive (<WellDefined (Equivalence.reflexive eq) pr 0<cBound))
... | (1/c , pr) = Equivalence.transitive eq (Equivalence.transitive eq (Equivalence.transitive eq (Equivalence.symmetric eq *Associative) (*WellDefined (Equivalence.reflexive eq) pr)) *Commutative) (identIsIdent)
0<e/c : 0G < e/c
0<e/c = ringCanCancelPositive {0G} {e/c} 0<cBound (<WellDefined (Equivalence.symmetric eq (Equivalence.transitive eq *Commutative timesZero)) (Equivalence.symmetric eq e/cPr) 0<e)
abBound : ℕ
abBound with a=b e/c 0<e/c
... | Na=b , _ = Na=b
abPr : {m : ℕ} → (abBound <N m) → abs (index (apply _+_ (CauchyCompletion.elts a) (map inverse (CauchyCompletion.elts b))) m) < e/c
abPr with a=b e/c 0<e/c
... | Na=b , pr = pr
N : ℕ
N = abBound +N cBoundN
cBounded : (m : ℕ) → (N <N m) → abs (index (CauchyCompletion.elts c) m) < cBound
cBounded m N<m = cBoundPr m (inequalityShrinkRight N<m)
a-bSmall : (m : ℕ) → N <N m → abs ((index (CauchyCompletion.elts a) m) + inverse (index (CauchyCompletion.elts b) m)) < e/c
a-bSmall m N<m with abPr {m} (inequalityShrinkLeft N<m)
... | f rewrite indexAndApply (CauchyCompletion.elts a) (map inverse (CauchyCompletion.elts b)) _+_ {m} | equalityCommutative (mapAndIndex (CauchyCompletion.elts b) inverse m) = f
ans : {m : ℕ} → N <N m → abs (index (apply _+_ (apply _*_ (CauchyCompletion.elts a) (CauchyCompletion.elts c)) (map inverse (apply _*_ (CauchyCompletion.elts b) (CauchyCompletion.elts c)))) m) < ε
ans {m} N<m rewrite indexAndApply (apply _*_ (CauchyCompletion.elts a) (CauchyCompletion.elts c)) (map inverse (apply _*_ (CauchyCompletion.elts b) (CauchyCompletion.elts c))) _+_ {m} | equalityCommutative (mapAndIndex (apply _*_ (CauchyCompletion.elts b) (CauchyCompletion.elts c)) inverse m) | indexAndApply (CauchyCompletion.elts b) (CauchyCompletion.elts c) _*_ {m} | indexAndApply (CauchyCompletion.elts a) (CauchyCompletion.elts c) _*_ {m} = <WellDefined (absWellDefined _ _ (+WellDefined (Equivalence.reflexive eq) (ringMinusExtracts' R))) (Equivalence.reflexive eq) (<WellDefined (absWellDefined ((index (CauchyCompletion.elts a) m + inverse (index (CauchyCompletion.elts b) m)) * index (CauchyCompletion.elts c) m) _ (Equivalence.transitive eq (Equivalence.transitive eq *Commutative *DistributesOver+) (+WellDefined *Commutative *Commutative))) (Equivalence.reflexive eq) (<WellDefined (Equivalence.symmetric eq (absRespectsTimes _ _)) (Equivalence.reflexive eq) (<WellDefined (Equivalence.reflexive eq) e/cPr (ans' (index (CauchyCompletion.elts a) m) (index (CauchyCompletion.elts b) m) (index (CauchyCompletion.elts c) m) (a-bSmall m N<m) (cBounded m N<m)))))
where
ans' : (a b c : A) → abs (a + inverse b) < e/c → abs c < cBound → (abs (a + inverse b) * abs c) < (e/c * cBound)
ans' a b c a-b<e/c c<bound with SetoidTotalOrder.totality tOrder 0R c
ans' a b c a-b<e/c c<bound | inl (inl 0<c) with totality 0G (a + inverse b)
ans' a b c a-b<e/c c<bound | inl (inl 0<c) | inl (inl 0<a-b) = ringMultiplyPositives 0<a-b 0<c a-b<e/c c<bound
ans' a b c a-b<e/c c<bound | inl (inl 0<c) | inl (inr a-b<0) = ringMultiplyPositives (lemm2 (a + inverse b) a-b<0) 0<c a-b<e/c c<bound
ans' a b c a-b<e/c c<bound | inl (inl 0<c) | inr 0=a-b = <WellDefined (Equivalence.symmetric eq (Equivalence.transitive eq (*WellDefined (Equivalence.symmetric eq 0=a-b) (Equivalence.reflexive eq)) (Equivalence.transitive eq *Commutative timesZero))) (Equivalence.reflexive eq) (orderRespectsMultiplication 0<e/c 0<cBound)
ans' a b c a-b<e/c c<bound | inl (inr c<0) with totality 0G (a + inverse b)
ans' a b c a-b<e/c c<bound | inl (inr c<0) | inl (inl 0<a-b) = ringMultiplyPositives 0<a-b (lemm2 c c<0) a-b<e/c c<bound
ans' a b c a-b<e/c c<bound | inl (inr c<0) | inl (inr a-b<0) = ringMultiplyPositives (lemm2 (a + inverse b) a-b<0) (lemm2 c c<0) a-b<e/c c<bound
ans' a b c a-b<e/c c<bound | inl (inr c<0) | inr 0=a-b = <WellDefined (Equivalence.symmetric eq (Equivalence.transitive eq (*WellDefined (Equivalence.symmetric eq 0=a-b) (Equivalence.reflexive eq)) (Equivalence.transitive eq *Commutative timesZero))) (Equivalence.reflexive eq) (orderRespectsMultiplication 0<e/c 0<cBound)
ans' a b c a-b<e/c c<bound | inr 0=c = <WellDefined (Equivalence.symmetric eq (Equivalence.transitive eq (*WellDefined (Equivalence.reflexive eq) (Equivalence.symmetric eq 0=c)) timesZero)) (Equivalence.reflexive eq) (orderRespectsMultiplication 0<e/c 0<cBound)
multiplicationWellDefinedLeft : (a b c : CauchyCompletion) → Setoid._∼_ cauchyCompletionSetoid a b → Setoid._∼_ cauchyCompletionSetoid (a *C c) (b *C c)
multiplicationWellDefinedLeft with SetoidTotalOrder.totality tOrder 0R 1R
... | inl (inl 0<1') = multiplicationWellDefinedLeft' (λ pr → irreflexive {0G} (<WellDefined (Equivalence.reflexive eq) (Equivalence.symmetric eq pr) 0<1'))
... | inl (inr 1<0) = multiplicationWellDefinedLeft' (λ pr → irreflexive {0G} (<WellDefined (Equivalence.symmetric eq pr) (Equivalence.reflexive eq) 1<0))
... | inr (0=1) = λ a b c a=b → Equivalence.transitive (Setoid.eq cauchyCompletionSetoid) {a *C c} {injection 0G} {b *C c} (Equivalence.symmetric (Setoid.eq cauchyCompletionSetoid) {injection 0G} {a *C c} (trivialIfInputTrivial 0=1 (a *C c))) (trivialIfInputTrivial 0=1 (b *C c))
multiplicationWellDefinedLeft : (a b c : CauchyCompletion) → Setoid._∼_ cauchyCompletionSetoid a b → Setoid._∼_ cauchyCompletionSetoid (a *C c) (b *C c)
multiplicationWellDefinedLeft with SetoidTotalOrder.totality tOrder 0R 1R
... | inl (inl 0<1') = multiplicationWellDefinedLeft' (λ pr → irreflexive {0G} (<WellDefined (Equivalence.reflexive eq) (Equivalence.symmetric eq pr) 0<1'))
... | inl (inr 1<0) = multiplicationWellDefinedLeft' (λ pr → irreflexive {0G} (<WellDefined (Equivalence.symmetric eq pr) (Equivalence.reflexive eq) 1<0))
... | inr (0=1) = λ a b c a=b → Equivalence.transitive (Setoid.eq cauchyCompletionSetoid) {a *C c} {injection 0G} {b *C c} (Equivalence.symmetric (Setoid.eq cauchyCompletionSetoid) {injection 0G} {a *C c} (trivialIfInputTrivial 0=1 (a *C c))) (trivialIfInputTrivial 0=1 (b *C c))
multiplicationPreservedLeft : {a b : A} {c : CauchyCompletion} → (a ∼ b) → Setoid._∼_ cauchyCompletionSetoid (injection a *C c) (injection b *C c)
multiplicationPreservedLeft {a} {b} {c} a=b = multiplicationWellDefinedLeft (injection a) (injection b) c (injectionPreservesSetoid a b a=b)
multiplicationPreservedLeft : {a b : A} {c : CauchyCompletion} → (a ∼ b) → Setoid._∼_ cauchyCompletionSetoid (injection a *C c) (injection b *C c)
multiplicationPreservedLeft {a} {b} {c} a=b = multiplicationWellDefinedLeft (injection a) (injection b) c (injectionPreservesSetoid a b a=b)
multiplicationPreservedRight : {a b : A} {c : CauchyCompletion} → (a ∼ b) → Setoid._∼_ cauchyCompletionSetoid (c *C injection a) (c *C injection b)
multiplicationPreservedRight {a} {b} {c} a=b = Equivalence.transitive (Setoid.eq cauchyCompletionSetoid) {c *C injection a} {injection a *C c} {c *C injection b} (*CCommutative {c} {injection a}) (Equivalence.transitive (Setoid.eq cauchyCompletionSetoid) {injection a *C c} {injection b *C c} {c *C injection b} (multiplicationPreservedLeft {a} {b} {c} a=b) (*CCommutative {injection b} {c}))
multiplicationPreservedRight : {a b : A} {c : CauchyCompletion} → (a ∼ b) → Setoid._∼_ cauchyCompletionSetoid (c *C injection a) (c *C injection b)
multiplicationPreservedRight {a} {b} {c} a=b = Equivalence.transitive (Setoid.eq cauchyCompletionSetoid) {c *C injection a} {injection a *C c} {c *C injection b} (*CCommutative {c} {injection a}) (Equivalence.transitive (Setoid.eq cauchyCompletionSetoid) {injection a *C c} {injection b *C c} {c *C injection b} (multiplicationPreservedLeft {a} {b} {c} a=b) (*CCommutative {injection b} {c}))
multiplicationPreserved : {a b c d : A} → (a ∼ b) → (c ∼ d) → Setoid._∼_ cauchyCompletionSetoid (injection a *C injection c) (injection b *C injection d)
multiplicationPreserved {a} {b} {c} {d} a=b c=d = Equivalence.transitive (Setoid.eq cauchyCompletionSetoid) {injection a *C injection c} {injection a *C injection d} {injection b *C injection d} (multiplicationPreservedRight {c} {d} {injection a} c=d) (multiplicationPreservedLeft {a} {b} {injection d} a=b)
multiplicationPreserved : {a b c d : A} → (a ∼ b) → (c ∼ d) → Setoid._∼_ cauchyCompletionSetoid (injection a *C injection c) (injection b *C injection d)
multiplicationPreserved {a} {b} {c} {d} a=b c=d = Equivalence.transitive (Setoid.eq cauchyCompletionSetoid) {injection a *C injection c} {injection a *C injection d} {injection b *C injection d} (multiplicationPreservedRight {c} {d} {injection a} c=d) (multiplicationPreservedLeft {a} {b} {injection d} a=b)
multiplicationWellDefinedRight : (a b c : CauchyCompletion) → Setoid._∼_ cauchyCompletionSetoid b c → Setoid._∼_ cauchyCompletionSetoid (a *C b) (a *C c)
multiplicationWellDefinedRight a b c b=c = Equivalence.transitive (Setoid.eq cauchyCompletionSetoid) {a *C b} {b *C a} {a *C c} (*CCommutative {a} {b}) (Equivalence.transitive (Setoid.eq cauchyCompletionSetoid) {b *C a} {c *C a} {a *C c} (multiplicationWellDefinedLeft b c a b=c) (*CCommutative {c} {a}))
multiplicationWellDefinedRight : (a b c : CauchyCompletion) → Setoid._∼_ cauchyCompletionSetoid b c → Setoid._∼_ cauchyCompletionSetoid (a *C b) (a *C c)
multiplicationWellDefinedRight a b c b=c = Equivalence.transitive (Setoid.eq cauchyCompletionSetoid) {a *C b} {b *C a} {a *C c} (*CCommutative {a} {b}) (Equivalence.transitive (Setoid.eq cauchyCompletionSetoid) {b *C a} {c *C a} {a *C c} (multiplicationWellDefinedLeft b c a b=c) (*CCommutative {c} {a}))
multiplicationWellDefined : {a b c d : CauchyCompletion} → Setoid._∼_ cauchyCompletionSetoid a b → Setoid._∼_ cauchyCompletionSetoid c d → Setoid._∼_ cauchyCompletionSetoid (a *C c) (b *C d)
multiplicationWellDefined {a} {b} {c} {d} a=b c=d = Equivalence.transitive (Setoid.eq cauchyCompletionSetoid) {a *C c} {a *C d} {b *C d} (multiplicationWellDefinedRight a c d c=d) (multiplicationWellDefinedLeft a b d a=b)
multiplicationWellDefined : {a b c d : CauchyCompletion} → Setoid._∼_ cauchyCompletionSetoid a b → Setoid._∼_ cauchyCompletionSetoid c d → Setoid._∼_ cauchyCompletionSetoid (a *C c) (b *C d)
multiplicationWellDefined {a} {b} {c} {d} a=b c=d = Equivalence.transitive (Setoid.eq cauchyCompletionSetoid) {a *C c} {a *C d} {b *C d} (multiplicationWellDefinedRight a c d c=d) (multiplicationWellDefinedLeft a b d a=b)

26
Fields/Lemmas.agda
View File

@@ -16,17 +16,19 @@ open import Numbers.Naturals.Naturals
module Fields.Lemmas {m n : _} {A : Set m} {S : Setoid {m} {n} A} {_+_ : A → A → A} {_*_ : A → A → A} {R : Ring S _+_ _*_} (F : Field R) where
open Setoid S
open Field F
open Ring R
open Group additiveGroup
abstract
halve : (charNot2 : ((1R + 1R) ∼ 0R) → False) → (a : A) → Sg A (λ i → i + i ∼ a)
halve charNot2 a with allInvertible (1R + 1R) charNot2
... | 1/2 , pr1/2 = (a * 1/2) , Equivalence.transitive eq (+WellDefined *Commutative *Commutative) (Equivalence.transitive eq (Equivalence.symmetric eq (*DistributesOver+ {1/2} {a} {a})) (Equivalence.transitive eq (*WellDefined (Equivalence.reflexive eq) r) (Equivalence.transitive eq (*Associative) (Equivalence.transitive eq (*WellDefined pr1/2 (Equivalence.reflexive eq)) identIsIdent))))
where
r : a + a ∼ (1R + 1R) * a
r = Equivalence.symmetric eq (Equivalence.transitive eq *Commutative (Equivalence.transitive eq *DistributesOver+ (+WellDefined (Equivalence.transitive eq *Commutative identIsIdent) (Equivalence.transitive eq *Commutative identIsIdent))))
open Setoid S
open Field F
open Ring R
open Group additiveGroup
halfHalves : {x : A} (1/2 : A) (pr : 1/2 + 1/2 ∼ 1R) → (x + x) * 1/2 ∼ x
halfHalves {x} 1/2 pr = Equivalence.transitive eq (Equivalence.transitive eq (Equivalence.transitive eq *Commutative (Equivalence.transitive eq (Equivalence.transitive eq *DistributesOver+ (Equivalence.transitive eq (+WellDefined *Commutative *Commutative) (Equivalence.symmetric eq *DistributesOver+))) *Commutative)) (*WellDefined pr (Equivalence.reflexive eq))) identIsIdent
halve : (charNot2 : ((1R + 1R) ∼ 0R) → False) → (a : A) → Sg A (λ i → i + i ∼ a)
halve charNot2 a with allInvertible (1R + 1R) charNot2
... | 1/2 , pr1/2 = (a * 1/2) , Equivalence.transitive eq (+WellDefined *Commutative *Commutative) (Equivalence.transitive eq (Equivalence.symmetric eq (*DistributesOver+ {1/2} {a} {a})) (Equivalence.transitive eq (*WellDefined (Equivalence.reflexive eq) r) (Equivalence.transitive eq (*Associative) (Equivalence.transitive eq (*WellDefined pr1/2 (Equivalence.reflexive eq)) identIsIdent))))
where
r : a + a ∼ (1R + 1R) * a
r = Equivalence.symmetric eq (Equivalence.transitive eq *Commutative (Equivalence.transitive eq *DistributesOver+ (+WellDefined (Equivalence.transitive eq *Commutative identIsIdent) (Equivalence.transitive eq *Commutative identIsIdent))))
halfHalves : {x : A} (1/2 : A) (pr : 1/2 + 1/2 ∼ 1R) → (x + x) * 1/2 ∼ x
halfHalves {x} 1/2 pr = Equivalence.transitive eq (Equivalence.transitive eq (Equivalence.transitive eq *Commutative (Equivalence.transitive eq (Equivalence.transitive eq *DistributesOver+ (Equivalence.transitive eq (+WellDefined *Commutative *Commutative) (Equivalence.symmetric eq *DistributesOver+))) *Commutative)) (*WellDefined pr (Equivalence.reflexive eq))) identIsIdent

70
Fields/Orders/Lemmas.agda
View File

@@ -19,44 +19,46 @@ open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
module Fields.Orders.Lemmas {m n o : _} {A : Set m} {S : Setoid {m} {n} A} {_+_ : A → A → A} {_*_ : A → A → A} {_<_ : Rel {_} {o} A} {R : Ring S _+_ _*_} {pOrder : SetoidPartialOrder S _<_} {tOrder : SetoidTotalOrder pOrder} {F : Field R} (oF : OrderedField F tOrder) where
open Ring R
open Group additiveGroup
open OrderedRing (OrderedField.oRing oF)
open import Rings.Orders.Lemmas (OrderedField.oRing oF)
open import Fields.Lemmas F
open Setoid S
open SetoidPartialOrder pOrder
abstract
clearDenominatorHalf : (x y 1/2 : A) → (1/2 + 1/2 ∼ 1R) → x < (y * 1/2) → (x + x) < y
clearDenominatorHalf x y 1/2 pr1/2 x<1/2y = <WellDefined (Equivalence.reflexive eq) (Equivalence.transitive eq (Equivalence.transitive eq (Equivalence.symmetric eq *DistributesOver+) (Equivalence.transitive eq *Commutative (*WellDefined pr1/2 (Equivalence.reflexive eq)))) identIsIdent) (ringAddInequalities x<1/2y x<1/2y)
open Ring R
open Group additiveGroup
open OrderedRing (OrderedField.oRing oF)
open import Rings.Orders.Lemmas (OrderedField.oRing oF)
open import Fields.Lemmas F
open Setoid S
open SetoidPartialOrder pOrder
clearDenominatorHalf' : (x y 1/2 : A) → (1/2 + 1/2 ∼ 1R) → (x * 1/2) < y → x < (y + y)
clearDenominatorHalf' x y 1/2 pr1/2 1/2x<y = <WellDefined (Equivalence.transitive eq (Equivalence.symmetric eq *DistributesOver+) (Equivalence.transitive eq (Equivalence.transitive eq *Commutative (*WellDefined pr1/2 (Equivalence.reflexive eq))) identIsIdent)) (Equivalence.reflexive eq) (ringAddInequalities 1/2x<y 1/2x<y)
clearDenominatorHalf : (x y 1/2 : A) → (1/2 + 1/2 ∼ 1R) → x < (y * 1/2) → (x + x) < y
clearDenominatorHalf x y 1/2 pr1/2 x<1/2y = <WellDefined (Equivalence.reflexive eq) (Equivalence.transitive eq (Equivalence.transitive eq (Equivalence.symmetric eq *DistributesOver+) (Equivalence.transitive eq *Commutative (*WellDefined pr1/2 (Equivalence.reflexive eq)))) identIsIdent) (ringAddInequalities x<1/2y x<1/2y)
halveInequality : (x y 1/2 : A) → (1/2 + 1/2 ∼ 1R) → (x + x) < y → x < (y * 1/2)
halveInequality x y 1/2 pr1/2 2x<y with SetoidTotalOrder.totality tOrder 0R 1R
... | inl (inl 0<1') = <WellDefined (halfHalves 1/2 pr1/2) (Equivalence.reflexive eq) (ringCanMultiplyByPositive {_} {_} {1/2} (halvePositive 1/2 (<WellDefined (Equivalence.reflexive eq) (Equivalence.symmetric eq pr1/2) (0<1 λ bad → irreflexive {0R} (<WellDefined (Equivalence.reflexive eq) (Equivalence.symmetric eq bad) 0<1')))) 2x<y)
... | inl (inr 1<0) = <WellDefined (halfHalves 1/2 pr1/2) (Equivalence.reflexive eq) (ringCanMultiplyByPositive {_} {_} {1/2} (halvePositive 1/2 (<WellDefined (Equivalence.reflexive eq) (Equivalence.symmetric eq pr1/2) (0<1 λ bad → irreflexive {0R} (<WellDefined (Equivalence.symmetric eq bad) (Equivalence.reflexive eq) 1<0)))) 2x<y)
... | inr 0=1 = exFalso (irreflexive {0R} (<WellDefined (oneZeroImpliesAllZero R 0=1) (oneZeroImpliesAllZero R 0=1) 2x<y))
clearDenominatorHalf' : (x y 1/2 : A) → (1/2 + 1/2 ∼ 1R) → (x * 1/2) < y → x < (y + y)
clearDenominatorHalf' x y 1/2 pr1/2 1/2x<y = <WellDefined (Equivalence.transitive eq (Equivalence.symmetric eq *DistributesOver+) (Equivalence.transitive eq (Equivalence.transitive eq *Commutative (*WellDefined pr1/2 (Equivalence.reflexive eq))) identIsIdent)) (Equivalence.reflexive eq) (ringAddInequalities 1/2x<y 1/2x<y)
halveInequality' : (x y 1/2 : A) → (1/2 + 1/2 ∼ 1R) → x < (y + y) → (x * 1/2) < y
halveInequality' x y 1/2 pr1/2 x<2y with halveInequality (inverse y) (inverse x) 1/2 pr1/2 (<WellDefined (invContravariant additiveGroup) (Equivalence.reflexive eq) (ringSwapNegatives' x<2y))
... | bl = ringSwapNegatives (<WellDefined (Equivalence.reflexive eq) (ringMinusExtracts' R) bl)
halveInequality : (x y 1/2 : A) → (1/2 + 1/2 ∼ 1R) → (x + x) < y → x < (y * 1/2)
halveInequality x y 1/2 pr1/2 2x<y with SetoidTotalOrder.totality tOrder 0R 1R
... | inl (inl 0<1') = <WellDefined (halfHalves 1/2 pr1/2) (Equivalence.reflexive eq) (ringCanMultiplyByPositive {_} {_} {1/2} (halvePositive 1/2 (<WellDefined (Equivalence.reflexive eq) (Equivalence.symmetric eq pr1/2) (0<1 λ bad → irreflexive {0R} (<WellDefined (Equivalence.reflexive eq) (Equivalence.symmetric eq bad) 0<1')))) 2x<y)
... | inl (inr 1<0) = <WellDefined (halfHalves 1/2 pr1/2) (Equivalence.reflexive eq) (ringCanMultiplyByPositive {_} {_} {1/2} (halvePositive 1/2 (<WellDefined (Equivalence.reflexive eq) (Equivalence.symmetric eq pr1/2) (0<1 λ bad → irreflexive {0R} (<WellDefined (Equivalence.symmetric eq bad) (Equivalence.reflexive eq) 1<0)))) 2x<y)
... | inr 0=1 = exFalso (irreflexive {0R} (<WellDefined (oneZeroImpliesAllZero R 0=1) (oneZeroImpliesAllZero R 0=1) 2x<y))
dense : (charNot2 : ((1R + 1R) ∼ 0R) → False) {x y : A} → (x < y) → Sg A (λ i → (x < i) && (i < y))
dense charNot2 {x} {y} x<y with halve charNot2 1R
dense charNot2 {x} {y} x<y | 1/2 , pr1/2 = ((x + y) * 1/2) , (halveInequality x (x + y) 1/2 pr1/2 (<WellDefined (Equivalence.reflexive eq) groupIsAbelian (orderRespectsAddition x<y x)) ,, halveInequality' (x + y) y 1/2 pr1/2 (orderRespectsAddition x<y y))
halveInequality' : (x y 1/2 : A) → (1/2 + 1/2 ∼ 1R) → x < (y + y) → (x * 1/2) < y
halveInequality' x y 1/2 pr1/2 x<2y with halveInequality (inverse y) (inverse x) 1/2 pr1/2 (<WellDefined (invContravariant additiveGroup) (Equivalence.reflexive eq) (ringSwapNegatives' x<2y))
... | bl = ringSwapNegatives (<WellDefined (Equivalence.reflexive eq) (ringMinusExtracts' R) bl)
halfLess : (e/2 e : A) → (0<e : 0G < e) → (pr : e/2 + e/2 ∼ e) → e/2 < e
halfLess e/2 e 0<e pr with halvePositive e/2 (<WellDefined (Equivalence.reflexive eq) (Equivalence.symmetric eq pr) 0<e)
... | 0<e/2 = <WellDefined identLeft pr (orderRespectsAddition 0<e/2 e/2)
dense : (charNot2 : ((1R + 1R) ∼ 0R) → False) {x y : A} → (x < y) → Sg A (λ i → (x < i) && (i < y))
dense charNot2 {x} {y} x<y with halve charNot2 1R
dense charNot2 {x} {y} x<y | 1/2 , pr1/2 = ((x + y) * 1/2) , (halveInequality x (x + y) 1/2 pr1/2 (<WellDefined (Equivalence.reflexive eq) groupIsAbelian (orderRespectsAddition x<y x)) ,, halveInequality' (x + y) y 1/2 pr1/2 (orderRespectsAddition x<y y))
inversePositiveIsPositive : {a b : A} → (a * b) ∼ 1R → 0R < b → 0R < a
inversePositiveIsPositive {a} {b} ab=1 0<b with SetoidTotalOrder.totality tOrder 0R a
inversePositiveIsPositive {a} {b} ab=1 0<b | inl (inl 0<a) = 0<a
inversePositiveIsPositive {a} {b} ab=1 0<b | inl (inr a<0) with <WellDefined *Commutative (Equivalence.reflexive eq) (posTimesNeg _ _ 0<b a<0)
... | ab<0 = exFalso (1<0False (<WellDefined ab=1 (Equivalence.reflexive eq) ab<0))
inversePositiveIsPositive {a} {b} ab=1 0<b | inr 0=a = exFalso (irreflexive {0G} (<WellDefined (Equivalence.reflexive eq) (oneZeroImpliesAllZero R 0=1) 0<b))
where
0=1 : 0R ∼ 1R
0=1 = Equivalence.transitive eq (Equivalence.symmetric eq (Equivalence.transitive eq (*WellDefined (Equivalence.symmetric eq 0=a) (Equivalence.reflexive eq)) (Equivalence.transitive eq *Commutative timesZero))) ab=1
halfLess : (e/2 e : A) → (0<e : 0G < e) → (pr : e/2 + e/2 ∼ e) → e/2 < e
halfLess e/2 e 0<e pr with halvePositive e/2 (<WellDefined (Equivalence.reflexive eq) (Equivalence.symmetric eq pr) 0<e)
... | 0<e/2 = <WellDefined identLeft pr (orderRespectsAddition 0<e/2 e/2)
inversePositiveIsPositive : {a b : A} → (a * b) ∼ 1R → 0R < b → 0R < a
inversePositiveIsPositive {a} {b} ab=1 0<b with SetoidTotalOrder.totality tOrder 0R a
inversePositiveIsPositive {a} {b} ab=1 0<b | inl (inl 0<a) = 0<a
inversePositiveIsPositive {a} {b} ab=1 0<b | inl (inr a<0) with <WellDefined *Commutative (Equivalence.reflexive eq) (posTimesNeg _ _ 0<b a<0)
... | ab<0 = exFalso (1<0False (<WellDefined ab=1 (Equivalence.reflexive eq) ab<0))
inversePositiveIsPositive {a} {b} ab=1 0<b | inr 0=a = exFalso (irreflexive {0G} (<WellDefined (Equivalence.reflexive eq) (oneZeroImpliesAllZero R 0=1) 0<b))
where
0=1 : 0R ∼ 1R
0=1 = Equivalence.transitive eq (Equivalence.symmetric eq (Equivalence.transitive eq (*WellDefined (Equivalence.symmetric eq 0=a) (Equivalence.reflexive eq)) (Equivalence.transitive eq *Commutative timesZero))) ab=1

52
Rings/Lemmas.agda
View File

@@ -12,34 +12,36 @@ open import Sets.EquivalenceRelations
module Rings.Lemmas {a b : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ : A → A → A} {_*_ : A → A → A} (R : Ring S _+_ _*_) where
open Setoid S
open Ring R
open Group additiveGroup
abstract
ringMinusExtracts : {x y : A} → Setoid._∼_ S (x * Group.inverse (Ring.additiveGroup R) y) (Group.inverse (Ring.additiveGroup R) (x * y))
ringMinusExtracts {x = x} {y} = transferToRight' additiveGroup (transitive (symmetric *DistributesOver+) (transitive (*WellDefined reflexive invLeft) (Ring.timesZero R)))
where
open Equivalence eq
open Setoid S
open Ring R
open Group additiveGroup
ringMinusExtracts' : {x y : A} → ((inverse x) * y) ∼ inverse (x * y)
ringMinusExtracts' {x = x} {y} = transitive *Commutative (transitive ringMinusExtracts (inverseWellDefined additiveGroup *Commutative))
where
open Equivalence eq
ringMinusExtracts : {x y : A} → Setoid._∼_ S (x * Group.inverse (Ring.additiveGroup R) y) (Group.inverse (Ring.additiveGroup R) (x * y))
ringMinusExtracts {x = x} {y} = transferToRight' additiveGroup (transitive (symmetric *DistributesOver+) (transitive (*WellDefined reflexive invLeft) (Ring.timesZero R)))
where
open Equivalence eq
twoNegativesTimes : {a b : A} → (inverse a) * (inverse b) ∼ a * b
twoNegativesTimes {a} {b} = transitive (ringMinusExtracts) (transitive (inverseWellDefined additiveGroup ringMinusExtracts') (invTwice additiveGroup (a * b)))
where
open Equivalence eq
ringMinusExtracts' : {x y : A} → ((inverse x) * y) ∼ inverse (x * y)
ringMinusExtracts' {x = x} {y} = transitive *Commutative (transitive ringMinusExtracts (inverseWellDefined additiveGroup *Commutative))
where
open Equivalence eq
groupLemmaMove0G : {a b : _} → {A : Set a} → {_·_ : A → A → A} → {S : Setoid {a} {b} A} → (G : Group S _·_) → {x : A} → (Setoid._∼_ S (Group.0G G) (Group.inverse G x)) → Setoid._∼_ S x (Group.0G G)
groupLemmaMove0G {S = S} G {x} pr = transitive (symmetric (invInv G)) (transitive (symmetric p) (invIdent G))
where
open Equivalence (Setoid.eq S)
p : Setoid._∼_ S (Group.inverse G (Group.0G G)) (Group.inverse G (Group.inverse G x))
p = inverseWellDefined G pr
twoNegativesTimes : {a b : A} → (inverse a) * (inverse b) ∼ a * b
twoNegativesTimes {a} {b} = transitive (ringMinusExtracts) (transitive (inverseWellDefined additiveGroup ringMinusExtracts') (invTwice additiveGroup (a * b)))
where
open Equivalence eq
groupLemmaMove0G' : {a b : _} → {A : Set a} → {_·_ : A → A → A} → {S : Setoid {a} {b} A} → (G : Group S _·_) → {x : A} → Setoid._∼_ S x (Group.0G G) → (Setoid._∼_ S (Group.0G G) (Group.inverse G x))
groupLemmaMove0G' {S = S} G {x} pr = transferToRight' G (Equivalence.transitive (Setoid.eq S) (Group.identLeft G) pr)
groupLemmaMove0G : {a b : _} → {A : Set a} → {_·_ : A → A → A} → {S : Setoid {a} {b} A} → (G : Group S _·_) → {x : A} → (Setoid._∼_ S (Group.0G G) (Group.inverse G x)) → Setoid._∼_ S x (Group.0G G)
groupLemmaMove0G {S = S} G {x} pr = transitive (symmetric (invInv G)) (transitive (symmetric p) (invIdent G))
where
open Equivalence (Setoid.eq S)
p : Setoid._∼_ S (Group.inverse G (Group.0G G)) (Group.inverse G (Group.inverse G x))
p = inverseWellDefined G pr
oneZeroImpliesAllZero : 0R ∼ 1R → {x : A} → x ∼ 0R
oneZeroImpliesAllZero 0=1 = Equivalence.transitive eq (Equivalence.symmetric eq identIsIdent) (Equivalence.transitive eq (*WellDefined (Equivalence.symmetric eq 0=1) (Equivalence.reflexive eq)) (Equivalence.transitive eq *Commutative timesZero))
groupLemmaMove0G' : {a b : _} → {A : Set a} → {_·_ : A → A → A} → {S : Setoid {a} {b} A} → (G : Group S _·_) → {x : A} → Setoid._∼_ S x (Group.0G G) → (Setoid._∼_ S (Group.0G G) (Group.inverse G x))
groupLemmaMove0G' {S = S} G {x} pr = transferToRight' G (Equivalence.transitive (Setoid.eq S) (Group.identLeft G) pr)
oneZeroImpliesAllZero : 0R ∼ 1R → {x : A} → x ∼ 0R
oneZeroImpliesAllZero 0=1 = Equivalence.transitive eq (Equivalence.symmetric eq identIsIdent) (Equivalence.transitive eq (*WellDefined (Equivalence.symmetric eq 0=1) (Equivalence.reflexive eq)) (Equivalence.transitive eq *Commutative timesZero))

30
Rings/Orders/Definition.agda
View File

@@ -28,17 +28,19 @@ record OrderedRing {p : _} {_<_ : Rel {_} {p} A} {pOrder : SetoidPartialOrder S
abs a | inl (inl 0<a) = a
abs a | inl (inr a<0) = inverse a
abs a | inr 0=a = a
absWellDefined : (a b : A) → a ∼ b → abs a ∼ abs b
absWellDefined a b a=b with SetoidTotalOrder.totality order 0R a
absWellDefined a b a=b | inl (inl 0<a) with SetoidTotalOrder.totality order 0R b
absWellDefined a b a=b | inl (inl 0<a) | inl (inl 0<b) = a=b
absWellDefined a b a=b | inl (inl 0<a) | inl (inr b<0) = exFalso (irreflexive {0G} (transitive 0<a (<WellDefined (Equivalence.symmetric eq a=b) (Equivalence.reflexive eq) b<0)))
absWellDefined a b a=b | inl (inl 0<a) | inr 0=b = exFalso (irreflexive {0G} (<WellDefined (Equivalence.reflexive eq) (Equivalence.transitive eq a=b (Equivalence.symmetric eq 0=b)) 0<a))
absWellDefined a b a=b | inl (inr a<0) with SetoidTotalOrder.totality order 0R b
absWellDefined a b a=b | inl (inr a<0) | inl (inl 0<b) = exFalso (irreflexive {0G} (transitive 0<b (<WellDefined a=b (Equivalence.reflexive eq) a<0)))
absWellDefined a b a=b | inl (inr a<0) | inl (inr b<0) = inverseWellDefined additiveGroup a=b
absWellDefined a b a=b | inl (inr a<0) | inr 0=b = exFalso (irreflexive {0G} (<WellDefined (Equivalence.transitive eq a=b (Equivalence.symmetric eq 0=b)) (Equivalence.reflexive eq) a<0))
absWellDefined a b a=b | inr 0=a with SetoidTotalOrder.totality order 0R b
absWellDefined a b a=b | inr 0=a | inl (inl 0<b) = exFalso (irreflexive {0G} (<WellDefined (Equivalence.reflexive eq) (Equivalence.symmetric eq (Equivalence.transitive eq 0=a a=b)) 0<b))
absWellDefined a b a=b | inr 0=a | inl (inr b<0) = exFalso (irreflexive {0G} (<WellDefined (Equivalence.symmetric eq (Equivalence.transitive eq 0=a a=b)) (Equivalence.reflexive eq) b<0))
absWellDefined a b a=b | inr 0=a | inr 0=b = a=b
abstract
absWellDefined : (a b : A) → a ∼ b → abs a ∼ abs b
absWellDefined a b a=b with SetoidTotalOrder.totality order 0R a
absWellDefined a b a=b | inl (inl 0<a) with SetoidTotalOrder.totality order 0R b
absWellDefined a b a=b | inl (inl 0<a) | inl (inl 0<b) = a=b
absWellDefined a b a=b | inl (inl 0<a) | inl (inr b<0) = exFalso (irreflexive {0G} (transitive 0<a (<WellDefined (Equivalence.symmetric eq a=b) (Equivalence.reflexive eq) b<0)))
absWellDefined a b a=b | inl (inl 0<a) | inr 0=b = exFalso (irreflexive {0G} (<WellDefined (Equivalence.reflexive eq) (Equivalence.transitive eq a=b (Equivalence.symmetric eq 0=b)) 0<a))
absWellDefined a b a=b | inl (inr a<0) with SetoidTotalOrder.totality order 0R b
absWellDefined a b a=b | inl (inr a<0) | inl (inl 0<b) = exFalso (irreflexive {0G} (transitive 0<b (<WellDefined a=b (Equivalence.reflexive eq) a<0)))
absWellDefined a b a=b | inl (inr a<0) | inl (inr b<0) = inverseWellDefined additiveGroup a=b
absWellDefined a b a=b | inl (inr a<0) | inr 0=b = exFalso (irreflexive {0G} (<WellDefined (Equivalence.transitive eq a=b (Equivalence.symmetric eq 0=b)) (Equivalence.reflexive eq) a<0))
absWellDefined a b a=b | inr 0=a with SetoidTotalOrder.totality order 0R b
absWellDefined a b a=b | inr 0=a | inl (inl 0<b) = exFalso (irreflexive {0G} (<WellDefined (Equivalence.reflexive eq) (Equivalence.symmetric eq (Equivalence.transitive eq 0=a a=b)) 0<b))
absWellDefined a b a=b | inr 0=a | inl (inr b<0) = exFalso (irreflexive {0G} (<WellDefined (Equivalence.symmetric eq (Equivalence.transitive eq 0=a a=b)) (Equivalence.reflexive eq) b<0))
absWellDefined a b a=b | inr 0=a | inr 0=b = a=b

656
Rings/Orders/Lemmas.agda
View File

@@ -16,364 +16,372 @@ open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
module Rings.Orders.Lemmas {n m p : _} {A : Set n} {S : Setoid {n} {m} A} {_+_ : A → A → A} {_*_ : A → A → A} {_<_ : Rel {_} {p} A} {R : Ring S _+_ _*_} {pOrder : SetoidPartialOrder S _<_} {tOrder : SetoidTotalOrder pOrder} (order : OrderedRing R tOrder) where
open OrderedRing order
open Setoid S
open SetoidPartialOrder pOrder
open SetoidTotalOrder tOrder
open Ring R
open Group additiveGroup
abstract
open import Rings.Lemmas R
open OrderedRing order
open Setoid S
open SetoidPartialOrder pOrder
open SetoidTotalOrder tOrder
open Ring R
open Group additiveGroup
ringAddInequalities : {w x y z : A} → w < x → y < z → (w + y) < (x + z)
ringAddInequalities {w = w} {x} {y} {z} w<x y<z = transitive (orderRespectsAddition w<x y) (<WellDefined groupIsAbelian groupIsAbelian (orderRespectsAddition y<z x))
open import Rings.Lemmas R
lemm2 : (a : A) → a < 0G → 0G < inverse a
lemm2 a a<0 with SetoidTotalOrder.totality tOrder 0R (inverse a)
lemm2 a a<0 | inl (inl 0<-a) = 0<-a
lemm2 a a<0 | inl (inr -a<0) = exFalso (irreflexive {0G} (SetoidPartialOrder.transitive pOrder (<WellDefined (invLeft {a}) (identLeft {a}) (orderRespectsAddition -a<0 a)) a<0))
lemm2 a a<0 | inr 0=-a = exFalso (irreflexive {0G} (<WellDefined (Equivalence.transitive eq (Equivalence.symmetric eq identRight) t) (Equivalence.reflexive eq) a<0))
where
t : a + 0G ∼ 0G
t = Equivalence.transitive eq (+WellDefined (Equivalence.reflexive eq) 0=-a) (invRight {a})
ringAddInequalities : {w x y z : A} → w < x → y < z → (w + y) < (x + z)
ringAddInequalities {w = w} {x} {y} {z} w<x y<z = transitive (orderRespectsAddition w<x y) (<WellDefined groupIsAbelian groupIsAbelian (orderRespectsAddition y<z x))
lemm2' : (a : A) → 0G < a → inverse a < 0G
lemm2' a 0<a with SetoidTotalOrder.totality tOrder 0R (inverse a)
lemm2' a 0<a | inl (inl 0<-a) = exFalso (irreflexive {0G} (SetoidPartialOrder.transitive pOrder 0<a (<WellDefined (identLeft {a}) (invLeft {a}) (orderRespectsAddition 0<-a a))))
lemm2' a 0<a | inl (inr -a<0) = -a<0
lemm2' a 0<a | inr 0=-a = exFalso (irreflexive {0G} (<WellDefined (Equivalence.reflexive eq) (Equivalence.transitive eq (Equivalence.symmetric eq identRight) t) 0<a))
where
t : a + 0G ∼ 0G
t = Equivalence.transitive eq (+WellDefined (Equivalence.reflexive eq) 0=-a) (invRight {a})
lemm2 : (a : A) → a < 0G → 0G < inverse a
lemm2 a a<0 with SetoidTotalOrder.totality tOrder 0R (inverse a)
lemm2 a a<0 | inl (inl 0<-a) = 0<-a
lemm2 a a<0 | inl (inr -a<0) = exFalso (irreflexive {0G} (SetoidPartialOrder.transitive pOrder (<WellDefined (invLeft {a}) (identLeft {a}) (orderRespectsAddition -a<0 a)) a<0))
lemm2 a a<0 | inr 0=-a = exFalso (irreflexive {0G} (<WellDefined (Equivalence.transitive eq (Equivalence.symmetric eq identRight) t) (Equivalence.reflexive eq) a<0))
where
t : a + 0G ∼ 0G
t = Equivalence.transitive eq (+WellDefined (Equivalence.reflexive eq) 0=-a) (invRight {a})
lemm3 : (a b : A) → 0G ∼ (a + b) → 0G ∼ a → 0G ∼ b
lemm3 a b pr1 pr2 with transferToRight' additiveGroup (Equivalence.symmetric eq pr1)
... | a=-b with Equivalence.transitive eq pr2 a=-b
... | 0=-b with inverseWellDefined additiveGroup 0=-b
... | -0=--b = Equivalence.transitive eq (Equivalence.symmetric eq (invIdentity additiveGroup)) (Equivalence.transitive eq -0=--b (invTwice additiveGroup b))
lemm2' : (a : A) → 0G < a → inverse a < 0G
lemm2' a 0<a with SetoidTotalOrder.totality tOrder 0R (inverse a)
lemm2' a 0<a | inl (inl 0<-a) = exFalso (irreflexive {0G} (SetoidPartialOrder.transitive pOrder 0<a (<WellDefined (identLeft {a}) (invLeft {a}) (orderRespectsAddition 0<-a a))))
lemm2' a 0<a | inl (inr -a<0) = -a<0
lemm2' a 0<a | inr 0=-a = exFalso (irreflexive {0G} (<WellDefined (Equivalence.reflexive eq) (Equivalence.transitive eq (Equivalence.symmetric eq identRight) t) 0<a))
where
t : a + 0G ∼ 0G
t = Equivalence.transitive eq (+WellDefined (Equivalence.reflexive eq) 0=-a) (invRight {a})
lemm3 : (a b : A) → 0G ∼ (a + b) → 0G ∼ a → 0G ∼ b
lemm3 a b pr1 pr2 with transferToRight' additiveGroup (Equivalence.symmetric eq pr1)
... | a=-b with Equivalence.transitive eq pr2 a=-b
... | 0=-b with inverseWellDefined additiveGroup 0=-b
... | -0=--b = Equivalence.transitive eq (Equivalence.symmetric eq (invIdentity additiveGroup)) (Equivalence.transitive eq -0=--b (invTwice additiveGroup b))
triangleInequality : (a b : A) → ((abs (a + b)) < ((abs a) + (abs b))) || (abs (a + b) ∼ (abs a) + (abs b))
triangleInequality a b with totality 0R (a + b)
triangleInequality a b | inl (inl 0<a+b) with totality 0R a
triangleInequality a b | inl (inl 0<a+b) | inl (inl 0<a) with totality 0R b
triangleInequality a b | inl (inl 0<a+b) | inl (inl 0<a) | inl (inl 0<b) = inr (Equivalence.reflexive eq)
triangleInequality a b | inl (inl 0<a+b) | inl (inl 0<a) | inl (inr b<0) = inl (<WellDefined groupIsAbelian groupIsAbelian (orderRespectsAddition (SetoidPartialOrder.transitive pOrder b<0 (lemm2 b b<0)) a))
triangleInequality a b | inl (inl 0<a+b) | inl (inl 0<a) | inr 0=b = inr (Equivalence.reflexive eq)
triangleInequality a b | inl (inl 0<a+b) | inl (inr a<0) with totality 0R b
triangleInequality a b | inl (inl 0<a+b) | inl (inr a<0) | inl (inl 0<b) = inl (orderRespectsAddition (SetoidPartialOrder.transitive pOrder a<0 (lemm2 a a<0)) b)
triangleInequality a b | inl (inl 0<a+b) | inl (inr a<0) | inl (inr b<0) = exFalso (irreflexive {0G} (SetoidPartialOrder.transitive pOrder 0<a+b (<WellDefined (Equivalence.reflexive eq) identLeft (ringAddInequalities a<0 b<0))))
triangleInequality a b | inl (inl 0<a+b) | inl (inr a<0) | inr 0=b = inl (orderRespectsAddition (SetoidPartialOrder.transitive pOrder a<0 (lemm2 a a<0)) b)
triangleInequality a b | inl (inl 0<a+b) | inr 0=a with totality 0R b
triangleInequality a b | inl (inl 0<a+b) | inr 0=a | inl (inl 0<b) = inr (Equivalence.reflexive eq)
triangleInequality a b | inl (inl 0<a+b) | inr 0=a | inl (inr b<0) = inl (<WellDefined groupIsAbelian groupIsAbelian (orderRespectsAddition (SetoidPartialOrder.transitive pOrder b<0 (lemm2 b b<0)) a))
triangleInequality a b | inl (inl 0<a+b) | inr 0=a | inr 0=b = inr (Equivalence.reflexive eq)
triangleInequality a b | inl (inr a+b<0) with totality 0G a
triangleInequality a b | inl (inr a+b<0) | inl (inl 0<a) with totality 0G b
triangleInequality a b | inl (inr a+b<0) | inl (inl 0<a) | inl (inl 0<b) = exFalso (irreflexive {0G} (SetoidPartialOrder.transitive pOrder (<WellDefined identLeft (Equivalence.reflexive eq) (ringAddInequalities 0<a 0<b)) a+b<0))
triangleInequality a b | inl (inr a+b<0) | inl (inl 0<a) | inl (inr b<0) = inl (<WellDefined (Equivalence.transitive eq (Equivalence.symmetric eq (invContravariant additiveGroup)) (inverseWellDefined additiveGroup groupIsAbelian)) (Equivalence.reflexive eq) (orderRespectsAddition (SetoidPartialOrder.transitive pOrder (lemm2' _ 0<a) 0<a) (inverse b)))
triangleInequality a b | inl (inr a+b<0) | inl (inl 0<a) | inr 0=b = exFalso (irreflexive {0G} (SetoidPartialOrder.transitive pOrder 0<a (<WellDefined (Equivalence.transitive eq (+WellDefined (Equivalence.reflexive eq) (Equivalence.symmetric eq 0=b)) identRight) (Equivalence.reflexive eq) a+b<0)))
triangleInequality a b | inl (inr a+b<0) | inl (inr a<0) with totality 0G b
triangleInequality a b | inl (inr a+b<0) | inl (inr a<0) | inl (inl 0<b) = inl (<WellDefined (Equivalence.symmetric eq (invContravariant additiveGroup)) groupIsAbelian (orderRespectsAddition (SetoidPartialOrder.transitive pOrder (lemm2' _ 0<b) 0<b) (inverse a)))
triangleInequality a b | inl (inr a+b<0) | inl (inr a<0) | inl (inr b<0) = inr (Equivalence.transitive eq (invContravariant additiveGroup) groupIsAbelian)
triangleInequality a b | inl (inr a+b<0) | inl (inr a<0) | inr 0=b = inr (Equivalence.transitive eq (invContravariant additiveGroup) (Equivalence.transitive eq (Equivalence.transitive eq (Equivalence.transitive eq (+WellDefined (Equivalence.transitive eq (inverseWellDefined additiveGroup (Equivalence.symmetric eq 0=b)) (invIdentity additiveGroup)) (Equivalence.reflexive eq)) identLeft) (Equivalence.symmetric eq identRight)) (+WellDefined (Equivalence.reflexive eq) 0=b)))
triangleInequality a b | inl (inr a+b<0) | inr 0=a with totality 0G b
triangleInequality a b | inl (inr a+b<0) | inr 0=a | inl (inl 0<b) = exFalso (irreflexive {0G} (SetoidPartialOrder.transitive pOrder 0<b (<WellDefined (Equivalence.transitive eq (+WellDefined (Equivalence.symmetric eq 0=a) (Equivalence.reflexive eq)) identLeft) (Equivalence.reflexive eq) a+b<0)))
triangleInequality a b | inl (inr a+b<0) | inr 0=a | inl (inr b<0) = inr (Equivalence.transitive eq (invContravariant additiveGroup) (Equivalence.transitive eq groupIsAbelian (+WellDefined (Equivalence.transitive eq (Equivalence.transitive eq (Equivalence.symmetric eq (inverseWellDefined additiveGroup 0=a)) (invIdentity additiveGroup)) 0=a) (Equivalence.reflexive eq))))
triangleInequality a b | inl (inr a+b<0) | inr 0=a | inr 0=b = exFalso (irreflexive {0G} (<WellDefined (Equivalence.transitive eq (+WellDefined (Equivalence.symmetric eq 0=a) (Equivalence.symmetric eq 0=b)) identLeft) (Equivalence.reflexive eq) a+b<0))
triangleInequality a b | inr 0=a+b with totality 0G a
triangleInequality a b | inr 0=a+b | inl (inl 0<a) with totality 0G b
triangleInequality a b | inr 0=a+b | inl (inl 0<a) | inl (inl 0<b) = exFalso (irreflexive {0G} (<WellDefined identLeft (Equivalence.symmetric eq 0=a+b) (ringAddInequalities 0<a 0<b)))
triangleInequality a b | inr 0=a+b | inl (inl 0<a) | inl (inr b<0) = inl (<WellDefined groupIsAbelian groupIsAbelian (orderRespectsAddition (SetoidPartialOrder.transitive pOrder b<0 (lemm2 _ b<0)) a))
triangleInequality a b | inr 0=a+b | inl (inl 0<a) | inr 0=b = exFalso (irreflexive {0G} (<WellDefined (Equivalence.reflexive eq) (Equivalence.symmetric eq (lemm3 _ _ (Equivalence.transitive eq 0=a+b groupIsAbelian) 0=b)) 0<a))
triangleInequality a b | inr 0=a+b | inl (inr a<0) with totality 0G b
triangleInequality a b | inr 0=a+b | inl (inr a<0) | inl (inl 0<b) = inl (orderRespectsAddition (SetoidPartialOrder.transitive pOrder a<0 (lemm2 _ a<0)) b)
triangleInequality a b | inr 0=a+b | inl (inr a<0) | inl (inr b<0) = exFalso (irreflexive {0G} (<WellDefined (Equivalence.symmetric eq 0=a+b) identLeft (ringAddInequalities a<0 b<0)))
triangleInequality a b | inr 0=a+b | inl (inr a<0) | inr 0=b = exFalso (irreflexive {0G} (<WellDefined (Equivalence.symmetric eq (lemm3 _ _ (Equivalence.transitive eq 0=a+b groupIsAbelian) 0=b)) (Equivalence.reflexive eq) a<0))
triangleInequality a b | inr 0=a+b | inr 0=a with totality 0G b
triangleInequality a b | inr 0=a+b | inr 0=a | inl (inl 0<b) = exFalso (irreflexive {0G} (<WellDefined (Equivalence.reflexive eq) (Equivalence.symmetric eq (lemm3 a b 0=a+b 0=a)) 0<b))
triangleInequality a b | inr 0=a+b | inr 0=a | inl (inr b<0) = exFalso (irreflexive {0G} (<WellDefined (Equivalence.symmetric eq (lemm3 a b 0=a+b 0=a)) (Equivalence.reflexive eq) b<0))
triangleInequality a b | inr 0=a+b | inr 0=a | inr 0=b = inr (Equivalence.reflexive eq)
triangleInequality : (a b : A) → ((abs (a + b)) < ((abs a) + (abs b))) || (abs (a + b) ∼ (abs a) + (abs b))
triangleInequality a b with totality 0R (a + b)
triangleInequality a b | inl (inl 0<a+b) with totality 0R a
triangleInequality a b | inl (inl 0<a+b) | inl (inl 0<a) with totality 0R b
triangleInequality a b | inl (inl 0<a+b) | inl (inl 0<a) | inl (inl 0<b) = inr (Equivalence.reflexive eq)
triangleInequality a b | inl (inl 0<a+b) | inl (inl 0<a) | inl (inr b<0) = inl (<WellDefined groupIsAbelian groupIsAbelian (orderRespectsAddition (SetoidPartialOrder.transitive pOrder b<0 (lemm2 b b<0)) a))
triangleInequality a b | inl (inl 0<a+b) | inl (inl 0<a) | inr 0=b = inr (Equivalence.reflexive eq)
triangleInequality a b | inl (inl 0<a+b) | inl (inr a<0) with totality 0R b
triangleInequality a b | inl (inl 0<a+b) | inl (inr a<0) | inl (inl 0<b) = inl (orderRespectsAddition (SetoidPartialOrder.transitive pOrder a<0 (lemm2 a a<0)) b)
triangleInequality a b | inl (inl 0<a+b) | inl (inr a<0) | inl (inr b<0) = exFalso (irreflexive {0G} (SetoidPartialOrder.transitive pOrder 0<a+b (<WellDefined (Equivalence.reflexive eq) identLeft (ringAddInequalities a<0 b<0))))
triangleInequality a b | inl (inl 0<a+b) | inl (inr a<0) | inr 0=b = inl (orderRespectsAddition (SetoidPartialOrder.transitive pOrder a<0 (lemm2 a a<0)) b)
triangleInequality a b | inl (inl 0<a+b) | inr 0=a with totality 0R b
triangleInequality a b | inl (inl 0<a+b) | inr 0=a | inl (inl 0<b) = inr (Equivalence.reflexive eq)
triangleInequality a b | inl (inl 0<a+b) | inr 0=a | inl (inr b<0) = inl (<WellDefined groupIsAbelian groupIsAbelian (orderRespectsAddition (SetoidPartialOrder.transitive pOrder b<0 (lemm2 b b<0)) a))
triangleInequality a b | inl (inl 0<a+b) | inr 0=a | inr 0=b = inr (Equivalence.reflexive eq)
triangleInequality a b | inl (inr a+b<0) with totality 0G a
triangleInequality a b | inl (inr a+b<0) | inl (inl 0<a) with totality 0G b
triangleInequality a b | inl (inr a+b<0) | inl (inl 0<a) | inl (inl 0<b) = exFalso (irreflexive {0G} (SetoidPartialOrder.transitive pOrder (<WellDefined identLeft (Equivalence.reflexive eq) (ringAddInequalities 0<a 0<b)) a+b<0))
triangleInequality a b | inl (inr a+b<0) | inl (inl 0<a) | inl (inr b<0) = inl (<WellDefined (Equivalence.transitive eq (Equivalence.symmetric eq (invContravariant additiveGroup)) (inverseWellDefined additiveGroup groupIsAbelian)) (Equivalence.reflexive eq) (orderRespectsAddition (SetoidPartialOrder.transitive pOrder (lemm2' _ 0<a) 0<a) (inverse b)))
triangleInequality a b | inl (inr a+b<0) | inl (inl 0<a) | inr 0=b = exFalso (irreflexive {0G} (SetoidPartialOrder.transitive pOrder 0<a (<WellDefined (Equivalence.transitive eq (+WellDefined (Equivalence.reflexive eq) (Equivalence.symmetric eq 0=b)) identRight) (Equivalence.reflexive eq) a+b<0)))
triangleInequality a b | inl (inr a+b<0) | inl (inr a<0) with totality 0G b
triangleInequality a b | inl (inr a+b<0) | inl (inr a<0) | inl (inl 0<b) = inl (<WellDefined (Equivalence.symmetric eq (invContravariant additiveGroup)) groupIsAbelian (orderRespectsAddition (SetoidPartialOrder.transitive pOrder (lemm2' _ 0<b) 0<b) (inverse a)))
triangleInequality a b | inl (inr a+b<0) | inl (inr a<0) | inl (inr b<0) = inr (Equivalence.transitive eq (invContravariant additiveGroup) groupIsAbelian)
triangleInequality a b | inl (inr a+b<0) | inl (inr a<0) | inr 0=b = inr (Equivalence.transitive eq (invContravariant additiveGroup) (Equivalence.transitive eq (Equivalence.transitive eq (Equivalence.transitive eq (+WellDefined (Equivalence.transitive eq (inverseWellDefined additiveGroup (Equivalence.symmetric eq 0=b)) (invIdentity additiveGroup)) (Equivalence.reflexive eq)) identLeft) (Equivalence.symmetric eq identRight)) (+WellDefined (Equivalence.reflexive eq) 0=b)))
triangleInequality a b | inl (inr a+b<0) | inr 0=a with totality 0G b
triangleInequality a b | inl (inr a+b<0) | inr 0=a | inl (inl 0<b) = exFalso (irreflexive {0G} (SetoidPartialOrder.transitive pOrder 0<b (<WellDefined (Equivalence.transitive eq (+WellDefined (Equivalence.symmetric eq 0=a) (Equivalence.reflexive eq)) identLeft) (Equivalence.reflexive eq) a+b<0)))
triangleInequality a b | inl (inr a+b<0) | inr 0=a | inl (inr b<0) = inr (Equivalence.transitive eq (invContravariant additiveGroup) (Equivalence.transitive eq groupIsAbelian (+WellDefined (Equivalence.transitive eq (Equivalence.transitive eq (Equivalence.symmetric eq (inverseWellDefined additiveGroup 0=a)) (invIdentity additiveGroup)) 0=a) (Equivalence.reflexive eq))))
triangleInequality a b | inl (inr a+b<0) | inr 0=a | inr 0=b = exFalso (irreflexive {0G} (<WellDefined (Equivalence.transitive eq (+WellDefined (Equivalence.symmetric eq 0=a) (Equivalence.symmetric eq 0=b)) identLeft) (Equivalence.reflexive eq) a+b<0))
triangleInequality a b | inr 0=a+b with totality 0G a
triangleInequality a b | inr 0=a+b | inl (inl 0<a) with totality 0G b
triangleInequality a b | inr 0=a+b | inl (inl 0<a) | inl (inl 0<b) = exFalso (irreflexive {0G} (<WellDefined identLeft (Equivalence.symmetric eq 0=a+b) (ringAddInequalities 0<a 0<b)))
triangleInequality a b | inr 0=a+b | inl (inl 0<a) | inl (inr b<0) = inl (<WellDefined groupIsAbelian groupIsAbelian (orderRespectsAddition (SetoidPartialOrder.transitive pOrder b<0 (lemm2 _ b<0)) a))
triangleInequality a b | inr 0=a+b | inl (inl 0<a) | inr 0=b = exFalso (irreflexive {0G} (<WellDefined (Equivalence.reflexive eq) (Equivalence.symmetric eq (lemm3 _ _ (Equivalence.transitive eq 0=a+b groupIsAbelian) 0=b)) 0<a))
triangleInequality a b | inr 0=a+b | inl (inr a<0) with totality 0G b
triangleInequality a b | inr 0=a+b | inl (inr a<0) | inl (inl 0<b) = inl (orderRespectsAddition (SetoidPartialOrder.transitive pOrder a<0 (lemm2 _ a<0)) b)
triangleInequality a b | inr 0=a+b | inl (inr a<0) | inl (inr b<0) = exFalso (irreflexive {0G} (<WellDefined (Equivalence.symmetric eq 0=a+b) identLeft (ringAddInequalities a<0 b<0)))
triangleInequality a b | inr 0=a+b | inl (inr a<0) | inr 0=b = exFalso (irreflexive {0G} (<WellDefined (Equivalence.symmetric eq (lemm3 _ _ (Equivalence.transitive eq 0=a+b groupIsAbelian) 0=b)) (Equivalence.reflexive eq) a<0))
triangleInequality a b | inr 0=a+b | inr 0=a with totality 0G b
triangleInequality a b | inr 0=a+b | inr 0=a | inl (inl 0<b) = exFalso (irreflexive {0G} (<WellDefined (Equivalence.reflexive eq) (Equivalence.symmetric eq (lemm3 a b 0=a+b 0=a)) 0<b))
triangleInequality a b | inr 0=a+b | inr 0=a | inl (inr b<0) = exFalso (irreflexive {0G} (<WellDefined (Equivalence.symmetric eq (lemm3 a b 0=a+b 0=a)) (Equivalence.reflexive eq) b<0))
triangleInequality a b | inr 0=a+b | inr 0=a | inr 0=b = inr (Equivalence.reflexive eq)
ringMinusFlipsOrder : {x : A} → (Ring.0R R) < x → (Group.inverse (Ring.additiveGroup R) x) < (Ring.0R R)
ringMinusFlipsOrder {x = x} 0<x with SetoidTotalOrder.totality tOrder (Ring.0R R) (Group.inverse (Ring.additiveGroup R) x)
ringMinusFlipsOrder {x} 0<x | inl (inl 0<inv) = exFalso (SetoidPartialOrder.irreflexive pOrder bad')
where
bad : (Group.0G (Ring.additiveGroup R) + Group.0G (Ring.additiveGroup R)) < (x + Group.inverse (Ring.additiveGroup R) x)
bad = ringAddInequalities 0<x 0<inv
bad' : (Group.0G (Ring.additiveGroup R)) < (Group.0G (Ring.additiveGroup R))
bad' = SetoidPartialOrder.<WellDefined pOrder (Group.identRight (Ring.additiveGroup R)) (Group.invRight (Ring.additiveGroup R)) bad
ringMinusFlipsOrder {x} 0<x | inl (inr inv<0) = inv<0
ringMinusFlipsOrder {x} 0<x | inr 0=inv = exFalso (SetoidPartialOrder.irreflexive pOrder (SetoidPartialOrder.<WellDefined pOrder (Equivalence.reflexive (Setoid.eq S)) (groupLemmaMove0G (Ring.additiveGroup R) 0=inv) 0<x))
ringMinusFlipsOrder : {x : A} → (Ring.0R R) < x → (Group.inverse (Ring.additiveGroup R) x) < (Ring.0R R)
ringMinusFlipsOrder {x = x} 0<x with SetoidTotalOrder.totality tOrder (Ring.0R R) (Group.inverse (Ring.additiveGroup R) x)
ringMinusFlipsOrder {x} 0<x | inl (inl 0<inv) = exFalso (SetoidPartialOrder.irreflexive pOrder bad')
where
bad : (Group.0G (Ring.additiveGroup R) + Group.0G (Ring.additiveGroup R)) < (x + Group.inverse (Ring.additiveGroup R) x)
bad = ringAddInequalities 0<x 0<inv
bad' : (Group.0G (Ring.additiveGroup R)) < (Group.0G (Ring.additiveGroup R))
bad' = SetoidPartialOrder.<WellDefined pOrder (Group.identRight (Ring.additiveGroup R)) (Group.invRight (Ring.additiveGroup R)) bad
ringMinusFlipsOrder {x} 0<x | inl (inr inv<0) = inv<0
ringMinusFlipsOrder {x} 0<x | inr 0=inv = exFalso (SetoidPartialOrder.irreflexive pOrder (SetoidPartialOrder.<WellDefined pOrder (Equivalence.reflexive (Setoid.eq S)) (groupLemmaMove0G (Ring.additiveGroup R) 0=inv) 0<x))
ringMinusFlipsOrder' : {x : A} → (Group.inverse (Ring.additiveGroup R) x) < (Ring.0R R) → (Ring.0R R) < x
ringMinusFlipsOrder' {x} -x<0 with SetoidTotalOrder.totality tOrder (Ring.0R R) x
ringMinusFlipsOrder' {x} -x<0 | inl (inl 0<x) = 0<x
ringMinusFlipsOrder' {x} -x<0 | inl (inr x<0) = exFalso (SetoidPartialOrder.irreflexive pOrder (SetoidPartialOrder.<WellDefined pOrder (Group.invLeft (Ring.additiveGroup R)) (Group.identRight (Ring.additiveGroup R)) bad))
where
bad : ((Group.inverse (Ring.additiveGroup R) x) + x) < (Group.0G (Ring.additiveGroup R) + Group.0G (Ring.additiveGroup R))
bad = ringAddInequalities -x<0 x<0
ringMinusFlipsOrder' {x} -x<0 | inr 0=x = exFalso (SetoidPartialOrder.irreflexive pOrder (SetoidPartialOrder.<WellDefined pOrder (symmetric (groupLemmaMove0G' (Ring.additiveGroup R) (symmetric 0=x))) (Equivalence.reflexive (Setoid.eq S)) -x<0))
where
open Equivalence eq
ringMinusFlipsOrder' : {x : A} → (Group.inverse (Ring.additiveGroup R) x) < (Ring.0R R) → (Ring.0R R) < x
ringMinusFlipsOrder' {x} -x<0 with SetoidTotalOrder.totality tOrder (Ring.0R R) x
ringMinusFlipsOrder' {x} -x<0 | inl (inl 0<x) = 0<x
ringMinusFlipsOrder' {x} -x<0 | inl (inr x<0) = exFalso (SetoidPartialOrder.irreflexive pOrder (SetoidPartialOrder.<WellDefined pOrder (Group.invLeft (Ring.additiveGroup R)) (Group.identRight (Ring.additiveGroup R)) bad))
where
bad : ((Group.inverse (Ring.additiveGroup R) x) + x) < (Group.0G (Ring.additiveGroup R) + Group.0G (Ring.additiveGroup R))
bad = ringAddInequalities -x<0 x<0
ringMinusFlipsOrder' {x} -x<0 | inr 0=x = exFalso (SetoidPartialOrder.irreflexive pOrder (SetoidPartialOrder.<WellDefined pOrder (symmetric (groupLemmaMove0G' (Ring.additiveGroup R) (symmetric 0=x))) (Equivalence.reflexive (Setoid.eq S)) -x<0))
where
open Equivalence eq
ringMinusFlipsOrder'' : {x : A} → x < (Ring.0R R) → (Ring.0R R) < Group.inverse (Ring.additiveGroup R) x
ringMinusFlipsOrder'' {x} x<0 = ringMinusFlipsOrder' (SetoidPartialOrder.<WellDefined pOrder {x} {Group.inverse (Ring.additiveGroup R) (Group.inverse (Ring.additiveGroup R) x)} {Ring.0R R} {Ring.0R R} (Equivalence.symmetric (Setoid.eq S) (invInv (Ring.additiveGroup R))) (Equivalence.reflexive (Setoid.eq S)) x<0)
ringMinusFlipsOrder'' : {x : A} → x < (Ring.0R R) → (Ring.0R R) < Group.inverse (Ring.additiveGroup R) x
ringMinusFlipsOrder'' {x} x<0 = ringMinusFlipsOrder' (SetoidPartialOrder.<WellDefined pOrder {x} {Group.inverse (Ring.additiveGroup R) (Group.inverse (Ring.additiveGroup R) x)} {Ring.0R R} {Ring.0R R} (Equivalence.symmetric (Setoid.eq S) (invInv (Ring.additiveGroup R))) (Equivalence.reflexive (Setoid.eq S)) x<0)
ringMinusFlipsOrder''' : {x : A} → (Ring.0R R) < (Group.inverse (Ring.additiveGroup R) x) → x < (Ring.0R R)
ringMinusFlipsOrder''' {x} 0<-x = SetoidPartialOrder.<WellDefined pOrder (invInv (Ring.additiveGroup R)) (Equivalence.reflexive (Setoid.eq S)) (ringMinusFlipsOrder 0<-x)
ringMinusFlipsOrder''' : {x : A} → (Ring.0R R) < (Group.inverse (Ring.additiveGroup R) x) → x < (Ring.0R R)
ringMinusFlipsOrder''' {x} 0<-x = SetoidPartialOrder.<WellDefined pOrder (invInv (Ring.additiveGroup R)) (Equivalence.reflexive (Setoid.eq S)) (ringMinusFlipsOrder 0<-x)
ringCanMultiplyByPositive : {x y c : A} → (Ring.0R R) < c → x < y → (x * c) < (y * c)
ringCanMultiplyByPositive {x} {y} {c} 0<c x<y = SetoidPartialOrder.<WellDefined pOrder reflexive (Group.identRight additiveGroup) q'
where
open Equivalence eq
have : 0R < (y + Group.inverse additiveGroup x)
have = SetoidPartialOrder.<WellDefined pOrder (Group.invRight additiveGroup) reflexive (OrderedRing.orderRespectsAddition order x<y (Group.inverse additiveGroup x))
p1 : 0R < ((y * c) + ((Group.inverse additiveGroup x) * c))
p1 = SetoidPartialOrder.<WellDefined pOrder reflexive (Equivalence.transitive eq *Commutative (Equivalence.transitive eq *DistributesOver+ ((Group.+WellDefined additiveGroup) *Commutative *Commutative))) (OrderedRing.orderRespectsMultiplication order have 0<c)
p' : 0R < ((y * c) + (Group.inverse additiveGroup (x * c)))
p' = SetoidPartialOrder.<WellDefined pOrder reflexive (Group.+WellDefined additiveGroup reflexive (Equivalence.transitive eq (Equivalence.transitive eq *Commutative ringMinusExtracts) (inverseWellDefined additiveGroup *Commutative))) p1
q : (0R + (x * c)) < (((y * c) + (Group.inverse additiveGroup (x * c))) + (x * c))
q = OrderedRing.orderRespectsAddition order p' (x * c)
q' : (x * c) < ((y * c) + 0R)
q' = SetoidPartialOrder.<WellDefined pOrder (Group.identLeft additiveGroup) (Equivalence.transitive eq (symmetric (Group.+Associative additiveGroup)) (Group.+WellDefined additiveGroup reflexive (Group.invLeft additiveGroup))) q
ringCanMultiplyByPositive : {x y c : A} → (Ring.0R R) < c → x < y → (x * c) < (y * c)
ringCanMultiplyByPositive {x} {y} {c} 0<c x<y = SetoidPartialOrder.<WellDefined pOrder reflexive (Group.identRight additiveGroup) q'
where
open Equivalence eq
have : 0R < (y + Group.inverse additiveGroup x)
have = SetoidPartialOrder.<WellDefined pOrder (Group.invRight additiveGroup) reflexive (OrderedRing.orderRespectsAddition order x<y (Group.inverse additiveGroup x))
p1 : 0R < ((y * c) + ((Group.inverse additiveGroup x) * c))
p1 = SetoidPartialOrder.<WellDefined pOrder reflexive (Equivalence.transitive eq *Commutative (Equivalence.transitive eq *DistributesOver+ ((Group.+WellDefined additiveGroup) *Commutative *Commutative))) (OrderedRing.orderRespectsMultiplication order have 0<c)
p' : 0R < ((y * c) + (Group.inverse additiveGroup (x * c)))
p' = SetoidPartialOrder.<WellDefined pOrder reflexive (Group.+WellDefined additiveGroup reflexive (Equivalence.transitive eq (Equivalence.transitive eq *Commutative ringMinusExtracts) (inverseWellDefined additiveGroup *Commutative))) p1
q : (0R + (x * c)) < (((y * c) + (Group.inverse additiveGroup (x * c))) + (x * c))
q = OrderedRing.orderRespectsAddition order p' (x * c)
q' : (x * c) < ((y * c) + 0R)
q' = SetoidPartialOrder.<WellDefined pOrder (Group.identLeft additiveGroup) (Equivalence.transitive eq (symmetric (Group.+Associative additiveGroup)) (Group.+WellDefined additiveGroup reflexive (Group.invLeft additiveGroup))) q
ringMultiplyPositives : {x y a b : A} → 0R < x → 0R < a → (x < y) → (a < b) → (x * a) < (y * b)
ringMultiplyPositives {x} {y} {a} {b} 0<x 0<a x<y a<b = SetoidPartialOrder.transitive pOrder (ringCanMultiplyByPositive 0<a x<y) (<WellDefined *Commutative *Commutative (ringCanMultiplyByPositive (SetoidPartialOrder.transitive pOrder 0<x x<y) a<b))
ringMultiplyPositives : {x y a b : A} → 0R < x → 0R < a → (x < y) → (a < b) → (x * a) < (y * b)
ringMultiplyPositives {x} {y} {a} {b} 0<x 0<a x<y a<b = SetoidPartialOrder.transitive pOrder (ringCanMultiplyByPositive 0<a x<y) (<WellDefined *Commutative *Commutative (ringCanMultiplyByPositive (SetoidPartialOrder.transitive pOrder 0<x x<y) a<b))
ringCanCancelPositive : {x y c : A} → (Ring.0R R) < c → (x * c) < (y * c) → x < y
ringCanCancelPositive {x} {y} {c} 0<c xc<yc = SetoidPartialOrder.<WellDefined pOrder (Group.identLeft additiveGroup) (Equivalence.transitive eq (symmetric (Group.+Associative additiveGroup)) (Equivalence.transitive eq (Group.+WellDefined additiveGroup reflexive (Group.invLeft additiveGroup)) (Group.identRight additiveGroup))) q''
where
open Equivalence (Setoid.eq S)
have : 0R < ((y * c) + (Group.inverse additiveGroup (x * c)))
have = SetoidPartialOrder.<WellDefined pOrder (Group.invRight additiveGroup) reflexive (OrderedRing.orderRespectsAddition order xc<yc (Group.inverse additiveGroup _))
p1 : 0R < ((y * c) + ((Group.inverse additiveGroup x) * c))
p1 = SetoidPartialOrder.<WellDefined pOrder reflexive (Group.+WellDefined additiveGroup reflexive (symmetric (Equivalence.transitive eq (*Commutative) (Equivalence.transitive eq ringMinusExtracts (inverseWellDefined additiveGroup *Commutative))))) have
q : 0R < ((y + Group.inverse additiveGroup x) * c)
q = SetoidPartialOrder.<WellDefined pOrder reflexive (Equivalence.transitive eq (Equivalence.transitive eq (Group.+WellDefined additiveGroup *Commutative *Commutative) (symmetric *DistributesOver+)) *Commutative) p1
q' : 0R < (y + Group.inverse additiveGroup x)
q' with SetoidTotalOrder.totality tOrder 0R (y + Group.inverse additiveGroup x)
q' | inl (inl pr) = pr
q' | inl (inr y-x<0) = exFalso (SetoidPartialOrder.irreflexive pOrder (SetoidPartialOrder.<WellDefined pOrder reflexive (Equivalence.transitive eq *Commutative (Ring.timesZero R)) k))
where
f : ((y + inverse x) + (inverse (y + inverse x))) < (0G + inverse (y + inverse x))
f = OrderedRing.orderRespectsAddition order y-x<0 _
g : 0G < inverse (y + inverse x)
g = SetoidPartialOrder.<WellDefined pOrder invRight identLeft f
h : (0G * c) < ((inverse (y + inverse x)) * c)
h = ringCanMultiplyByPositive 0<c g
i : (0R + (0G * c)) < (((y + inverse x) * c) + ((inverse (y + inverse x)) * c))
i = ringAddInequalities q h
j : 0R < (((y + inverse x) + (inverse (y + inverse x))) * c)
j = SetoidPartialOrder.<WellDefined pOrder (Equivalence.transitive eq identLeft (Equivalence.transitive eq *Commutative (Ring.timesZero R))) (symmetric (Equivalence.transitive eq *Commutative (Equivalence.transitive eq *DistributesOver+ (Group.+WellDefined additiveGroup *Commutative *Commutative)))) i
k : 0R < (0R * c)
k = SetoidPartialOrder.<WellDefined pOrder reflexive (*WellDefined invRight reflexive) j
q' | inr 0=y-x = exFalso (SetoidPartialOrder.irreflexive pOrder (SetoidPartialOrder.<WellDefined pOrder (*WellDefined x=y reflexive) reflexive xc<yc))
where
f : inverse 0G ∼ inverse (y + inverse x)
f = inverseWellDefined additiveGroup 0=y-x
g : 0G ∼ (inverse y) + x
g = Equivalence.transitive eq (symmetric (invIdentity additiveGroup)) (Equivalence.transitive eq f (Equivalence.transitive eq (Equivalence.transitive eq (invContravariant additiveGroup) groupIsAbelian) (+WellDefined reflexive (invInv additiveGroup))))
x=y : x ∼ y
x=y = transferToRight additiveGroup (symmetric (Equivalence.transitive eq g groupIsAbelian))
q'' : (0R + x) < ((y + Group.inverse additiveGroup x) + x)
q'' = OrderedRing.orderRespectsAddition order q' x
ringCanCancelPositive : {x y c : A} → (Ring.0R R) < c → (x * c) < (y * c) → x < y
ringCanCancelPositive {x} {y} {c} 0<c xc<yc = SetoidPartialOrder.<WellDefined pOrder (Group.identLeft additiveGroup) (Equivalence.transitive eq (symmetric (Group.+Associative additiveGroup)) (Equivalence.transitive eq (Group.+WellDefined additiveGroup reflexive (Group.invLeft additiveGroup)) (Group.identRight additiveGroup))) q''
where
open Equivalence (Setoid.eq S)
have : 0R < ((y * c) + (Group.inverse additiveGroup (x * c)))
have = SetoidPartialOrder.<WellDefined pOrder (Group.invRight additiveGroup) reflexive (OrderedRing.orderRespectsAddition order xc<yc (Group.inverse additiveGroup _))
p1 : 0R < ((y * c) + ((Group.inverse additiveGroup x) * c))
p1 = SetoidPartialOrder.<WellDefined pOrder reflexive (Group.+WellDefined additiveGroup reflexive (symmetric (Equivalence.transitive eq (*Commutative) (Equivalence.transitive eq ringMinusExtracts (inverseWellDefined additiveGroup *Commutative))))) have
q : 0R < ((y + Group.inverse additiveGroup x) * c)
q = SetoidPartialOrder.<WellDefined pOrder reflexive (Equivalence.transitive eq (Equivalence.transitive eq (Group.+WellDefined additiveGroup *Commutative *Commutative) (symmetric *DistributesOver+)) *Commutative) p1
q' : 0R < (y + Group.inverse additiveGroup x)
q' with SetoidTotalOrder.totality tOrder 0R (y + Group.inverse additiveGroup x)
q' | inl (inl pr) = pr
q' | inl (inr y-x<0) = exFalso (SetoidPartialOrder.irreflexive pOrder (SetoidPartialOrder.<WellDefined pOrder reflexive (Equivalence.transitive eq *Commutative (Ring.timesZero R)) k))
where
f : ((y + inverse x) + (inverse (y + inverse x))) < (0G + inverse (y + inverse x))
f = OrderedRing.orderRespectsAddition order y-x<0 _
g : 0G < inverse (y + inverse x)
g = SetoidPartialOrder.<WellDefined pOrder invRight identLeft f
h : (0G * c) < ((inverse (y + inverse x)) * c)
h = ringCanMultiplyByPositive 0<c g
i : (0R + (0G * c)) < (((y + inverse x) * c) + ((inverse (y + inverse x)) * c))
i = ringAddInequalities q h
j : 0R < (((y + inverse x) + (inverse (y + inverse x))) * c)
j = SetoidPartialOrder.<WellDefined pOrder (Equivalence.transitive eq identLeft (Equivalence.transitive eq *Commutative (Ring.timesZero R))) (symmetric (Equivalence.transitive eq *Commutative (Equivalence.transitive eq *DistributesOver+ (Group.+WellDefined additiveGroup *Commutative *Commutative)))) i
k : 0R < (0R * c)
k = SetoidPartialOrder.<WellDefined pOrder reflexive (*WellDefined invRight reflexive) j
q' | inr 0=y-x = exFalso (SetoidPartialOrder.irreflexive pOrder (SetoidPartialOrder.<WellDefined pOrder (*WellDefined x=y reflexive) reflexive xc<yc))
where
f : inverse 0G ∼ inverse (y + inverse x)
f = inverseWellDefined additiveGroup 0=y-x
g : 0G ∼ (inverse y) + x
g = Equivalence.transitive eq (symmetric (invIdentity additiveGroup)) (Equivalence.transitive eq f (Equivalence.transitive eq (Equivalence.transitive eq (invContravariant additiveGroup) groupIsAbelian) (+WellDefined reflexive (invInv additiveGroup))))
x=y : x ∼ y
x=y = transferToRight additiveGroup (symmetric (Equivalence.transitive eq g groupIsAbelian))
q'' : (0R + x) < ((y + Group.inverse additiveGroup x) + x)
q'' = OrderedRing.orderRespectsAddition order q' x
ringSwapNegatives : {x y : A} → (Group.inverse (Ring.additiveGroup R) x) < (Group.inverse (Ring.additiveGroup R) y) → y < x
ringSwapNegatives {x} {y} -x<-y = SetoidPartialOrder.<WellDefined pOrder (Equivalence.transitive eq (symmetric (Group.+Associative additiveGroup)) (Equivalence.transitive eq (Group.+WellDefined additiveGroup reflexive (Group.invLeft additiveGroup)) (Group.identRight additiveGroup))) (Group.identLeft additiveGroup) v
where
open Equivalence eq
t : ((Group.inverse additiveGroup x) + y) < ((Group.inverse additiveGroup y) + y)
t = OrderedRing.orderRespectsAddition order -x<-y y
u : (y + (Group.inverse additiveGroup x)) < 0R
u = SetoidPartialOrder.<WellDefined pOrder (groupIsAbelian) (Group.invLeft additiveGroup) t
v : ((y + (Group.inverse additiveGroup x)) + x) < (0R + x)
v = OrderedRing.orderRespectsAddition order u x
ringSwapNegatives : {x y : A} → (Group.inverse (Ring.additiveGroup R) x) < (Group.inverse (Ring.additiveGroup R) y) → y < x
ringSwapNegatives {x} {y} -x<-y = SetoidPartialOrder.<WellDefined pOrder (Equivalence.transitive eq (symmetric (Group.+Associative additiveGroup)) (Equivalence.transitive eq (Group.+WellDefined additiveGroup reflexive (Group.invLeft additiveGroup)) (Group.identRight additiveGroup))) (Group.identLeft additiveGroup) v
where
open Equivalence eq
t : ((Group.inverse additiveGroup x) + y) < ((Group.inverse additiveGroup y) + y)
t = OrderedRing.orderRespectsAddition order -x<-y y
u : (y + (Group.inverse additiveGroup x)) < 0R
u = SetoidPartialOrder.<WellDefined pOrder (groupIsAbelian) (Group.invLeft additiveGroup) t
v : ((y + (Group.inverse additiveGroup x)) + x) < (0R + x)
v = OrderedRing.orderRespectsAddition order u x
ringSwapNegatives' : {x y : A} → x < y → (Group.inverse (Ring.additiveGroup R) y) < (Group.inverse (Ring.additiveGroup R) x)
ringSwapNegatives' {x} {y} x<y = ringSwapNegatives (<WellDefined (Equivalence.symmetric eq (invTwice additiveGroup _)) (Equivalence.symmetric eq (invTwice additiveGroup _)) x<y)
ringSwapNegatives' : {x y : A} → x < y → (Group.inverse (Ring.additiveGroup R) y) < (Group.inverse (Ring.additiveGroup R) x)
ringSwapNegatives' {x} {y} x<y = ringSwapNegatives (<WellDefined (Equivalence.symmetric eq (invTwice additiveGroup _)) (Equivalence.symmetric eq (invTwice additiveGroup _)) x<y)
ringCanMultiplyByNegative : {x y c : A} → c < (Ring.0R R) → x < y → (y * c) < (x * c)
ringCanMultiplyByNegative {x} {y} {c} c<0 x<y = ringSwapNegatives u
where
open Equivalence eq
p1 : (c + Group.inverse additiveGroup c) < (0R + Group.inverse additiveGroup c)
p1 = OrderedRing.orderRespectsAddition order c<0 _
0<-c : 0R < (Group.inverse additiveGroup c)
0<-c = SetoidPartialOrder.<WellDefined pOrder (Group.invRight additiveGroup) (Group.identLeft additiveGroup) p1
t : (x * Group.inverse additiveGroup c) < (y * Group.inverse additiveGroup c)
t = ringCanMultiplyByPositive 0<-c x<y
u : (Group.inverse additiveGroup (x * c)) < Group.inverse additiveGroup (y * c)
u = SetoidPartialOrder.<WellDefined pOrder ringMinusExtracts ringMinusExtracts t
ringCanMultiplyByNegative : {x y c : A} → c < (Ring.0R R) → x < y → (y * c) < (x * c)
ringCanMultiplyByNegative {x} {y} {c} c<0 x<y = ringSwapNegatives u
where
open Equivalence eq
p1 : (c + Group.inverse additiveGroup c) < (0R + Group.inverse additiveGroup c)
p1 = OrderedRing.orderRespectsAddition order c<0 _
0<-c : 0R < (Group.inverse additiveGroup c)
0<-c = SetoidPartialOrder.<WellDefined pOrder (Group.invRight additiveGroup) (Group.identLeft additiveGroup) p1
t : (x * Group.inverse additiveGroup c) < (y * Group.inverse additiveGroup c)
t = ringCanMultiplyByPositive 0<-c x<y
u : (Group.inverse additiveGroup (x * c)) < Group.inverse additiveGroup (y * c)
u = SetoidPartialOrder.<WellDefined pOrder ringMinusExtracts ringMinusExtracts t
ringCanCancelNegative : {x y c : A} → c < (Ring.0R R) → (x * c) < (y * c) → y < x
ringCanCancelNegative {x} {y} {c} c<0 xc<yc = r
where
open Equivalence eq
p0 : 0R < ((y * c) + inverse (x * c))
p0 = SetoidPartialOrder.<WellDefined pOrder invRight reflexive (OrderedRing.orderRespectsAddition order xc<yc (inverse (x * c)))
p1 : 0R < ((y * c) + ((inverse x) * c))
p1 = SetoidPartialOrder.<WellDefined pOrder reflexive (Group.+WellDefined additiveGroup reflexive (Equivalence.transitive eq (inverseWellDefined additiveGroup *Commutative) (Equivalence.transitive eq (symmetric ringMinusExtracts) *Commutative))) p0
p2 : 0R < ((y + inverse x) * c)
p2 = SetoidPartialOrder.<WellDefined pOrder reflexive (Equivalence.transitive eq (Group.+WellDefined additiveGroup *Commutative *Commutative) (Equivalence.transitive eq (symmetric *DistributesOver+) *Commutative)) p1
q : (y + inverse x) < 0R
q with SetoidTotalOrder.totality tOrder 0R (y + inverse x)
q | inl (inl pr) = exFalso (SetoidPartialOrder.irreflexive pOrder (SetoidPartialOrder.transitive pOrder bad c<0))
where
bad : 0R < c
bad = ringCanCancelPositive pr (SetoidPartialOrder.<WellDefined pOrder (symmetric (Equivalence.transitive eq *Commutative (Ring.timesZero R))) *Commutative p2)
q | inl (inr pr) = pr
q | inr 0=y-x = exFalso (SetoidPartialOrder.irreflexive pOrder (SetoidPartialOrder.<WellDefined pOrder (*WellDefined x=y reflexive) reflexive xc<yc))
where
x=y : x ∼ y
x=y = Equivalence.transitive eq (symmetric identLeft) (Equivalence.transitive eq (Group.+WellDefined additiveGroup 0=y-x reflexive) (Equivalence.transitive eq (symmetric (Group.+Associative additiveGroup)) (Equivalence.transitive eq (Group.+WellDefined additiveGroup reflexive invLeft) identRight)))
r : y < x
r = SetoidPartialOrder.<WellDefined pOrder (Equivalence.transitive eq (symmetric (Group.+Associative additiveGroup)) (Equivalence.transitive eq (Group.+WellDefined additiveGroup reflexive (invLeft)) identRight)) (Group.identLeft additiveGroup) (OrderedRing.orderRespectsAddition order q x)
ringCanCancelNegative : {x y c : A} → c < (Ring.0R R) → (x * c) < (y * c) → y < x
ringCanCancelNegative {x} {y} {c} c<0 xc<yc = r
where
open Equivalence eq
p0 : 0R < ((y * c) + inverse (x * c))
p0 = SetoidPartialOrder.<WellDefined pOrder invRight reflexive (OrderedRing.orderRespectsAddition order xc<yc (inverse (x * c)))
p1 : 0R < ((y * c) + ((inverse x) * c))
p1 = SetoidPartialOrder.<WellDefined pOrder reflexive (Group.+WellDefined additiveGroup reflexive (Equivalence.transitive eq (inverseWellDefined additiveGroup *Commutative) (Equivalence.transitive eq (symmetric ringMinusExtracts) *Commutative))) p0
p2 : 0R < ((y + inverse x) * c)
p2 = SetoidPartialOrder.<WellDefined pOrder reflexive (Equivalence.transitive eq (Group.+WellDefined additiveGroup *Commutative *Commutative) (Equivalence.transitive eq (symmetric *DistributesOver+) *Commutative)) p1
q : (y + inverse x) < 0R
q with SetoidTotalOrder.totality tOrder 0R (y + inverse x)
q | inl (inl pr) = exFalso (SetoidPartialOrder.irreflexive pOrder (SetoidPartialOrder.transitive pOrder bad c<0))
where
bad : 0R < c
bad = ringCanCancelPositive pr (SetoidPartialOrder.<WellDefined pOrder (symmetric (Equivalence.transitive eq *Commutative (Ring.timesZero R))) *Commutative p2)
q | inl (inr pr) = pr
q | inr 0=y-x = exFalso (SetoidPartialOrder.irreflexive pOrder (SetoidPartialOrder.<WellDefined pOrder (*WellDefined x=y reflexive) reflexive xc<yc))
where
x=y : x ∼ y
x=y = Equivalence.transitive eq (symmetric identLeft) (Equivalence.transitive eq (Group.+WellDefined additiveGroup 0=y-x reflexive) (Equivalence.transitive eq (symmetric (Group.+Associative additiveGroup)) (Equivalence.transitive eq (Group.+WellDefined additiveGroup reflexive invLeft) identRight)))
r : y < x
r = SetoidPartialOrder.<WellDefined pOrder (Equivalence.transitive eq (symmetric (Group.+Associative additiveGroup)) (Equivalence.transitive eq (Group.+WellDefined additiveGroup reflexive (invLeft)) identRight)) (Group.identLeft additiveGroup) (OrderedRing.orderRespectsAddition order q x)
absZero : {a b c : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ : A → A → A} {_*_ : A → A → A} {R : Ring S _+_ _*_} {_<_ : Rel {a} {c} A} {p : SetoidPartialOrder S _<_} {t : SetoidTotalOrder p} (o : OrderedRing R t) → OrderedRing.abs o (Ring.0R R) ≡ Ring.0R R
absZero {R = R} {t = t} oR with SetoidTotalOrder.totality t (Ring.0R R) (Ring.0R R)
absZero {R = R} {t = t} oR | inl (inl x) = exFalso (SetoidPartialOrder.irreflexive (SetoidTotalOrder.partial t) x)
absZero {R = R} {t = t} oR | inl (inr x) = exFalso (SetoidPartialOrder.irreflexive (SetoidTotalOrder.partial t) x)
absZero {R = R} {t = t} oR | inr x = refl
absZero : {a b c : _} {A : Set a} {S : Setoid {a} {b} A} {_+_ : A → A → A} {_*_ : A → A → A} {R : Ring S _+_ _*_} {_<_ : Rel {a} {c} A} {p : SetoidPartialOrder S _<_} {t : SetoidTotalOrder p} (o : OrderedRing R t) → OrderedRing.abs o (Ring.0R R) ≡ Ring.0R R
absZero {R = R} {t = t} oR with SetoidTotalOrder.totality t (Ring.0R R) (Ring.0R R)
absZero {R = R} {t = t} oR | inl (inl x) = exFalso (SetoidPartialOrder.irreflexive (SetoidTotalOrder.partial t) x)
absZero {R = R} {t = t} oR | inl (inr x) = exFalso (SetoidPartialOrder.irreflexive (SetoidTotalOrder.partial t) x)
absZero {R = R} {t = t} oR | inr x = refl
absNegation : (a : A) → (abs a) ∼ (abs (inverse a))
absNegation a with totality 0R a
absNegation a | inl (inl 0<a) with totality 0G (inverse a)
absNegation a | inl (inl 0<a) | inl (inl 0<-a) = exFalso (irreflexive {0G} (SetoidPartialOrder.transitive pOrder 0<-a (lemm2' a 0<a)))
absNegation a | inl (inl 0<a) | inl (inr -a<0) = Equivalence.symmetric eq (invTwice additiveGroup a)
absNegation a | inl (inl 0<a) | inr 0=-a = exFalso (irreflexive {0G} (<WellDefined (Equivalence.reflexive eq) (Equivalence.transitive eq (Equivalence.transitive eq (Equivalence.symmetric eq (invTwice additiveGroup a)) (inverseWellDefined additiveGroup (Equivalence.symmetric eq 0=-a))) (invIdent additiveGroup)) 0<a))
absNegation a | inl (inr a<0) with totality 0G (inverse a)
absNegation a | inl (inr a<0) | inl (inl 0<-a) = Equivalence.reflexive eq
absNegation a | inl (inr a<0) | inl (inr -a<0) = exFalso (irreflexive {0G} (SetoidPartialOrder.transitive pOrder (<WellDefined (Equivalence.reflexive eq) (invTwice additiveGroup a) (lemm2 (inverse a) -a<0)) a<0))
absNegation a | inl (inr a<0) | inr 0=-a = exFalso (irreflexive {0G} (<WellDefined (Equivalence.transitive eq (Equivalence.symmetric eq (Equivalence.transitive eq (inverseWellDefined additiveGroup 0=-a) (invTwice additiveGroup a))) (invIdent additiveGroup)) (Equivalence.reflexive eq) a<0))
absNegation a | inr 0=a with totality 0G (inverse a)
absNegation a | inr 0=a | inl (inl 0<-a) = exFalso (irreflexive {0G} (<WellDefined (Equivalence.reflexive eq) (Equivalence.transitive eq (inverseWellDefined additiveGroup (Equivalence.symmetric eq 0=a)) (invIdent additiveGroup)) 0<-a))
absNegation a | inr 0=a | inl (inr -a<0) = exFalso (irreflexive {0G} (<WellDefined (Equivalence.transitive eq (inverseWellDefined additiveGroup (Equivalence.symmetric eq 0=a)) (invIdent additiveGroup)) (Equivalence.reflexive eq) -a<0))
absNegation a | inr 0=a | inr 0=-a = Equivalence.transitive eq (Equivalence.symmetric eq 0=a) 0=-a
absNegation : (a : A) → (abs a) ∼ (abs (inverse a))
absNegation a with totality 0R a
absNegation a | inl (inl 0<a) with totality 0G (inverse a)
absNegation a | inl (inl 0<a) | inl (inl 0<-a) = exFalso (irreflexive {0G} (SetoidPartialOrder.transitive pOrder 0<-a (lemm2' a 0<a)))
absNegation a | inl (inl 0<a) | inl (inr -a<0) = Equivalence.symmetric eq (invTwice additiveGroup a)
absNegation a | inl (inl 0<a) | inr 0=-a = exFalso (irreflexive {0G} (<WellDefined (Equivalence.reflexive eq) (Equivalence.transitive eq (Equivalence.transitive eq (Equivalence.symmetric eq (invTwice additiveGroup a)) (inverseWellDefined additiveGroup (Equivalence.symmetric eq 0=-a))) (invIdent additiveGroup)) 0<a))
absNegation a | inl (inr a<0) with totality 0G (inverse a)
absNegation a | inl (inr a<0) | inl (inl 0<-a) = Equivalence.reflexive eq
absNegation a | inl (inr a<0) | inl (inr -a<0) = exFalso (irreflexive {0G} (SetoidPartialOrder.transitive pOrder (<WellDefined (Equivalence.reflexive eq) (invTwice additiveGroup a) (lemm2 (inverse a) -a<0)) a<0))
absNegation a | inl (inr a<0) | inr 0=-a = exFalso (irreflexive {0G} (<WellDefined (Equivalence.transitive eq (Equivalence.symmetric eq (Equivalence.transitive eq (inverseWellDefined additiveGroup 0=-a) (invTwice additiveGroup a))) (invIdent additiveGroup)) (Equivalence.reflexive eq) a<0))
absNegation a | inr 0=a with totality 0G (inverse a)
absNegation a | inr 0=a | inl (inl 0<-a) = exFalso (irreflexive {0G} (<WellDefined (Equivalence.reflexive eq) (Equivalence.transitive eq (inverseWellDefined additiveGroup (Equivalence.symmetric eq 0=a)) (invIdent additiveGroup)) 0<-a))
absNegation a | inr 0=a | inl (inr -a<0) = exFalso (irreflexive {0G} (<WellDefined (Equivalence.transitive eq (inverseWellDefined additiveGroup (Equivalence.symmetric eq 0=a)) (invIdent additiveGroup)) (Equivalence.reflexive eq) -a<0))
absNegation a | inr 0=a | inr 0=-a = Equivalence.transitive eq (Equivalence.symmetric eq 0=a) 0=-a
posTimesNeg : (a b : A) → (0G < a) → (b < 0G) → (a * b) < 0G
posTimesNeg a b 0<a b<0 with orderRespectsMultiplication 0<a (lemm2 _ b<0)
... | bl = <WellDefined (invTwice additiveGroup _) (Equivalence.reflexive eq) (lemm2' _ (<WellDefined (Equivalence.reflexive eq) ringMinusExtracts bl))
posTimesNeg : (a b : A) → (0G < a) → (b < 0G) → (a * b) < 0G
posTimesNeg a b 0<a b<0 with orderRespectsMultiplication 0<a (lemm2 _ b<0)
... | bl = <WellDefined (invTwice additiveGroup _) (Equivalence.reflexive eq) (lemm2' _ (<WellDefined (Equivalence.reflexive eq) ringMinusExtracts bl))
negTimesPos : (a b : A) → (a < 0G) → (b < 0G) → 0G < (a * b)
negTimesPos a b a<0 b<0 with orderRespectsMultiplication (lemm2 _ a<0) (lemm2 _ b<0)
... | bl = <WellDefined (Equivalence.reflexive eq) twoNegativesTimes bl
negTimesPos : (a b : A) → (a < 0G) → (b < 0G) → 0G < (a * b)
negTimesPos a b a<0 b<0 with orderRespectsMultiplication (lemm2 _ a<0) (lemm2 _ b<0)
... | bl = <WellDefined (Equivalence.reflexive eq) twoNegativesTimes bl
absRespectsTimes : (a b : A) → abs (a * b) ∼ (abs a) * (abs b)
absRespectsTimes a b with totality 0R a
absRespectsTimes a b | inl (inl 0<a) with totality 0R b
absRespectsTimes a b | inl (inl 0<a) | inl (inl 0<b) with totality 0R (a * b)
absRespectsTimes a b | inl (inl 0<a) | inl (inl 0<b) | inl (inl 0<ab) = Equivalence.reflexive eq
absRespectsTimes a b | inl (inl 0<a) | inl (inl 0<b) | inl (inr ab<0) = exFalso (irreflexive {0G} (SetoidPartialOrder.transitive pOrder (orderRespectsMultiplication 0<a 0<b) ab<0))
absRespectsTimes a b | inl (inl 0<a) | inl (inl 0<b) | inr 0=ab = exFalso (irreflexive {0G} (<WellDefined (Equivalence.reflexive eq) (Equivalence.symmetric eq 0=ab) (orderRespectsMultiplication 0<a 0<b)))
absRespectsTimes a b | inl (inl 0<a) | inl (inr b<0) with totality 0R (a * b)
absRespectsTimes a b | inl (inl 0<a) | inl (inr b<0) | inl (inl 0<ab) with <WellDefined (Equivalence.reflexive eq) ringMinusExtracts (orderRespectsMultiplication 0<a (lemm2 b b<0))
... | bl = exFalso (irreflexive {0G} (SetoidPartialOrder.transitive pOrder 0<ab (<WellDefined (invTwice additiveGroup _) (Equivalence.reflexive eq) (lemm2' _ bl))))
absRespectsTimes a b | inl (inl 0<a) | inl (inr b<0) | inl (inr ab<0) = Equivalence.symmetric eq ringMinusExtracts
absRespectsTimes a b | inl (inl 0<a) | inl (inr b<0) | inr 0=ab = exFalso (irreflexive {0G} (<WellDefined (Equivalence.symmetric eq 0=ab) (Equivalence.reflexive eq) (posTimesNeg a b 0<a b<0)))
absRespectsTimes a b | inl (inl 0<a) | inr 0=b with totality 0R (a * b)
absRespectsTimes a b | inl (inl 0<a) | inr 0=b | inl (inl 0<ab) = exFalso (irreflexive {0G} (<WellDefined (Equivalence.reflexive eq) (Equivalence.transitive eq (*WellDefined (Equivalence.reflexive eq) (Equivalence.symmetric eq 0=b)) (timesZero {a})) 0<ab))
absRespectsTimes a b | inl (inl 0<a) | inr 0=b | inl (inr ab<0) = exFalso ((irreflexive {0G} (<WellDefined (Equivalence.transitive eq (*WellDefined (Equivalence.reflexive eq) (Equivalence.symmetric eq 0=b)) (timesZero {a})) (Equivalence.reflexive eq) ab<0)))
absRespectsTimes a b | inl (inl 0<a) | inr 0=b | inr 0=ab = Equivalence.reflexive eq
absRespectsTimes a b | inl (inr a<0) with totality 0R b
absRespectsTimes a b | inl (inr a<0) | inl (inl 0<b) with totality 0R (a * b)
absRespectsTimes a b | inl (inr a<0) | inl (inl 0<b) | inl (inl 0<ab) = exFalso (irreflexive {0G} (SetoidPartialOrder.transitive pOrder 0<ab (<WellDefined *Commutative (Equivalence.reflexive eq) (posTimesNeg b a 0<b a<0))))
absRespectsTimes a b | inl (inr a<0) | inl (inl 0<b) | inl (inr ab<0) = Equivalence.symmetric eq ringMinusExtracts'
absRespectsTimes a b | inl (inr a<0) | inl (inl 0<b) | inr 0=ab = exFalso (irreflexive {0G} (<WellDefined (Equivalence.symmetric eq (Equivalence.transitive eq 0=ab *Commutative)) (Equivalence.reflexive eq) (posTimesNeg b a 0<b a<0)))
absRespectsTimes a b | inl (inr a<0) | inl (inr b<0) with totality 0R (a * b)
absRespectsTimes a b | inl (inr a<0) | inl (inr b<0) | inl (inl 0<ab) = Equivalence.symmetric eq twoNegativesTimes
absRespectsTimes a b | inl (inr a<0) | inl (inr b<0) | inl (inr ab<0) = exFalso (irreflexive {0G} (SetoidPartialOrder.transitive pOrder (negTimesPos a b a<0 b<0) ab<0))
absRespectsTimes a b | inl (inr a<0) | inl (inr b<0) | inr 0=ab = exFalso (exFalso (irreflexive {0G} (<WellDefined (Equivalence.reflexive eq) (Equivalence.symmetric eq 0=ab) (negTimesPos a b a<0 b<0))))
absRespectsTimes a b | inl (inr a<0) | inr 0=b with totality 0R (a * b)
absRespectsTimes a b | inl (inr a<0) | inr 0=b | inl (inl 0<ab) = exFalso (irreflexive {0R} (<WellDefined (Equivalence.reflexive eq) (Equivalence.transitive eq (*WellDefined (Equivalence.reflexive eq) (Equivalence.symmetric eq 0=b)) (timesZero {a})) 0<ab))
absRespectsTimes a b | inl (inr a<0) | inr 0=b | inl (inr ab<0) = exFalso (irreflexive {0R} (<WellDefined (Equivalence.transitive eq (*WellDefined (Equivalence.reflexive eq) (Equivalence.symmetric eq 0=b)) timesZero) (Equivalence.reflexive eq) ab<0))
absRespectsTimes a b | inl (inr a<0) | inr 0=b | inr 0=ab = Equivalence.transitive eq (*WellDefined (Equivalence.reflexive eq) (Equivalence.symmetric eq 0=b)) (Equivalence.transitive eq (Equivalence.transitive eq timesZero (Equivalence.symmetric eq timesZero)) (*WellDefined (Equivalence.reflexive eq) 0=b))
absRespectsTimes a b | inr 0=a with totality 0R b
absRespectsTimes a b | inr 0=a | inl (inl 0<b) with totality 0R (a * b)
absRespectsTimes a b | inr 0=a | inl (inl 0<b) | inl (inl 0<ab) = Equivalence.reflexive eq
absRespectsTimes a b | inr 0=a | inl (inl 0<b) | inl (inr ab<0) = Equivalence.transitive eq (Equivalence.transitive eq (Equivalence.transitive eq (inverseWellDefined additiveGroup (Equivalence.transitive eq (*WellDefined (Equivalence.symmetric eq 0=a) (Equivalence.reflexive eq)) (Equivalence.transitive eq *Commutative timesZero))) (invIdent additiveGroup)) (Equivalence.transitive eq (Equivalence.symmetric eq timesZero) *Commutative)) (*WellDefined 0=a (Equivalence.reflexive eq))
absRespectsTimes a b | inr 0=a | inl (inl 0<b) | inr 0=ab = Equivalence.reflexive eq
absRespectsTimes a b | inr 0=a | inl (inr b<0) with totality 0R (a * b)
absRespectsTimes a b | inr 0=a | inl (inr b<0) | inl (inl 0<ab) = Equivalence.transitive eq (Equivalence.transitive eq (*WellDefined (Equivalence.symmetric eq 0=a) (Equivalence.reflexive eq)) *Commutative) (Equivalence.transitive eq timesZero (Equivalence.transitive eq (Equivalence.symmetric eq (Equivalence.transitive eq *Commutative timesZero)) (*WellDefined 0=a (Equivalence.reflexive eq))))
absRespectsTimes a b | inr 0=a | inl (inr b<0) | inl (inr ab<0) = Equivalence.symmetric eq ringMinusExtracts
absRespectsTimes a b | inr 0=a | inl (inr b<0) | inr 0=ab = Equivalence.transitive eq (Equivalence.transitive eq (*WellDefined (Equivalence.symmetric eq 0=a) (Equivalence.reflexive eq)) *Commutative) (Equivalence.transitive eq timesZero (Equivalence.transitive eq (Equivalence.symmetric eq (Equivalence.transitive eq *Commutative timesZero)) (*WellDefined 0=a (Equivalence.reflexive eq))))
absRespectsTimes a b | inr 0=a | inr 0=b with totality 0R (a * b)
absRespectsTimes a b | inr 0=a | inr 0=b | inl (inl 0<ab) = exFalso (irreflexive {0R} (<WellDefined (Equivalence.reflexive eq) (Equivalence.transitive eq (*WellDefined (Equivalence.reflexive eq) (Equivalence.symmetric eq 0=b)) timesZero) 0<ab))
absRespectsTimes a b | inr 0=a | inr 0=b | inl (inr ab<0) = exFalso (irreflexive {0R} (<WellDefined (Equivalence.transitive eq (*WellDefined (Equivalence.reflexive eq) (Equivalence.symmetric eq 0=b)) timesZero) (Equivalence.reflexive eq) ab<0))
absRespectsTimes a b | inr 0=a | inr 0=b | inr 0=ab = Equivalence.reflexive eq
absRespectsTimes : (a b : A) → abs (a * b) ∼ (abs a) * (abs b)
absRespectsTimes a b with totality 0R a
absRespectsTimes a b | inl (inl 0<a) with totality 0R b
absRespectsTimes a b | inl (inl 0<a) | inl (inl 0<b) with totality 0R (a * b)
absRespectsTimes a b | inl (inl 0<a) | inl (inl 0<b) | inl (inl 0<ab) = Equivalence.reflexive eq
absRespectsTimes a b | inl (inl 0<a) | inl (inl 0<b) | inl (inr ab<0) = exFalso (irreflexive {0G} (SetoidPartialOrder.transitive pOrder (orderRespectsMultiplication 0<a 0<b) ab<0))
absRespectsTimes a b | inl (inl 0<a) | inl (inl 0<b) | inr 0=ab = exFalso (irreflexive {0G} (<WellDefined (Equivalence.reflexive eq) (Equivalence.symmetric eq 0=ab) (orderRespectsMultiplication 0<a 0<b)))
absRespectsTimes a b | inl (inl 0<a) | inl (inr b<0) with totality 0R (a * b)
absRespectsTimes a b | inl (inl 0<a) | inl (inr b<0) | inl (inl 0<ab) with <WellDefined (Equivalence.reflexive eq) ringMinusExtracts (orderRespectsMultiplication 0<a (lemm2 b b<0))
... | bl = exFalso (irreflexive {0G} (SetoidPartialOrder.transitive pOrder 0<ab (<WellDefined (invTwice additiveGroup _) (Equivalence.reflexive eq) (lemm2' _ bl))))
absRespectsTimes a b | inl (inl 0<a) | inl (inr b<0) | inl (inr ab<0) = Equivalence.symmetric eq ringMinusExtracts
absRespectsTimes a b | inl (inl 0<a) | inl (inr b<0) | inr 0=ab = exFalso (irreflexive {0G} (<WellDefined (Equivalence.symmetric eq 0=ab) (Equivalence.reflexive eq) (posTimesNeg a b 0<a b<0)))
absRespectsTimes a b | inl (inl 0<a) | inr 0=b with totality 0R (a * b)
absRespectsTimes a b | inl (inl 0<a) | inr 0=b | inl (inl 0<ab) = exFalso (irreflexive {0G} (<WellDefined (Equivalence.reflexive eq) (Equivalence.transitive eq (*WellDefined (Equivalence.reflexive eq) (Equivalence.symmetric eq 0=b)) (timesZero {a})) 0<ab))
absRespectsTimes a b | inl (inl 0<a) | inr 0=b | inl (inr ab<0) = exFalso ((irreflexive {0G} (<WellDefined (Equivalence.transitive eq (*WellDefined (Equivalence.reflexive eq) (Equivalence.symmetric eq 0=b)) (timesZero {a})) (Equivalence.reflexive eq) ab<0)))
absRespectsTimes a b | inl (inl 0<a) | inr 0=b | inr 0=ab = Equivalence.reflexive eq
absRespectsTimes a b | inl (inr a<0) with totality 0R b
absRespectsTimes a b | inl (inr a<0) | inl (inl 0<b) with totality 0R (a * b)
absRespectsTimes a b | inl (inr a<0) | inl (inl 0<b) | inl (inl 0<ab) = exFalso (irreflexive {0G} (SetoidPartialOrder.transitive pOrder 0<ab (<WellDefined *Commutative (Equivalence.reflexive eq) (posTimesNeg b a 0<b a<0))))
absRespectsTimes a b | inl (inr a<0) | inl (inl 0<b) | inl (inr ab<0) = Equivalence.symmetric eq ringMinusExtracts'
absRespectsTimes a b | inl (inr a<0) | inl (inl 0<b) | inr 0=ab = exFalso (irreflexive {0G} (<WellDefined (Equivalence.symmetric eq (Equivalence.transitive eq 0=ab *Commutative)) (Equivalence.reflexive eq) (posTimesNeg b a 0<b a<0)))
absRespectsTimes a b | inl (inr a<0) | inl (inr b<0) with totality 0R (a * b)
absRespectsTimes a b | inl (inr a<0) | inl (inr b<0) | inl (inl 0<ab) = Equivalence.symmetric eq twoNegativesTimes
absRespectsTimes a b | inl (inr a<0) | inl (inr b<0) | inl (inr ab<0) = exFalso (irreflexive {0G} (SetoidPartialOrder.transitive pOrder (negTimesPos a b a<0 b<0) ab<0))
absRespectsTimes a b | inl (inr a<0) | inl (inr b<0) | inr 0=ab = exFalso (exFalso (irreflexive {0G} (<WellDefined (Equivalence.reflexive eq) (Equivalence.symmetric eq 0=ab) (negTimesPos a b a<0 b<0))))
absRespectsTimes a b | inl (inr a<0) | inr 0=b with totality 0R (a * b)
absRespectsTimes a b | inl (inr a<0) | inr 0=b | inl (inl 0<ab) = exFalso (irreflexive {0R} (<WellDefined (Equivalence.reflexive eq) (Equivalence.transitive eq (*WellDefined (Equivalence.reflexive eq) (Equivalence.symmetric eq 0=b)) (timesZero {a})) 0<ab))
absRespectsTimes a b | inl (inr a<0) | inr 0=b | inl (inr ab<0) = exFalso (irreflexive {0R} (<WellDefined (Equivalence.transitive eq (*WellDefined (Equivalence.reflexive eq) (Equivalence.symmetric eq 0=b)) timesZero) (Equivalence.reflexive eq) ab<0))
absRespectsTimes a b | inl (inr a<0) | inr 0=b | inr 0=ab = Equivalence.transitive eq (*WellDefined (Equivalence.reflexive eq) (Equivalence.symmetric eq 0=b)) (Equivalence.transitive eq (Equivalence.transitive eq timesZero (Equivalence.symmetric eq timesZero)) (*WellDefined (Equivalence.reflexive eq) 0=b))
absRespectsTimes a b | inr 0=a with totality 0R b
absRespectsTimes a b | inr 0=a | inl (inl 0<b) with totality 0R (a * b)
absRespectsTimes a b | inr 0=a | inl (inl 0<b) | inl (inl 0<ab) = Equivalence.reflexive eq
absRespectsTimes a b | inr 0=a | inl (inl 0<b) | inl (inr ab<0) = Equivalence.transitive eq (Equivalence.transitive eq (Equivalence.transitive eq (inverseWellDefined additiveGroup (Equivalence.transitive eq (*WellDefined (Equivalence.symmetric eq 0=a) (Equivalence.reflexive eq)) (Equivalence.transitive eq *Commutative timesZero))) (invIdent additiveGroup)) (Equivalence.transitive eq (Equivalence.symmetric eq timesZero) *Commutative)) (*WellDefined 0=a (Equivalence.reflexive eq))
absRespectsTimes a b | inr 0=a | inl (inl 0<b) | inr 0=ab = Equivalence.reflexive eq
absRespectsTimes a b | inr 0=a | inl (inr b<0) with totality 0R (a * b)
absRespectsTimes a b | inr 0=a | inl (inr b<0) | inl (inl 0<ab) = Equivalence.transitive eq (Equivalence.transitive eq (*WellDefined (Equivalence.symmetric eq 0=a) (Equivalence.reflexive eq)) *Commutative) (Equivalence.transitive eq timesZero (Equivalence.transitive eq (Equivalence.symmetric eq (Equivalence.transitive eq *Commutative timesZero)) (*WellDefined 0=a (Equivalence.reflexive eq))))
absRespectsTimes a b | inr 0=a | inl (inr b<0) | inl (inr ab<0) = Equivalence.symmetric eq ringMinusExtracts
absRespectsTimes a b | inr 0=a | inl (inr b<0) | inr 0=ab = Equivalence.transitive eq (Equivalence.transitive eq (*WellDefined (Equivalence.symmetric eq 0=a) (Equivalence.reflexive eq)) *Commutative) (Equivalence.transitive eq timesZero (Equivalence.transitive eq (Equivalence.symmetric eq (Equivalence.transitive eq *Commutative timesZero)) (*WellDefined 0=a (Equivalence.reflexive eq))))
absRespectsTimes a b | inr 0=a | inr 0=b with totality 0R (a * b)
absRespectsTimes a b | inr 0=a | inr 0=b | inl (inl 0<ab) = exFalso (irreflexive {0R} (<WellDefined (Equivalence.reflexive eq) (Equivalence.transitive eq (*WellDefined (Equivalence.reflexive eq) (Equivalence.symmetric eq 0=b)) timesZero) 0<ab))
absRespectsTimes a b | inr 0=a | inr 0=b | inl (inr ab<0) = exFalso (irreflexive {0R} (<WellDefined (Equivalence.transitive eq (*WellDefined (Equivalence.reflexive eq) (Equivalence.symmetric eq 0=b)) timesZero) (Equivalence.reflexive eq) ab<0))
absRespectsTimes a b | inr 0=a | inr 0=b | inr 0=ab = Equivalence.reflexive eq
absNonnegative : {a : A} → (abs a < 0R) → False
absNonnegative {a} pr with SetoidTotalOrder.totality tOrder 0R a
absNonnegative {a} pr | inl (inl x) = irreflexive {0G} (SetoidPartialOrder.transitive pOrder x pr)
absNonnegative {a} pr | inl (inr x) = irreflexive {0G} (SetoidPartialOrder.transitive pOrder (<WellDefined (Equivalence.reflexive eq) (invTwice additiveGroup a) (lemm2 (inverse a) pr)) x)
absNonnegative {a} pr | inr x = irreflexive {0G} (<WellDefined (Equivalence.symmetric eq x) (Equivalence.reflexive eq) pr)
absNonnegative : {a : A} → (abs a < 0R) → False
absNonnegative {a} pr with SetoidTotalOrder.totality tOrder 0R a
absNonnegative {a} pr | inl (inl x) = irreflexive {0G} (SetoidPartialOrder.transitive pOrder x pr)
absNonnegative {a} pr | inl (inr x) = irreflexive {0G} (SetoidPartialOrder.transitive pOrder (<WellDefined (Equivalence.reflexive eq) (invTwice additiveGroup a) (lemm2 (inverse a) pr)) x)
absNonnegative {a} pr | inr x = irreflexive {0G} (<WellDefined (Equivalence.symmetric eq x) (Equivalence.reflexive eq) pr)
a-bPos : {a b : A} → ((a ∼ b) → False) → 0R < abs (a + inverse b)
a-bPos {a} {b} a!=b with totality 0R (a + inverse b)
a-bPos {a} {b} a!=b | inl (inl x) = x
a-bPos {a} {b} a!=b | inl (inr x) = lemm2 _ x
a-bPos {a} {b} a!=b | inr x = exFalso (a!=b (transferToRight additiveGroup (Equivalence.symmetric eq x)))
a-bPos : {a b : A} → ((a ∼ b) → False) → 0R < abs (a + inverse b)
a-bPos {a} {b} a!=b with totality 0R (a + inverse b)
a-bPos {a} {b} a!=b | inl (inl x) = x
a-bPos {a} {b} a!=b | inl (inr x) = lemm2 _ x
a-bPos {a} {b} a!=b | inr x = exFalso (a!=b (transferToRight additiveGroup (Equivalence.symmetric eq x)))
absZeroImpliesZero : {a : A} → abs a ∼ 0R → a ∼ 0R
absZeroImpliesZero {a} a=0 with totality 0R a
absZeroImpliesZero {a} a=0 | inl (inl 0<a) = exFalso (irreflexive {0G} (<WellDefined (Equivalence.reflexive eq) a=0 0<a))
absZeroImpliesZero {a} a=0 | inl (inr a<0) = Equivalence.symmetric eq (lemm3 (inverse a) a (Equivalence.symmetric eq invLeft) (Equivalence.symmetric eq a=0))
absZeroImpliesZero {a} a=0 | inr 0=a = a=0
absZeroImpliesZero : {a : A} → abs a ∼ 0R → a ∼ 0R
absZeroImpliesZero {a} a=0 with totality 0R a
absZeroImpliesZero {a} a=0 | inl (inl 0<a) = exFalso (irreflexive {0G} (<WellDefined (Equivalence.reflexive eq) a=0 0<a))
absZeroImpliesZero {a} a=0 | inl (inr a<0) = Equivalence.symmetric eq (lemm3 (inverse a) a (Equivalence.symmetric eq invLeft) (Equivalence.symmetric eq a=0))
absZeroImpliesZero {a} a=0 | inr 0=a = a=0
halvePositive : (a : A) → 0R < (a + a) → 0R < a
halvePositive a 0<2a with totality 0R a
halvePositive a 0<2a | inl (inl x) = x
halvePositive a 0<2a | inl (inr a<0) = exFalso (irreflexive {a + a} (SetoidPartialOrder.transitive pOrder (<WellDefined (Equivalence.reflexive eq) identRight (ringAddInequalities a<0 a<0)) 0<2a))
halvePositive a 0<2a | inr x = exFalso (irreflexive {0G} (<WellDefined (Equivalence.reflexive eq) (Equivalence.transitive eq (+WellDefined (Equivalence.symmetric eq x) (Equivalence.symmetric eq x)) identRight) 0<2a))
halvePositive : (a : A) → 0R < (a + a) → 0R < a
halvePositive a 0<2a with totality 0R a
halvePositive a 0<2a | inl (inl x) = x
halvePositive a 0<2a | inl (inr a<0) = exFalso (irreflexive {a + a} (SetoidPartialOrder.transitive pOrder (<WellDefined (Equivalence.reflexive eq) identRight (ringAddInequalities a<0 a<0)) 0<2a))
halvePositive a 0<2a | inr x = exFalso (irreflexive {0G} (<WellDefined (Equivalence.reflexive eq) (Equivalence.transitive eq (+WellDefined (Equivalence.symmetric eq x) (Equivalence.symmetric eq x)) identRight) 0<2a))
0<1 : (0R ∼ 1R → False) → 0R < 1R
0<1 0!=1 with SetoidTotalOrder.totality tOrder 0R 1R
0<1 0!=1 | inl (inl x) = x
0<1 0!=1 | inl (inr x) = <WellDefined (Equivalence.reflexive eq) (Equivalence.transitive eq twoNegativesTimes identIsIdent) (orderRespectsMultiplication (lemm2 1R x) (lemm2 1R x))
0<1 0!=1 | inr x = exFalso (0!=1 x)
0<1 : (0R ∼ 1R → False) → 0R < 1R
0<1 0!=1 with SetoidTotalOrder.totality tOrder 0R 1R
0<1 0!=1 | inl (inl x) = x
0<1 0!=1 | inl (inr x) = <WellDefined (Equivalence.reflexive eq) (Equivalence.transitive eq twoNegativesTimes identIsIdent) (orderRespectsMultiplication (lemm2 1R x) (lemm2 1R x))
0<1 0!=1 | inr x = exFalso (0!=1 x)
addingAbsCannotShrink : {a b : A} → 0G < b → 0G < ((abs a) + b)
addingAbsCannotShrink {a} {b} 0<b with SetoidTotalOrder.totality tOrder 0G a
addingAbsCannotShrink {a} {b} 0<b | inl (inl x) = <WellDefined identLeft (Equivalence.reflexive eq) (ringAddInequalities x 0<b)
addingAbsCannotShrink {a} {b} 0<b | inl (inr x) = <WellDefined identLeft (Equivalence.reflexive eq) (ringAddInequalities (lemm2 a x) 0<b)
addingAbsCannotShrink {a} {b} 0<b | inr x = <WellDefined (Equivalence.reflexive eq) (Equivalence.transitive eq (Equivalence.symmetric eq identLeft) (+WellDefined x (Equivalence.reflexive eq))) 0<b
addingAbsCannotShrink : {a b : A} → 0G < b → 0G < ((abs a) + b)
addingAbsCannotShrink {a} {b} 0<b with SetoidTotalOrder.totality tOrder 0G a
addingAbsCannotShrink {a} {b} 0<b | inl (inl x) = <WellDefined identLeft (Equivalence.reflexive eq) (ringAddInequalities x 0<b)
addingAbsCannotShrink {a} {b} 0<b | inl (inr x) = <WellDefined identLeft (Equivalence.reflexive eq) (ringAddInequalities (lemm2 a x) 0<b)
addingAbsCannotShrink {a} {b} 0<b | inr x = <WellDefined (Equivalence.reflexive eq) (Equivalence.transitive eq (Equivalence.symmetric eq identLeft) (+WellDefined x (Equivalence.reflexive eq))) 0<b
1<0False : (1R < 0R) → False
1<0False 1<0 with orderRespectsMultiplication (lemm2 _ 1<0) (lemm2 _ 1<0)
... | bl = exFalso (irreflexive (SetoidPartialOrder.transitive pOrder 1<0 (<WellDefined (Equivalence.reflexive eq) (Equivalence.transitive eq (twoNegativesTimes) identIsIdent) bl)))
1<0False : (1R < 0R) → False
1<0False 1<0 with orderRespectsMultiplication (lemm2 _ 1<0) (lemm2 _ 1<0)
... | bl = exFalso (irreflexive (SetoidPartialOrder.transitive pOrder 1<0 (<WellDefined (Equivalence.reflexive eq) (Equivalence.transitive eq (twoNegativesTimes) identIsIdent) bl)))
greaterZeroImpliesEqualAbs : {a : A} → 0R < a → a ∼ abs a
greaterZeroImpliesEqualAbs {a} 0<a with totality 0R a
... | inl (inl _) = Equivalence.reflexive eq
... | inl (inr a<0) = exFalso (irreflexive (SetoidPartialOrder.transitive pOrder a<0 0<a))
... | inr 0=a = exFalso (irreflexive (<WellDefined 0=a (Equivalence.reflexive eq) 0<a))
greaterZeroImpliesEqualAbs : {a : A} → 0R < a → a ∼ abs a
greaterZeroImpliesEqualAbs {a} 0<a with totality 0R a
... | inl (inl _) = Equivalence.reflexive eq
... | inl (inr a<0) = exFalso (irreflexive (SetoidPartialOrder.transitive pOrder a<0 0<a))
... | inr 0=a = exFalso (irreflexive (<WellDefined 0=a (Equivalence.reflexive eq) 0<a))
lessZeroImpliesEqualNegAbs : {a : A} → a < 0R → abs a ∼ inverse a
lessZeroImpliesEqualNegAbs {a} a<0 with totality 0R a
... | inl (inr _) = Equivalence.reflexive eq
... | inl (inl 0<a) = exFalso (irreflexive (SetoidPartialOrder.transitive pOrder a<0 0<a))
... | inr 0=a = exFalso (irreflexive (<WellDefined (Equivalence.reflexive eq) 0=a a<0))
lessZeroImpliesEqualNegAbs : {a : A} → a < 0R → abs a ∼ inverse a
lessZeroImpliesEqualNegAbs {a} a<0 with totality 0R a
... | inl (inr _) = Equivalence.reflexive eq
... | inl (inl 0<a) = exFalso (irreflexive (SetoidPartialOrder.transitive pOrder a<0 0<a))
... | inr 0=a = exFalso (irreflexive (<WellDefined (Equivalence.reflexive eq) 0=a a<0))
absZeroIsZero : abs 0R ∼ 0R
absZeroIsZero with totality 0R 0R
... | inl (inl bad) = exFalso (irreflexive bad)
... | inl (inr bad) = exFalso (irreflexive bad)
... | inr _ = Equivalence.reflexive eq
absZeroIsZero : abs 0R ∼ 0R
absZeroIsZero with totality 0R 0R
... | inl (inl bad) = exFalso (irreflexive bad)
... | inl (inr bad) = exFalso (irreflexive bad)
... | inr _ = Equivalence.reflexive eq
greaterThanAbsImpliesGreaterThan0 : {a b : A} → (abs a) < b → 0R < b
greaterThanAbsImpliesGreaterThan0 {a} {b} a<b with totality 0R a
greaterThanAbsImpliesGreaterThan0 {a} {b} a<b | inl (inl 0<a) = SetoidPartialOrder.transitive pOrder 0<a a<b
greaterThanAbsImpliesGreaterThan0 {a} {b} a<b | inl (inr a<0) = SetoidPartialOrder.transitive pOrder (lemm2 _ a<0) a<b
greaterThanAbsImpliesGreaterThan0 {a} {b} a<b | inr 0=a = <WellDefined (Equivalence.symmetric eq 0=a) (Equivalence.reflexive eq) a<b
greaterThanAbsImpliesGreaterThan0 : {a b : A} → (abs a) < b → 0R < b
greaterThanAbsImpliesGreaterThan0 {a} {b} a<b with totality 0R a
greaterThanAbsImpliesGreaterThan0 {a} {b} a<b | inl (inl 0<a) = SetoidPartialOrder.transitive pOrder 0<a a<b
greaterThanAbsImpliesGreaterThan0 {a} {b} a<b | inl (inr a<0) = SetoidPartialOrder.transitive pOrder (lemm2 _ a<0) a<b
greaterThanAbsImpliesGreaterThan0 {a} {b} a<b | inr 0=a = <WellDefined (Equivalence.symmetric eq 0=a) (Equivalence.reflexive eq) a<b
anyComparisonImpliesNontrivial : {a b : A} → a < b → (0R ∼ 1R) → False
anyComparisonImpliesNontrivial {a} {b} a<b 0=1 = irreflexive (<WellDefined (oneZeroImpliesAllZero 0=1) (oneZeroImpliesAllZero 0=1) a<b)
anyComparisonImpliesNontrivial : {a b : A} → a < b → (0R ∼ 1R) → False
anyComparisonImpliesNontrivial {a} {b} a<b 0=1 = irreflexive (<WellDefined (oneZeroImpliesAllZero 0=1) (oneZeroImpliesAllZero 0=1) a<b)
abs1Is1 : abs 1R ∼ 1R
abs1Is1 with totality 0R 1R
abs1Is1 | inl (inl 0<1) = Equivalence.reflexive eq
abs1Is1 | inl (inr 1<0) = exFalso (1<0False 1<0)
abs1Is1 | inr 0=1 = Equivalence.reflexive eq
abs1Is1 : abs 1R ∼ 1R
abs1Is1 with totality 0R 1R
abs1Is1 | inl (inl 0<1) = Equivalence.reflexive eq
abs1Is1 | inl (inr 1<0) = exFalso (1<0False 1<0)
abs1Is1 | inr 0=1 = Equivalence.reflexive eq
charNot2ImpliesNontrivial : ((1R + 1R) ∼ 0R → False) → (0R ∼ 1R) → False
charNot2ImpliesNontrivial charNot2 0=1 = charNot2 (Equivalence.transitive eq (+WellDefined (Equivalence.symmetric eq 0=1) (Equivalence.symmetric eq 0=1)) identRight)
charNot2ImpliesNontrivial : ((1R + 1R) ∼ 0R → False) → (0R ∼ 1R) → False
charNot2ImpliesNontrivial charNot2 0=1 = charNot2 (Equivalence.transitive eq (+WellDefined (Equivalence.symmetric eq 0=1) (Equivalence.symmetric eq 0=1)) identRight)
absBoundedImpliesBounded : {a b : A} → abs a < b → a < b
absBoundedImpliesBounded {a} {b} a<b with SetoidTotalOrder.totality tOrder 0G a
absBoundedImpliesBounded {a} {b} a<b | inl (inl x) = a<b
absBoundedImpliesBounded {a} {b} a<b | inl (inr x) = SetoidPartialOrder.transitive pOrder x (SetoidPartialOrder.transitive pOrder (lemm2 a x) a<b)
absBoundedImpliesBounded {a} {b} a<b | inr x = a<b