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. --- Everything.agda | 15 ++++ .../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 ++++++++++++++++++++++ src/Helium/Data/Pseudocode/Algebra/Properties.agda | 65 +++++++++++++++++ 7 files changed, 284 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 create mode 100644 src/Helium/Data/Pseudocode/Algebra/Properties.agda 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_ +⁻¹-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 ∎ 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 -- cgit v1.2.3