diff options
Diffstat (limited to 'src/Helium/Algebra/Ordered/StrictTotal/Properties')
4 files changed, 198 insertions, 0 deletions
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 ⁻¹ ∎ diff --git a/src/Helium/Algebra/Ordered/StrictTotal/Properties/CommutativeRing.agda b/src/Helium/Algebra/Ordered/StrictTotal/Properties/CommutativeRing.agda new file mode 100644 index 0000000..24b2663 --- /dev/null +++ b/src/Helium/Algebra/Ordered/StrictTotal/Properties/CommutativeRing.agda @@ -0,0 +1,27 @@ +------------------------------------------------------------------------ +-- Agda Helium +-- +-- Algebraic properties of ordered commutative rings +------------------------------------------------------------------------ + +{-# OPTIONS --safe --without-K #-} + +open import Helium.Algebra.Ordered.StrictTotal.Bundles + +module Helium.Algebra.Ordered.StrictTotal.Properties.CommutativeRing + {ℓ₁ ℓ₂ ℓ₃} + (commutativeRing : CommutativeRing ℓ₁ ℓ₂ ℓ₃) + where + +open CommutativeRing commutativeRing + +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.CommutativeSemiring.Exp.TCOptimised Unordered.commutativeSemiring public +open import Helium.Algebra.Ordered.StrictTotal.Properties.Ring ring public + using + ( <⇒≱; ≤⇒≯; >⇒≉; ≈⇒≯; <⇒≉; ≈⇒≮; ≤∧≉⇒<; ≥∧≉⇒> + ; x<y⇒0<y-x; -‿anti-mono + ; ⊤′; number; negative + ; 0≤1; 1≉0+n≉0⇒0<+n; 1≉0+n≉0⇒-n<0) diff --git a/src/Helium/Algebra/Ordered/StrictTotal/Properties/Group.agda b/src/Helium/Algebra/Ordered/StrictTotal/Properties/Group.agda new file mode 100644 index 0000000..c0723b3 --- /dev/null +++ b/src/Helium/Algebra/Ordered/StrictTotal/Properties/Group.agda @@ -0,0 +1,59 @@ +------------------------------------------------------------------------ +-- Agda Helium +-- +-- Algebraic properties of ordered groups +------------------------------------------------------------------------ + +{-# OPTIONS --safe --without-K #-} + +open import Helium.Algebra.Ordered.StrictTotal.Bundles + +module Helium.Algebra.Ordered.StrictTotal.Properties.Group + {ℓ₁ ℓ₂ ℓ₃} + (group : Group ℓ₁ ℓ₂ ℓ₃) + where + +open Group group + +open import Data.Sum using (inj₂; [_,_]′; fromInj₁) +open import Function using (_∘_; flip) +open import Relation.Binary using (tri<; tri≈; tri>) +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<y x≥y with compare x y +... | tri< _ x≉y x≱y = [ x≱y , x≉y ∘ Eq.sym ]′ x≥y +... | tri≈ x≮y _ _ = x≮y x<y +... | tri> x≮y _ _ = x≮y x<y + +≤⇒≯ : ∀ {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<y = >⇒≉ x<y ∘ Eq.sym + +≈⇒≮ : ∀ {x y} → x ≈ y → ¬ x < y +≈⇒≮ = flip <⇒≉ + +≤∧≉⇒< : ∀ {x y} → x ≤ y → x ≉ y → x < y +≤∧≉⇒< x≤y x≉y = fromInj₁ (λ x≈y → contradiction x≈y x≉y) x≤y + +≥∧≉⇒> : ∀ {x y} → x ≥ y → x ≉ y → x > y +≥∧≉⇒> x≥y x≉y = ≤∧≉⇒< x≥y (x≉y ∘ Eq.sym) + +x<y⇒ε<yx⁻¹ : ∀ {x y} → x < y → ε < y ∙ x ⁻¹ +x<y⇒ε<yx⁻¹ {x} {y} x<y = begin-strict + ε ≈˘⟨ inverseʳ x ⟩ + x ∙ x ⁻¹ <⟨ ∙-invariantʳ (x ⁻¹) x<y ⟩ + y ∙ x ⁻¹ ∎ diff --git a/src/Helium/Algebra/Ordered/StrictTotal/Properties/Ring.agda b/src/Helium/Algebra/Ordered/StrictTotal/Properties/Ring.agda new file mode 100644 index 0000000..484143c --- /dev/null +++ b/src/Helium/Algebra/Ordered/StrictTotal/Properties/Ring.agda @@ -0,0 +1,81 @@ +------------------------------------------------------------------------ +-- Agda Helium +-- +-- Algebraic properties of ordered rings +------------------------------------------------------------------------ + +{-# OPTIONS --safe --without-K #-} + +open import Helium.Algebra.Ordered.StrictTotal.Bundles + +module Helium.Algebra.Ordered.StrictTotal.Properties.Ring + {ℓ₁ ℓ₂ ℓ₃} + (ring : Ring ℓ₁ ℓ₂ ℓ₃) + where + +open Ring ring + +open import Agda.Builtin.FromNat +open import Agda.Builtin.FromNeg +open import Data.Nat using (suc; NonZero) +open import Data.Sum using (inj₁; inj₂) +open import Data.Unit.Polymorphic using (⊤) +open import Relation.Binary using (tri<; tri≈; tri>) +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<y⇒ε<yx⁻¹ to x<y⇒0<y-x + ; ⁻¹-anti-mono to -‿anti-mono + ) + +instance + ⊤′ : ∀ {ℓ} → ⊤ {ℓ = ℓ} + ⊤′ = _ + + number : Number Carrier + number = record + { Constraint = λ _ → ⊤ + ; fromNat = _× 1# + } + + negative : Negative Carrier + negative = record + { Constraint = λ _ → ⊤ + ; fromNeg = λ x → - (x × 1#) + } + +0≤1 : 0 ≤ 1 +0≤1 with compare 0 1 +... | tri< 0<1 _ _ = inj₁ 0<1 +... | tri≈ _ 0≈1 _ = inj₂ 0≈1 +... | tri> _ _ 0>1 = inj₁ (begin-strict + 0 <⟨ 0<a+0<b⇒0<ab 0<-1 0<-1 ⟩ + -1 * -1 ≈˘⟨ -‿distribˡ-* 1 -1 ⟩ + - (1 * -1) ≈⟨ -‿cong (*-identityˡ -1) ⟩ + - -1 ≈⟨ -‿involutive 1 ⟩ + 1 ∎) + where + 0<-1 = begin-strict + 0 ≈˘⟨ -0≈0 ⟩ + - 0 <⟨ -‿anti-mono 0>1 ⟩ + -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 ∎ |