Add some properties of algebraic pseudocode types.

7 files changed, 284 insertions, 6 deletions

diff --git a/Everything.agda b/Everything.agda
index f6c6f84..1bebcbe 100644
--- a/Everything.agda
+++ b/Everything.agda
@@ -41,6 +41,18 @@ import Helium.Algebra.Ordered.Definitions
 -- (packed in records together with sets, operations, etc.)
 import Helium.Algebra.Ordered.StrictTotal.Bundles
 
+-- Algebraic properties of ordered abelian groups
+import Helium.Algebra.Ordered.StrictTotal.Properties.AbelianGroup
+
+-- Algebraic properties of ordered commutative rings
+import Helium.Algebra.Ordered.StrictTotal.Properties.CommutativeRing
+
+-- Algebraic properties of ordered groups
+import Helium.Algebra.Ordered.StrictTotal.Properties.Group
+
+-- Algebraic properties of ordered rings
+import Helium.Algebra.Ordered.StrictTotal.Properties.Ring
+
 -- Some ordered algebraic structures (not packed up with sets,
 -- operations, etc.)
 import Helium.Algebra.Ordered.StrictTotal.Structures
@@ -51,6 +63,9 @@ import Helium.Algebra.Structures
 -- Definition of types and operations used by the Armv8-M pseudocode.
 import Helium.Data.Pseudocode.Algebra
 
+-- Algebraic properties of types used by the Armv8-M pseudocode.
+import Helium.Data.Pseudocode.Algebra.Properties
+
 -- Definition of the Armv8-M pseudocode.
 import Helium.Data.Pseudocode.Core
 
diff --git a/src/Helium/Algebra/Ordered/StrictTotal/Bundles.agda b/src/Helium/Algebra/Ordered/StrictTotal/Bundles.agda
index a9430e9..831f591 100644
--- a/src/Helium/Algebra/Ordered/StrictTotal/Bundles.agda
+++ b/src/Helium/Algebra/Ordered/StrictTotal/Bundles.agda
@@ -250,7 +250,7 @@ record AbelianGroup c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
       record { isAbelianGroup = IsAbelianGroup.Unordered.isAbelianGroup isAbelianGroup }
 
     open NoOrder.AbelianGroup abelianGroup public
-      using (rawMagma; rawMonoid; rawGroup; magma; semigroup; monoid; group)
+      using (rawMagma; rawMonoid; rawGroup; magma; semigroup; monoid; commutativeMonoid; group)
 
     open IsAbelianGroup.Unordered isAbelianGroup public
 
@@ -358,7 +358,7 @@ record Ring c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
     open NoOrder.Ring ring public
       using
       ( +-rawMagma; +-rawMonoid
-      ; +-magma; +-semigroup; +-monoid; +-group; +-abelianGroup
+      ; +-magma; +-semigroup; +-monoid; +-commutativeMonoid; +-group; +-abelianGroup
       ; rawRing; semiring
       )
 
@@ -404,8 +404,8 @@ record CommutativeRing c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) whe
     open NoOrder.CommutativeRing commutativeRing public
       using
       ( +-rawMagma; +-rawMonoid
-      ; +-magma; +-semigroup; +-monoid; +-group; +-abelianGroup
-      ; rawRing; semiring; ring
+      ; +-magma; +-semigroup; +-monoid; +-commutativeMonoid; +-group; +-abelianGroup
+      ; rawRing; semiring; commutativeSemiring; ring
       )
 
     open NoOrder.Semiring semiring public
@@ -537,7 +537,7 @@ record DivisionRing c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
     open NoOrder′.DivisionRing divisionRing public
       using
       ( +-rawMagma; +-rawMonoid
-      ; +-magma; +-semigroup; +-monoid; +-group; +-abelianGroup
+      ; +-magma; +-semigroup; +-monoid; +-commutativeMonoid; +-group; +-abelianGroup
       ; rawSemiring; rawRing
       ; semiring; ring
       )
@@ -589,7 +589,7 @@ record Field c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where
     open NoOrder′.Field field′ public
       using
       ( +-rawMagma; +-rawMonoid
-      ; +-magma; +-semigroup; +-monoid; +-group; +-abelianGroup
+      ; +-magma; +-semigroup; +-monoid; +-commutativeMonoid; +-group; +-abelianGroup
       ; rawSemiring; rawRing
       ; semiring; ring; divisionRing
       )
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           ∎
diff --git a/src/Helium/Data/Pseudocode/Algebra/Properties.agda b/src/Helium/Data/Pseudocode/Algebra/Properties.agda
new file mode 100644
index 0000000..3ea96be
--- /dev/null
+++ b/src/Helium/Data/Pseudocode/Algebra/Properties.agda
@@ -0,0 +1,65 @@
+------------------------------------------------------------------------
+-- Agda Helium
+--
+-- Algebraic properties of types used by the Armv8-M pseudocode.
+------------------------------------------------------------------------
+
+{-# OPTIONS --safe --without-K #-}
+
+open import Helium.Data.Pseudocode.Algebra
+
+module Helium.Data.Pseudocode.Algebra.Properties
+  {b₁ b₂ i₁ i₂ i₃ r₁ r₂ r₃}
+  (pseudocode : Pseudocode b₁ b₂ i₁ i₂ i₃ r₁ r₂ r₃)
+  where
+
+open import Agda.Builtin.FromNat
+open import Agda.Builtin.FromNeg
+import Helium.Algebra.Ordered.StrictTotal.Properties.CommutativeRing as CommRingₚ
+open import Data.Nat using (NonZero)
+
+private
+  module pseudocode = Pseudocode pseudocode
+
+open pseudocode public
+  hiding
+  (1≉0; module ℤ; module ℤ′; module ℝ; module ℝ′; module ℤ-Reasoning; module ℝ-Reasoning)
+
+module ℤ where
+  open pseudocode.ℤ public hiding (ℤ; 0ℤ; 1ℤ)
+  module Reasoning = pseudocode.ℤ-Reasoning
+
+  open CommRingₚ integerRing public
+    hiding (1≉0+n≉0⇒0<+n; 1≉0+n≉0⇒-n<0)
+
+  1≉0 : 1 ≉ 0
+  1≉0 = pseudocode.1≉0
+
+  n≉0⇒0<+n : ∀ n → {{NonZero n}} → 0 < fromNat n
+  n≉0⇒0<+n = CommRingₚ.1≉0+n≉0⇒0<+n integerRing 1≉0
+
+  n≉0⇒-n<0 : ∀ n → {{NonZero n}} → fromNeg n < 0
+  n≉0⇒-n<0 = CommRingₚ.1≉0+n≉0⇒-n<0 integerRing 1≉0
+
+module ℝ where
+  open pseudocode.ℝ public hiding (ℝ; 0ℝ; 1ℝ)
+  module Reasoning = pseudocode.ℝ-Reasoning
+
+  open CommRingₚ commutativeRing public
+    hiding ()
+
+  1≉0 : 1 ≉ 0
+  1≉0 1≈0 = ℤ.1≉0 (begin-equality
+    1        ≈˘⟨ ⌊⌋∘/1≗id 1 ⟩
+    ⌊ 1 /1 ⌋ ≈⟨  ⌊⌋.cong /1.1#-homo ⟩
+    ⌊ 1 ⌋    ≈⟨  ⌊⌋.cong 1≈0 ⟩
+    ⌊ 0 ⌋    ≈˘⟨ ⌊⌋.cong /1.0#-homo ⟩
+    ⌊ 0 /1 ⌋ ≈⟨  ⌊⌋∘/1≗id 0 ⟩
+    0        ∎)
+    where open ℤ.Reasoning
+
+  n≉0⇒0<+n : ∀ n → {{NonZero n}} → 0 < fromNat n
+  n≉0⇒0<+n = CommRingₚ.1≉0+n≉0⇒0<+n commutativeRing 1≉0
+
+  n≉0⇒-n<0 : ∀ n → {{NonZero n}} → fromNeg n < 0
+  n≉0⇒-n<0 = CommRingₚ.1≉0+n≉0⇒-n<0 commutativeRing 1≉0