From 91bc16d54ec0a6e5d904673951fe091a9973d9b4 Mon Sep 17 00:00:00 2001
From: Greg Brown <greg.brown@cl.cam.ac.uk>
Date: Tue, 18 Jan 2022 22:01:46 +0000
Subject: Define the semantics of pseudocode data types.

---
 .../Algebra/Ordered/StrictTotal/Structures.agda    | 160 +++++++++++++++++----
 1 file changed, 135 insertions(+), 25 deletions(-)

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

diff --git a/src/Helium/Algebra/Ordered/StrictTotal/Structures.agda b/src/Helium/Algebra/Ordered/StrictTotal/Structures.agda
index 9dc0043..6f6b38d 100644
--- a/src/Helium/Algebra/Ordered/StrictTotal/Structures.agda
+++ b/src/Helium/Algebra/Ordered/StrictTotal/Structures.agda
@@ -18,11 +18,11 @@ module Helium.Algebra.Ordered.StrictTotal.Structures
 import Algebra.Consequences.Setoid as Consequences
 open import Algebra.Core
 open import Algebra.Definitions _≈_
-import Algebra.Structures _≈_ as Unordered
+import Algebra.Structures _≈_ as NoOrder
 open import Data.Product using (_,_; proj₁; proj₂)
 open import Helium.Algebra.Core
 open import Helium.Algebra.Definitions _≈_
-open import Helium.Algebra.Structures _≈_ using (IsAlmostGroup)
+import Helium.Algebra.Structures _≈_ as NoOrder′
 open import Helium.Algebra.Ordered.Definitions _<_
 open import Level using (_⊔_)
 
@@ -52,26 +52,55 @@ record IsMagma (∙ : Op₂ A) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
   ∙-invariantʳ : RightInvariant ∙
   ∙-invariantʳ = proj₂ ∙-invariant
 
+  module Unordered where
+    isMagma : NoOrder.IsMagma ∙
+    isMagma = record { isEquivalence = isEquivalence ; ∙-cong = ∙-cong }
+
 record IsSemigroup (∙ : Op₂ A) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
   field
     isMagma : IsMagma ∙
     assoc   : Associative ∙
 
   open IsMagma isMagma public
+    hiding (module Unordered)
+
+  module Unordered where
+    isSemigroup : NoOrder.IsSemigroup ∙
+    isSemigroup = record
+      { isMagma = IsMagma.Unordered.isMagma isMagma
+      ; assoc   = assoc
+      }
+
+    open NoOrder.IsSemigroup isSemigroup public
+      using (isMagma)
 
-record IsMonoid (∙ : Op₂ A) (ε : A) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
+record IsMonoid (_∙_ : Op₂ A) (ε : A) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
   field
-    isSemigroup : IsSemigroup ∙
-    identity    : Identity ε ∙
+    isSemigroup : IsSemigroup _∙_
+    identity    : Identity ε _∙_
 
   open IsSemigroup isSemigroup public
+    hiding (module Unordered)
 
-  identityˡ : LeftIdentity ε ∙
+  identityˡ : LeftIdentity ε _∙_
   identityˡ = proj₁ identity
 
-  identityʳ : RightIdentity ε ∙
+  identityʳ : RightIdentity ε _∙_
   identityʳ = proj₂ identity
 
+  identity² : (ε ∙ ε) ≈ ε
+  identity² = identityˡ ε
+
+  module Unordered where
+    isMonoid : NoOrder.IsMonoid _∙_ ε
+    isMonoid = record
+      { isSemigroup = IsSemigroup.Unordered.isSemigroup isSemigroup
+      ; identity    = identity
+      }
+
+    open NoOrder.IsMonoid isMonoid public
+      using (isMagma; isSemigroup)
+
 record IsGroup (_∙_ : Op₂ A) (ε : A) (_⁻¹ : Op₁ A) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
   field
     isMonoid  : IsMonoid _∙_ ε
@@ -79,6 +108,7 @@ record IsGroup (_∙_ : Op₂ A) (ε : A) (_⁻¹ : Op₁ A) : Set (a ⊔ ℓ₁
     ⁻¹-cong   : Congruent₁ _⁻¹
 
   open IsMonoid isMonoid public
+    hiding (module Unordered)
 
   infixl 6 _-_
   _-_ : Op₂ A
@@ -98,6 +128,17 @@ record IsGroup (_∙_ : Op₂ A) (ε : A) (_⁻¹ : Op₁ A) : Set (a ⊔ ℓ₁
   uniqueʳ-⁻¹ = Consequences.assoc+id+invˡ⇒invʳ-unique
                 strictTotalOrder.Eq.setoid ∙-cong assoc identity inverseˡ
 
+  module Unordered where
+    isGroup : NoOrder.IsGroup _∙_ ε _⁻¹
+    isGroup = record
+      { isMonoid = IsMonoid.Unordered.isMonoid isMonoid
+      ; inverse  = inverse
+      ; ⁻¹-cong  = ⁻¹-cong
+      }
+
+    open NoOrder.IsGroup isGroup public
+      using (isMagma; isSemigroup; isMonoid)
+
 record IsAbelianGroup (∙ : Op₂ A)
                       (ε : A) (⁻¹ : Op₁ A) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
   field
@@ -105,14 +146,25 @@ record IsAbelianGroup (∙ : Op₂ A)
     comm    : Commutative ∙
 
   open IsGroup isGroup public
+    hiding (module Unordered)
+
+  module Unordered where
+    isAbelianGroup : NoOrder.IsAbelianGroup ∙ ε ⁻¹
+    isAbelianGroup = record
+      { isGroup = IsGroup.Unordered.isGroup isGroup
+      ; comm    = comm
+      }
 
-record IsRing (+ * : Op₂ A) (-_ : Op₁ A) (0# 1# : A) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
+    open NoOrder.IsAbelianGroup isAbelianGroup public
+      using (isMagma; isSemigroup; isMonoid; isGroup)
+
+record IsRing (+ _*_ : Op₂ A) (-_ : Op₁ A) (0# 1# : A) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
   field
-    +-isAbelianGroup  : IsAbelianGroup + 0# -_
-    *-isMonoid        : Unordered.IsMonoid * 1#
-    distrib           : * DistributesOver +
-    zero              : Zero 0# *
-    preservesPositive : PreservesPositive 0# *
+    +-isAbelianGroup : IsAbelianGroup + 0# -_
+    *-isMonoid       : NoOrder.IsMonoid _*_ 1#
+    distrib          : _*_ DistributesOver +
+    zero             : Zero 0# _*_
+    0<a+0<b⇒0<ab     : PreservesPositive 0# _*_
 
   open IsAbelianGroup +-isAbelianGroup public
     renaming
@@ -120,9 +172,13 @@ record IsRing (+ * : Op₂ A) (-_ : Op₁ A) (0# 1# : A) : Set (a ⊔ ℓ₁ ⊔
     ; ∙-cong                 to +-cong
     ; ∙-congˡ                to +-congˡ
     ; ∙-congʳ                to +-congʳ
+    ; ∙-invariant            to +-invariant
+    ; ∙-invariantˡ           to +-invariantˡ
+    ; ∙-invariantʳ           to +-invariantʳ
     ; identity               to +-identity
     ; identityˡ              to +-identityˡ
     ; identityʳ              to +-identityʳ
+    ; identity²              to +-identity²
     ; inverse                to -‿inverse
     ; inverseˡ               to -‿inverseˡ
     ; inverseʳ               to -‿inverseʳ
@@ -133,8 +189,9 @@ record IsRing (+ * : Op₂ A) (-_ : Op₁ A) (0# 1# : A) : Set (a ⊔ ℓ₁ ⊔
     ; isMonoid               to +-isMonoid
     ; isGroup                to +-isGroup
     )
+    hiding (module Unordered)
 
-  open Unordered.IsMonoid *-isMonoid public
+  open NoOrder.IsMonoid *-isMonoid public
     using ()
     renaming
     ( assoc       to *-assoc
@@ -148,18 +205,33 @@ record IsRing (+ * : Op₂ A) (-_ : Op₁ A) (0# 1# : A) : Set (a ⊔ ℓ₁ ⊔
     ; isSemigroup to *-isSemigroup
     )
 
-  distribˡ : * DistributesOverˡ +
+  *-identity² : (1# * 1#) ≈ 1#
+  *-identity² = *-identityˡ 1#
+
+  distribˡ : _*_ DistributesOverˡ +
   distribˡ = proj₁ distrib
 
-  distribʳ : * DistributesOverʳ +
+  distribʳ : _*_ DistributesOverʳ +
   distribʳ = proj₂ distrib
 
-  zeroˡ : LeftZero 0# *
+  zeroˡ : LeftZero 0# _*_
   zeroˡ = proj₁ zero
 
-  zeroʳ : RightZero 0# *
+  zeroʳ : RightZero 0# _*_
   zeroʳ = proj₂ zero
 
+  module Unordered where
+    isRing : NoOrder.IsRing + _*_ -_ 0# 1#
+    isRing = record
+      { +-isAbelianGroup = IsAbelianGroup.Unordered.isAbelianGroup +-isAbelianGroup
+      ; *-isMonoid       = *-isMonoid
+      ; distrib          = distrib
+      ; zero             = zero
+      }
+
+    open NoOrder.IsRing isRing
+      using (+-isMagma; +-isSemigroup; +-isMonoid; +-isGroup)
+
 record IsCommutativeRing
          (+ * : Op₂ A) (- : Op₁ A) (0# 1# : A) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
   field
@@ -167,16 +239,27 @@ record IsCommutativeRing
     *-comm : Commutative *
 
   open IsRing isRing public
+    hiding (module Unordered)
+
+  module Unordered where
+    isCommutativeRing : NoOrder.IsCommutativeRing + * (-) 0# 1#
+    isCommutativeRing = record
+      { isRing = IsRing.Unordered.isRing isRing
+      ; *-comm = *-comm
+      }
+
+    open NoOrder.IsCommutativeRing isCommutativeRing public
+      using (+-isMagma; +-isSemigroup; +-isMonoid; +-isGroup; isRing)
 
 record IsDivisionRing
          (+ _*_ : Op₂ A) (-_ : Op₁ A) (0# 1# : A)
          (_⁻¹ : AlmostOp₁ _≈_ 0#) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
   field
-    +-isAbelianGroup  : IsAbelianGroup + 0# -_
-    *-isAlmostGroup   : IsAlmostGroup _*_ 0# 1# _⁻¹
-    distrib           : _*_ DistributesOver +
-    zero              : Zero 0# _*_
-    preservesPositive : PreservesPositive 0# _*_
+    +-isAbelianGroup : IsAbelianGroup + 0# -_
+    *-isAlmostGroup  : NoOrder′.IsAlmostGroup _*_ 0# 1# _⁻¹
+    distrib          : _*_ DistributesOver +
+    zero             : Zero 0# _*_
+    0<a+0<b⇒0<ab     : PreservesPositive 0# _*_
 
   infixl 7 _/_
   _/_ : AlmostOp₂ _≈_ 0#
@@ -203,8 +286,9 @@ record IsDivisionRing
     ; isMonoid               to +-isMonoid
     ; isGroup                to +-isGroup
     )
+    hiding (module Unordered)
 
-  open IsAlmostGroup *-isAlmostGroup public
+  open NoOrder′.IsAlmostGroup *-isAlmostGroup public
     using (⁻¹-cong; uniqueˡ-⁻¹; uniqueʳ-⁻¹)
     renaming
     ( assoc       to *-assoc
@@ -228,12 +312,24 @@ record IsDivisionRing
     ; *-isMonoid = *-isMonoid
     ; distrib = distrib
     ; zero = zero
-    ; preservesPositive = preservesPositive
+    ; 0<a+0<b⇒0<ab = 0<a+0<b⇒0<ab
     }
 
   open IsRing isRing public
     using (distribˡ ; distribʳ ; zeroˡ ; zeroʳ)
 
+  module Unordered where
+    isDivisionRing : NoOrder′.IsDivisionRing + _*_ -_ 0# 1# _⁻¹
+    isDivisionRing = record
+      { +-isAbelianGroup = IsAbelianGroup.Unordered.isAbelianGroup +-isAbelianGroup
+      ; *-isAlmostGroup  = *-isAlmostGroup
+      ; distrib          = distrib
+      ; zero             = zero
+      }
+
+    open NoOrder′.IsDivisionRing isDivisionRing
+      using (+-isMagma; +-isSemigroup; +-isMonoid; +-isGroup; isRing)
+
 record IsField
          (+ * : Op₂ A) (-_ : Op₁ A) (0# 1# : A)
          (⁻¹ : AlmostOp₁ _≈_ 0#) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
@@ -242,9 +338,23 @@ record IsField
     *-comm         : Commutative *
 
   open IsDivisionRing isDivisionRing public
+    hiding (module Unordered)
 
   isCommutativeRing : IsCommutativeRing + * -_ 0# 1#
   isCommutativeRing = record
     { isRing = isRing
     ; *-comm = *-comm
     }
+
+  module Unordered where
+    isField : NoOrder′.IsField + * -_ 0# 1# ⁻¹
+    isField = record
+      { isDivisionRing = IsDivisionRing.Unordered.isDivisionRing isDivisionRing
+      ; *-comm         = *-comm
+      }
+
+    open NoOrder′.IsField isField
+      using
+      ( +-isMagma; +-isSemigroup; +-isMonoid; +-isGroup
+      ; isRing; isDivisionRing
+      )
-- 
cgit v1.2.3