From 5202560ea008a76048587f6ab63797f7517fbdc0 Mon Sep 17 00:00:00 2001 From: Greg Brown Date: Mon, 21 Mar 2022 16:37:12 +0000 Subject: Add some properties of algebraic pseudocode types. --- .../Algebra/Ordered/StrictTotal/Bundles.agda | 12 ++-- .../StrictTotal/Properties/AbelianGroup.agda | 31 +++++++++ .../StrictTotal/Properties/CommutativeRing.agda | 27 ++++++++ .../Ordered/StrictTotal/Properties/Group.agda | 59 ++++++++++++++++ .../Ordered/StrictTotal/Properties/Ring.agda | 81 ++++++++++++++++++++++ 5 files changed, 204 insertions(+), 6 deletions(-) create mode 100644 src/Helium/Algebra/Ordered/StrictTotal/Properties/AbelianGroup.agda create mode 100644 src/Helium/Algebra/Ordered/StrictTotal/Properties/CommutativeRing.agda create mode 100644 src/Helium/Algebra/Ordered/StrictTotal/Properties/Group.agda create mode 100644 src/Helium/Algebra/Ordered/StrictTotal/Properties/Ring.agda (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 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_ +⁻¹-anti-mono {x} {y} x⇒≉; ≈⇒≯; <⇒≉; ≈⇒≮; ≤∧≉⇒<; ≥∧≉⇒> + ; x) +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 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⇒≉ x : ∀ {x y} → x ≥ y → x ≉ y → x > y +≥∧≉⇒> x≥y x≉y = ≤∧≉⇒< x≥y (x≉y ∘ Eq.sym) + +x) +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 _ _ 0>1 = inj₁ (begin-strict + 0 <⟨ 01 ⟩ + -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 ∎ -- cgit v1.2.3