Add some more ordered division ring properties.

3 files changed, 129 insertions, 11 deletions

diff --git a/src/Helium/Algebra/Ordered/StrictTotal/Properties/DivisionRing.agda b/src/Helium/Algebra/Ordered/StrictTotal/Properties/DivisionRing.agda
index 03e8ecd..ab8a37b 100644
--- a/src/Helium/Algebra/Ordered/StrictTotal/Properties/DivisionRing.agda
+++ b/src/Helium/Algebra/Ordered/StrictTotal/Properties/DivisionRing.agda
@@ -21,8 +21,21 @@ open DivisionRing divisionRing
   ; 0<a+0<b⇒0<ab to x>0∧y>0⇒x*y>0
   )
 
+open import Function using (_∘_)
+open import Relation.Binary.Reasoning.StrictPartialOrder strictPartialOrder
+
 open import Algebra.Properties.Ring Unordered.ring public
   renaming (-0#≈0# to -0≈0)
+open import Helium.Algebra.Properties.AlmostGroup *-almostGroup public
+  renaming
+  ( x≉0⇒∙-cancelˡ to x≉0⇒*-cancelˡ
+  ; x≉0⇒∙-cancelʳ to x≉0⇒*-cancelʳ
+  ; ⁻¹-anti-homo-∙ to ⁻¹-anti-homo-*
+  ; identityˡ-unique to *-identityˡ-unique
+  ; identityʳ-unique to *-identityʳ-unique
+  ; inverseˡ-unique to *-inverseˡ-unique
+  ; inverseʳ-unique to *-inverseʳ-unique
+  )
 open import Algebra.Properties.Semiring.Mult.TCOptimised Unordered.semiring public
 open import Algebra.Properties.Semiring.Exp.TCOptimised Unordered.semiring public
 open import Helium.Relation.Binary.Properties.StrictTotalOrder strictTotalOrder public
@@ -98,3 +111,96 @@ open import Helium.Algebra.Ordered.StrictTotal.Properties.Ring ring public
   ; x>1∧n≢0⇒x^n>1; 0≤x<1∧n≢0⇒x^n<1
   ; x≥1⇒x^n≥1; 0≤x≤1⇒x^n≤1
   )
+
+--------------------------------------------------------------------------------
+---- Properties of _⁻¹
+
+---- Miscellaneous
+
+x≉0⇒x⁻¹≉0 : ∀ {x} → (x≉0 : x ≉ 0#) → x≉0 ⁻¹ ≉ 0#
+x≉0⇒x⁻¹≉0 {x} x≉0 x⁻¹≈0 = x≉0 (begin-equality
+  x              ≈˘⟨ *-identityˡ x ⟩
+  1# * x         ≈˘⟨ *-congʳ (⁻¹-inverseʳ x≉0) ⟩
+  x * x≉0 ⁻¹ * x ≈⟨  *-congʳ (*-congˡ x⁻¹≈0) ⟩
+  x * 0# * x     ≈⟨  *-congʳ (zeroʳ x) ⟩
+  0# * x         ≈⟨  zeroˡ x ⟩
+  0#             ∎)
+
+---- Preserves signs
+
+x>0⇒x⁻¹>0 : ∀ {x} → (x>0 : x > 0#) → (<⇒≉ x>0 ∘ Eq.sym) ⁻¹ > 0#
+x>0⇒x⁻¹>0 {x} x>0 = ≰⇒> (λ x⁻¹≤0 → <⇒≱ (x<y⇒0<1 x>0) (begin
+  1#                        ≈˘⟨ ⁻¹-inverseʳ (<⇒≉ x>0 ∘ Eq.sym) ⟩
+  x * (<⇒≉ x>0 ∘ Eq.sym) ⁻¹ ≤⟨  x≥0∧y≤0⇒x*y≤0 (<⇒≤ x>0) x⁻¹≤0 ⟩
+  0#                        ∎))
+
+x<0⇒x⁻¹<0 : ∀ {x} → (x<0 : x < 0#) → (<⇒≉ x<0) ⁻¹ < 0#
+x<0⇒x⁻¹<0 {x} x<0 = ≰⇒> (λ x⁻¹≥0 → <⇒≱ (x<y⇒0<1 x<0) (begin
+  1#               ≈˘⟨ ⁻¹-inverseʳ (<⇒≉ x<0) ⟩
+  x * (<⇒≉ x<0) ⁻¹ ≤⟨  x≤0∧y≥0⇒x*y≤0 (<⇒≤ x<0) x⁻¹≥0 ⟩
+  0#               ∎))
+
+---- Respects signs
+
+x⁻¹>0⇒x>0 : ∀ {x} {x≉0 : x ≉ 0#} → x≉0 ⁻¹ > 0# → x > 0#
+x⁻¹>0⇒x>0 {x} {x≉0} x⁻¹>0 = begin-strict
+  0#                      <⟨ x>0⇒x⁻¹>0 x⁻¹>0 ⟩
+  (<⇒≉ x⁻¹>0 ∘ Eq.sym) ⁻¹ ≈⟨ ⁻¹-involutive x≉0 (<⇒≉ x⁻¹>0 ∘ Eq.sym) ⟩
+  x                       ∎
+
+x⁻¹<0⇒x<0 : ∀ {x} {x≉0 : x ≉ 0#} → x≉0 ⁻¹ < 0# → x < 0#
+x⁻¹<0⇒x<0 {x} {x≉0} x⁻¹<0 = begin-strict
+  x              ≈˘⟨ ⁻¹-involutive x≉0 (<⇒≉ x⁻¹<0) ⟩
+  (<⇒≉ x⁻¹<0) ⁻¹ <⟨  x<0⇒x⁻¹<0 x⁻¹<0 ⟩
+  0#             ∎
+
+---- Preserves size
+
+x>1⇒x⁻¹<1 : ∀ {x} → (x>1 : x > 1#) → (<⇒≉ (≤-<-trans 0≤1 x>1) ∘ Eq.sym) ⁻¹ < 1#
+x>1⇒x⁻¹<1 {x} x>1 = ≰⇒>
+  ( <-irrefl (Eq.sym (⁻¹-inverseʳ (<⇒≉ (≤-<-trans 0≤1 x>1) ∘ Eq.sym)))
+  ∘ x>1∧y≥1⇒x*y>1 x>1
+  )
+
+0<x<1⇒x⁻¹>1 : ∀ {x} (0<x : 0# < x) → x < 1# → (<⇒≉ 0<x ∘ Eq.sym) ⁻¹ > 1#
+0<x<1⇒x⁻¹>1 {x} 0<x x<1 = ≰⇒>
+  ( <-irrefl (⁻¹-inverseʳ (<⇒≉ 0<x ∘ Eq.sym))
+  ∘ 0≤x<1∧y≤1⇒x*y<1 (<⇒≤ 0<x) x<1
+  )
+
+---- Respects size
+
+x⁻¹>1⇒x<1 : ∀ {x} {x≉0 : x ≉ 0#} → x≉0 ⁻¹ > 1# → x < 1#
+x⁻¹>1⇒x<1 {x} {x≉0} x⁻¹>1 = ≰⇒>
+  ( <-irrefl (Eq.sym (⁻¹-inverseˡ x≉0))
+  ∘ x>1∧y≥1⇒x*y>1 x⁻¹>1
+  )
+
+0<x⁻¹<1⇒x>1 : ∀ {x} {x≉0 : x ≉ 0#} → 0# < x≉0 ⁻¹ → x≉0 ⁻¹ < 1# → x > 1#
+0<x⁻¹<1⇒x>1 {x} {x≉0} 0<x⁻¹ x⁻¹<1 = ≰⇒>
+  ( <-irrefl (⁻¹-inverseˡ x≉0)
+  ∘ 0≤x<1∧y≤1⇒x*y<1 (<⇒≤ 0<x⁻¹) x⁻¹<1
+  )
+
+--------------------------------------------------------------------------------
+---- Properties of -_ and _⁻¹
+
+-‿⁻¹-comm : ∀ {x} (x≉0 : x ≉ 0#) → - x≉0 ⁻¹ ≈ (x≉0 ∘ -x≈0⇒x≈0) ⁻¹
+-‿⁻¹-comm {x} x≉0 = *-inverseˡ-unique (x≉0 ∘ -x≈0⇒x≈0) (begin-equality
+  - x≉0 ⁻¹ * - x ≈⟨ -x*-y≈x*y (x≉0 ⁻¹) x ⟩
+  x≉0 ⁻¹ * x     ≈⟨ ⁻¹-inverseˡ x≉0 ⟩
+  1#             ∎)
+
+-- ---- Congruences
+
+-- -- _<_
+
+-- ⁻¹-anti-mono-< : ∀ {x y} (x≉0 : x ≉ 0#) (y≉0 : y ≉ 0#) → x < y → x≉0 ⁻¹ > y≉0 ⁻¹
+-- ⁻¹-anti-mono-< {x} {y} x≉0 y≉0 x<y = begin-strict
+--   y≉0 ⁻¹                ≈˘⟨ *-identityˡ (y≉0 ⁻¹) ⟩
+--   1# * y≉0 ⁻¹           ≈˘⟨ *-congʳ (⁻¹-inverseˡ x≉0) ⟩
+--   x≉0 ⁻¹ * x * y≉0 ⁻¹   <⟨  {!!} ⟩
+--   x≉0 ⁻¹ * y * y≉0 ⁻¹   ≈⟨  *-assoc (x≉0 ⁻¹) y (y≉0 ⁻¹) ⟩
+--   x≉0 ⁻¹ * (y * y≉0 ⁻¹) ≈⟨  *-congˡ (⁻¹-inverseʳ y≉0) ⟩
+--   x≉0 ⁻¹ * 1#           ≈⟨  *-identityʳ (x≉0 ⁻¹) ⟩
+--   x≉0 ⁻¹                ∎
diff --git a/src/Helium/Algebra/Ordered/StrictTotal/Properties/Field.agda b/src/Helium/Algebra/Ordered/StrictTotal/Properties/Field.agda
index 51a054e..33578e0 100644
--- a/src/Helium/Algebra/Ordered/StrictTotal/Properties/Field.agda
+++ b/src/Helium/Algebra/Ordered/StrictTotal/Properties/Field.agda
@@ -23,6 +23,16 @@ open Field field′
 
 open import Algebra.Properties.Ring Unordered.ring public
   renaming (-0#≈0# to -0≈0)
+open import Helium.Algebra.Properties.AlmostGroup *-almostGroup public
+  renaming
+  ( x≉0⇒∙-cancelˡ to x≉0⇒*-cancelˡ
+  ; x≉0⇒∙-cancelʳ to x≉0⇒*-cancelʳ
+  ; ⁻¹-anti-homo-∙ to ⁻¹-anti-homo-*
+  ; identityˡ-unique to *-identityˡ-unique
+  ; identityʳ-unique to *-identityʳ-unique
+  ; inverseˡ-unique to *-inverseˡ-unique
+  ; inverseʳ-unique to *-inverseʳ-unique
+  )
 open import Algebra.Properties.Semiring.Mult.TCOptimised Unordered.semiring public
 open import Algebra.Properties.CommutativeSemiring.Exp.TCOptimised Unordered.commutativeSemiring public
 open import Helium.Relation.Binary.Properties.StrictTotalOrder strictTotalOrder public
@@ -97,4 +107,15 @@ open import Helium.Algebra.Ordered.StrictTotal.Properties.DivisionRing divisionR
 
   ; x>1∧n≢0⇒x^n>1; 0≤x<1∧n≢0⇒x^n<1
   ; x≥1⇒x^n≥1; 0≤x≤1⇒x^n≤1
+
+  ; x>0⇒x⁻¹>0 ; x<0⇒x⁻¹<0
+
+  ; x⁻¹>0⇒x>0 ; x⁻¹<0⇒x<0
+
+  ; x>1⇒x⁻¹<1; 0<x<1⇒x⁻¹>1
+
+  ; x⁻¹>1⇒x<1; 0<x⁻¹<1⇒x>1
+
+  ; -‿⁻¹-comm
+  ; x≉0⇒x⁻¹≉0
   )
diff --git a/src/Helium/Data/Pseudocode/Algebra/Properties.agda b/src/Helium/Data/Pseudocode/Algebra/Properties.agda
index 3c22216..1c52cda 100644
--- a/src/Helium/Data/Pseudocode/Algebra/Properties.agda
+++ b/src/Helium/Data/Pseudocode/Algebra/Properties.agda
@@ -22,6 +22,7 @@ open import Data.Sum using (_⊎_; inj₁; inj₂; map)
 import Data.Unit
 open import Function using (_∘_)
 import Helium.Algebra.Ordered.StrictTotal.Properties.CommutativeRing as CommRingₚ
+import Helium.Algebra.Ordered.StrictTotal.Properties.Field as Fieldₚ
 open import Level using (_⊔_)
 open import Relation.Binary.Core using (_Preserves_⟶_)
 open import Relation.Binary.Definitions using (tri<; tri≈; tri>)
@@ -77,7 +78,7 @@ module ℝ where
     )
   module Reasoning = pseudocode.ℝ-Reasoning
 
-  open CommRingₚ commutativeRing public
+  open Fieldₚ realField public
     hiding ()
 
   1≉0 : 1ℝ ≉ 0ℝ
@@ -92,16 +93,6 @@ module ℝ where
     open ℤ.Reasoning
     open pseudocode using (module /1; module ⌊⌋)
 
-  x>0⇒x⁻¹>0 : ∀ {x} → (x≉0 : x ≉ 0ℝ) → x > 0ℝ → x≉0 ⁻¹ > 0ℝ
-  x>0⇒x⁻¹>0 {x} x≉0 x>0 = ≰⇒> (λ x⁻¹≤0 → <⇒≱ x>0 (begin
-    x               ≈˘⟨ *-identityˡ x ⟩
-    1ℝ * x          ≈˘⟨ *-congʳ (⁻¹-inverseˡ x≉0) ⟩
-    x≉0 ⁻¹ * x * x  ≤⟨  x≥0⇒*-monoʳ-≤ (<⇒≤ x>0) (x≤0⇒*-anti-monoˡ-≤ x⁻¹≤0 (<⇒≤ x>0)) ⟩
-    x≉0 ⁻¹ * 0ℝ * x ≈⟨  *-congʳ (zeroʳ (x≉0 ⁻¹)) ⟩
-    0ℝ * x          ≈⟨  zeroˡ x ⟩
-    0ℝ              ∎))
-    where open Reasoning
-
   record IsMonotoneContinuous (f : ℝ → ℝ) : Set (r₁ ⊔ r₂ ⊔ r₃) where
     field
       cong : f Preserves _≈_ ⟶ _≈_