diff --git a/CHANGELOG.md b/CHANGELOG.md index f9961d3a1a..b51443d7e0 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -105,6 +105,14 @@ Non-backwards compatible changes their definitions and signatures updated to use `IsMagmaHomomorphism` and `IsMonoidHomomorphism` respectively +* The definitions of `LeftCancellative`/`RightCancellative` in `Algebra.Definitions` + have been altered to make the quantification for each argument explicit. The + definitions of `AlmostLeftCancellative`/`AlmostRightCancellative` have also been + changed to rephrase them in 'positive' logical terms. These definitions have been + propagated through the numeric types `X` in `Data.X.Properties`. As part of this + refactoring, lemmas in `Algebra.Properties.CancellativeCommutativeSemiring` no + longer require a `Decidable _≈_` hypothesis. + Minor improvements ------------------ @@ -165,6 +173,11 @@ Deprecated names ^-monoid-morphism ↦ ^-isMonoidHomomorphism ``` +* In `Algebra.Properties.CancellativeCommutativeSemiring`: + ```agda + *-almostCancelʳ ↦ Algebra.Structures.IsCancellativeCommutativeSemiring.*-cancelʳ-nonZero + ``` + * In `Effect.Monad.Partiality`: ```agda _≟-Kind_ ↦ _≡?-Kind_ @@ -238,6 +251,36 @@ New modules Additions to existing modules ----------------------------- +* In `Algebra.Consequences.Base`: + ```agda + almost⇒exceptˡ : _AlmostLeftCancellative′_ _≈_ P _•_ → + Except_LeftCancellative_ _≈_ P _•_ + almost⇒exceptʳ : _AlmostRightCancellative′_ _≈_ P _•_ → + Except_RightCancellative_ _≈_ P _•_ + except⇒almostˡ : Decidable P → Except_LeftCancellative_ _≈_ P _•_ → + _AlmostLeftCancellative′_ _≈_ P _•_ + except⇒almostʳ : Decidable P → Except_RightCancellative_ _≈_ P _•_ → + _AlmostRightCancellative′_ _≈_ P _•_ + ``` + +* In `Algebra.Consequences.Setoid`: + ```agda + comm∧cancelAtˡ⇒cancelAtʳ : LeftCancellativeAt x _∙_ → RightCancellativeAt x _∙_ + comm∧cancelAtʳ⇒cancelAtˡ : RightCancellativeAt x _∙_ → LeftCancellativeAt x _∙_ + ``` + +* In `Algebra.Definitions`: + ```agda + LeftCancellativeAt : A → Op₂ A → Set _ + RightCancellativeAt : A → Op₂ A → Set _ + _AlmostLeftCancellative′_ : (P : Pred A p) → Op₂ A → Set _ + Provided_LeftCancellative_ : (P : Pred A p) → Op₂ A → Set _ + Except_LeftCancellative_ : (P : Pred A p) → Op₂ A → Set _ + _AlmostRightCancellative′_ : (P : Pred A p) → Op₂ A → Set _ + Provided_RightCancellative_ : (P : Pred A p) → Op₂ A → Set _ + Except_RightCancellative_ : (P : Pred A p) → Op₂ A → Set _ + ``` + * In `Algebra.Properties.KleeneAlgebra`: ```agda ≤-reflexive : _≈_ ⇒ _≤_ @@ -287,6 +330,11 @@ Additions to existing modules product-locate : ∀ ns → product ns ≡ 0 → 0 ∈ ns ``` +* In `Data.Nat.Properties`: + ```agda + *-almostCancelʳ-≡ : AlmostRightCancellative 0 _*_ + ``` + * In `Data.Rational.Properties`: ```agda ↥[i/1]≡i : (i : ℤ) → ↥ (i / 1) ≡ i diff --git a/src/Algebra/Consequences/Base.agda b/src/Algebra/Consequences/Base.agda index 79df2817f8..99a6efa620 100644 --- a/src/Algebra/Consequences/Base.agda +++ b/src/Algebra/Consequences/Base.agda @@ -15,12 +15,20 @@ module Algebra.Consequences.Base open import Algebra.Core using (Op₁; Op₂) open import Algebra.Definitions _≈_ using (Congruent₂; LeftCongruent; RightCongruent - ; Selective; Idempotent; SelfInverse; Involutive) -open import Data.Sum.Base using (reduce) + ; Selective; Idempotent; SelfInverse; Involutive + ; _AlmostLeftCancellative′_; Except_LeftCancellative_ + ; _AlmostRightCancellative′_; Except_RightCancellative_) +open import Data.Sum.Base using (inj₁; inj₂; [_,_]′; reduce) +open import Function.Base using (flip) open import Level using (Level) open import Relation.Binary.Consequences using (mono₂⇒monoˡ; mono₂⇒monoʳ) open import Relation.Binary.Definitions using (Reflexive) +open import Relation.Nullary.Decidable.Core using (yes; no) +open import Relation.Nullary.Negation.Core using (contradiction) +open import Relation.Nullary.Recomputable using (¬-recompute) +open import Relation.Unary using (Pred; Decidable) + private variable @@ -53,6 +61,32 @@ reflexive∧selfInverse⇒involutive : Reflexive _≈_ → SelfInverse f → Involutive f reflexive∧selfInverse⇒involutive refl inv _ = inv refl +module _ {p} {P : Pred A p} where + + almost⇒exceptˡ : _AlmostLeftCancellative′_ P _∙_ → + Except_LeftCancellative_ P _∙_ + almost⇒exceptˡ cancel x y z {{¬px}} = + [ flip contradiction (¬-recompute ¬px) , (λ cancel → cancel y z) ]′ (cancel x) + + almost⇒exceptʳ : _AlmostRightCancellative′_ P _∙_ → + Except_RightCancellative_ P _∙_ + almost⇒exceptʳ cancel x y z {{¬px}} = + [ flip contradiction (¬-recompute ¬px) , (λ cancel → cancel y z) ]′ (cancel x) + +module _ {p} {_∙_ : Op₂ A} (_≈_ : Rel A ℓ) + {P : Pred A p} (dec : Decidable P) where + + except⇒almostˡ : Except_LeftCancellative_ P _∙_ → + _AlmostLeftCancellative′_ P _∙_ + except⇒almostˡ cancel x with dec x + ... | yes px = inj₁ px + ... | no ¬px = inj₂ (λ y z → cancel x y z {{¬px}}) + + except⇒almostʳ : Except_RightCancellative_ P _∙_ → + _AlmostRightCancellative′_ P _∙_ + except⇒almostʳ cancel x with dec x + ... | yes px = inj₁ px + ... | no ¬px = inj₂ λ y z → cancel x y z {{¬px}} ------------------------------------------------------------------------ diff --git a/src/Algebra/Consequences/Setoid.agda b/src/Algebra/Consequences/Setoid.agda index 0062013332..2fa651aaa8 100644 --- a/src/Algebra/Consequences/Setoid.agda +++ b/src/Algebra/Consequences/Setoid.agda @@ -12,7 +12,7 @@ open import Relation.Binary.Bundles using (Setoid) module Algebra.Consequences.Setoid {a ℓ} (S : Setoid a ℓ) where open import Algebra.Core -open import Data.Sum.Base using (inj₁; inj₂) +open import Data.Sum.Base using (inj₁; inj₂; map₂) open import Data.Product.Base using (_,_) open import Function.Base using (_$_; id; _∘_) open import Function.Definitions @@ -116,20 +116,28 @@ module _ (self : SelfInverse f) where module _ (comm : Commutative _∙_) where - comm∧cancelˡ⇒cancelʳ : LeftCancellative _∙_ → RightCancellative _∙_ - comm∧cancelˡ⇒cancelʳ cancelˡ x y z eq = cancelˡ x y z $ begin + comm∧cancelAtˡ⇒cancelAtʳ : ∀ {x} → LeftCancellativeAt x _∙_ → + RightCancellativeAt x _∙_ + comm∧cancelAtˡ⇒cancelAtʳ {x = x} cancel y z eq = cancel y z $ begin x ∙ y ≈⟨ comm x y ⟩ y ∙ x ≈⟨ eq ⟩ z ∙ x ≈⟨ comm z x ⟩ x ∙ z ∎ - comm∧cancelʳ⇒cancelˡ : RightCancellative _∙_ → LeftCancellative _∙_ - comm∧cancelʳ⇒cancelˡ cancelʳ x y z eq = cancelʳ x y z $ begin + comm∧cancelˡ⇒cancelʳ : LeftCancellative _∙_ → RightCancellative _∙_ + comm∧cancelˡ⇒cancelʳ cancel = comm∧cancelAtˡ⇒cancelAtʳ ∘ cancel + + comm∧cancelAtʳ⇒cancelAtˡ : ∀ {x} → RightCancellativeAt x _∙_ → + LeftCancellativeAt x _∙_ + comm∧cancelAtʳ⇒cancelAtˡ {x = x} cancel y z eq = cancel y z $ begin y ∙ x ≈⟨ comm y x ⟩ x ∙ y ≈⟨ eq ⟩ x ∙ z ≈⟨ comm x z ⟩ z ∙ x ∎ + comm∧cancelʳ⇒cancelˡ : RightCancellative _∙_ → LeftCancellative _∙_ + comm∧cancelʳ⇒cancelˡ cancel = comm∧cancelAtʳ⇒cancelAtˡ ∘ cancel + ------------------------------------------------------------------------ -- Monoid-like structures @@ -173,21 +181,13 @@ module _ (comm : Commutative _∙_) where comm∧almostCancelˡ⇒almostCancelʳ : AlmostLeftCancellative e _∙_ → AlmostRightCancellative e _∙_ - comm∧almostCancelˡ⇒almostCancelʳ {e = e} cancelˡ-nonZero x y z x≉e yx≈zx = - cancelˡ-nonZero x y z x≉e $ begin - x ∙ y ≈⟨ comm x y ⟩ - y ∙ x ≈⟨ yx≈zx ⟩ - z ∙ x ≈⟨ comm z x ⟩ - x ∙ z ∎ + comm∧almostCancelˡ⇒almostCancelʳ cancel = + map₂ (comm∧cancelAtˡ⇒cancelAtʳ comm) ∘ cancel comm∧almostCancelʳ⇒almostCancelˡ : AlmostRightCancellative e _∙_ → AlmostLeftCancellative e _∙_ - comm∧almostCancelʳ⇒almostCancelˡ {e = e} cancelʳ-nonZero x y z x≉e xy≈xz = - cancelʳ-nonZero x y z x≉e $ begin - y ∙ x ≈⟨ comm y x ⟩ - x ∙ y ≈⟨ xy≈xz ⟩ - x ∙ z ≈⟨ comm x z ⟩ - z ∙ x ∎ + comm∧almostCancelʳ⇒almostCancelˡ cancel = + map₂ (comm∧cancelAtʳ⇒cancelAtˡ comm) ∘ cancel module _ {_∙_ : Op₂ A} {e : A} where diff --git a/src/Algebra/Definitions.agda b/src/Algebra/Definitions.agda index f4d174e4e4..eca7aa054a 100644 --- a/src/Algebra/Definitions.agda +++ b/src/Algebra/Definitions.agda @@ -15,7 +15,7 @@ {-# OPTIONS --without-K --safe #-} -open import Relation.Binary.Core using (Rel) +open import Relation.Binary.Core using (Rel; _Preserves_⟶_; _Preserves₂_⟶_⟶_) module Algebra.Definitions {a ℓ} {A : Set a} -- The underlying set @@ -28,6 +28,7 @@ open import Data.Sum.Base using (_⊎_) open import Relation.Binary.Definitions using (Monotonic₁; Monotonic₂; module KleeneAlgebra) open import Relation.Nullary.Negation.Core using (¬_) +open import Relation.Unary using (Pred; ∁) ------------------------------------------------------------------------ @@ -148,20 +149,45 @@ SelfInverse f = ∀ {x y} → f x ≈ y → f y ≈ x Involutive : Op₁ A → Set _ Involutive f = ∀ x → f (f x) ≈ x +LeftCancellativeAt : A → Op₂ A → Set _ +LeftCancellativeAt x _•_ = ∀ y z → (x • y) ≈ (x • z) → y ≈ z + LeftCancellative : Op₂ A → Set _ -LeftCancellative _•_ = ∀ x y z → (x • y) ≈ (x • z) → y ≈ z +LeftCancellative _•_ = ∀ x → LeftCancellativeAt x _•_ + +RightCancellativeAt : A → Op₂ A → Set _ +RightCancellativeAt x _•_ = ∀ y z → (y • x) ≈ (z • x) → y ≈ z RightCancellative : Op₂ A → Set _ -RightCancellative _•_ = ∀ x y z → (y • x) ≈ (z • x) → y ≈ z +RightCancellative _•_ = ∀ x → RightCancellativeAt x _•_ Cancellative : Op₂ A → Set _ Cancellative _•_ = (LeftCancellative _•_) × (RightCancellative _•_) +_AlmostLeftCancellative′_ : ∀ {p} (P : Pred A p) → Op₂ A → Set _ + +P AlmostLeftCancellative′ _•_ = ∀ x → P x ⊎ LeftCancellativeAt x _•_ + +Provided_LeftCancellative_ : ∀ {p} (P : Pred A p) → Op₂ A → Set _ +Provided P LeftCancellative _•_ = ∀ x y z → .{{P x}} → (x • y) ≈ (x • z) → y ≈ z + +Except_LeftCancellative_ : ∀ {p} (P : Pred A p) → Op₂ A → Set _ +Except P LeftCancellative _•_ = Provided (∁ P) LeftCancellative _•_ + AlmostLeftCancellative : A → Op₂ A → Set _ -AlmostLeftCancellative e _•_ = ∀ x y z → ¬ x ≈ e → (x • y) ≈ (x • z) → y ≈ z +AlmostLeftCancellative e = (_≈ e) AlmostLeftCancellative′_ + +_AlmostRightCancellative′_ : ∀ {p} (P : Pred A p) → Op₂ A → Set _ +P AlmostRightCancellative′ _•_ = ∀ x → P x ⊎ RightCancellativeAt x _•_ + +Provided_RightCancellative_ : ∀ {p} (P : Pred A p) → Op₂ A → Set _ +Provided P RightCancellative _•_ = ∀ x y z → .{{P x}} → (y • x) ≈ (z • x) → y ≈ z + +Except_RightCancellative_ : ∀ {p} (P : Pred A p) → Op₂ A → Set _ +Except_RightCancellative_ P = Provided (∁ P) RightCancellative_ AlmostRightCancellative : A → Op₂ A → Set _ -AlmostRightCancellative e _•_ = ∀ x y z → ¬ x ≈ e → (y • x) ≈ (z • x) → y ≈ z +AlmostRightCancellative e = (_≈ e) AlmostRightCancellative′_ AlmostCancellative : A → Op₂ A → Set _ AlmostCancellative e _•_ = AlmostLeftCancellative e _•_ × AlmostRightCancellative e _•_ diff --git a/src/Algebra/Properties/CancellativeCommutativeSemiring.agda b/src/Algebra/Properties/CancellativeCommutativeSemiring.agda index c539aaf3db..39f15136b8 100644 --- a/src/Algebra/Properties/CancellativeCommutativeSemiring.agda +++ b/src/Algebra/Properties/CancellativeCommutativeSemiring.agda @@ -12,29 +12,33 @@ module Algebra.Properties.CancellativeCommutativeSemiring {a ℓ} (R : CancellativeCommutativeSemiring a ℓ) where -open import Algebra.Definitions using (AlmostRightCancellative) -open import Data.Sum.Base using (_⊎_; inj₁; inj₂) -open import Relation.Binary.Definitions using (Decidable) -open import Relation.Nullary.Decidable using (yes; no) -open import Relation.Nullary.Negation using (contradiction) - -open CancellativeCommutativeSemiring R -open import Algebra.Consequences.Setoid setoid -open import Relation.Binary.Reasoning.Setoid setoid - -*-almostCancelʳ : AlmostRightCancellative _≈_ 0# _*_ -*-almostCancelʳ = comm∧almostCancelˡ⇒almostCancelʳ *-comm *-cancelˡ-nonZero - -xy≈0⇒x≈0∨y≈0 : Decidable _≈_ → ∀ {x y} → x * y ≈ 0# → x ≈ 0# ⊎ y ≈ 0# -xy≈0⇒x≈0∨y≈0 _≈?_ {x} {y} xy≈0 with x ≈? 0# | y ≈? 0# -... | yes x≈0 | _ = inj₁ x≈0 -... | no _ | yes y≈0 = inj₂ y≈0 -... | no x≉0 | no y≉0 = contradiction y≈0 y≉0 - where - xy≈x*0 = trans xy≈0 (sym (zeroʳ x)) - y≈0 = *-cancelˡ-nonZero _ y 0# x≉0 xy≈x*0 +open import Data.Sum.Base using (_⊎_; [_,_]′; map₂) + +open CancellativeCommutativeSemiring R renaming (Carrier to A) + +private + variable + x y : A + + +xy≈0⇒x≈0∨y≈0 : x * y ≈ 0# → x ≈ 0# ⊎ y ≈ 0# +xy≈0⇒x≈0∨y≈0 {x} {y} xy≈0 = + map₂ (λ cancel → cancel _ _ (trans xy≈0 (sym (zeroʳ x)))) (*-cancelˡ-nonZero x) + +x≉0∧y≉0⇒xy≉0 : x ≉ 0# → y ≉ 0# → x * y ≉ 0# +x≉0∧y≉0⇒xy≉0 x≉0 y≉0 xy≈0 = [ x≉0 , y≉0 ]′ (xy≈0⇒x≈0∨y≈0 xy≈0) + + +------------------------------------------------------------------------ +-- DEPRECATED NAMES +------------------------------------------------------------------------ +-- Please use the new names as continuing support for the old names is +-- not guaranteed. + +-- Version 3.0 -x≉0∧y≉0⇒xy≉0 : Decidable _≈_ → ∀ {x y} → x ≉ 0# → y ≉ 0# → x * y ≉ 0# -x≉0∧y≉0⇒xy≉0 _≈?_ x≉0 y≉0 xy≈0 with xy≈0⇒x≈0∨y≈0 _≈?_ xy≈0 -... | inj₁ x≈0 = x≉0 x≈0 -... | inj₂ y≈0 = y≉0 y≈0 +*-almostCancelʳ = *-cancelʳ-nonZero +{-# WARNING_ON_USAGE *-almostCancelʳ +"Warning: *-almostCancelʳ was deprecated in v3.0. +Please use Algebra.Structures.IsCancellativeCommutativeSemiring.*-cancelʳ-nonZero instead." +#-} diff --git a/src/Data/Integer/Properties.agda b/src/Data/Integer/Properties.agda index a8c0291e20..0977988ced 100644 --- a/src/Data/Integer/Properties.agda +++ b/src/Data/Integer/Properties.agda @@ -45,7 +45,7 @@ open import Relation.Nullary.Negation.Core using (¬_; contradiction) import Relation.Nullary.Decidable as Dec open import Algebra.Definitions {A = ℤ} _≡_ -open import Algebra.Consequences.Propositional +open import Algebra.Consequences.Propositional {A = ℤ} using (comm∧idˡ⇒idʳ; comm∧invˡ⇒invʳ; comm∧zeˡ⇒zeʳ; comm∧distrʳ⇒distrˡ) open import Algebra.Structures {A = ℤ} _≡_ module ℤtoℕ = Morphism.Definitions ℤ ℕ _≡_ diff --git a/src/Data/Nat/Properties.agda b/src/Data/Nat/Properties.agda index 5b8827897c..c683fbd0c0 100644 --- a/src/Data/Nat/Properties.agda +++ b/src/Data/Nat/Properties.agda @@ -17,9 +17,6 @@ open import Algebra.Bundles ; Semiring; CommutativeSemiring; CommutativeSemiringWithoutOne) open import Algebra.Definitions.RawMagma using (_,_) open import Algebra.Morphism -open import Algebra.Consequences.Propositional - using (comm∧cancelˡ⇒cancelʳ; comm∧distrʳ⇒distrˡ; comm∧distrˡ⇒distrʳ - ; comm⇒sym[distribˡ]) open import Algebra.Construct.NaturalChoice.Base using (MinOperator; MaxOperator) import Algebra.Construct.NaturalChoice.MinMaxOp as MinMaxOp @@ -54,6 +51,11 @@ open import Relation.Nullary.Negation.Core using (¬_; contradiction) open import Relation.Nullary.Reflects using (fromEquivalence; Reflects; invert) +open import Algebra.Consequences.Propositional {A = ℕ} + using ( comm∧cancelˡ⇒cancelʳ + ; comm∧distrʳ⇒distrˡ; comm∧distrˡ⇒distrʳ + ; comm⇒sym[distribˡ] + ; almost⇒exceptʳ) open import Algebra.Definitions {A = ℕ} _≡_ hiding (LeftCancellative; RightCancellative; Cancellative) open import Algebra.Definitions @@ -930,10 +932,16 @@ m+n≮m m n = subst (_≮ m) (+-comm n m) (m+n≮n n m) ------------------------------------------------------------------------ -- Other properties of _*_ and _≡_ +*-almostCancelʳ-≡ : AlmostRightCancellative 0 _*_ +*-almostCancelʳ-≡ zero = inj₁ refl +*-almostCancelʳ-≡ o@(suc _) = inj₂ lemma + module *-AlmostRightCancellative where + lemma : RightCancellativeAt o _*_ + lemma zero zero _ = refl + lemma (suc m) (suc n) eq = cong suc (lemma m n (+-cancelˡ-≡ o (m * o) (n * o) eq)) + *-cancelʳ-≡ : ∀ m n o .{{_ : NonZero o}} → m * o ≡ n * o → m ≡ n -*-cancelʳ-≡ zero zero (suc o) eq = refl -*-cancelʳ-≡ (suc m) (suc n) (suc o) eq = - cong suc (*-cancelʳ-≡ m n (suc o) (+-cancelˡ-≡ (suc o) (m * suc o) (n * suc o) eq)) +*-cancelʳ-≡ m n o = almost⇒exceptʳ *-almostCancelʳ-≡ _ _ _ {{≢-nonZero⁻¹ _}} *-cancelˡ-≡ : ∀ m n o .{{_ : NonZero o}} → o * m ≡ o * n → m ≡ n *-cancelˡ-≡ m n o rewrite *-comm o m | *-comm o n = *-cancelʳ-≡ m n o diff --git a/src/Data/Rational/Properties.agda b/src/Data/Rational/Properties.agda index c2d1428974..c96442ccff 100644 --- a/src/Data/Rational/Properties.agda +++ b/src/Data/Rational/Properties.agda @@ -16,7 +16,6 @@ open import Algebra.Construct.NaturalChoice.Base using (MinOperator; MaxOperator) import Algebra.Construct.NaturalChoice.MinMaxOp as MinMaxOp import Algebra.Lattice.Construct.NaturalChoice.MinMaxOp as LatticeMinMaxOp -open import Algebra.Consequences.Propositional open import Algebra.Morphism open import Algebra.Bundles import Algebra.Morphism.MagmaMonomorphism as MagmaMonomorphisms @@ -173,9 +172,9 @@ drop-*≡* (*≡* eq) = eq ℤ.∣ n₁ ∣ ℕ.* suc d₂ ∎) helper : mkℚ n₁ d₁ c₁ ≡ mkℚ n₂ d₂ c₂ - helper with ∣-antisym 1+d₁∣1+d₂ 1+d₂∣1+d₁ - ... | refl with ℤ.*-cancelʳ-≡ n₁ n₂ (+ suc d₁) eq - ... | refl = refl + helper with refl ← ∣-antisym 1+d₁∣1+d₂ 1+d₂∣1+d₁ + with refl ← ℤ.*-cancelʳ-≡ n₁ n₂ (+ suc d₁) eq + = refl ≃-sym : Symmetric _≃_ ≃-sym = ≡⇒≃ ∘′ sym ∘′ ≃⇒≡ @@ -914,14 +913,14 @@ toℚᵘ-homo-+ p@record{} q@record{} with +-nf p q ℤ.≡? 0ℤ eq : ↥ (p + q) ≡ 0ℤ eq rewrite eq2 = cong ↥_ (0/n≡0 (↧ₙ p ℕ.* ↧ₙ q)) -... | no nf[p,q]≢0 = *≡* (ℤ.*-cancelʳ-≡ _ _ (+-nf p q) {{ℤ.≢-nonZero nf[p,q]≢0}} $ begin +... | no nf[p,q]≢0 = *≡* (ℤ.*-cancelʳ-≡ _ _ (+-nf p q) {{ℤ.≢-nonZero nf[p,q]≢0}} (begin (↥ᵘ (toℚᵘ (p + q))) ℤ.* ↧+ᵘ p q ℤ.* +-nf p q ≡⟨ cong (λ v → v ℤ.* ↧+ᵘ p q ℤ.* +-nf p q) (↥ᵘ-toℚᵘ (p + q)) ⟩ ↥ (p + q) ℤ.* ↧+ᵘ p q ℤ.* +-nf p q ≡⟨ xy∙z≈xz∙y (↥ (p + q)) _ _ ⟩ ↥ (p + q) ℤ.* +-nf p q ℤ.* ↧+ᵘ p q ≡⟨ cong (ℤ._* ↧+ᵘ p q) (↥-+ p q) ⟩ ↥+ᵘ p q ℤ.* ↧+ᵘ p q ≡⟨ cong (↥+ᵘ p q ℤ.*_) (sym (↧-+ p q)) ⟩ ↥+ᵘ p q ℤ.* (↧ (p + q) ℤ.* +-nf p q) ≡⟨ x∙yz≈xy∙z (↥+ᵘ p q) _ _ ⟩ ↥+ᵘ p q ℤ.* ↧ (p + q) ℤ.* +-nf p q ≡⟨ cong (λ v → ↥+ᵘ p q ℤ.* v ℤ.* +-nf p q) (↧ᵘ-toℚᵘ (p + q)) ⟨ - ↥+ᵘ p q ℤ.* ↧ᵘ (toℚᵘ (p + q)) ℤ.* +-nf p q ∎) + ↥+ᵘ p q ℤ.* ↧ᵘ (toℚᵘ (p + q)) ℤ.* +-nf p q ∎)) where open ≡-Reasoning; open CommSemigroupProperties ℤ.*-commutativeSemigroup toℚᵘ-isMagmaHomomorphism-+ : IsMagmaHomomorphism +-rawMagma ℚᵘ.+-rawMagma toℚᵘ @@ -1149,14 +1148,14 @@ toℚᵘ-homo-* p@record{} q@record{} with *-nf p q ℤ.≡? 0ℤ eq : ↥ (p * q) ≡ 0ℤ eq rewrite eq2 = cong ↥_ (0/n≡0 (↧ₙ p ℕ.* ↧ₙ q)) -... | no nf[p,q]≢0 = *≡* (ℤ.*-cancelʳ-≡ _ _ (*-nf p q) {{ℤ.≢-nonZero nf[p,q]≢0}} $ begin +... | no nf[p,q]≢0 = *≡* (ℤ.*-cancelʳ-≡ _ _ (*-nf p q) {{ℤ.≢-nonZero nf[p,q]≢0}} (begin ↥ᵘ (toℚᵘ (p * q)) ℤ.* (↧ p ℤ.* ↧ q) ℤ.* *-nf p q ≡⟨ cong (λ v → v ℤ.* (↧ p ℤ.* ↧ q) ℤ.* *-nf p q) (↥ᵘ-toℚᵘ (p * q)) ⟩ ↥ (p * q) ℤ.* (↧ p ℤ.* ↧ q) ℤ.* *-nf p q ≡⟨ xy∙z≈xz∙y (↥ (p * q)) _ _ ⟩ ↥ (p * q) ℤ.* *-nf p q ℤ.* (↧ p ℤ.* ↧ q) ≡⟨ cong (ℤ._* (↧ p ℤ.* ↧ q)) (↥-* p q) ⟩ (↥ p ℤ.* ↥ q) ℤ.* (↧ p ℤ.* ↧ q) ≡⟨ cong ((↥ p ℤ.* ↥ q) ℤ.*_) (sym (↧-* p q)) ⟩ (↥ p ℤ.* ↥ q) ℤ.* (↧ (p * q) ℤ.* *-nf p q) ≡⟨ x∙yz≈xy∙z (↥ p ℤ.* ↥ q) _ _ ⟩ (↥ p ℤ.* ↥ q) ℤ.* ↧ (p * q) ℤ.* *-nf p q ≡⟨ cong (λ v → (↥ p ℤ.* ↥ q) ℤ.* v ℤ.* *-nf p q) (↧ᵘ-toℚᵘ (p * q)) ⟨ - (↥ p ℤ.* ↥ q) ℤ.* ↧ᵘ (toℚᵘ (p * q)) ℤ.* *-nf p q ∎) + (↥ p ℤ.* ↥ q) ℤ.* ↧ᵘ (toℚᵘ (p * q)) ℤ.* *-nf p q ∎)) where open ≡-Reasoning; open CommSemigroupProperties ℤ.*-commutativeSemigroup toℚᵘ-homo-1/ : ∀ p .{{_ : NonZero p}} → toℚᵘ (1/ p) ℚᵘ.≃ (ℚᵘ.1/ toℚᵘ p) diff --git a/src/Data/Rational/Unnormalised/Properties.agda b/src/Data/Rational/Unnormalised/Properties.agda index d8313d985d..b94abc461a 100644 --- a/src/Data/Rational/Unnormalised/Properties.agda +++ b/src/Data/Rational/Unnormalised/Properties.agda @@ -11,18 +11,17 @@ module Data.Rational.Unnormalised.Properties where open import Algebra.Definitions open import Algebra.Structures - using (IsMagma; IsSemigroup; IsBand; IsSelectiveMagma; IsMonoid - ; IsCommutativeMonoid; IsGroup; IsAbelianGroup; IsRing - ; IsCommutativeRing) + using (IsMagma; IsSemigroup; IsBand; IsSelectiveMagma + ; IsMonoid; IsCommutativeMonoid; IsGroup; IsAbelianGroup + ; IsRing; IsCommutativeRing) open import Algebra.Bundles open import Algebra.Apartness using (IsHeytingCommutativeRing; IsHeytingField ; HeytingCommutativeRing; HeytingField) open import Algebra.Lattice - using (IsLattice; IsDistributiveLattice; IsSemilattice - ; Semilattice; Lattice; DistributiveLattice; RawLattice) + using (IsSemilattice; IsLattice; IsDistributiveLattice + ; RawLattice; Semilattice; Lattice; DistributiveLattice) import Algebra.Consequences.Setoid as Consequences -open import Algebra.Consequences.Propositional open import Algebra.Construct.NaturalChoice.Base using (MaxOperator; MinOperator) import Algebra.Construct.NaturalChoice.MinMaxOp as MinMaxOp @@ -63,6 +62,7 @@ import Relation.Binary.Properties.Poset as PosetProperties import Relation.Binary.Reasoning.Setoid as ≈-Reasoning open import Relation.Binary.Reasoning.Syntax +open import Algebra.Consequences.Propositional {A = ℚᵘ} open import Algebra.Properties.CommutativeSemigroup ℤ.*-commutativeSemigroup private @@ -780,7 +780,7 @@ neg⇒nonZero (mkℚᵘ (-[1+ _ ]) _) = _ +-identityˡ p = ≃-reflexive (+-identityˡ-≡ p) +-identityʳ-≡ : RightIdentity _≡_ 0ℚᵘ _+_ -+-identityʳ-≡ = comm∧idˡ⇒idʳ +-comm-≡ {e = 0ℚᵘ} +-identityˡ-≡ ++-identityʳ-≡ = comm∧idˡ⇒idʳ +-comm-≡ +-identityˡ-≡ +-identityʳ : RightIdentity _≃_ 0ℚᵘ _+_ +-identityʳ p = ≃-reflexive (+-identityʳ-≡ p) @@ -808,8 +808,8 @@ neg⇒nonZero (mkℚᵘ (-[1+ _ ]) _) = _ +-inverse : Inverse _≃_ 0ℚᵘ -_ _+_ +-inverse = +-inverseˡ , +-inverseʳ -+-cancelˡ : ∀ {r p q} → r + p ≃ r + q → p ≃ q -+-cancelˡ {r} {p} {q} r+p≃r+q = begin-equality ++-cancelˡ : LeftCancellative _≃_ _+_ ++-cancelˡ r p q r+p≃r+q = begin-equality p ≃⟨ +-identityʳ p ⟨ p + 0ℚᵘ ≃⟨ +-congʳ p (+-inverseʳ r) ⟨ p + (r - r) ≃⟨ +-assoc p r (- r) ⟨ @@ -821,12 +821,8 @@ neg⇒nonZero (mkℚᵘ (-[1+ _ ]) _) = _ q + 0ℚᵘ ≃⟨ +-identityʳ q ⟩ q ∎ where open ≤-Reasoning -+-cancelʳ : ∀ {r p q} → p + r ≃ q + r → p ≃ q -+-cancelʳ {r} {p} {q} p+r≃q+r = +-cancelˡ {r} $ begin-equality - r + p ≃⟨ +-comm r p ⟩ - p + r ≃⟨ p+r≃q+r ⟩ - q + r ≃⟨ +-comm q r ⟩ - r + q ∎ where open ≤-Reasoning ++-cancelʳ : RightCancellative _≃_ _+_ ++-cancelʳ = Consequences.comm∧cancelˡ⇒cancelʳ ≃-setoid +-comm +-cancelˡ p+p≃0⇒p≃0 : ∀ p → p + p ≃ 0ℚᵘ → p ≃ 0ℚᵘ p+p≃0⇒p≃0 (mkℚᵘ ℤ.+0 _) (*≡* _) = *≡* refl