diff options
Diffstat (limited to 'src/Helium/Algebra')
11 files changed, 1537 insertions, 171 deletions
diff --git a/src/Helium/Algebra/Morphism/Structures.agda b/src/Helium/Algebra/Morphism/Structures.agda deleted file mode 100644 index bf219ef..0000000 --- a/src/Helium/Algebra/Morphism/Structures.agda +++ /dev/null @@ -1,42 +0,0 @@ ------------------------------------------------------------------------- --- Agda Helium --- --- Redefine Ring monomorphisms to resolve problems with overloading. ------------------------------------------------------------------------- - -{-# OPTIONS --safe --without-K #-} - -module Helium.Algebra.Morphism.Structures where - -open import Algebra.Bundles using (RawRing) -open import Algebra.Morphism.Structures - hiding (IsRingHomomorphism; module RingMorphisms) -open import Level using (Level; _⊔_) - -private - variable - a b ℓ₁ ℓ₂ : Level - -module RingMorphisms (R₁ : RawRing a ℓ₁) (R₂ : RawRing b ℓ₂) where - module R₁ = RawRing R₁ renaming (Carrier to A) - module R₂ = RawRing R₂ renaming (Carrier to B) - open R₁ using (A) - open R₂ using (B) - - private - module +′ = GroupMorphisms R₁.+-rawGroup R₂.+-rawGroup - module *′ = MonoidMorphisms R₁.*-rawMonoid R₂.*-rawMonoid - - record IsRingHomomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where - field - +-isGroupHomomorphism : +′.IsGroupHomomorphism ⟦_⟧ - *-isMonoidHomomorphism : *′.IsMonoidHomomorphism ⟦_⟧ - - open +′.IsGroupHomomorphism +-isGroupHomomorphism public - renaming (homo to +-homo; ε-homo to 0#-homo; ⁻¹-homo to -‿homo) - - open *′.IsMonoidHomomorphism *-isMonoidHomomorphism public - hiding (⟦⟧-cong) - renaming (homo to *-homo; ε-homo to 1#-homo) - -open RingMorphisms public diff --git a/src/Helium/Algebra/Ordered/StrictTotal/Bundles.agda b/src/Helium/Algebra/Ordered/StrictTotal/Bundles.agda index 831f591..0f8df22 100644 --- a/src/Helium/Algebra/Ordered/StrictTotal/Bundles.agda +++ b/src/Helium/Algebra/Ordered/StrictTotal/Bundles.agda @@ -30,19 +30,6 @@ record RawMagma c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where _<_ : Rel Carrier ℓ₂ _∙_ : Op₂ Carrier - infix 4 _≉_ _≤_ _>_ _≥_ - _≉_ : Rel Carrier _ - x ≉ y = N.¬ x ≈ y - - _≤_ : Rel Carrier _ - x ≤ y = x < y ⊎ x ≈ y - - _>_ : Rel Carrier _ - _>_ = flip _<_ - - _≥_ : Rel Carrier _ - _≥_ = flip _≤_ - module Unordered where rawMagma : NoOrder.RawMagma c ℓ₁ rawMagma = record { _≈_ = _≈_ ; _∙_ = _∙_ } @@ -63,9 +50,6 @@ record Magma c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where rawMagma : RawMagma _ _ _ rawMagma = record { _≈_ = _≈_; _<_ = _<_; _∙_ = _∙_ } - open RawMagma rawMagma public - using (_≉_; _≤_; _>_; _≥_) - module Unordered where magma : NoOrder.Magma c ℓ₁ magma = record { isMagma = IsMagma.Unordered.isMagma isMagma } @@ -92,7 +76,7 @@ record Semigroup c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where magma = record { isMagma = isMagma } open Magma magma public - using (_≉_; _≤_; _>_; _≥_; rawMagma) + using (rawMagma) module Unordered where semigroup : NoOrder.Semigroup c ℓ₁ @@ -117,9 +101,6 @@ record RawMonoid c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where rawMagma : RawMagma c ℓ₁ ℓ₂ rawMagma = record { _≈_ = _≈_; _<_ = _<_; _∙_ = _∙_ } - open RawMagma rawMagma public - using (_≉_; _≤_; _>_; _≥_) - module Unordered where rawMonoid : NoOrder.RawMonoid c ℓ₁ rawMonoid = record { _≈_ = _≈_; _∙_ = _∙_; ε = ε } @@ -145,7 +126,7 @@ record Monoid c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where semigroup = record { isSemigroup = isSemigroup } open Semigroup semigroup public - using (_≉_; _≤_; _>_; _≥_; rawMagma; magma) + using (rawMagma; magma) rawMonoid : RawMonoid _ _ _ rawMonoid = record { _≈_ = _≈_; _<_ = _<_; _∙_ = _∙_; ε = ε} @@ -175,7 +156,7 @@ record RawGroup c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where rawMonoid = record { _≈_ = _≈_; _<_ = _<_; _∙_ = _∙_; ε = ε } open RawMonoid rawMonoid public - using (_≉_; _≤_; _>_; _≥_; rawMagma) + using (rawMagma) module Unordered where rawGroup : NoOrder.RawGroup c ℓ₁ @@ -207,7 +188,7 @@ record Group c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where monoid = record { isMonoid = isMonoid } open Monoid monoid public - using (_≉_; _≤_; _>_; _≥_; rawMagma; magma; semigroup; rawMonoid) + using (rawMagma; magma; semigroup; rawMonoid) module Unordered where group : NoOrder.Group c ℓ₁ @@ -239,8 +220,7 @@ record AbelianGroup c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where open Group group public using - ( _≉_; _≤_; _>_; _≥_ - ; magma; semigroup; monoid + ( magma; semigroup; monoid ; rawMagma; rawMonoid; rawGroup ) @@ -273,7 +253,7 @@ record RawRing c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where +-rawGroup = record { _≈_ = _≈_; _<_ = _<_; _∙_ = _+_; ε = 0#; _⁻¹ = -_ } open RawGroup +-rawGroup public - using ( _≉_; _≤_; _>_; _≥_ ) + using () renaming ( rawMagma to +-rawMagma ; rawMonoid to +-rawMonoid @@ -328,7 +308,7 @@ record Ring c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where +-abelianGroup = record { isAbelianGroup = +-isAbelianGroup } open AbelianGroup +-abelianGroup public - using ( _≉_; _≤_; _>_; _≥_ ) + using () renaming ( rawMagma to +-rawMagma ; rawMonoid to +-rawMonoid @@ -388,8 +368,7 @@ record CommutativeRing c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) whe open Ring ring public using - ( _≉_; _≤_; _>_; _≥_ - ; rawRing + ( rawRing ; +-rawMagma; +-rawMonoid; +-rawGroup ; +-magma; +-semigroup; +-monoid; +-group; +-abelianGroup ; *-rawMagma; *-rawMonoid @@ -447,8 +426,7 @@ record RawField c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where open RawRing rawRing public using - ( _≉_; _≤_; _>_; _≥_ - ; +-rawMagma; +-rawMonoid; +-rawGroup + ( +-rawMagma; +-rawMonoid; +-rawGroup ; *-rawMagma; *-rawMonoid ) @@ -514,8 +492,7 @@ record DivisionRing c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where open Ring ring public using - ( _≉_; _≤_; _>_; _≥_ - ; rawRing + ( rawRing ; +-rawMagma; +-rawMonoid; +-rawGroup ; +-magma; +-semigroup; +-monoid; +-group; +-abelianGroup ; *-rawMagma; *-rawMonoid @@ -570,8 +547,7 @@ record Field c ℓ₁ ℓ₂ : Set (suc (c ⊔ ℓ₁ ⊔ ℓ₂)) where open DivisionRing divisionRing public using - ( _≉_; _≤_; _>_; _≥_ - ; rawRing; rawField; ring + ( rawRing; rawField; ring ; +-rawMagma; +-rawMonoid; +-rawGroup ; +-magma; +-semigroup; +-monoid; +-group; +-abelianGroup ; *-rawMagma; *-rawMonoid; *-rawAlmostGroup diff --git a/src/Helium/Algebra/Ordered/StrictTotal/Consequences.agda b/src/Helium/Algebra/Ordered/StrictTotal/Consequences.agda new file mode 100644 index 0000000..7696f98 --- /dev/null +++ b/src/Helium/Algebra/Ordered/StrictTotal/Consequences.agda @@ -0,0 +1,137 @@ +------------------------------------------------------------------------ +-- Agda Helium +-- +-- Relations between algebraic properties of ordered structures +------------------------------------------------------------------------ + +{-# OPTIONS --safe --without-K #-} + +open import Relation.Binary + +module Helium.Algebra.Ordered.StrictTotal.Consequences + {a ℓ₁ ℓ₂} + (strictTotalOrder : StrictTotalOrder a ℓ₁ ℓ₂) + where + +open StrictTotalOrder strictTotalOrder + renaming + ( Carrier to A + ; trans to <-trans + ; irrefl to <-irrefl + ; asym to <-asym + ) + +open import Helium.Relation.Binary.Properties.StrictTotalOrder strictTotalOrder +open import Relation.Binary.Reasoning.StrictPartialOrder strictPartialOrder + +open import Algebra.Core +open import Algebra.Definitions +open import Data.Product using (_,_) +open import Data.Sum using (inj₁; inj₂) +open import Function using (_∘_) +open import Function.Definitions +open import Helium.Algebra.Ordered.Definitions +open import Relation.Nullary using (¬_) + +---- +-- Consequences for a single unary operation +module _ {f : Op₁ A} where + cong₁+mono₁-<⇒mono₁-≤ : Congruent₁ _≈_ f → Congruent₁ _<_ f → Congruent₁ _≤_ f + cong₁+mono₁-<⇒mono₁-≤ cong mono (inj₁ x<y) = inj₁ (mono x<y) + cong₁+mono₁-<⇒mono₁-≤ cong mono (inj₂ x≈y) = inj₂ (cong x≈y) + + cong₁+anti-mono₁-<⇒anti-mono₁-≤ : Congruent₁ _≈_ f → f Preserves _<_ ⟶ _>_ → f Preserves _≤_ ⟶ _≥_ + cong₁+anti-mono₁-<⇒anti-mono₁-≤ cong anti-mono (inj₁ x<y) = inj₁ (anti-mono x<y) + cong₁+anti-mono₁-<⇒anti-mono₁-≤ cong anti-mono (inj₂ x≈y) = inj₂ (cong (Eq.sym x≈y)) + + mono₁-<⇒cancel₁-≤ : Congruent₁ _<_ f → Injective _≤_ _≤_ f + mono₁-<⇒cancel₁-≤ mono fx≤fy = ≮⇒≥ (≤⇒≯ fx≤fy ∘ mono) + + mono₁-≤⇒cancel₁-< : Congruent₁ _≤_ f → Injective _<_ _<_ f + mono₁-≤⇒cancel₁-< mono fx<fy = ≰⇒> (<⇒≱ fx<fy ∘ mono) + + cancel₁-<⇒mono₁-≤ : Injective _<_ _<_ f → Congruent₁ _≤_ f + cancel₁-<⇒mono₁-≤ cancel x≤y = ≮⇒≥ (≤⇒≯ x≤y ∘ cancel) + + cancel₁-≤⇒mono₁-< : Injective _≤_ _≤_ f → Congruent₁ _<_ f + cancel₁-≤⇒mono₁-< cancel x<y = ≰⇒> (<⇒≱ x<y ∘ cancel) + + anti-mono₁-<⇒anti-cancel₁-≤ : f Preserves _<_ ⟶ _>_ → Injective _≤_ _≥_ f + anti-mono₁-<⇒anti-cancel₁-≤ anti-mono fx≥fy = ≮⇒≥ (≤⇒≯ fx≥fy ∘ anti-mono) + + anti-mono₁-≤⇒anti-cancel₁-< : f Preserves _≤_ ⟶ _≥_ → Injective _<_ _>_ f + anti-mono₁-≤⇒anti-cancel₁-< anti-mono fx>fy = ≰⇒> (<⇒≱ fx>fy ∘ anti-mono) + + mono₁-<⇒cancel₁ : Congruent₁ _<_ f → Injective _≈_ _≈_ f + mono₁-<⇒cancel₁ mono fx≈fy = ≮∧≯⇒≈ (<-irrefl fx≈fy ∘ mono) (<-irrefl (Eq.sym fx≈fy) ∘ mono) + + anti-mono₁-<⇒cancel₁ : f Preserves _<_ ⟶ _>_ → Injective _≈_ _≈_ f + anti-mono₁-<⇒cancel₁ anti-mono fx≈fy = ≮∧≯⇒≈ + (<-irrefl (Eq.sym fx≈fy) ∘ anti-mono) + (<-irrefl fx≈fy ∘ anti-mono) + +---- +-- Consequences for a single binary operation +module _ {_∙_ : Op₂ A} where + invariant⇒mono-< : Invariant _<_ _∙_ → Congruent₂ _<_ _∙_ + invariant⇒mono-< (invˡ , invʳ) {x} {y} {u} {v} x<y u<v = begin-strict + x ∙ u <⟨ invˡ x u<v ⟩ + x ∙ v <⟨ invʳ v x<y ⟩ + y ∙ v ∎ + + invariantˡ⇒monoˡ-< : LeftInvariant _<_ _∙_ → LeftCongruent _<_ _∙_ + invariantˡ⇒monoˡ-< invˡ u<v = invˡ _ u<v + + invariantʳ⇒monoʳ-< : RightInvariant _<_ _∙_ → RightCongruent _<_ _∙_ + invariantʳ⇒monoʳ-< invʳ x<y = invʳ _ x<y + + cong+invariant⇒mono-≤ : Congruent₂ _≈_ _∙_ → Invariant _<_ _∙_ → Congruent₂ _≤_ _∙_ + cong+invariant⇒mono-≤ cong inv@(invˡ , invʳ) (inj₁ x<y) (inj₁ u<v) = inj₁ (invariant⇒mono-< inv x<y u<v) + cong+invariant⇒mono-≤ cong inv@(invˡ , invʳ) (inj₁ x<y) (inj₂ u≈v) = inj₁ (<-respʳ-≈ (cong Eq.refl u≈v) (invʳ _ x<y)) + cong+invariant⇒mono-≤ cong inv@(invˡ , invʳ) (inj₂ x≈y) (inj₁ u<v) = inj₁ (<-respʳ-≈ (cong x≈y Eq.refl) (invˡ _ u<v)) + cong+invariant⇒mono-≤ cong inv@(invˡ , invʳ) (inj₂ x≈y) (inj₂ u≤v) = inj₂ (cong x≈y u≤v) + + congˡ+monoˡ-<⇒monoˡ-≤ : LeftCongruent _≈_ _∙_ → LeftCongruent _<_ _∙_ → LeftCongruent _≤_ _∙_ + congˡ+monoˡ-<⇒monoˡ-≤ congˡ monoˡ = cong₁+mono₁-<⇒mono₁-≤ congˡ monoˡ + + congʳ+monoʳ-<⇒monoʳ-≤ : RightCongruent _≈_ _∙_ → RightCongruent _<_ _∙_ → RightCongruent _≤_ _∙_ + congʳ+monoʳ-<⇒monoʳ-≤ congʳ monoʳ = cong₁+mono₁-<⇒mono₁-≤ congʳ monoʳ + + monoˡ-<⇒cancelˡ-≤ : LeftCongruent _<_ _∙_ → LeftCancellative _≤_ _∙_ + monoˡ-<⇒cancelˡ-≤ monoˡ _ = mono₁-<⇒cancel₁-≤ monoˡ + + monoʳ-<⇒cancelʳ-≤ : RightCongruent _<_ _∙_ → RightCancellative _≤_ _∙_ + monoʳ-<⇒cancelʳ-≤ monoʳ _ _ = mono₁-<⇒cancel₁-≤ monoʳ + + monoˡ-≤⇒cancelˡ-< : LeftCongruent _≤_ _∙_ → LeftCancellative _<_ _∙_ + monoˡ-≤⇒cancelˡ-< monoˡ _ = mono₁-≤⇒cancel₁-< monoˡ + + monoʳ-≤⇒cancelʳ-< : RightCongruent _≤_ _∙_ → RightCancellative _<_ _∙_ + monoʳ-≤⇒cancelʳ-< monoʳ _ _ = mono₁-≤⇒cancel₁-< monoʳ + + cancelˡ-<⇒monoˡ-≤ : LeftCancellative _<_ _∙_ → LeftCongruent _≤_ _∙_ + cancelˡ-<⇒monoˡ-≤ cancelˡ = cancel₁-<⇒mono₁-≤ (cancelˡ _) + + cancelʳ-<⇒monoʳ-≤ : RightCancellative _<_ _∙_ → RightCongruent _≤_ _∙_ + cancelʳ-<⇒monoʳ-≤ cancelʳ = cancel₁-<⇒mono₁-≤ (cancelʳ _ _) + + cancelˡ-≤⇒monoˡ-< : LeftCancellative _≤_ _∙_ → LeftCongruent _<_ _∙_ + cancelˡ-≤⇒monoˡ-< cancelˡ = cancel₁-≤⇒mono₁-< (cancelˡ _) + + cancelʳ-≤⇒monoʳ-< : RightCancellative _≤_ _∙_ → RightCongruent _<_ _∙_ + cancelʳ-≤⇒monoʳ-< cancelʳ = cancel₁-≤⇒mono₁-< (cancelʳ _ _) + + monoˡ-<⇒cancelˡ : LeftCongruent _<_ _∙_ → LeftCancellative _≈_ _∙_ + monoˡ-<⇒cancelˡ monoˡ _ = mono₁-<⇒cancel₁ monoˡ + + monoʳ-<⇒cancelʳ : RightCongruent _<_ _∙_ → RightCancellative _≈_ _∙_ + monoʳ-<⇒cancelʳ monoʳ _ _ = mono₁-<⇒cancel₁ monoʳ + + ¬comm-< : A → ¬ Commutative _<_ _∙_ + ¬comm-< a comm = <-irrefl Eq.refl (comm a a ) + + -- cong+mono-<⇒mono-≤ : Congruent₂ _≈_ _∙_ → Congruent₂ _<_ _∙_ → Congruent₂ _≤_ _∙_ + -- cong+mono-<⇒mono-≤ cong mono (inj₁ x<y) (inj₁ u<v) = inj₁ (mono x<y u<v) + -- cong+mono-<⇒mono-≤ cong mono (inj₁ x<y) (inj₂ u≈v) = inj₁ {!!} + -- cong+mono-<⇒mono-≤ cong mono (inj₂ x≈y) (inj₁ u<v) = inj₁ {!!} + -- cong+mono-<⇒mono-≤ cong mono (inj₂ x≈y) (inj₂ u≈v) = inj₂ (cong x≈y u≈v) diff --git a/src/Helium/Algebra/Ordered/StrictTotal/Morphism/Structures.agda b/src/Helium/Algebra/Ordered/StrictTotal/Morphism/Structures.agda new file mode 100644 index 0000000..dbce970 --- /dev/null +++ b/src/Helium/Algebra/Ordered/StrictTotal/Morphism/Structures.agda @@ -0,0 +1,98 @@ +------------------------------------------------------------------------ +-- Agda Helium +-- +-- Morphisms for ordered algebraic structures. +------------------------------------------------------------------------ + +{-# OPTIONS --safe --without-K #-} + +module Helium.Algebra.Ordered.StrictTotal.Morphism.Structures where + +import Algebra.Morphism.Definitions as MorphismDefinitions +open import Helium.Algebra.Ordered.StrictTotal.Bundles +open import Level using (Level; _⊔_) +open import Relation.Binary.Morphism.Structures + +private + variable + a b ℓ₁ ℓ₂ ℓ₃ ℓ₄ : Level + +module MagmaMorphisms (M₁ : RawMagma a ℓ₁ ℓ₂) (M₂ : RawMagma b ℓ₃ ℓ₄) where + private + module M₁ = RawMagma M₁ + module M₂ = RawMagma M₂ + + open M₁ using () renaming (Carrier to A) + open M₂ using () renaming (Carrier to B) + open MorphismDefinitions A B M₂._≈_ + + record IsMagmaHomomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂ ⊔ ℓ₃ ⊔ ℓ₄) where + field + isOrderHomomorphism : IsOrderHomomorphism M₁._≈_ M₂._≈_ M₁._<_ M₂._<_ ⟦_⟧ + homo : Homomorphic₂ ⟦_⟧ M₁._∙_ M₂._∙_ + + open IsOrderHomomorphism isOrderHomomorphism public + +module MonoidMorphisms (M₁ : RawMonoid a ℓ₁ ℓ₂) (M₂ : RawMonoid b ℓ₃ ℓ₄) where + private + module M₁ = RawMonoid M₁ + module M₂ = RawMonoid M₂ + + open M₁ using () renaming (Carrier to A) + open M₂ using () renaming (Carrier to B) + open MorphismDefinitions A B M₂._≈_ + open MagmaMorphisms M₁.rawMagma M₂.rawMagma + + record IsMonoidHomomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂ ⊔ ℓ₃ ⊔ ℓ₄) where + field + isMagmaHomomorphism : IsMagmaHomomorphism ⟦_⟧ + ε-homo : Homomorphic₀ ⟦_⟧ M₁.ε M₂.ε + + open IsMagmaHomomorphism isMagmaHomomorphism public + +module GroupMorphisms (G₁ : RawGroup a ℓ₁ ℓ₂) (G₂ : RawGroup b ℓ₃ ℓ₄) where + private + module G₁ = RawGroup G₁ + module G₂ = RawGroup G₂ + + open G₁ using () renaming (Carrier to A) + open G₂ using () renaming (Carrier to B) + open MorphismDefinitions A B G₂._≈_ + open MonoidMorphisms G₁.rawMonoid G₂.rawMonoid + + record IsGroupHomomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂ ⊔ ℓ₃ ⊔ ℓ₄) where + field + isMonoidHomomorphism : IsMonoidHomomorphism ⟦_⟧ + ⁻¹-homo : Homomorphic₁ ⟦_⟧ G₁._⁻¹ G₂._⁻¹ + + open IsMonoidHomomorphism isMonoidHomomorphism public + +module RingMorphisms (R₁ : RawRing a ℓ₁ ℓ₂) (R₂ : RawRing b ℓ₃ ℓ₄) where + private + module R₁ = RawRing R₁ + module R₂ = RawRing R₂ + + open R₁ using () renaming (Carrier to A) + open R₂ using () renaming (Carrier to B) + open MorphismDefinitions A B R₂._≈_ + open GroupMorphisms R₁.+-rawGroup R₂.+-rawGroup + + record IsRingHomomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂ ⊔ ℓ₃ ⊔ ℓ₄) where + field + +-isGroupHomomorphism : IsGroupHomomorphism ⟦_⟧ + *-homo : Homomorphic₂ ⟦_⟧ R₁._*_ R₂._*_ + 1#-homo : Homomorphic₀ ⟦_⟧ R₁.1# R₂.1# + + open IsGroupHomomorphism +-isGroupHomomorphism public + renaming + ( homo to +-homo + ; ε-homo to 0#-homo + ; ⁻¹-homo to -‿homo + ; isMagmaHomomorphism to +-isMagmaHomomorphism + ; isMonoidHomomorphism to +-isMonoidHomomorphism + ) + +open MagmaMorphisms public +open MonoidMorphisms public +open GroupMorphisms public +open RingMorphisms public diff --git a/src/Helium/Algebra/Ordered/StrictTotal/Properties/AbelianGroup.agda b/src/Helium/Algebra/Ordered/StrictTotal/Properties/AbelianGroup.agda index fe64b32..a6cbcab 100644 --- a/src/Helium/Algebra/Ordered/StrictTotal/Properties/AbelianGroup.agda +++ b/src/Helium/Algebra/Ordered/StrictTotal/Properties/AbelianGroup.agda @@ -14,18 +14,60 @@ module Helium.Algebra.Ordered.StrictTotal.Properties.AbelianGroup where open AbelianGroup abelianGroup - + renaming + ( trans to <-trans + ; irrefl to <-irrefl + ; asym to <-asym + ) 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.Relation.Binary.Properties.StrictTotalOrder strictTotalOrder 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 ⁻¹ ∎ + using + ( ∙-mono-<; ∙-monoˡ-<; ∙-monoʳ-< + ; ∙-mono-≤; ∙-monoˡ-≤; ∙-monoʳ-≤ + + ; ∙-cancelˡ-<; ∙-cancelʳ-<; ∙-cancel-< + ; ∙-cancelˡ-≤; ∙-cancelʳ-≤; ∙-cancel-≤ + -- _∙_ pres signs + ; x≥ε∧y>ε⇒x∙y>ε; x>ε∧y≥ε⇒x∙y>ε + ; x≤ε∧y<ε⇒x∙y<ε; x<ε∧y≤ε⇒x∙y<ε + ; x≥ε∧y≥ε⇒x∙y≥ε; x≤ε∧y≤ε⇒x∙y≤ε + -- _∙_ resp signs + ; x≤ε∧x∙y>ε⇒y>ε; x≤ε∧y∙x>ε⇒y>ε + ; x<ε∧x∙y≥ε⇒y>ε; x<ε∧y∙x≥ε⇒y>ε + ; x≥ε∧x∙y<ε⇒y<ε; x≥ε∧y∙x<ε⇒y<ε + ; x>ε∧x∙y≤ε⇒y<ε; x>ε∧y∙x≤ε⇒y<ε + ; x≤ε∧x∙y≥ε⇒y≥ε; x≤ε∧y∙x≥ε⇒y≥ε + ; x≥ε∧x∙y≤ε⇒y≤ε; x≥ε∧y∙x≤ε⇒y≤ε + + ; ×-zeroˡ; ×-zeroʳ + ; ×-identityˡ + + ; n≢0⇒×-monoˡ-<; x>ε⇒×-monoʳ-<; x<ε⇒×-anti-monoʳ-< + ; ×-monoˡ-≤; x≥ε⇒×-monoʳ-≤; x≤ε⇒×-anti-monoʳ-≤ + + ; ×-cancelˡ-<; x≥ε⇒×-cancelʳ-<; x≤ε⇒×-anti-cancelʳ-< + ; n≢0⇒×-cancelˡ-≤; x>ε⇒×-cancelʳ-≤; x<ε⇒×-anti-cancelʳ-≤ + -- _×_ pres signs + ; n≢0∧x>ε⇒n×x>ε; n≢0∧x<ε⇒n×x<ε + ; x≥ε⇒n×x≥ε; x≤ε⇒n×x≤ε + -- _×_ resp signs + ; n×x>ε⇒x>ε; n×x<ε⇒x<ε + ; n≢0∧n×x≥ε⇒x≥ε; n≢0∧n×x≤ε⇒x≤ε + + ; ⁻¹-anti-mono-<; ⁻¹-anti-mono-≤ + + ; ⁻¹-cancel; ⁻¹-anti-cancel-<; ⁻¹-anti-cancel-≤ + + ; x<ε⇒x⁻¹>ε; x>ε⇒x⁻¹<ε + ; x≤ε⇒x⁻¹≥ε; x≥ε⇒x⁻¹≤ε + + ; x⁻¹<ε⇒x>ε; x⁻¹>ε⇒x<ε + ; x⁻¹≤ε⇒x≥ε; x⁻¹≥ε⇒x≤ε + + ; x<y⇒ε<y∙x⁻¹ ; ε<y∙x⁻¹⇒x<y + ) diff --git a/src/Helium/Algebra/Ordered/StrictTotal/Properties/CommutativeRing.agda b/src/Helium/Algebra/Ordered/StrictTotal/Properties/CommutativeRing.agda index 24b2663..d303c99 100644 --- a/src/Helium/Algebra/Ordered/StrictTotal/Properties/CommutativeRing.agda +++ b/src/Helium/Algebra/Ordered/StrictTotal/Properties/CommutativeRing.agda @@ -14,14 +14,87 @@ module Helium.Algebra.Ordered.StrictTotal.Properties.CommutativeRing where open CommutativeRing commutativeRing + renaming + ( trans to <-trans + ; irrefl to <-irrefl + ; asym to <-asym + ; 0<a+0<b⇒0<ab to x>0∧y>0⇒x*y>0 + ) 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.Relation.Binary.Properties.StrictTotalOrder strictTotalOrder 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) + ( +-mono-<; +-monoˡ-<; +-monoʳ-< + ; +-mono-≤; +-monoˡ-≤; +-monoʳ-≤ + + ; +-cancel-<; +-cancelˡ-<; +-cancelʳ-< + ; +-cancel-≤; +-cancelˡ-≤; +-cancelʳ-≤ + + ; x≥0∧y>0⇒x+y>0 ; x>0∧y≥0⇒x+y>0 + ; x≤0∧y<0⇒x+y<0 ; x<0∧y≤0⇒x+y<0 + ; x≥0∧y≥0⇒x+y≥0 ; x≤0∧y≤0⇒x+y≤0 + + ; x≤0∧x+y>0⇒y>0 ; x≤0∧y+x>0⇒y>0 ; x<0∧x+y≥0⇒y>0 ; x<0∧y+x≥0⇒y>0 + ; x≥0∧x+y<0⇒y<0 ; x≥0∧y+x<0⇒y<0 ; x>0∧x+y≤0⇒y<0 ; x>0∧y+x≤0⇒y<0 + ; x≤0∧x+y≥0⇒y≥0 ; x≤0∧y+x≥0⇒y≥0 + ; x≥0∧x+y≤0⇒y≤0 ; x≥0∧y+x≤0⇒y≤0 + + ; ×-zeroˡ; ×-zeroʳ + ; ×-identityˡ + + ; n≢0⇒×-monoˡ-< ; x>0⇒×-monoʳ-< ; x<0⇒×-anti-monoʳ-< + ; ×-monoˡ-≤; x≥0⇒×-monoʳ-≤; x≤0⇒×-anti-monoʳ-≤ + + ; ×-cancelˡ-<; x≥0⇒×-cancelʳ-<; x≤0⇒×-anti-cancelʳ-< + ; n≢0⇒×-cancelˡ-≤ ; x>0⇒×-cancelʳ-≤ ; x<0⇒×-anti-cancelʳ-≤ + + ; n≢0∧x>0⇒n×x>0; n≢0∧x<0⇒n×x<0 + ; x≥0⇒n×x≥0; x≤0⇒n×x≤0 + + ; n×x>0⇒x>0; n×x<0⇒x<0 + ; n≢0∧n×x≥0⇒x≥0; n≢0∧n×x≤0⇒x≤0 + + ; -‿anti-mono-<; -‿anti-mono-≤ + ; -‿cancel; -‿anti-cancel-<; -‿anti-cancel-≤ + + ; x<0⇒-x>0; x>0⇒-x<0; x≤0⇒-x≥0; x≥0⇒-x≤0 + ; -x<0⇒x>0; -x>0⇒x<0; -x≤0⇒x≥0; -x≥0⇒x≤0 + + ; x<y⇒0<y-x; 0<y-x⇒x<y + + ; 0≤1; 1≈0⇒x≈y; x<y⇒0<1 + + ; x>0⇒*-monoˡ-<; x>0⇒*-monoʳ-<; x<0⇒*-anti-monoˡ-<; x<0⇒*-anti-monoʳ-< + ; x≥0⇒*-monoˡ-≤; x≥0⇒*-monoʳ-≤; x≤0⇒*-anti-monoˡ-≤; x≤0⇒*-anti-monoʳ-≤ + + ; x≥0⇒*-cancelˡ-<; x≥0⇒*-cancelʳ-<; x≤0⇒*-anti-cancelˡ-<; x≤0⇒*-anti-cancelʳ-< + ; x>0⇒*-cancelˡ-≤; x>0⇒*-cancelʳ-≤; x<0⇒*-anti-cancelˡ-≤; x<0⇒*-anti-cancelʳ-≤ + + ; x≈0⇒x*y≈0; x≈0⇒y*x≈0 + + ; -x*-y≈x*y + ; x>0∧y<0⇒x*y<0; x<0∧y>0⇒x*y<0; x<0∧y<0⇒x*y>0 + ; x≥0∧y≥0⇒x*y≥0; x≥0∧y≤0⇒x*y≤0; x≤0∧y≥0⇒x*y≤0; x≤0∧y≤0⇒x*y≥0 + + ; x>1∧y≥1⇒x*y>1; x≥1∧y>1⇒x*y>1; 0≤x<1∧y≤1⇒x*y<1; x≤1∧0≤y<1⇒x*y<1 + ; x≥1∧y≥1⇒x*y≥1; 0≤x≤1∧y≤1⇒x*y≤1; x≤1∧0≤y≤1⇒x*y≤1 + + ; x*x≥0 + + ; ^-zeroˡ; ^-zeroʳ + ; ^-identityʳ + + ; n≢0⇒0^n≈0 + ; x>1⇒^-monoˡ-<; 0<x<1⇒^-anti-monoˡ-< + ; x≥1⇒^-monoˡ-≤; 0≤x≤1⇒^-anti-monoˡ-≤ + + ; x>0⇒x^n>0 + ; x≥0⇒x^n≥0 + + ; x>1∧n≢0⇒x^n>1; 0≤x<1∧n≢0⇒x^n<1 + ; x≥1⇒x^n≥1; 0≤x≤1⇒x^n≤1 + ) diff --git a/src/Helium/Algebra/Ordered/StrictTotal/Properties/Group.agda b/src/Helium/Algebra/Ordered/StrictTotal/Properties/Group.agda index c0723b3..d72ae10 100644 --- a/src/Helium/Algebra/Ordered/StrictTotal/Properties/Group.agda +++ b/src/Helium/Algebra/Ordered/StrictTotal/Properties/Group.agda @@ -14,46 +14,205 @@ module Helium.Algebra.Ordered.StrictTotal.Properties.Group where open Group group + renaming + ( trans to <-trans + ; irrefl to <-irrefl + ; asym to <-asym + ) -open import Data.Sum using (inj₂; [_,_]′; fromInj₁) -open import Function using (_∘_; flip) -open import Relation.Binary using (tri<; tri≈; tri>) +open import Algebra.Definitions +open import Function using (_∘_; flip; Injective) +open import Relation.Binary.Core 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 +open import Helium.Algebra.Ordered.StrictTotal.Properties.Monoid monoid public + using + ( ∙-mono-<; ∙-monoˡ-<; ∙-monoʳ-< + ; ∙-mono-≤; ∙-monoˡ-≤; ∙-monoʳ-≤ -<⇒≱ : ∀ {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 + ; ∙-cancelˡ-<; ∙-cancelʳ-<; ∙-cancel-< + ; ∙-cancelˡ-≤; ∙-cancelʳ-≤; ∙-cancel-≤ + -- _∙_ pres signs + ; x≥ε∧y>ε⇒x∙y>ε; x>ε∧y≥ε⇒x∙y>ε + ; x≤ε∧y<ε⇒x∙y<ε; x<ε∧y≤ε⇒x∙y<ε + ; x≥ε∧y≥ε⇒x∙y≥ε; x≤ε∧y≤ε⇒x∙y≤ε + -- _∙_ resp signs + ; x≤ε∧x∙y>ε⇒y>ε; x≤ε∧y∙x>ε⇒y>ε + ; x<ε∧x∙y≥ε⇒y>ε; x<ε∧y∙x≥ε⇒y>ε + ; x≥ε∧x∙y<ε⇒y<ε; x≥ε∧y∙x<ε⇒y<ε + ; x>ε∧x∙y≤ε⇒y<ε; x>ε∧y∙x≤ε⇒y<ε + ; x≤ε∧x∙y≥ε⇒y≥ε; x≤ε∧y∙x≥ε⇒y≥ε + ; x≥ε∧x∙y≤ε⇒y≤ε; x≥ε∧y∙x≤ε⇒y≤ε -≤⇒≯ : ∀ {x y} → x ≤ y → ¬ x > y -≤⇒≯ = flip <⇒≱ + ; ×-zeroˡ; ×-zeroʳ + ; ×-identityˡ ->⇒≉ : ∀ {x y} → x > y → x ≉ y ->⇒≉ x>y = <⇒≱ x>y ∘ inj₂ + ; n≢0⇒×-monoˡ-<; x>ε⇒×-monoʳ-<; x<ε⇒×-anti-monoʳ-< + ; ×-monoˡ-≤; x≥ε⇒×-monoʳ-≤; x≤ε⇒×-anti-monoʳ-≤ -≈⇒≯ : ∀ {x y} → x ≈ y → ¬ x > y -≈⇒≯ = flip >⇒≉ + ; ×-cancelˡ-<; x≥ε⇒×-cancelʳ-<; x≤ε⇒×-anti-cancelʳ-< + ; n≢0⇒×-cancelˡ-≤; x>ε⇒×-cancelʳ-≤; x<ε⇒×-anti-cancelʳ-≤ + -- _×_ pres signs + ; n≢0∧x>ε⇒n×x>ε; n≢0∧x<ε⇒n×x<ε + ; x≥ε⇒n×x≥ε; x≤ε⇒n×x≤ε + -- _×_ resp signs + ; n×x>ε⇒x>ε; n×x<ε⇒x<ε + ; n≢0∧n×x≥ε⇒x≥ε; n≢0∧n×x≤ε⇒x≤ε + ) +open import Helium.Relation.Binary.Properties.StrictTotalOrder strictTotalOrder public -<⇒≉ : ∀ {x y} → x < y → x ≉ y -<⇒≉ x<y = >⇒≉ x<y ∘ Eq.sym +-------------------------------------------------------------------------------- +---- Properties of _⁻¹ -≈⇒≮ : ∀ {x y} → x ≈ y → ¬ x < y -≈⇒≮ = flip <⇒≉ +---- Congruences -≤∧≉⇒< : ∀ {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) +⁻¹-anti-mono-< : _⁻¹ Preserves _<_ ⟶ _>_ +⁻¹-anti-mono-< {x} {y} x<y = begin-strict + y ⁻¹ ≈˘⟨ identityˡ (y ⁻¹) ⟩ + ε ∙ y ⁻¹ ≈˘⟨ ∙-congʳ (inverseˡ x) ⟩ + x ⁻¹ ∙ x ∙ y ⁻¹ <⟨ ∙-monoʳ-< (∙-monoˡ-< x<y) ⟩ + x ⁻¹ ∙ y ∙ y ⁻¹ ≈⟨ assoc (x ⁻¹) y (y ⁻¹) ⟩ + x ⁻¹ ∙ (y ∙ y ⁻¹) ≈⟨ ∙-congˡ (inverseʳ y) ⟩ + x ⁻¹ ∙ ε ≈⟨ identityʳ (x ⁻¹) ⟩ + x ⁻¹ ∎ -x<y⇒ε<yx⁻¹ : ∀ {x y} → x < y → ε < y ∙ x ⁻¹ -x<y⇒ε<yx⁻¹ {x} {y} x<y = begin-strict +-- _≤_ + +⁻¹-anti-mono-≤ : _⁻¹ Preserves _≤_ ⟶ _≥_ +⁻¹-anti-mono-≤ {x} {y} x≤y = begin + y ⁻¹ ≈˘⟨ identityˡ (y ⁻¹) ⟩ + ε ∙ y ⁻¹ ≈˘⟨ ∙-congʳ (inverseˡ x) ⟩ + x ⁻¹ ∙ x ∙ y ⁻¹ ≤⟨ ∙-monoʳ-≤ (∙-monoˡ-≤ x≤y) ⟩ + x ⁻¹ ∙ y ∙ y ⁻¹ ≈⟨ assoc (x ⁻¹) y (y ⁻¹) ⟩ + x ⁻¹ ∙ (y ∙ y ⁻¹) ≈⟨ ∙-congˡ (inverseʳ y) ⟩ + x ⁻¹ ∙ ε ≈⟨ identityʳ (x ⁻¹) ⟩ + x ⁻¹ ∎ + +---- Cancellative + +-- _≈_ + +⁻¹-cancel : Injective _≈_ _≈_ _⁻¹ +⁻¹-cancel {x} {y} x⁻¹≈y⁻¹ = begin-equality + x ≈⟨ inverseˡ-unique x (y ⁻¹) (begin-equality + x ∙ y ⁻¹ ≈˘⟨ ∙-congˡ x⁻¹≈y⁻¹ ⟩ + x ∙ x ⁻¹ ≈⟨ inverseʳ x ⟩ + ε ∎) ⟩ + y ⁻¹ ⁻¹ ≈⟨ ⁻¹-involutive y ⟩ + y ∎ + +-- _<_ + +⁻¹-anti-cancel-< : Injective _<_ _>_ _⁻¹ +⁻¹-anti-cancel-< x⁻¹>y⁻¹ = ≰⇒> (<⇒≱ x⁻¹>y⁻¹ ∘ ⁻¹-anti-mono-≤) + +-- _≤_ + +⁻¹-anti-cancel-≤ : Injective _≤_ _≥_ _⁻¹ +⁻¹-anti-cancel-≤ x⁻¹≥y⁻¹ = ≮⇒≥ (≤⇒≯ x⁻¹≥y⁻¹ ∘ ⁻¹-anti-mono-<) + +---- Preserves signs + +-- _<_ + +x<ε⇒x⁻¹>ε : ∀ {x} → x < ε → x ⁻¹ > ε +x<ε⇒x⁻¹>ε {x} x<ε = begin-strict + ε ≈˘⟨ ε⁻¹≈ε ⟩ + ε ⁻¹ <⟨ ⁻¹-anti-mono-< x<ε ⟩ + x ⁻¹ ∎ + +x>ε⇒x⁻¹<ε : ∀ {x} → x > ε → x ⁻¹ < ε +x>ε⇒x⁻¹<ε {x} x>ε = begin-strict + x ⁻¹ <⟨ ⁻¹-anti-mono-< x>ε ⟩ + ε ⁻¹ ≈⟨ ε⁻¹≈ε ⟩ + ε ∎ + +-- _≤_ + +x≤ε⇒x⁻¹≥ε : ∀ {x} → x ≤ ε → x ⁻¹ ≥ ε +x≤ε⇒x⁻¹≥ε {x} x≤ε = begin + ε ≈˘⟨ ε⁻¹≈ε ⟩ + ε ⁻¹ ≤⟨ ⁻¹-anti-mono-≤ x≤ε ⟩ + x ⁻¹ ∎ + +x≥ε⇒x⁻¹≤ε : ∀ {x} → x ≥ ε → x ⁻¹ ≤ ε +x≥ε⇒x⁻¹≤ε {x} x≥ε = begin + x ⁻¹ ≤⟨ ⁻¹-anti-mono-≤ x≥ε ⟩ + ε ⁻¹ ≈⟨ ε⁻¹≈ε ⟩ + ε ∎ + +---- Respects signs + +-- _<_ + +x⁻¹<ε⇒x>ε : ∀ {x} → x ⁻¹ < ε → x > ε +x⁻¹<ε⇒x>ε {x} x⁻¹<ε = begin-strict + ε <⟨ x<ε⇒x⁻¹>ε x⁻¹<ε ⟩ + x ⁻¹ ⁻¹ ≈⟨ ⁻¹-involutive x ⟩ + x ∎ + +x⁻¹>ε⇒x<ε : ∀ {x} → x ⁻¹ > ε → x < ε +x⁻¹>ε⇒x<ε {x} x⁻¹>ε = begin-strict + x ≈˘⟨ ⁻¹-involutive x ⟩ + x ⁻¹ ⁻¹ <⟨ x>ε⇒x⁻¹<ε x⁻¹>ε ⟩ + ε ∎ + +-- _≤_ + +x⁻¹≤ε⇒x≥ε : ∀ {x} → x ⁻¹ ≤ ε → x ≥ ε +x⁻¹≤ε⇒x≥ε {x} x⁻¹≤ε = begin + ε ≤⟨ x≤ε⇒x⁻¹≥ε x⁻¹≤ε ⟩ + x ⁻¹ ⁻¹ ≈⟨ ⁻¹-involutive x ⟩ + x ∎ + +x⁻¹≥ε⇒x≤ε : ∀ {x} → x ⁻¹ ≥ ε → x ≤ ε +x⁻¹≥ε⇒x≤ε {x} x⁻¹≥ε = begin + x ≈˘⟨ ⁻¹-involutive x ⟩ + x ⁻¹ ⁻¹ ≤⟨ x≥ε⇒x⁻¹≤ε x⁻¹≥ε ⟩ + ε ∎ + +-- ---- Infer signs + +-- -- _≈_ + +-- x⁻¹≈x⇒x≈ε : ∀ {x} → x ⁻¹ ≈ x → x ≈ ε +-- x⁻¹≈x⇒x≈ε {x} x⁻¹≈x = ≮∧≯⇒≈ +-- (λ x<ε → <-asym x<ε (begin-strict +-- ε <⟨ x<ε⇒x⁻¹>ε x<ε ⟩ +-- x ⁻¹ ≈⟨ x⁻¹≈x ⟩ +-- x ∎)) +-- (λ x>ε → <-asym x>ε (begin-strict +-- x ≈˘⟨ x⁻¹≈x ⟩ +-- x ⁻¹ <⟨ x>ε⇒x⁻¹<ε x>ε ⟩ +-- ε ∎)) + +-- -- _<_ + +-- x⁻¹<x⇒x>ε : ∀ {x} → x ⁻¹ < x → x > ε +-- x⁻¹<x⇒x>ε x⁻¹<x = ≰⇒> (<⇒≱ x⁻¹<x ∘ λ x≤ε → ≤-trans x≤ε (x≤ε⇒x⁻¹≥ε x≤ε)) + +-- x⁻¹>x⇒x<ε : ∀ {x} → x ⁻¹ > x → x < ε +-- x⁻¹>x⇒x<ε x⁻¹>x = ≰⇒> (<⇒≱ x⁻¹>x ∘ λ x≥ε → ≤-trans (x≥ε⇒x⁻¹≤ε x≥ε) x≥ε) + +-- -- _≤_ + +---- Miscellaneous + +x<y⇒ε<y∙x⁻¹ : ∀ {x y} → x < y → ε < y ∙ x ⁻¹ +x<y⇒ε<y∙x⁻¹ {x} {y} x<y = begin-strict ε ≈˘⟨ inverseʳ x ⟩ x ∙ x ⁻¹ <⟨ ∙-invariantʳ (x ⁻¹) x<y ⟩ y ∙ x ⁻¹ ∎ + +ε<y∙x⁻¹⇒x<y : ∀ {x y} → ε < y ∙ x ⁻¹ → x < y +ε<y∙x⁻¹⇒x<y {x} {y} ε<yx⁻¹ = begin-strict + x ≈˘⟨ identityˡ x ⟩ + ε ∙ x <⟨ ∙-invariantʳ x ε<yx⁻¹ ⟩ + y ∙ x ⁻¹ ∙ x ≈⟨ assoc y (x ⁻¹) x ⟩ + y ∙ (x ⁻¹ ∙ x) ≈⟨ ∙-congˡ (inverseˡ x) ⟩ + y ∙ ε ≈⟨ identityʳ y ⟩ + y ∎ diff --git a/src/Helium/Algebra/Ordered/StrictTotal/Properties/Magma.agda b/src/Helium/Algebra/Ordered/StrictTotal/Properties/Magma.agda new file mode 100644 index 0000000..91d4b3e --- /dev/null +++ b/src/Helium/Algebra/Ordered/StrictTotal/Properties/Magma.agda @@ -0,0 +1,89 @@ +------------------------------------------------------------------------ +-- Agda Helium +-- +-- Algebraic properties of ordered magmas +------------------------------------------------------------------------ + +{-# OPTIONS --safe --without-K #-} + +open import Helium.Algebra.Ordered.StrictTotal.Bundles + +module Helium.Algebra.Ordered.StrictTotal.Properties.Magma + {ℓ₁ ℓ₂ ℓ₃} + (magma : Magma ℓ₁ ℓ₂ ℓ₃) + where + +open Magma magma + renaming + ( trans to <-trans + ; irrefl to <-irrefl + ; asym to <-asym + ) + +open import Algebra.Definitions +open import Data.Product using (_,_) +open import Helium.Algebra.Ordered.StrictTotal.Consequences strictTotalOrder + +open import Helium.Relation.Binary.Properties.StrictTotalOrder strictTotalOrder public + +-------------------------------------------------------------------------------- +-- Properties of _∙_ + +---- Congruences + +-- _<_ + +∙-mono-< : Congruent₂ _<_ _∙_ +∙-mono-< = invariant⇒mono-< ∙-invariant + +∙-monoˡ-< : LeftCongruent _<_ _∙_ +∙-monoˡ-< = invariantˡ⇒monoˡ-< ∙-invariantˡ + +∙-monoʳ-< : RightCongruent _<_ _∙_ +∙-monoʳ-< = invariantʳ⇒monoʳ-< ∙-invariantʳ + +-- _≤_ + +∙-mono-≤ : Congruent₂ _≤_ _∙_ +∙-mono-≤ = cong+invariant⇒mono-≤ ∙-cong ∙-invariant + +∙-monoˡ-≤ : LeftCongruent _≤_ _∙_ +∙-monoˡ-≤ {x} = congˡ+monoˡ-<⇒monoˡ-≤ (∙-congˡ {x}) (∙-monoˡ-< {x}) {x} + +∙-monoʳ-≤ : RightCongruent _≤_ _∙_ +∙-monoʳ-≤ {x} = congʳ+monoʳ-<⇒monoʳ-≤ (∙-congʳ {x}) (∙-monoʳ-< {x}) {x} + +---- Cancelling + +-- _≈_ + +∙-cancelˡ : LeftCancellative _≈_ _∙_ +∙-cancelˡ = monoˡ-<⇒cancelˡ ∙-monoˡ-< + +∙-cancelʳ : RightCancellative _≈_ _∙_ +∙-cancelʳ {x} = monoʳ-<⇒cancelʳ (∙-monoʳ-< {x}) {x} + +∙-cancel : Cancellative _≈_ _∙_ +∙-cancel = ∙-cancelˡ , ∙-cancelʳ + +-- _<_ + +∙-cancelˡ-< : LeftCancellative _<_ _∙_ +∙-cancelˡ-< = monoˡ-≤⇒cancelˡ-< ∙-monoˡ-≤ + +∙-cancelʳ-< : RightCancellative _<_ _∙_ +∙-cancelʳ-< {x} = monoʳ-≤⇒cancelʳ-< (∙-monoʳ-≤ {x}) {x} + +∙-cancel-< : Cancellative _<_ _∙_ +∙-cancel-< = ∙-cancelˡ-< , ∙-cancelʳ-< + +-- _≤_ + +∙-cancelˡ-≤ : LeftCancellative _≤_ _∙_ +∙-cancelˡ-≤ = monoˡ-<⇒cancelˡ-≤ ∙-monoˡ-< + +∙-cancelʳ-≤ : RightCancellative _≤_ _∙_ +∙-cancelʳ-≤ {x} = monoʳ-<⇒cancelʳ-≤ (∙-monoʳ-< {x}) {x} + +∙-cancel-≤ : Cancellative _≤_ _∙_ +∙-cancel-≤ = ∙-cancelˡ-≤ , ∙-cancelʳ-≤ diff --git a/src/Helium/Algebra/Ordered/StrictTotal/Properties/Monoid.agda b/src/Helium/Algebra/Ordered/StrictTotal/Properties/Monoid.agda new file mode 100644 index 0000000..220175c --- /dev/null +++ b/src/Helium/Algebra/Ordered/StrictTotal/Properties/Monoid.agda @@ -0,0 +1,329 @@ +------------------------------------------------------------------------ +-- Agda Helium +-- +-- Algebraic properties of ordered monoids +------------------------------------------------------------------------ + +{-# OPTIONS --safe --without-K #-} + +open import Helium.Algebra.Ordered.StrictTotal.Bundles + +module Helium.Algebra.Ordered.StrictTotal.Properties.Monoid + {ℓ₁ ℓ₂ ℓ₃} + (monoid : Monoid ℓ₁ ℓ₂ ℓ₃) + where + +open Monoid monoid + renaming + ( trans to <-trans + ; irrefl to <-irrefl + ; asym to <-asym + ) + +open import Algebra.Definitions +open import Data.Nat as ℕ using (suc; NonZero) +import Data.Nat.Properties as ℕₚ +open import Function using (_∘_; flip) +open import Function.Definitions +open import Helium.Algebra.Ordered.StrictTotal.Consequences strictTotalOrder +open import Relation.Binary.Core + +open import Algebra.Properties.Monoid.Mult.TCOptimised Unordered.monoid public +open import Helium.Algebra.Ordered.StrictTotal.Properties.Semigroup semigroup public + using + ( ∙-mono-<; ∙-monoˡ-<; ∙-monoʳ-< + ; ∙-mono-≤; ∙-monoˡ-≤; ∙-monoʳ-≤ + ; ∙-cancelˡ; ∙-cancelʳ; ∙-cancel + ; ∙-cancelˡ-<; ∙-cancelʳ-<; ∙-cancel-< + ; ∙-cancelˡ-≤; ∙-cancelʳ-≤; ∙-cancel-≤ + ) +open import Helium.Relation.Binary.Properties.StrictTotalOrder strictTotalOrder public + +open import Relation.Binary.Reasoning.StrictPartialOrder strictPartialOrder + +-------------------------------------------------------------------------------- +---- Properties of _∙_ + +---- Preserves signs + +-- _<_ + +x≥ε∧y>ε⇒x∙y>ε : ∀ {x y} → x ≥ ε → y > ε → x ∙ y > ε +x≥ε∧y>ε⇒x∙y>ε {x} {y} x≥ε y>ε = begin-strict + ε ≈˘⟨ identity² ⟩ + ε ∙ ε <⟨ ∙-monoˡ-< y>ε ⟩ + ε ∙ y ≤⟨ ∙-monoʳ-≤ x≥ε ⟩ + x ∙ y ∎ + +x>ε∧y≥ε⇒x∙y>ε : ∀ {x y} → x > ε → y ≥ ε → x ∙ y > ε +x>ε∧y≥ε⇒x∙y>ε {x} {y} x>ε y≤ε = begin-strict + ε ≈˘⟨ identity² ⟩ + ε ∙ ε ≤⟨ ∙-monoˡ-≤ y≤ε ⟩ + ε ∙ y <⟨ ∙-monoʳ-< x>ε ⟩ + x ∙ y ∎ + +x≤ε∧y<ε⇒x∙y<ε : ∀ {x y} → x ≤ ε → y < ε → x ∙ y < ε +x≤ε∧y<ε⇒x∙y<ε {x} {y} x≤ε y<ε = begin-strict + x ∙ y ≤⟨ ∙-monoʳ-≤ x≤ε ⟩ + ε ∙ y <⟨ ∙-monoˡ-< y<ε ⟩ + ε ∙ ε ≈⟨ identity² ⟩ + ε ∎ + +x<ε∧y≤ε⇒x∙y<ε : ∀ {x y} → x < ε → y ≤ ε → x ∙ y < ε +x<ε∧y≤ε⇒x∙y<ε {x} {y} x<ε y≤ε = begin-strict + x ∙ y <⟨ ∙-monoʳ-< x<ε ⟩ + ε ∙ y ≤⟨ ∙-monoˡ-≤ y≤ε ⟩ + ε ∙ ε ≈⟨ identity² ⟩ + ε ∎ + +-- _≤_ + +x≥ε∧y≥ε⇒x∙y≥ε : ∀ {x y} → x ≥ ε → y ≥ ε → x ∙ y ≥ ε +x≥ε∧y≥ε⇒x∙y≥ε {x} {y} x≥ε y≥ε = begin + ε ≈˘⟨ identity² ⟩ + ε ∙ ε ≤⟨ ∙-mono-≤ x≥ε y≥ε ⟩ + x ∙ y ∎ + +x≤ε∧y≤ε⇒x∙y≤ε : ∀ {x y} → x ≤ ε → y ≤ ε → x ∙ y ≤ ε +x≤ε∧y≤ε⇒x∙y≤ε {x} {y} x≥ε y≥ε = begin + x ∙ y ≤⟨ ∙-mono-≤ x≥ε y≥ε ⟩ + ε ∙ ε ≈⟨ identity² ⟩ + ε ∎ + +---- Respects signs + +-- _<_ + +x≤ε∧x∙y>ε⇒y>ε : ∀ {x y} → x ≤ ε → x ∙ y > ε → y > ε +x≤ε∧x∙y>ε⇒y>ε x≤ε x∙y>ε = ≰⇒> (<⇒≱ x∙y>ε ∘ x≤ε∧y≤ε⇒x∙y≤ε x≤ε) + +x≤ε∧y∙x>ε⇒y>ε : ∀ {x y} → x ≤ ε → y ∙ x > ε → y > ε +x≤ε∧y∙x>ε⇒y>ε x≤ε y∙x>ε = ≰⇒> (<⇒≱ y∙x>ε ∘ flip x≤ε∧y≤ε⇒x∙y≤ε x≤ε) + +x<ε∧x∙y≥ε⇒y>ε : ∀ {x y} → x < ε → x ∙ y ≥ ε → y > ε +x<ε∧x∙y≥ε⇒y>ε x<ε x∙y≥ε = ≰⇒> (≤⇒≯ x∙y≥ε ∘ x<ε∧y≤ε⇒x∙y<ε x<ε) + +x<ε∧y∙x≥ε⇒y>ε : ∀ {x y} → x < ε → y ∙ x ≥ ε → y > ε +x<ε∧y∙x≥ε⇒y>ε x<ε y∙x≥ε = ≰⇒> (≤⇒≯ y∙x≥ε ∘ flip x≤ε∧y<ε⇒x∙y<ε x<ε) + +x≥ε∧x∙y<ε⇒y<ε : ∀ {x y} → x ≥ ε → x ∙ y < ε → y < ε +x≥ε∧x∙y<ε⇒y<ε x≥ε x∙y<ε = ≰⇒> (<⇒≱ x∙y<ε ∘ x≥ε∧y≥ε⇒x∙y≥ε x≥ε) + +x≥ε∧y∙x<ε⇒y<ε : ∀ {x y} → x ≥ ε → y ∙ x < ε → y < ε +x≥ε∧y∙x<ε⇒y<ε x≥ε y∙x<ε = ≰⇒> (<⇒≱ y∙x<ε ∘ flip x≥ε∧y≥ε⇒x∙y≥ε x≥ε) + +x>ε∧x∙y≤ε⇒y<ε : ∀ {x y} → x > ε → x ∙ y ≤ ε → y < ε +x>ε∧x∙y≤ε⇒y<ε x>ε x∙y≤ε = ≰⇒> (≤⇒≯ x∙y≤ε ∘ x>ε∧y≥ε⇒x∙y>ε x>ε) + +x>ε∧y∙x≤ε⇒y<ε : ∀ {x y} → x > ε → y ∙ x ≤ ε → y < ε +x>ε∧y∙x≤ε⇒y<ε x>ε y∙x≤ε = ≰⇒> (≤⇒≯ y∙x≤ε ∘ flip x≥ε∧y>ε⇒x∙y>ε x>ε) + +-- _≤_ + +x≤ε∧x∙y≥ε⇒y≥ε : ∀ {x y} → x ≤ ε → x ∙ y ≥ ε → y ≥ ε +x≤ε∧x∙y≥ε⇒y≥ε x≤ε x∙y≥ε = ≮⇒≥ (≤⇒≯ x∙y≥ε ∘ x≤ε∧y<ε⇒x∙y<ε x≤ε) + +x≤ε∧y∙x≥ε⇒y≥ε : ∀ {x y} → x ≤ ε → y ∙ x ≥ ε → y ≥ ε +x≤ε∧y∙x≥ε⇒y≥ε x≤ε y∙x≥ε = ≮⇒≥ (≤⇒≯ y∙x≥ε ∘ flip x<ε∧y≤ε⇒x∙y<ε x≤ε) + +x≥ε∧x∙y≤ε⇒y≤ε : ∀ {x y} → x ≥ ε → x ∙ y ≤ ε → y ≤ ε +x≥ε∧x∙y≤ε⇒y≤ε x≥ε x∙y≤ε = ≮⇒≥ (≤⇒≯ x∙y≤ε ∘ x≥ε∧y>ε⇒x∙y>ε x≥ε) + +x≥ε∧y∙x≤ε⇒y≤ε : ∀ {x y} → x ≥ ε → y ∙ x ≤ ε → y ≤ ε +x≥ε∧y∙x≤ε⇒y≤ε x≥ε y∙x≤ε = ≮⇒≥ (≤⇒≯ y∙x≤ε ∘ flip x>ε∧y≥ε⇒x∙y>ε x≥ε) + +-- ---- Infer signs + +-- -- _≈_ + +-- x∙y≈x⇒y≈ε : ∀ {x y} → x ∙ y ≈ x → y ≈ ε +-- x∙y≈x⇒y≈ε {x} {y} x∙y≈x = ∙-cancelˡ x (Eq.trans x∙y≈x (Eq.sym (identityʳ x))) + +-- x∙y≈y⇒x≈ε : ∀ {x y} → x ∙ y ≈ y → x ≈ ε +-- x∙y≈y⇒x≈ε {x} {y} x∙y≈y = ∙-cancelʳ x ε (Eq.trans x∙y≈y (Eq.sym (identityˡ y))) + +-- -- _<_ + +-- x∙y<x⇒y<ε : ∀ {x y} → x ∙ y < x → y < ε +-- x∙y<x⇒y<ε {x} {y} x∙y<x = ∙-cancelˡ-< x (<-respʳ-≈ (Eq.sym (identityʳ x)) x∙y<x) + +-- x∙y<y⇒x<ε : ∀ {x y} → x ∙ y < y → x < ε +-- x∙y<y⇒x<ε {x} {y} x∙y<y = ∙-cancelʳ-< x ε (<-respʳ-≈ (Eq.sym (identityˡ y)) x∙y<y) + +-- x∙y>x⇒y>ε : ∀ {x y} → x ∙ y > x → y > ε +-- x∙y>x⇒y>ε {x} {y} x∙y>x = ∙-cancelˡ-< x (<-respˡ-≈ (Eq.sym (identityʳ x)) x∙y>x) + +-- x∙y>y⇒x>ε : ∀ {x y} → x ∙ y > y → x > ε +-- x∙y>y⇒x>ε {x} {y} x∙y>y = ∙-cancelʳ-< ε x (<-respˡ-≈ (Eq.sym (identityˡ y)) x∙y>y) + +-- -- _≤_ + +-- x∙y≤x⇒y≤ε : ∀ {x y} → x ∙ y ≤ x → y ≤ ε +-- x∙y≤x⇒y≤ε {x} {y} x∙y≤x = ∙-cancelˡ-≤ x (≤-respʳ-≈ (Eq.sym (identityʳ x)) x∙y≤x) + +-- x∙y≤y⇒x≤ε : ∀ {x y} → x ∙ y ≤ y → x ≤ ε +-- x∙y≤y⇒x≤ε {x} {y} x∙y≤y = ∙-cancelʳ-≤ x ε (≤-respʳ-≈ (Eq.sym (identityˡ y)) x∙y≤y) + +-- x∙y≥x⇒y≥ε : ∀ {x y} → x ∙ y ≥ x → y ≥ ε +-- x∙y≥x⇒y≥ε {x} {y} x∙y≥x = ∙-cancelˡ-≤ x (≤-respˡ-≈ (Eq.sym (identityʳ x)) x∙y≥x) + +-- x∙y≥y⇒x≥ε : ∀ {x y} → x ∙ y ≥ y → x ≥ ε +-- x∙y≥y⇒x≥ε {x} {y} x∙y≥y = ∙-cancelʳ-≤ ε x (≤-respˡ-≈ (Eq.sym (identityˡ y)) x∙y≥y) + +-- -------------------------------------------------------------------------------- +---- Properties of _×_ + +---- Zero + +×-zeroˡ : ∀ x → 0 × x ≈ ε +×-zeroˡ x = Eq.refl + +×-zeroʳ : ∀ n → n × ε ≈ ε +×-zeroʳ 0 = Eq.refl +×-zeroʳ (suc n) = begin-equality + suc n × ε ≈⟨ 1+× n ε ⟩ + ε ∙ n × ε ≈⟨ ∙-congˡ (×-zeroʳ n) ⟩ + ε ∙ ε ≈⟨ identity² ⟩ + ε ∎ + +---- Identity + +×-identityˡ : ∀ x → 1 × x ≈ x +×-identityˡ x = Eq.refl + +---- Preserves signs + +-- _≤_ + +x≥ε⇒n×x≥ε : ∀ n {x} → x ≥ ε → n × x ≥ ε +x≥ε⇒n×x≥ε 0 {x} x≥ε = ≤-refl +x≥ε⇒n×x≥ε (suc n) {x} x≥ε = begin + ε ≤⟨ x≥ε∧y≥ε⇒x∙y≥ε x≥ε (x≥ε⇒n×x≥ε n x≥ε) ⟩ + x ∙ n × x ≈˘⟨ 1+× n x ⟩ + suc n × x ∎ + +x≤ε⇒n×x≤ε : ∀ n {x} → x ≤ ε → n × x ≤ ε +x≤ε⇒n×x≤ε 0 {x} x≤ε = ≤-refl +x≤ε⇒n×x≤ε (suc n) {x} x≤ε = begin + suc n × x ≈⟨ 1+× n x ⟩ + x ∙ n × x ≤⟨ x≤ε∧y≤ε⇒x∙y≤ε x≤ε (x≤ε⇒n×x≤ε n x≤ε) ⟩ + ε ∎ + +-- _<_ + +n≢0∧x>ε⇒n×x>ε : ∀ n {x} → ⦃ NonZero n ⦄ → x > ε → n × x > ε +n≢0∧x>ε⇒n×x>ε (suc n) {x} x>ε = begin-strict + ε <⟨ x>ε∧y≥ε⇒x∙y>ε x>ε (x≥ε⇒n×x≥ε n (<⇒≤ x>ε)) ⟩ + x ∙ n × x ≈˘⟨ 1+× n x ⟩ + suc n × x ∎ + +n≢0∧x<ε⇒n×x<ε : ∀ n {x} → ⦃ NonZero n ⦄ → x < ε → n × x < ε +n≢0∧x<ε⇒n×x<ε (suc n) {x} x<ε = begin-strict + suc n × x ≈⟨ 1+× n x ⟩ + x ∙ n × x <⟨ x<ε∧y≤ε⇒x∙y<ε x<ε (x≤ε⇒n×x≤ε n (<⇒≤ x<ε)) ⟩ + ε ∎ + +---- Congruences + +-- _≤_ + +×-monoˡ-≤ : ∀ n → Congruent₁ _≤_ (n ×_) +×-monoˡ-≤ 0 x≤y = ≤-refl +×-monoˡ-≤ (suc n) {x} {y} x≤y = begin + suc n × x ≈⟨ 1+× n x ⟩ + x ∙ n × x ≤⟨ ∙-mono-≤ x≤y (×-monoˡ-≤ n x≤y) ⟩ + y ∙ n × y ≈˘⟨ 1+× n y ⟩ + suc n × y ∎ + +x≥ε⇒×-monoʳ-≤ : ∀ {x} → x ≥ ε → (_× x) Preserves ℕ._≤_ ⟶ _≤_ +x≥ε⇒×-monoʳ-≤ {x} x≥ε {.0} {n} ℕ.z≤n = x≥ε⇒n×x≥ε n x≥ε +x≥ε⇒×-monoʳ-≤ {x} x≥ε {.suc m} {.suc n} (ℕ.s≤s m≤n) = begin + suc m × x ≈⟨ 1+× m x ⟩ + x ∙ m × x ≤⟨ ∙-monoˡ-≤ (x≥ε⇒×-monoʳ-≤ x≥ε m≤n) ⟩ + x ∙ n × x ≈˘⟨ 1+× n x ⟩ + suc n × x ∎ + +x≤ε⇒×-anti-monoʳ-≤ : ∀ {x} → x ≤ ε → (_× x) Preserves ℕ._≤_ ⟶ _≥_ +x≤ε⇒×-anti-monoʳ-≤ {x} x≤ε {.0} {n} ℕ.z≤n = x≤ε⇒n×x≤ε n x≤ε +x≤ε⇒×-anti-monoʳ-≤ {x} x≤ε {.suc m} {.suc n} (ℕ.s≤s m≤n) = begin + suc n × x ≈⟨ 1+× n x ⟩ + x ∙ n × x ≤⟨ ∙-monoˡ-≤ (x≤ε⇒×-anti-monoʳ-≤ x≤ε m≤n) ⟩ + x ∙ m × x ≈˘⟨ 1+× m x ⟩ + suc m × x ∎ + +-- _<_ + +n≢0⇒×-monoˡ-< : ∀ n → ⦃ NonZero n ⦄ → Congruent₁ _<_ (n ×_) +n≢0⇒×-monoˡ-< (suc n) {x} {y} x<y = begin-strict + suc n × x ≈⟨ 1+× n x ⟩ + x ∙ n × x ≤⟨ ∙-monoˡ-≤ (×-monoˡ-≤ n (<⇒≤ x<y)) ⟩ + x ∙ n × y <⟨ ∙-monoʳ-< x<y ⟩ + y ∙ n × y ≈˘⟨ 1+× n y ⟩ + suc n × y ∎ + +x>ε⇒×-monoʳ-< : ∀ {x} → x > ε → (_× x) Preserves ℕ._<_ ⟶ _<_ +x>ε⇒×-monoʳ-< {x} x>ε {m} {.suc n} (ℕ.s≤s m≤n) = begin-strict + m × x ≈˘⟨ identityˡ (m × x) ⟩ + ε ∙ m × x ≤⟨ ∙-monoˡ-≤ (x≥ε⇒×-monoʳ-≤ (<⇒≤ x>ε) m≤n) ⟩ + ε ∙ n × x <⟨ ∙-monoʳ-< x>ε ⟩ + x ∙ n × x ≈˘⟨ 1+× n x ⟩ + suc n × x ∎ + +x<ε⇒×-anti-monoʳ-< : ∀ {x} → x < ε → (_× x) Preserves ℕ._<_ ⟶ _>_ +x<ε⇒×-anti-monoʳ-< {x} x<ε {m} {.suc n} (ℕ.s≤s m≤n) = begin-strict + suc n × x ≈⟨ 1+× n x ⟩ + x ∙ n × x <⟨ ∙-monoʳ-< x<ε ⟩ + ε ∙ n × x ≤⟨ ∙-monoˡ-≤ (x≤ε⇒×-anti-monoʳ-≤ (<⇒≤ x<ε) m≤n) ⟩ + ε ∙ m × x ≈⟨ identityˡ (m × x) ⟩ + m × x ∎ + +---- Cancellative + +-- _<_ + +×-cancelˡ-< : ∀ n → Injective _<_ _<_ (n ×_) +×-cancelˡ-< n = mono₁-≤⇒cancel₁-< (×-monoˡ-≤ n) + +x≥ε⇒×-cancelʳ-< : ∀ {x} → x ≥ ε → Injective ℕ._<_ _<_ (_× x) +x≥ε⇒×-cancelʳ-< x≥ε m×x<n×x = ℕₚ.≰⇒> (<⇒≱ m×x<n×x ∘ x≥ε⇒×-monoʳ-≤ x≥ε) + +x≤ε⇒×-anti-cancelʳ-< : ∀ {x} → x ≤ ε → Injective ℕ._<_ _>_ (_× x) +x≤ε⇒×-anti-cancelʳ-< x≤ε m×x>n×x = ℕₚ.≰⇒> (<⇒≱ m×x>n×x ∘ x≤ε⇒×-anti-monoʳ-≤ x≤ε) + +-- _≤_ + +n≢0⇒×-cancelˡ-≤ : ∀ n → ⦃ NonZero n ⦄ → Injective _≤_ _≤_ (n ×_) +n≢0⇒×-cancelˡ-≤ n = mono₁-<⇒cancel₁-≤ (n≢0⇒×-monoˡ-< n) + +x>ε⇒×-cancelʳ-≤ : ∀ {x} → x > ε → Injective ℕ._≤_ _≤_ (_× x) +x>ε⇒×-cancelʳ-≤ x>ε m×x≤n×x = ℕₚ.≮⇒≥ (≤⇒≯ m×x≤n×x ∘ x>ε⇒×-monoʳ-< x>ε) + +x<ε⇒×-anti-cancelʳ-≤ : ∀ {x} → x < ε → Injective ℕ._≤_ _≥_ (_× x) +x<ε⇒×-anti-cancelʳ-≤ x<ε m×x≥n×x = ℕₚ.≮⇒≥ (≤⇒≯ m×x≥n×x ∘ x<ε⇒×-anti-monoʳ-< x<ε) + +---- Respects signs + +-- _<_ + +n×x>ε⇒x>ε : ∀ {n x} → n × x > ε → x > ε +n×x>ε⇒x>ε {n} n×x>ε = ≰⇒> (<⇒≱ n×x>ε ∘ x≤ε⇒n×x≤ε n) + +n×x<ε⇒x<ε : ∀ {n x} → n × x < ε → x < ε +n×x<ε⇒x<ε {n} n×x<ε = ≰⇒> (<⇒≱ n×x<ε ∘ x≥ε⇒n×x≥ε n) + +-- _≥_ + +n≢0∧n×x≥ε⇒x≥ε : ∀ {n x} → ⦃ NonZero n ⦄ → n × x ≥ ε → x ≥ ε +n≢0∧n×x≥ε⇒x≥ε {n} n×x≥ε = ≮⇒≥ (≤⇒≯ n×x≥ε ∘ n≢0∧x<ε⇒n×x<ε n) + +n≢0∧n×x≤ε⇒x≤ε : ∀ {n x} → ⦃ NonZero n ⦄ → n × x ≤ ε → x ≤ ε +n≢0∧n×x≤ε⇒x≤ε {n} n×x≤ε = ≮⇒≥ (≤⇒≯ n×x≤ε ∘ n≢0∧x>ε⇒n×x>ε n) + +-- ---- Infer signs + +-- -- _≈_ + +-- n≢0∧n×x≈x⇒x≈ε : ∀ n {x} → ⦃ NonZero n ⦄ → n × x ≈ x → x ≈ ε +-- n≢0∧n×x≈x⇒x≈ε n n×x≈x = ≮∧≯⇒≈ +-- (λ x<ε → <-irrefl n×x≈x (<-trans (n≢0∧x<ε⇒n×x<ε {!!} {!!}) {!!})) +-- (λ x>ε → {!!}) diff --git a/src/Helium/Algebra/Ordered/StrictTotal/Properties/Ring.agda b/src/Helium/Algebra/Ordered/StrictTotal/Properties/Ring.agda index 484143c..5e51e89 100644 --- a/src/Helium/Algebra/Ordered/StrictTotal/Properties/Ring.agda +++ b/src/Helium/Algebra/Ordered/StrictTotal/Properties/Ring.agda @@ -14,68 +14,542 @@ module Helium.Algebra.Ordered.StrictTotal.Properties.Ring where open Ring ring + renaming + ( trans to <-trans + ; irrefl to <-irrefl + ; asym to <-asym + ; 0<a+0<b⇒0<ab to x>0∧y>0⇒x*y>0 + ) -open import Agda.Builtin.FromNat -open import Agda.Builtin.FromNeg -open import Data.Nat using (suc; NonZero) +open import Algebra.Definitions +open import Data.Nat as ℕ 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 Function using (_∘_) +open import Function.Definitions +open import Helium.Algebra.Ordered.StrictTotal.Consequences strictTotalOrder +open import Relation.Binary.Core +open import Relation.Binary.Definitions 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.Relation.Binary.Properties.StrictTotalOrder strictTotalOrder public open import Helium.Algebra.Ordered.StrictTotal.Properties.AbelianGroup +-abelianGroup public - using (<⇒≱; ≤⇒≯; >⇒≉; ≈⇒≯; <⇒≉; ≈⇒≮; ≤∧≉⇒<; ≥∧≉⇒>) + using + ( ×-zeroˡ; ×-zeroʳ + ; ×-identityˡ + ; n≢0⇒×-monoˡ-<; ×-monoˡ-≤ + ; ×-cancelˡ-<; n≢0⇒×-cancelˡ-≤ + ) 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 ∎ + ( ∙-mono-< to +-mono-< + ; ∙-monoˡ-< to +-monoˡ-< + ; ∙-monoʳ-< to +-monoʳ-< + ; ∙-mono-≤ to +-mono-≤ + ; ∙-monoˡ-≤ to +-monoˡ-≤ + ; ∙-monoʳ-≤ to +-monoʳ-≤ + + ; ∙-cancelˡ-< to +-cancelˡ-< + ; ∙-cancelʳ-< to +-cancelʳ-< + ; ∙-cancel-< to +-cancel-< + ; ∙-cancelˡ-≤ to +-cancelˡ-≤ + ; ∙-cancelʳ-≤ to +-cancelʳ-≤ + ; ∙-cancel-≤ to +-cancel-≤ + -- _∙_ pres signs + ; x≥ε∧y>ε⇒x∙y>ε to x≥0∧y>0⇒x+y>0 + ; x>ε∧y≥ε⇒x∙y>ε to x>0∧y≥0⇒x+y>0 + ; x≤ε∧y<ε⇒x∙y<ε to x≤0∧y<0⇒x+y<0 + ; x<ε∧y≤ε⇒x∙y<ε to x<0∧y≤0⇒x+y<0 + ; x≥ε∧y≥ε⇒x∙y≥ε to x≥0∧y≥0⇒x+y≥0 + ; x≤ε∧y≤ε⇒x∙y≤ε to x≤0∧y≤0⇒x+y≤0 + -- _∙_ resp signs + ; x≤ε∧x∙y>ε⇒y>ε to x≤0∧x+y>0⇒y>0 + ; x≤ε∧y∙x>ε⇒y>ε to x≤0∧y+x>0⇒y>0 + ; x<ε∧x∙y≥ε⇒y>ε to x<0∧x+y≥0⇒y>0 + ; x<ε∧y∙x≥ε⇒y>ε to x<0∧y+x≥0⇒y>0 + ; x≥ε∧x∙y<ε⇒y<ε to x≥0∧x+y<0⇒y<0 + ; x≥ε∧y∙x<ε⇒y<ε to x≥0∧y+x<0⇒y<0 + ; x>ε∧x∙y≤ε⇒y<ε to x>0∧x+y≤0⇒y<0 + ; x>ε∧y∙x≤ε⇒y<ε to x>0∧y+x≤0⇒y<0 + ; x≤ε∧x∙y≥ε⇒y≥ε to x≤0∧x+y≥0⇒y≥0 + ; x≤ε∧y∙x≥ε⇒y≥ε to x≤0∧y+x≥0⇒y≥0 + ; x≥ε∧x∙y≤ε⇒y≤ε to x≥0∧x+y≤0⇒y≤0 + ; x≥ε∧y∙x≤ε⇒y≤ε to x≥0∧y+x≤0⇒y≤0 + + ; x>ε⇒×-monoʳ-< to x>0⇒×-monoʳ-< + ; x<ε⇒×-anti-monoʳ-< to x<0⇒×-anti-monoʳ-< + ; x≥ε⇒×-monoʳ-≤ to x≥0⇒×-monoʳ-≤ + ; x≤ε⇒×-anti-monoʳ-≤ to x≤0⇒×-anti-monoʳ-≤ + + ; x≥ε⇒×-cancelʳ-< to x≥0⇒×-cancelʳ-< + ; x≤ε⇒×-anti-cancelʳ-< to x≤0⇒×-anti-cancelʳ-< + ; x>ε⇒×-cancelʳ-≤ to x>0⇒×-cancelʳ-≤ + ; x<ε⇒×-anti-cancelʳ-≤ to x<0⇒×-anti-cancelʳ-≤ + -- _×_ pres signs + ; n≢0∧x>ε⇒n×x>ε to n≢0∧x>0⇒n×x>0 + ; n≢0∧x<ε⇒n×x<ε to n≢0∧x<0⇒n×x<0 + ; x≥ε⇒n×x≥ε to x≥0⇒n×x≥0 + ; x≤ε⇒n×x≤ε to x≤0⇒n×x≤0 + -- _×_ resp signs + ; n×x>ε⇒x>ε to n×x>0⇒x>0 + ; n×x<ε⇒x<ε to n×x<0⇒x<0 + ; n≢0∧n×x≥ε⇒x≥ε to n≢0∧n×x≥0⇒x≥0 + ; n≢0∧n×x≤ε⇒x≤ε to n≢0∧n×x≤0⇒x≤0 + + ; ⁻¹-anti-mono-< to -‿anti-mono-< + ; ⁻¹-anti-mono-≤ to -‿anti-mono-≤ + + ; ⁻¹-cancel to -‿cancel + ; ⁻¹-anti-cancel-< to -‿anti-cancel-< + ; ⁻¹-anti-cancel-≤ to -‿anti-cancel-≤ + + ; x<ε⇒x⁻¹>ε to x<0⇒-x>0 + ; x>ε⇒x⁻¹<ε to x>0⇒-x<0 + ; x≤ε⇒x⁻¹≥ε to x≤0⇒-x≥0 + ; x≥ε⇒x⁻¹≤ε to x≥0⇒-x≤0 + + ; x⁻¹<ε⇒x>ε to -x<0⇒x>0 + ; x⁻¹>ε⇒x<ε to -x>0⇒x<0 + ; x⁻¹≤ε⇒x≥ε to -x≤0⇒x≥0 + ; x⁻¹≥ε⇒x≤ε to -x≥0⇒x≤0 + + ; x<y⇒ε<y∙x⁻¹ to x<y⇒0<y-x + ; ε<y∙x⁻¹⇒x<y to 0<y-x⇒x<y + ) + +-------------------------------------------------------------------------------- +---- Properties of _*_ and -_ + +-x*-y≈x*y : ∀ x y → - x * - y ≈ x * y +-x*-y≈x*y x y = begin-equality + - x * - y ≈˘⟨ -‿distribˡ-* x (- y) ⟩ + - (x * - y) ≈˘⟨ -‿cong (-‿distribʳ-* x y) ⟩ + - - (x * y) ≈⟨ -‿involutive (x * y) ⟩ + x * y ∎ + +-------------------------------------------------------------------------------- +---- Properties of _*_ + +---- Congruences + +-- _<_ + +x>0⇒*-monoˡ-< : ∀ {x} → x > 0# → Congruent₁ _<_ (x *_) +x>0⇒*-monoˡ-< {x} x>0 {y} {z} y<z = begin-strict + x * y ≈˘⟨ +-identityˡ (x * y) ⟩ + 0# + x * y ≈˘⟨ +-cong (-‿inverseʳ (x * z)) (-x*-y≈x*y x y) ⟩ + x * z - x * z + - x * - y ≈⟨ +-congʳ (+-congˡ (-‿distribˡ-* x z)) ⟩ + x * z + - x * z + - x * - y ≈⟨ +-assoc (x * z) (- x * z) (- x * - y) ⟩ + x * z + (- x * z + - x * - y) ≈˘⟨ +-congˡ (distribˡ (- x) z (- y)) ⟩ + x * z + - x * (z - y) ≈˘⟨ +-congˡ (-‿distribˡ-* x (z - y)) ⟩ + x * z - x * (z - y) <⟨ +-monoˡ-< (x>0⇒-x<0 (x>0∧y>0⇒x*y>0 x>0 (x<y⇒0<y-x y<z))) ⟩ + x * z + 0# ≈⟨ +-identityʳ (x * z) ⟩ + x * z ∎ + +x>0⇒*-monoʳ-< : ∀ {x} → x > 0# → Congruent₁ _<_ (_* x) +x>0⇒*-monoʳ-< {x} x>0 {y} {z} y<z = begin-strict + y * x ≈˘⟨ +-identityˡ (y * x) ⟩ + 0# + y * x ≈˘⟨ +-cong (-‿inverseʳ (z * x)) (-x*-y≈x*y y x) ⟩ + z * x - z * x + - y * - x ≈⟨ +-congʳ (+-congˡ (-‿distribʳ-* z x)) ⟩ + z * x + z * - x + - y * - x ≈⟨ +-assoc (z * x) (z * - x) (- y * - x) ⟩ + z * x + (z * - x + - y * - x) ≈˘⟨ +-congˡ (distribʳ (- x) z (- y)) ⟩ + z * x + (z - y) * - x ≈˘⟨ +-congˡ (-‿distribʳ-* (z - y) x) ⟩ + z * x - (z - y) * x <⟨ +-monoˡ-< (x>0⇒-x<0 (x>0∧y>0⇒x*y>0 (x<y⇒0<y-x y<z) x>0)) ⟩ + z * x + 0# ≈⟨ +-identityʳ (z * x) ⟩ + z * x ∎ + +x<0⇒*-anti-monoˡ-< : ∀ {x} → x < 0# → (x *_) Preserves _<_ ⟶ _>_ +x<0⇒*-anti-monoˡ-< {x} x<0 {y} {z} y<z = begin-strict + x * z ≈˘⟨ +-identityʳ (x * z) ⟩ + x * z + 0# <⟨ +-monoˡ-< (x>0∧y>0⇒x*y>0 (x<0⇒-x>0 x<0) (x<y⇒0<y-x y<z)) ⟩ + x * z + - x * (z - y) ≈⟨ +-congˡ (distribˡ (- x) z (- y)) ⟩ + x * z + (- x * z + - x * - y) ≈˘⟨ +-assoc (x * z) (- x * z) (- x * - y) ⟩ + x * z + - x * z + - x * - y ≈˘⟨ +-congʳ (+-congˡ (-‿distribˡ-* x z)) ⟩ + x * z - x * z + - x * - y ≈⟨ +-cong (-‿inverseʳ (x * z)) (-x*-y≈x*y x y) ⟩ + 0# + x * y ≈⟨ +-identityˡ (x * y) ⟩ + x * y ∎ + +x<0⇒*-anti-monoʳ-< : ∀ {x} → x < 0# → (_* x) Preserves _<_ ⟶ _>_ +x<0⇒*-anti-monoʳ-< {x} x<0 {y} {z} y<z = begin-strict + z * x ≈˘⟨ +-identityʳ (z * x) ⟩ + z * x + 0# <⟨ +-monoˡ-< (x>0∧y>0⇒x*y>0 (x<y⇒0<y-x y<z) (x<0⇒-x>0 x<0)) ⟩ + z * x + (z - y) * - x ≈⟨ +-congˡ (distribʳ (- x) z (- y)) ⟩ + z * x + (z * - x + - y * - x) ≈˘⟨ +-assoc (z * x) (z * - x) (- y * - x) ⟩ + z * x + z * - x + - y * - x ≈˘⟨ +-congʳ (+-congˡ (-‿distribʳ-* z x)) ⟩ + z * x - z * x + - y * - x ≈⟨ +-cong (-‿inverseʳ (z * x)) (-x*-y≈x*y y x) ⟩ + 0# + y * x ≈⟨ +-identityˡ (y * x) ⟩ + y * x ∎ + +-- _≤_ + +x≥0⇒*-monoˡ-≤ : ∀ {x} → x ≥ 0# → Congruent₁ _≤_ (x *_) +x≥0⇒*-monoˡ-≤ (inj₁ x>0) y≤z = cong₁+mono₁-<⇒mono₁-≤ *-congˡ (x>0⇒*-monoˡ-< x>0) y≤z +x≥0⇒*-monoˡ-≤ {x} (inj₂ 0≈x) {y} {z} y≤z = ≤-reflexive (begin-equality + x * y ≈˘⟨ *-congʳ 0≈x ⟩ + 0# * y ≈⟨ zeroˡ y ⟩ + 0# ≈˘⟨ zeroˡ z ⟩ + 0# * z ≈⟨ *-congʳ 0≈x ⟩ + x * z ∎) + +x≥0⇒*-monoʳ-≤ : ∀ {x} → x ≥ 0# → Congruent₁ _≤_ (_* x) +x≥0⇒*-monoʳ-≤ (inj₁ x>0) y≤z = cong₁+mono₁-<⇒mono₁-≤ *-congʳ (x>0⇒*-monoʳ-< x>0) y≤z +x≥0⇒*-monoʳ-≤ {x} (inj₂ 0≈x) {y} {z} y≤z = ≤-reflexive (begin-equality + y * x ≈˘⟨ *-congˡ 0≈x ⟩ + y * 0# ≈⟨ zeroʳ y ⟩ + 0# ≈˘⟨ zeroʳ z ⟩ + z * 0# ≈⟨ *-congˡ 0≈x ⟩ + z * x ∎) + +x≤0⇒*-anti-monoˡ-≤ : ∀ {x} → x ≤ 0# → (x *_) Preserves _≤_ ⟶ _≥_ +x≤0⇒*-anti-monoˡ-≤ (inj₁ x<0) y≤z = cong₁+anti-mono₁-<⇒anti-mono₁-≤ *-congˡ (x<0⇒*-anti-monoˡ-< x<0) y≤z +x≤0⇒*-anti-monoˡ-≤ {x} (inj₂ x≈0) {y} {z} y≤z = ≤-reflexive (begin-equality + x * z ≈⟨ *-congʳ x≈0 ⟩ + 0# * z ≈⟨ zeroˡ z ⟩ + 0# ≈˘⟨ zeroˡ y ⟩ + 0# * y ≈˘⟨ *-congʳ x≈0 ⟩ + x * y ∎) + +x≤0⇒*-anti-monoʳ-≤ : ∀ {x} → x ≤ 0# → (_* x) Preserves _≤_ ⟶ _≥_ +x≤0⇒*-anti-monoʳ-≤ (inj₁ x<0) y≤z = cong₁+anti-mono₁-<⇒anti-mono₁-≤ *-congʳ (x<0⇒*-anti-monoʳ-< x<0) y≤z +x≤0⇒*-anti-monoʳ-≤ {x} (inj₂ x≈0) {y} {z} y≤z = ≤-reflexive (begin-equality + z * x ≈⟨ *-congˡ x≈0 ⟩ + z * 0# ≈⟨ zeroʳ z ⟩ + 0# ≈˘⟨ zeroʳ y ⟩ + y * 0# ≈˘⟨ *-congˡ x≈0 ⟩ + y * x ∎) + +---- Cancellative + +-- _≈_ + +x>0⇒*-cancelˡ : ∀ {x} → x > 0# → Injective _≈_ _≈_ (x *_) +x>0⇒*-cancelˡ x>0 = mono₁-<⇒cancel₁ (x>0⇒*-monoˡ-< x>0) + +x>0⇒*-cancelʳ : ∀ {x} → x > 0# → Injective _≈_ _≈_ (_* x) +x>0⇒*-cancelʳ x>0 = mono₁-<⇒cancel₁ (x>0⇒*-monoʳ-< x>0) + +x<0⇒*-cancelˡ : ∀ {x} → x < 0# → Injective _≈_ _≈_ (x *_) +x<0⇒*-cancelˡ x<0 = anti-mono₁-<⇒cancel₁ (x<0⇒*-anti-monoˡ-< x<0) + +x<0⇒*-cancelʳ : ∀ {x} → x < 0# → Injective _≈_ _≈_ (_* x) +x<0⇒*-cancelʳ x<0 = anti-mono₁-<⇒cancel₁ (x<0⇒*-anti-monoʳ-< x<0) + +-- _<_ + +x≥0⇒*-cancelˡ-< : ∀ {x} → x ≥ 0# → Injective _<_ _<_ (x *_) +x≥0⇒*-cancelˡ-< = mono₁-≤⇒cancel₁-< ∘ x≥0⇒*-monoˡ-≤ + +x≥0⇒*-cancelʳ-< : ∀ {x} → x ≥ 0# → Injective _<_ _<_ (_* x) +x≥0⇒*-cancelʳ-< = mono₁-≤⇒cancel₁-< ∘ x≥0⇒*-monoʳ-≤ + +x≤0⇒*-anti-cancelˡ-< : ∀ {x} → x ≤ 0# → Injective _<_ _>_ (x *_) +x≤0⇒*-anti-cancelˡ-< = anti-mono₁-≤⇒anti-cancel₁-< ∘ x≤0⇒*-anti-monoˡ-≤ + +x≤0⇒*-anti-cancelʳ-< : ∀ {x} → x ≤ 0# → Injective _<_ _>_ (_* x) +x≤0⇒*-anti-cancelʳ-< = anti-mono₁-≤⇒anti-cancel₁-< ∘ x≤0⇒*-anti-monoʳ-≤ + +-- _≤_ + +x>0⇒*-cancelˡ-≤ : ∀ {x} → x > 0# → Injective _≤_ _≤_ (x *_) +x>0⇒*-cancelˡ-≤ = mono₁-<⇒cancel₁-≤ ∘ x>0⇒*-monoˡ-< + +x>0⇒*-cancelʳ-≤ : ∀ {x} → x > 0# → Injective _≤_ _≤_ (_* x) +x>0⇒*-cancelʳ-≤ = mono₁-<⇒cancel₁-≤ ∘ x>0⇒*-monoʳ-< + +x<0⇒*-anti-cancelˡ-≤ : ∀ {x} → x < 0# → Injective _≤_ _≥_ (x *_) +x<0⇒*-anti-cancelˡ-≤ = anti-mono₁-<⇒anti-cancel₁-≤ ∘ x<0⇒*-anti-monoˡ-< + +x<0⇒*-anti-cancelʳ-≤ : ∀ {x} → x < 0# → Injective _≤_ _≥_ (_* x) +x<0⇒*-anti-cancelʳ-≤ = anti-mono₁-<⇒anti-cancel₁-≤ ∘ x<0⇒*-anti-monoʳ-< + +---- Preserves signs + +-- _≈_ + +x≈0⇒x*y≈0 : ∀ {x} → x ≈ 0# → ∀ y → x * y ≈ 0# +x≈0⇒x*y≈0 {x} x≈0 y = begin-equality + x * y ≈⟨ *-congʳ x≈0 ⟩ + 0# * y ≈⟨ zeroˡ y ⟩ + 0# ∎ + +x≈0⇒y*x≈0 : ∀ {x} → x ≈ 0# → ∀ y → y * x ≈ 0# +x≈0⇒y*x≈0 {x} x≈0 y = begin-equality + y * x ≈⟨ *-congˡ x≈0 ⟩ + y * 0# ≈⟨ zeroʳ y ⟩ + 0# ∎ + +-- _<_ + +-- Have x>0∧y>0⇒x*y>0 by ring + +x>0∧y<0⇒x*y<0 : ∀ {x y} → x > 0# → y < 0# → x * y < 0# +x>0∧y<0⇒x*y<0 {x} {y} x>0 y<0 = -x>0⇒x<0 (begin-strict + 0# <⟨ x>0∧y>0⇒x*y>0 x>0 (x<0⇒-x>0 y<0) ⟩ + x * - y ≈˘⟨ -‿distribʳ-* x y ⟩ + - (x * y) ∎) + +x<0∧y>0⇒x*y<0 : ∀ {x y} → x < 0# → y > 0# → x * y < 0# +x<0∧y>0⇒x*y<0 {x} {y} x<0 y>0 = -x>0⇒x<0 (begin-strict + 0# <⟨ x>0∧y>0⇒x*y>0 (x<0⇒-x>0 x<0) y>0 ⟩ + - x * y ≈˘⟨ -‿distribˡ-* x y ⟩ + - (x * y) ∎) + +x<0∧y<0⇒x*y>0 : ∀ {x y} → x < 0# → y < 0# → x * y > 0# +x<0∧y<0⇒x*y>0 {x} {y} x<0 y<0 = begin-strict + 0# <⟨ x>0∧y>0⇒x*y>0 (x<0⇒-x>0 x<0) (x<0⇒-x>0 y<0) ⟩ + - x * - y ≈⟨ -x*-y≈x*y x y ⟩ + x * y ∎ + +-- _≤_ + +x≥0∧y≥0⇒x*y≥0 : ∀ {x y} → x ≥ 0# → y ≥ 0# → x * y ≥ 0# +x≥0∧y≥0⇒x*y≥0 {x} {y} (inj₁ x>0) (inj₁ y>0) = <⇒≤ (x>0∧y>0⇒x*y>0 x>0 y>0) +x≥0∧y≥0⇒x*y≥0 {x} {y} (inj₁ x>0) (inj₂ 0≈y) = ≤-reflexive (Eq.sym (x≈0⇒y*x≈0 (Eq.sym 0≈y) x)) +x≥0∧y≥0⇒x*y≥0 {x} {y} (inj₂ 0≈x) y≥0 = ≤-reflexive (Eq.sym (x≈0⇒x*y≈0 (Eq.sym 0≈x) y)) + +x≥0∧y≤0⇒x*y≤0 : ∀ {x y} → x ≥ 0# → y ≤ 0# → x * y ≤ 0# +x≥0∧y≤0⇒x*y≤0 {x} {y} (inj₁ x>0) (inj₁ y<0) = <⇒≤ (x>0∧y<0⇒x*y<0 x>0 y<0) +x≥0∧y≤0⇒x*y≤0 {x} {y} (inj₁ x>0) (inj₂ y≈0) = ≤-reflexive (x≈0⇒y*x≈0 y≈0 x) +x≥0∧y≤0⇒x*y≤0 {x} {y} (inj₂ 0≈x) y≤0 = ≤-reflexive (x≈0⇒x*y≈0 (Eq.sym 0≈x) y) + +x≤0∧y≥0⇒x*y≤0 : ∀ {x y} → x ≤ 0# → y ≥ 0# → x * y ≤ 0# +x≤0∧y≥0⇒x*y≤0 {x} {y} (inj₁ x<0) (inj₁ y>0) = <⇒≤ (x<0∧y>0⇒x*y<0 x<0 y>0) +x≤0∧y≥0⇒x*y≤0 {x} {y} (inj₁ x<0) (inj₂ 0≈y) = ≤-reflexive (x≈0⇒y*x≈0 (Eq.sym 0≈y) x) +x≤0∧y≥0⇒x*y≤0 {x} {y} (inj₂ x≈0) y≥0 = ≤-reflexive (x≈0⇒x*y≈0 x≈0 y) + +x≤0∧y≤0⇒x*y≥0 : ∀ {x y} → x ≤ 0# → y ≤ 0# → x * y ≥ 0# +x≤0∧y≤0⇒x*y≥0 {x} {y} (inj₁ x<0) (inj₁ y<0) = <⇒≤ (x<0∧y<0⇒x*y>0 x<0 y<0) +x≤0∧y≤0⇒x*y≥0 {x} {y} (inj₁ x<0) (inj₂ y≈0) = ≤-reflexive (Eq.sym (x≈0⇒y*x≈0 y≈0 x)) +x≤0∧y≤0⇒x*y≥0 {x} {y} (inj₂ x≈0) y≤0 = ≤-reflexive (Eq.sym (x≈0⇒x*y≈0 x≈0 y)) + +---- Respects signs + +-- _<_ + +-- x>0∧x*y>0⇒y>0 +-- x>0∧x*y<0⇒y<0 +-- x>0∧y*x>0⇒y>0 +-- x>0∧y*x<0⇒y<0 +-- x<0∧x*y>0⇒y<0 +-- x<0∧x*y<0⇒y>0 +-- x<0∧y*x>0⇒y<0 +-- x<0∧y*x<0⇒y>0 + +-- _≤_ + +-- x>0∧x*y≥0⇒y≥0 +-- x>0∧x*y≤0⇒y≤0 +-- x>0∧y*x≥0⇒y≥0 +-- x>0∧y*x≤0⇒y≤0 +-- x<0∧x*y≥0⇒y≤0 +-- x<0∧x*y≤0⇒y≥0 +-- x<0∧y*x≥0⇒y≤0 +-- x<0∧y*x≤0⇒y≥0 + +-------------------------------------------------------------------------------- +---- Properties of 0 and 1 + +0≤1 : 0# ≤ 1# +0≤1 = ≮⇒≥ (λ 0>1 → <-asym 0>1 (begin-strict + 0# <⟨ x<0∧y<0⇒x*y>0 0>1 0>1 ⟩ + 1# * 1# ≈⟨ *-identity² ⟩ + 1# ∎)) + +1≈0⇒x≈y : ∀ {x y} → 1# ≈ 0# → x ≈ y +1≈0⇒x≈y {x} {y} 1≈0 = begin-equality + x ≈˘⟨ *-identityʳ x ⟩ + x * 1# ≈⟨ x≈0⇒y*x≈0 1≈0 x ⟩ + 0# ≈˘⟨ x≈0⇒y*x≈0 1≈0 y ⟩ + y * 1# ≈⟨ *-identityʳ y ⟩ + y ∎ + +x<y⇒0<1 : ∀ {x y} → x < y → 0# < 1# +x<y⇒0<1 x<y = ≤∧≉⇒< 0≤1 (<⇒≉ x<y ∘ 1≈0⇒x≈y ∘ Eq.sym) + +-------------------------------------------------------------------------------- +---- Properties of _*_ (again) + +---- Preserves size + +-- _<_ + +x>1∧y≥1⇒x*y>1 : ∀ {x y} → x > 1# → y ≥ 1# → x * y > 1# +x>1∧y≥1⇒x*y>1 {x} {y} x>1 y≥1 = begin-strict + 1# ≈˘⟨ *-identity² ⟩ + 1# * 1# <⟨ x>0⇒*-monoʳ-< (x<y⇒0<1 x>1) x>1 ⟩ + x * 1# ≤⟨ x≥0⇒*-monoˡ-≤ (≤-trans 0≤1 (<⇒≤ x>1)) y≥1 ⟩ + x * y ∎ + +x≥1∧y>1⇒x*y>1 : ∀ {x y} → x ≥ 1# → y > 1# → x * y > 1# +x≥1∧y>1⇒x*y>1 {x} {y} x≥1 y>1 = begin-strict + 1# ≈˘⟨ *-identity² ⟩ + 1# * 1# <⟨ x>0⇒*-monoˡ-< (x<y⇒0<1 y>1) y>1 ⟩ + 1# * y ≤⟨ x≥0⇒*-monoʳ-≤ (≤-trans 0≤1 (<⇒≤ y>1)) x≥1 ⟩ + x * y ∎ + +0≤x<1∧y≤1⇒x*y<1 : ∀ {x y} → 0# ≤ x → x < 1# → y ≤ 1# → x * y < 1# +0≤x<1∧y≤1⇒x*y<1 {x} {y} 0≤x x<1 y≤1 = begin-strict + x * y ≤⟨ x≥0⇒*-monoˡ-≤ 0≤x y≤1 ⟩ + x * 1# <⟨ x>0⇒*-monoʳ-< (x<y⇒0<1 x<1) x<1 ⟩ + 1# * 1# ≈⟨ *-identity² ⟩ + 1# ∎ + +x≤1∧0≤y<1⇒x*y<1 : ∀ {x y} → x ≤ 1# → 0# ≤ y → y < 1# → x * y < 1# +x≤1∧0≤y<1⇒x*y<1 {x} {y} x≤1 0≤y y<1 = begin-strict + x * y ≤⟨ x≥0⇒*-monoʳ-≤ 0≤y x≤1 ⟩ + 1# * y <⟨ x>0⇒*-monoˡ-< (x<y⇒0<1 y<1) y<1 ⟩ + 1# * 1# ≈⟨ *-identity² ⟩ + 1# ∎ + +-- _≤_ + +x≥1∧y≥1⇒x*y≥1 : ∀ {x y} → x ≥ 1# → y ≥ 1# → x * y ≥ 1# +x≥1∧y≥1⇒x*y≥1 {x} {y} x≥1 y≥1 = begin + 1# ≈˘⟨ *-identity² ⟩ + 1# * 1# ≤⟨ x≥0⇒*-monoʳ-≤ 0≤1 x≥1 ⟩ + x * 1# ≤⟨ x≥0⇒*-monoˡ-≤ (≤-trans 0≤1 x≥1) y≥1 ⟩ + x * y ∎ + +0≤x≤1∧y≤1⇒x*y≤1 : ∀ {x y} → 0# ≤ x → x ≤ 1# → y ≤ 1# → x * y ≤ 1# +0≤x≤1∧y≤1⇒x*y≤1 {x} {y} 0≤x x≤1 y≤1 = begin + x * y ≤⟨ x≥0⇒*-monoˡ-≤ 0≤x y≤1 ⟩ + x * 1# ≤⟨ x≥0⇒*-monoʳ-≤ 0≤1 x≤1 ⟩ + 1# * 1# ≈⟨ *-identity² ⟩ + 1# ∎ + +x≤1∧0≤y≤1⇒x*y≤1 : ∀ {x y} → x ≤ 1# → 0# ≤ y → y ≤ 1# → x * y ≤ 1# +x≤1∧0≤y≤1⇒x*y≤1 {x} {y} x≤1 0≤y y≤1 = begin + x * y ≤⟨ x≥0⇒*-monoʳ-≤ 0≤y x≤1 ⟩ + 1# * y ≤⟨ x≥0⇒*-monoˡ-≤ 0≤1 y≤1 ⟩ + 1# * 1# ≈⟨ *-identity² ⟩ + 1# ∎ + +---- Miscellaneous + +x*x≥0 : ∀ x → x * x ≥ 0# +x*x≥0 x with compare x 0# +... | tri< x<0 _ _ = <⇒≤ (x<0∧y<0⇒x*y>0 x<0 x<0) +... | tri≈ _ x≈0 _ = ≤-reflexive (Eq.sym (x≈0⇒x*y≈0 x≈0 x)) +... | tri> _ _ x>0 = <⇒≤ (x>0∧y>0⇒x*y>0 x>0 x>0) + +-------------------------------------------------------------------------------- +---- Properties of _^_ + +---- Zero + +^-zeroˡ : ∀ n → 1# ^ n ≈ 1# +^-zeroˡ 0 = Eq.refl +^-zeroˡ (suc n) = begin-equality + 1# ^ suc n ≈⟨ ^-homo-* 1# 1 n ⟩ + 1# * 1# ^ n ≈⟨ *-congˡ (^-zeroˡ n) ⟩ + 1# * 1# ≈⟨ *-identity² ⟩ + 1# ∎ + +^-zeroʳ : ∀ x → x ^ 0 ≈ 1# +^-zeroʳ x = Eq.refl + +---- Identity + +^-identityʳ : ∀ x → x ^ 1 ≈ x +^-identityʳ x = Eq.refl + +---- Preserves sign + +-- _≤_ + +x≥0⇒x^n≥0 : ∀ {x} → x ≥ 0# → ∀ n → x ^ n ≥ 0# +x≥0⇒x^n≥0 {x} x≥0 0 = 0≤1 +x≥0⇒x^n≥0 {x} x≥0 (suc n) = begin + 0# ≤⟨ x≥0∧y≥0⇒x*y≥0 x≥0 (x≥0⇒x^n≥0 x≥0 n) ⟩ + x * x ^ n ≈˘⟨ ^-homo-* x 1 n ⟩ + x ^ suc n ∎ + +-- _<_ + +x>0⇒x^n>0 : ∀ {x} → x > 0# → ∀ n → x ^ n > 0# +x>0⇒x^n>0 {x} x>0 0 = x<y⇒0<1 x>0 +x>0⇒x^n>0 {x} x>0 (suc n) = begin-strict + 0# <⟨ x>0∧y>0⇒x*y>0 x>0 (x>0⇒x^n>0 x>0 n) ⟩ + x * x ^ n ≈˘⟨ ^-homo-* x 1 n ⟩ + x ^ suc n ∎ + +---- Preserves size + +-- _≤_ + +x≥1⇒x^n≥1 : ∀ {x} → x ≥ 1# → ∀ n → x ^ n ≥ 1# +x≥1⇒x^n≥1 {x} x≥1 0 = ≤-refl +x≥1⇒x^n≥1 {x} x≥1 (suc n) = begin + 1# ≤⟨ x≥1∧y≥1⇒x*y≥1 x≥1 (x≥1⇒x^n≥1 x≥1 n) ⟩ + x * x ^ n ≈˘⟨ ^-homo-* x 1 n ⟩ + x ^ suc n ∎ + +0≤x≤1⇒x^n≤1 : ∀ {x} → 0# ≤ x → x ≤ 1# → ∀ n → x ^ n ≤ 1# +0≤x≤1⇒x^n≤1 {x} 0≤x x≤1 0 = ≤-refl +0≤x≤1⇒x^n≤1 {x} 0≤x x≤1 (suc n) = begin + x ^ suc n ≈⟨ ^-homo-* x 1 n ⟩ + x * x ^ n ≤⟨ 0≤x≤1∧y≤1⇒x*y≤1 0≤x x≤1 (0≤x≤1⇒x^n≤1 0≤x x≤1 n) ⟩ + 1# ∎ + +-- _<_ + +x>1∧n≢0⇒x^n>1 : ∀ {x} → x > 1# → ∀ n → ⦃ NonZero n ⦄ → x ^ n > 1# +x>1∧n≢0⇒x^n>1 {x} x>1 (suc n) = begin-strict + 1# <⟨ x>1∧y≥1⇒x*y>1 x>1 (x≥1⇒x^n≥1 (<⇒≤ x>1) n) ⟩ + x * x ^ n ≈˘⟨ ^-homo-* x 1 n ⟩ + x ^ suc n ∎ + +0≤x<1∧n≢0⇒x^n<1 : ∀ {x} → 0# ≤ x → x < 1# → ∀ n → ⦃ NonZero n ⦄ → x ^ n < 1# +0≤x<1∧n≢0⇒x^n<1 {x} 0≤x x<1 (suc n) = begin-strict + x ^ suc n ≈⟨ ^-homo-* x 1 n ⟩ + x * x ^ n <⟨ 0≤x<1∧y≤1⇒x*y<1 0≤x x<1 (0≤x≤1⇒x^n≤1 0≤x (<⇒≤ x<1) n) ⟩ + 1# ∎ + +---- Congruences + +-- _≈_ + +n≢0⇒0^n≈0 : ∀ n → ⦃ NonZero n ⦄ → 0# ^ n ≈ 0# +n≢0⇒0^n≈0 (suc n) = begin-equality + 0# ^ suc n ≈⟨ ^-homo-* 0# 1 n ⟩ + 0# * 0# ^ n ≈⟨ zeroˡ (0# ^ n) ⟩ + 0# ∎ + +-- _≤_ + +x≥1⇒^-monoˡ-≤ : ∀ {x} → x ≥ 1# → (x ^_) Preserves ℕ._≤_ ⟶ _≤_ +x≥1⇒^-monoˡ-≤ {x} x≥1 {.0} {n} ℕ.z≤n = x≥1⇒x^n≥1 x≥1 n +x≥1⇒^-monoˡ-≤ {x} x≥1 {.suc m} {.suc n} (ℕ.s≤s m≤n) = begin + x ^ suc m ≈⟨ ^-homo-* x 1 m ⟩ + x * x ^ m ≤⟨ x≥0⇒*-monoˡ-≤ (≤-trans 0≤1 x≥1) (x≥1⇒^-monoˡ-≤ x≥1 m≤n) ⟩ + x * x ^ n ≈˘⟨ ^-homo-* x 1 n ⟩ + x ^ suc n ∎ + +0≤x≤1⇒^-anti-monoˡ-≤ : ∀ {x} → 0# ≤ x → x ≤ 1# → (x ^_) Preserves ℕ._≤_ ⟶ _≥_ +0≤x≤1⇒^-anti-monoˡ-≤ {x} 0≤x x≤1 {.0} {n} ℕ.z≤n = 0≤x≤1⇒x^n≤1 0≤x x≤1 n +0≤x≤1⇒^-anti-monoˡ-≤ {x} 0≤x x≤1 {.suc m} {.suc n} (ℕ.s≤s m≤n) = begin + x ^ suc n ≈⟨ ^-homo-* x 1 n ⟩ + x * x ^ n ≤⟨ x≥0⇒*-monoˡ-≤ 0≤x (0≤x≤1⇒^-anti-monoˡ-≤ 0≤x x≤1 m≤n) ⟩ + x * x ^ m ≈˘⟨ ^-homo-* x 1 m ⟩ + x ^ suc m ∎ + +-- _<_ + +x>1⇒^-monoˡ-< : ∀ {x} → x > 1# → (x ^_) Preserves ℕ._<_ ⟶ _<_ +x>1⇒^-monoˡ-< {x} x>1 {m} {.suc n} (ℕ.s≤s m≤n) = begin-strict + x ^ m ≤⟨ x≥1⇒^-monoˡ-≤ (<⇒≤ x>1) m≤n ⟩ + x ^ n ≈˘⟨ *-identityˡ (x ^ n) ⟩ + 1# * x ^ n <⟨ x>0⇒*-monoʳ-< (x>0⇒x^n>0 (≤-<-trans 0≤1 x>1) n) x>1 ⟩ + x * x ^ n ≈˘⟨ ^-homo-* x 1 n ⟩ + x ^ suc n ∎ + +0<x<1⇒^-anti-monoˡ-< : ∀ {x} → 0# < x → x < 1# → (x ^_) Preserves ℕ._<_ ⟶ _>_ +0<x<1⇒^-anti-monoˡ-< {x} 0<x x<1 {m} {.suc n} (ℕ.s≤s m≤n) = begin-strict + x ^ suc n ≈⟨ ^-homo-* x 1 n ⟩ + x * x ^ n <⟨ x>0⇒*-monoʳ-< (x>0⇒x^n>0 0<x n) x<1 ⟩ + 1# * x ^ n ≈⟨ *-identityˡ (x ^ n) ⟩ + x ^ n ≤⟨ 0≤x≤1⇒^-anti-monoˡ-≤ (<⇒≤ 0<x) (<⇒≤ x<1) m≤n ⟩ + x ^ m ∎ diff --git a/src/Helium/Algebra/Ordered/StrictTotal/Properties/Semigroup.agda b/src/Helium/Algebra/Ordered/StrictTotal/Properties/Semigroup.agda new file mode 100644 index 0000000..17228ac --- /dev/null +++ b/src/Helium/Algebra/Ordered/StrictTotal/Properties/Semigroup.agda @@ -0,0 +1,31 @@ +------------------------------------------------------------------------ +-- Agda Helium +-- +-- Algebraic properties of ordered semigroups +------------------------------------------------------------------------ + +{-# OPTIONS --safe --without-K #-} + +open import Helium.Algebra.Ordered.StrictTotal.Bundles + +module Helium.Algebra.Ordered.StrictTotal.Properties.Semigroup + {ℓ₁ ℓ₂ ℓ₃} + (semigroup : Semigroup ℓ₁ ℓ₂ ℓ₃) + where + +open Semigroup semigroup + renaming + ( trans to <-trans + ; irrefl to <-irrefl + ; asym to <-asym + ) + +open import Helium.Algebra.Ordered.StrictTotal.Properties.Magma magma public + using + ( ∙-mono-<; ∙-monoˡ-<; ∙-monoʳ-< + ; ∙-mono-≤; ∙-monoˡ-≤; ∙-monoʳ-≤ + ; ∙-cancelˡ; ∙-cancelʳ; ∙-cancel + ; ∙-cancelˡ-<; ∙-cancelʳ-<; ∙-cancel-< + ; ∙-cancelˡ-≤; ∙-cancelʳ-≤; ∙-cancel-≤ + ) +open import Helium.Relation.Binary.Properties.StrictTotalOrder strictTotalOrder public |