From 5202560ea008a76048587f6ab63797f7517fbdc0 Mon Sep 17 00:00:00 2001
From: Greg Brown <greg.brown@cl.cam.ac.uk>
Date: Mon, 21 Mar 2022 16:37:12 +0000
Subject: Add some properties of algebraic pseudocode types.

---
 .../StrictTotal/Properties/AbelianGroup.agda       | 31 ++++++++++++++++++++++
 1 file changed, 31 insertions(+)
 create mode 100644 src/Helium/Algebra/Ordered/StrictTotal/Properties/AbelianGroup.agda

(limited to 'src/Helium/Algebra/Ordered/StrictTotal/Properties/AbelianGroup.agda')

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 ⁻¹            ∎
-- 
cgit v1.2.3