From 91bc16d54ec0a6e5d904673951fe091a9973d9b4 Mon Sep 17 00:00:00 2001 From: Greg Brown Date: Tue, 18 Jan 2022 22:01:46 +0000 Subject: Define the semantics of pseudocode data types. --- .../Algebra/Ordered/StrictTotal/Bundles.agda | 182 +++++++++++++++++++-- .../Algebra/Ordered/StrictTotal/Structures.agda | 160 +++++++++++++++--- 2 files changed, 306 insertions(+), 36 deletions(-) (limited to 'src/Helium/Algebra/Ordered') diff --git a/src/Helium/Algebra/Ordered/StrictTotal/Bundles.agda b/src/Helium/Algebra/Ordered/StrictTotal/Bundles.agda index 6904bfb..a9430e9 100644 --- a/src/Helium/Algebra/Ordered/StrictTotal/Bundles.agda +++ b/src/Helium/Algebra/Ordered/StrictTotal/Bundles.agda @@ -10,13 +10,12 @@ module Helium.Algebra.Ordered.StrictTotal.Bundles where -import Algebra.Bundles as Unordered +import Algebra.Bundles as NoOrder open import Algebra.Core open import Data.Sum using (_⊎_) open import Function using (flip) open import Helium.Algebra.Core -open import Helium.Algebra.Bundles using - (RawAlmostGroup; AlmostGroup; AlmostAbelianGroup) +import Helium.Algebra.Bundles as NoOrder′ open import Helium.Algebra.Ordered.StrictTotal.Structures open import Level using (suc; _⊔_) open import Relation.Binary @@ -44,6 +43,10 @@ record RawMagma c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where _≥_ : Rel Carrier _ _≥_ = flip _≤_ + module Unordered where + rawMagma : NoOrder.RawMagma c ℓ₁ + rawMagma = record { _≈_ = _≈_ ; _∙_ = _∙_ } + record Magma c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where infixl 7 _∙_ infix 4 _≈_ _<_ @@ -55,6 +58,7 @@ record Magma c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where isMagma : IsMagma _≈_ _<_ _∙_ open IsMagma isMagma public + hiding (module Unordered) rawMagma : RawMagma _ _ _ rawMagma = record { _≈_ = _≈_; _<_ = _<_; _∙_ = _∙_ } @@ -62,6 +66,15 @@ record Magma c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where open RawMagma rawMagma public using (_≉_; _≤_; _>_; _≥_) + module Unordered where + magma : NoOrder.Magma c ℓ₁ + magma = record { isMagma = IsMagma.Unordered.isMagma isMagma } + + open NoOrder.Magma magma public + using (rawMagma) + + open IsMagma.Unordered isMagma public + record Semigroup c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where infixl 7 _∙_ infix 4 _≈_ _<_ @@ -73,6 +86,7 @@ record Semigroup c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where isSemigroup : IsSemigroup _≈_ _<_ _∙_ open IsSemigroup isSemigroup public + hiding (module Unordered) magma : Magma c ℓ₁ ℓ₂ magma = record { isMagma = isMagma } @@ -80,6 +94,16 @@ record Semigroup c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where open Magma magma public using (_≉_; _≤_; _>_; _≥_; rawMagma) + module Unordered where + semigroup : NoOrder.Semigroup c ℓ₁ + semigroup = + record { isSemigroup = IsSemigroup.Unordered.isSemigroup isSemigroup } + + open NoOrder.Semigroup semigroup public + using (rawMagma; magma) + + open IsSemigroup.Unordered isSemigroup public + record RawMonoid c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where infixl 7 _∙_ infix 4 _≈_ _<_ @@ -96,6 +120,13 @@ record RawMonoid c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where open RawMagma rawMagma public using (_≉_; _≤_; _>_; _≥_) + module Unordered where + rawMonoid : NoOrder.RawMonoid c ℓ₁ + rawMonoid = record { _≈_ = _≈_; _∙_ = _∙_; ε = ε } + + open NoOrder.RawMonoid rawMonoid public + using (rawMagma) + record Monoid c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where infixl 7 _∙_ infix 4 _≈_ _<_ @@ -108,6 +139,7 @@ record Monoid c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where isMonoid : IsMonoid _≈_ _<_ _∙_ ε open IsMonoid isMonoid public + hiding (module Unordered) semigroup : Semigroup _ _ _ semigroup = record { isSemigroup = isSemigroup } @@ -118,6 +150,15 @@ record Monoid c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where rawMonoid : RawMonoid _ _ _ rawMonoid = record { _≈_ = _≈_; _<_ = _<_; _∙_ = _∙_; ε = ε} + module Unordered where + monoid : NoOrder.Monoid c ℓ₁ + monoid = record { isMonoid = IsMonoid.Unordered.isMonoid isMonoid } + + open NoOrder.Monoid monoid public + using (rawMagma; rawMonoid; magma; semigroup) + + open IsMonoid.Unordered isMonoid public + record RawGroup c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where infix 8 _⁻¹ infixl 7 _∙_ @@ -136,6 +177,12 @@ record RawGroup c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where open RawMonoid rawMonoid public using (_≉_; _≤_; _>_; _≥_; rawMagma) + module Unordered where + rawGroup : NoOrder.RawGroup c ℓ₁ + rawGroup = record { _≈_ = _≈_; _∙_ = _∙_; ε = ε; _⁻¹ = _⁻¹ } + + open NoOrder.RawGroup rawGroup public + using (rawMagma; rawMonoid) record Group c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where infix 8 _⁻¹ @@ -151,6 +198,7 @@ record Group c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where isGroup : IsGroup _≈_ _<_ _∙_ ε _⁻¹ open IsGroup isGroup public + hiding (module Unordered) rawGroup : RawGroup _ _ _ rawGroup = record { _≈_ = _≈_; _<_ = _<_; _∙_ = _∙_; ε = ε; _⁻¹ = _⁻¹} @@ -161,6 +209,15 @@ record Group c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where open Monoid monoid public using (_≉_; _≤_; _>_; _≥_; rawMagma; magma; semigroup; rawMonoid) + module Unordered where + group : NoOrder.Group c ℓ₁ + group = record { isGroup = IsGroup.Unordered.isGroup isGroup } + + open NoOrder.Group group public + using (rawMagma; rawMonoid; rawGroup; magma; semigroup; monoid) + + open IsGroup.Unordered isGroup public + record AbelianGroup c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where infix 8 _⁻¹ infixl 7 _∙_ @@ -175,6 +232,7 @@ record AbelianGroup c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where isAbelianGroup : IsAbelianGroup _≈_ _<_ _∙_ ε _⁻¹ open IsAbelianGroup isAbelianGroup public + hiding (module Unordered) group : Group _ _ _ group = record { isGroup = isGroup } @@ -186,6 +244,16 @@ record AbelianGroup c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where ; rawMagma; rawMonoid; rawGroup ) + module Unordered where + abelianGroup : NoOrder.AbelianGroup c ℓ₁ + abelianGroup = + record { isAbelianGroup = IsAbelianGroup.Unordered.isAbelianGroup isAbelianGroup } + + open NoOrder.AbelianGroup abelianGroup public + using (rawMagma; rawMonoid; rawGroup; magma; semigroup; monoid; group) + + open IsAbelianGroup.Unordered isAbelianGroup public + record RawRing c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where infix 8 -_ infixl 7 _*_ @@ -211,13 +279,21 @@ record RawRing c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where ; rawMonoid to +-rawMonoid ) - *-rawMonoid : Unordered.RawMonoid c ℓ₁ + *-rawMonoid : NoOrder.RawMonoid c ℓ₁ *-rawMonoid = record { _≈_ = _≈_; _∙_ = _*_; ε = 1# } - open Unordered.RawMonoid *-rawMonoid public + open NoOrder.RawMonoid *-rawMonoid public using () renaming ( rawMagma to *-rawMagma ) + module Unordered where + rawRing : NoOrder.RawRing c ℓ₁ + rawRing = + record { _≈_ = _≈_ ; _+_ = _+_ ; _*_ = _*_ ; -_ = -_ ; 0# = 0# ; 1# = 1# } + + open NoOrder.RawRing rawRing public + using (+-rawMagma; +-rawMonoid; +-rawGroup; rawSemiring) + record Ring c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where infix 8 -_ infixl 7 _*_ @@ -235,6 +311,7 @@ record Ring c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where isRing : IsRing _≈_ _<_ _+_ _*_ -_ 0# 1# open IsRing isRing public + hiding (module Unordered) rawRing : RawRing c ℓ₁ ℓ₂ rawRing = record @@ -262,10 +339,10 @@ record Ring c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where ; group to +-group ) - *-monoid : Unordered.Monoid _ _ + *-monoid : NoOrder.Monoid _ _ *-monoid = record { isMonoid = *-isMonoid } - open Unordered.Monoid *-monoid public + open NoOrder.Monoid *-monoid public using () renaming ( rawMagma to *-rawMagma @@ -274,6 +351,19 @@ record Ring c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where ; semigroup to *-semigroup ) + module Unordered where + ring : NoOrder.Ring c ℓ₁ + ring = record { isRing = IsRing.Unordered.isRing isRing } + + open NoOrder.Ring ring public + using + ( +-rawMagma; +-rawMonoid + ; +-magma; +-semigroup; +-monoid; +-group; +-abelianGroup + ; rawRing; semiring + ) + + open IsRing.Unordered isRing public + record CommutativeRing c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where infix 8 -_ infixl 7 _*_ @@ -291,6 +381,7 @@ record CommutativeRing c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) whe isCommutativeRing : IsCommutativeRing _≈_ _<_ _+_ _*_ -_ 0# 1# open IsCommutativeRing isCommutativeRing public + hiding (module Unordered) ring : Ring _ _ _ ring = record { isRing = isRing } @@ -298,12 +389,30 @@ record CommutativeRing c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) whe open Ring ring public using ( _≉_; _≤_; _>_; _≥_ + ; rawRing ; +-rawMagma; +-rawMonoid; +-rawGroup ; +-magma; +-semigroup; +-monoid; +-group; +-abelianGroup ; *-rawMagma; *-rawMonoid ; *-magma; *-semigroup; *-monoid ) + module Unordered where + commutativeRing : NoOrder.CommutativeRing c ℓ₁ + commutativeRing = + record { isCommutativeRing = IsCommutativeRing.Unordered.isCommutativeRing isCommutativeRing } + + open NoOrder.CommutativeRing commutativeRing public + using + ( +-rawMagma; +-rawMonoid + ; +-magma; +-semigroup; +-monoid; +-group; +-abelianGroup + ; rawRing; semiring; ring + ) + + open NoOrder.Semiring semiring public + using (rawSemiring) + + open IsCommutativeRing.Unordered isCommutativeRing public + record RawField c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where infix 9 _⁻¹ infix 8 -_ @@ -343,7 +452,7 @@ record RawField c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where ; *-rawMagma; *-rawMonoid ) - *-rawAlmostGroup : RawAlmostGroup c ℓ₁ + *-rawAlmostGroup : NoOrder′.RawAlmostGroup c ℓ₁ *-rawAlmostGroup = record { _≈_ = _≈_ ; _∙_ = _*_ @@ -352,6 +461,21 @@ record RawField c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where ; _⁻¹ = _⁻¹ } + module Unordered where + rawField : NoOrder′.RawField c ℓ₁ + rawField = record + { _≈_ = _≈_ + ; _+_ = _+_ + ; _*_ = _*_ + ; -_ = -_ + ; 0# = 0# + ; 1# = 1# + ; _⁻¹ = _⁻¹ + } + + open NoOrder′.RawField rawField public + using (+-rawMagma; +-rawMonoid; +-rawGroup; rawSemiring; rawRing) + record DivisionRing c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where infix 9 _⁻¹ infix 8 -_ @@ -371,6 +495,7 @@ record DivisionRing c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where isDivisionRing : IsDivisionRing _≈_ _<_ _+_ _*_ -_ 0# 1# _⁻¹ open IsDivisionRing isDivisionRing public + hiding (module Unordered) rawField : RawField c ℓ₁ ℓ₂ rawField = record @@ -397,13 +522,28 @@ record DivisionRing c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where ; *-magma; *-semigroup; *-monoid ) - *-almostGroup : AlmostGroup _ _ + *-almostGroup : NoOrder′.AlmostGroup _ _ *-almostGroup = record { isAlmostGroup = *-isAlmostGroup } - open AlmostGroup *-almostGroup public + open NoOrder′.AlmostGroup *-almostGroup public using () renaming (rawAlmostGroup to *-rawAlmostGroup) + module Unordered where + divisionRing : NoOrder′.DivisionRing c ℓ₁ + divisionRing = + record { isDivisionRing = IsDivisionRing.Unordered.isDivisionRing isDivisionRing } + + open NoOrder′.DivisionRing divisionRing public + using + ( +-rawMagma; +-rawMonoid + ; +-magma; +-semigroup; +-monoid; +-group; +-abelianGroup + ; rawSemiring; rawRing + ; semiring; ring + ) + + open IsDivisionRing.Unordered isDivisionRing public + record Field c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where infix 9 _⁻¹ infix 8 -_ @@ -423,15 +563,35 @@ record Field c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where isField : IsField _≈_ _<_ _+_ _*_ -_ 0# 1# _⁻¹ open IsField isField public + hiding (module Unordered) divisionRing : DivisionRing c ℓ₁ ℓ₂ divisionRing = record { isDivisionRing = isDivisionRing } - open DivisionRing divisionRing + open DivisionRing divisionRing public using ( _≉_; _≤_; _>_; _≥_ + ; rawRing; rawField; ring ; +-rawMagma; +-rawMonoid; +-rawGroup ; +-magma; +-semigroup; +-monoid; +-group; +-abelianGroup ; *-rawMagma; *-rawMonoid; *-rawAlmostGroup ; *-magma; *-semigroup; *-monoid; *-almostGroup ) + + commutativeRing : CommutativeRing c ℓ₁ ℓ₂ + commutativeRing = record { isCommutativeRing = isCommutativeRing } + + module Unordered where + field′ : NoOrder′.Field c ℓ₁ + field′ = + record { isField = IsField.Unordered.isField isField } + + open NoOrder′.Field field′ public + using + ( +-rawMagma; +-rawMonoid + ; +-magma; +-semigroup; +-monoid; +-group; +-abelianGroup + ; rawSemiring; rawRing + ; semiring; ring; divisionRing + ) + + open IsField.Unordered isField public 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