Add some properties of algebraic pseudocode types.

4 files changed, 198 insertions, 0 deletions

diff --git a/src/Helium/Algebra/Ordered/StrictTotal/Properties/AbelianGroup.agda b/src/Helium/Algebra/Ordered/StrictTotal/Properties/AbelianGroup.agda
new file mode 100644
index 0000000..fe64b32
--- /dev/null
+++ b/src/Helium/Algebra/Ordered/StrictTotal/Properties/AbelianGroup.agda
@@ -0,0 +1,31 @@
+------------------------------------------------------------------------
+-- Agda Helium
+--
+-- Algebraic properties of ordered abelian groups
+------------------------------------------------------------------------
+
+{-# OPTIONS --safe --without-K #-}
+
+open import Helium.Algebra.Ordered.StrictTotal.Bundles
+
+module Helium.Algebra.Ordered.StrictTotal.Properties.AbelianGroup
+  {ℓ₁ ℓ₂ ℓ₃}
+  (abelianGroup : AbelianGroup ℓ₁ ℓ₂ ℓ₃)
+  where
+
+open AbelianGroup abelianGroup
+
+open import Relation.Binary.Core
+open import Relation.Binary.Reasoning.StrictPartialOrder strictPartialOrder
+
+open import Algebra.Properties.AbelianGroup Unordered.abelianGroup public
+open import Algebra.Properties.CommutativeMonoid.Mult.TCOptimised Unordered.commutativeMonoid public
+open import Helium.Algebra.Ordered.StrictTotal.Properties.Group group public
+  using (<⇒≱; ≤⇒≯; >⇒≉; ≈⇒≯; <⇒≉; ≈⇒≮; ≤∧≉⇒<; ≥∧≉⇒>; x<y⇒ε<yx⁻¹)
+
+⁻¹-anti-mono : _⁻¹ Preserves _<_ ⟶ _>_
+⁻¹-anti-mono {x} {y} x<y = begin-strict
+  y ⁻¹            ≈˘⟨ identityˡ (y ⁻¹) ⟩
+  ε ∙ y ⁻¹        <⟨  ∙-invariantʳ (y ⁻¹) (x<y⇒ε<yx⁻¹ x<y) ⟩
+  y ∙ x ⁻¹ ∙ y ⁻¹ ≈⟨  xyx⁻¹≈y y (x ⁻¹) ⟩
+  x ⁻¹            ∎
diff --git a/src/Helium/Algebra/Ordered/StrictTotal/Properties/CommutativeRing.agda b/src/Helium/Algebra/Ordered/StrictTotal/Properties/CommutativeRing.agda
new file mode 100644
index 0000000..24b2663
--- /dev/null
+++ b/src/Helium/Algebra/Ordered/StrictTotal/Properties/CommutativeRing.agda
@@ -0,0 +1,27 @@
+------------------------------------------------------------------------
+-- Agda Helium
+--
+-- Algebraic properties of ordered commutative rings
+------------------------------------------------------------------------
+
+{-# OPTIONS --safe --without-K #-}
+
+open import Helium.Algebra.Ordered.StrictTotal.Bundles
+
+module Helium.Algebra.Ordered.StrictTotal.Properties.CommutativeRing
+  {ℓ₁ ℓ₂ ℓ₃}
+  (commutativeRing : CommutativeRing ℓ₁ ℓ₂ ℓ₃)
+  where
+
+open CommutativeRing commutativeRing
+
+open import Algebra.Properties.Ring Unordered.ring public
+  renaming (-0#≈0# to -0≈0)
+open import Algebra.Properties.Semiring.Mult.TCOptimised Unordered.semiring public
+open import Algebra.Properties.CommutativeSemiring.Exp.TCOptimised Unordered.commutativeSemiring public
+open import Helium.Algebra.Ordered.StrictTotal.Properties.Ring ring public
+  using
+  ( <⇒≱; ≤⇒≯; >⇒≉; ≈⇒≯; <⇒≉; ≈⇒≮; ≤∧≉⇒<; ≥∧≉⇒>
+  ; x<y⇒0<y-x; -‿anti-mono
+  ; ⊤′; number; negative
+  ; 0≤1; 1≉0+n≉0⇒0<+n; 1≉0+n≉0⇒-n<0)
diff --git a/src/Helium/Algebra/Ordered/StrictTotal/Properties/Group.agda b/src/Helium/Algebra/Ordered/StrictTotal/Properties/Group.agda
new file mode 100644
index 0000000..c0723b3
--- /dev/null
+++ b/src/Helium/Algebra/Ordered/StrictTotal/Properties/Group.agda
@@ -0,0 +1,59 @@
+------------------------------------------------------------------------
+-- Agda Helium
+--
+-- Algebraic properties of ordered groups
+------------------------------------------------------------------------
+
+{-# OPTIONS --safe --without-K #-}
+
+open import Helium.Algebra.Ordered.StrictTotal.Bundles
+
+module Helium.Algebra.Ordered.StrictTotal.Properties.Group
+  {ℓ₁ ℓ₂ ℓ₃}
+  (group : Group ℓ₁ ℓ₂ ℓ₃)
+  where
+
+open Group group
+
+open import Data.Sum using (inj₂; [_,_]′; fromInj₁)
+open import Function using (_∘_; flip)
+open import Relation.Binary using (tri<; tri≈; tri>)
+open import Relation.Binary.Reasoning.StrictPartialOrder strictPartialOrder
+open import Relation.Nullary using (¬_)
+open import Relation.Nullary.Negation using (contradiction)
+
+open import Algebra.Properties.Group Unordered.group public
+open import Algebra.Properties.Monoid.Mult.TCOptimised Unordered.monoid public
+
+<⇒≱ : ∀ {x y} → x < y → ¬ x ≥ y
+<⇒≱ {x} {y} x<y x≥y with compare x y
+... | tri< _   x≉y x≱y = [ x≱y , x≉y ∘ Eq.sym ]′ x≥y
+... | tri≈ x≮y _   _   = x≮y x<y
+... | tri> x≮y _   _   = x≮y x<y
+
+≤⇒≯ : ∀ {x y} → x ≤ y → ¬ x > y
+≤⇒≯ = flip <⇒≱
+
+>⇒≉ : ∀ {x y} → x > y → x ≉ y
+>⇒≉ x>y = <⇒≱ x>y ∘ inj₂
+
+≈⇒≯ : ∀ {x y} → x ≈ y → ¬ x > y
+≈⇒≯ = flip >⇒≉
+
+<⇒≉ : ∀ {x y} → x < y → x ≉ y
+<⇒≉ x<y = >⇒≉ x<y ∘ Eq.sym
+
+≈⇒≮ : ∀ {x y} → x ≈ y → ¬ x < y
+≈⇒≮ = flip <⇒≉
+
+≤∧≉⇒< : ∀ {x y} → x ≤ y → x ≉ y → x < y
+≤∧≉⇒< x≤y x≉y = fromInj₁ (λ x≈y → contradiction x≈y x≉y) x≤y
+
+≥∧≉⇒> : ∀ {x y} → x ≥ y → x ≉ y → x > y
+≥∧≉⇒> x≥y x≉y = ≤∧≉⇒< x≥y (x≉y ∘ Eq.sym)
+
+x<y⇒ε<yx⁻¹ : ∀ {x y} → x < y → ε < y ∙ x ⁻¹
+x<y⇒ε<yx⁻¹ {x} {y} x<y = begin-strict
+  ε        ≈˘⟨ inverseʳ x ⟩
+  x ∙ x ⁻¹ <⟨  ∙-invariantʳ (x ⁻¹) x<y ⟩
+  y ∙ x ⁻¹ ∎
diff --git a/src/Helium/Algebra/Ordered/StrictTotal/Properties/Ring.agda b/src/Helium/Algebra/Ordered/StrictTotal/Properties/Ring.agda
new file mode 100644
index 0000000..484143c
--- /dev/null
+++ b/src/Helium/Algebra/Ordered/StrictTotal/Properties/Ring.agda
@@ -0,0 +1,81 @@
+------------------------------------------------------------------------
+-- Agda Helium
+--
+-- Algebraic properties of ordered rings
+------------------------------------------------------------------------
+
+{-# OPTIONS --safe --without-K #-}
+
+open import Helium.Algebra.Ordered.StrictTotal.Bundles
+
+module Helium.Algebra.Ordered.StrictTotal.Properties.Ring
+  {ℓ₁ ℓ₂ ℓ₃}
+  (ring : Ring ℓ₁ ℓ₂ ℓ₃)
+  where
+
+open Ring ring
+
+open import Agda.Builtin.FromNat
+open import Agda.Builtin.FromNeg
+open import Data.Nat using (suc; NonZero)
+open import Data.Sum using (inj₁; inj₂)
+open import Data.Unit.Polymorphic using (⊤)
+open import Relation.Binary using (tri<; tri≈; tri>)
+open import Relation.Binary.Reasoning.StrictPartialOrder strictPartialOrder
+
+open import Algebra.Properties.Ring Unordered.ring public
+  renaming (-0#≈0# to -0≈0)
+open import Algebra.Properties.Semiring.Mult.TCOptimised Unordered.semiring public
+open import Algebra.Properties.Semiring.Exp.TCOptimised Unordered.semiring public
+open import Helium.Algebra.Ordered.StrictTotal.Properties.AbelianGroup +-abelianGroup public
+  using (<⇒≱; ≤⇒≯; >⇒≉; ≈⇒≯; <⇒≉; ≈⇒≮; ≤∧≉⇒<; ≥∧≉⇒>)
+  renaming
+    ( x<y⇒ε<yx⁻¹ to x<y⇒0<y-x
+    ; ⁻¹-anti-mono to -‿anti-mono
+    )
+
+instance
+  ⊤′ : ∀ {ℓ} → ⊤ {ℓ = ℓ}
+  ⊤′ = _
+
+  number : Number Carrier
+  number = record
+    { Constraint = λ _ → ⊤
+    ; fromNat = _× 1#
+    }
+
+  negative : Negative Carrier
+  negative = record
+    { Constraint = λ _ → ⊤
+    ; fromNeg = λ x → - (x × 1#)
+    }
+
+0≤1 : 0 ≤ 1
+0≤1 with compare 0 1
+... | tri< 0<1 _ _ = inj₁ 0<1
+... | tri≈ _ 0≈1 _ = inj₂ 0≈1
+... | tri> _ _ 0>1 = inj₁ (begin-strict
+  0          <⟨  0<a+0<b⇒0<ab 0<-1 0<-1 ⟩
+  -1 * -1    ≈˘⟨ -‿distribˡ-* 1 -1 ⟩
+  - (1 * -1) ≈⟨  -‿cong (*-identityˡ -1) ⟩
+  - -1       ≈⟨  -‿involutive 1 ⟩
+  1          ∎)
+  where
+  0<-1 = begin-strict
+    0   ≈˘⟨ -0≈0 ⟩
+    - 0 <⟨  -‿anti-mono 0>1 ⟩
+    -1  ∎
+
+1≉0+n≉0⇒0<+n : 1 ≉ 0 → ∀ n → {{NonZero n}} → 0 < fromNat n
+1≉0+n≉0⇒0<+n 1≉0 (suc 0)       = ≥∧≉⇒> 0≤1 1≉0
+1≉0+n≉0⇒0<+n 1≉0 (suc (suc n)) = begin-strict
+  0                   ≈˘⟨ +-identity² ⟩
+  0 + 0               <⟨  +-invariantˡ 0 (≥∧≉⇒> 0≤1 1≉0) ⟩
+  0 + 1               <⟨  +-invariantʳ 1 (1≉0+n≉0⇒0<+n 1≉0 (suc n)) ⟩
+  fromNat (suc n) + 1 ∎
+
+1≉0+n≉0⇒-n<0 : 1 ≉ 0 → ∀ n → {{NonZero n}} → fromNeg n < 0
+1≉0+n≉0⇒-n<0 1≉0 n = begin-strict
+  - fromNat n <⟨ -‿anti-mono (1≉0+n≉0⇒0<+n 1≉0 n) ⟩
+  - 0         ≈⟨ -0≈0 ⟩
+  0           ∎