diff --git a/CHANGELOG.md b/CHANGELOG.md index a6f66aa2f5..d5fd79673b 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -25,6 +25,12 @@ Non-backwards compatible changes significantly faster. However, its reduction behaviour on open terms may have changed. +* 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`. + Minor improvements ------------------ @@ -57,18 +63,23 @@ Deprecated names *ₗ-assoc+comm⇒*ₗ-*ᵣ-assoc ↦ *ₗ-assoc∧comm⇒*ₗ-*ᵣ-assoc ``` -* In `Algebra.Modules.Structures.IsLeftModule`: +* In `Algebra.Module.Structures.IsLeftModule`: ```agda uniqueˡ‿⁻ᴹ ↦ Algebra.Module.Properties.LeftModule.inverseˡ-uniqueᴹ uniqueʳ‿⁻ᴹ ↦ Algebra.Module.Properties.LeftModule.inverseʳ-uniqueᴹ ``` -* In `Algebra.Modules.Structures.IsRightModule`: +* In `Algebra.Module.Structures.IsRightModule`: ```agda uniqueˡ‿⁻ᴹ ↦ Algebra.Module.Properties.RightModule.inverseˡ-uniqueᴹ uniqueʳ‿⁻ᴹ ↦ Algebra.Module.Properties.RightModule.inverseʳ-uniqueᴹ ``` +* In `Algebra.Properties.CancellativeCommutativeSemiring`: + ```agda + *-almostCancelʳ ↦ Algebra.Structures.IsCancellativeCommutativeSemiring.*-cancelʳ-nonZero + ``` + * In `Algebra.Properties.Magma.Divisibility`: ```agda ∣∣-sym ↦ ∥-sym @@ -152,6 +163,24 @@ 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.Construct.Pointwise`: ```agda isNearSemiring : IsNearSemiring _≈_ _+_ _*_ 0# → @@ -181,6 +210,18 @@ Additions to existing modules commutativeRing : CommutativeRing c ℓ → CommutativeRing (a ⊔ c) (a ⊔ ℓ) ``` +* 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.Modules.Properties`: ```agda inverseˡ-uniqueᴹ : x +ᴹ y ≈ 0ᴹ → x ≈ -ᴹ y @@ -232,6 +273,11 @@ Additions to existing modules filter-↭ : ∀ (P? : Pred.Decidable P) → xs ↭ ys → filter P? xs ↭ filter P? ys ``` +* In `Data.Nat.Properties`: + ```agda + *-almostCancelʳ-≡ : AlmostRightCancellative 0 _*_ + ``` + * In `Relation.Binary.Construct.Add.Infimum.Strict`: ```agda <₋-accessible-⊥₋ : Acc _<₋_ ⊥₋ diff --git a/src/Algebra/Consequences/Base.agda b/src/Algebra/Consequences/Base.agda index 102fac3978..4953781a6a 100644 --- a/src/Algebra/Consequences/Base.agda +++ b/src/Algebra/Consequences/Base.agda @@ -12,16 +12,52 @@ module Algebra.Consequences.Base open import Algebra.Core using (Op₁; Op₂) open import Algebra.Definitions - using (Selective; Idempotent; SelfInverse; Involutive) -open import Data.Sum.Base using (_⊎_; reduce) + using (Selective; Idempotent; SelfInverse; Involutive + ; _AlmostLeftCancellative′_; Except_LeftCancellative_ + ; _AlmostRightCancellative′_; Except_RightCancellative_) +open import Data.Sum.Base using (inj₁; inj₂; reduce; [_,_]′) +open import Function.Base using (id; const; flip) open import Relation.Binary.Core using (Rel) 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) + module _ {ℓ} {_•_ : Op₂ A} (_≈_ : Rel A ℓ) where sel⇒idem : Selective _≈_ _•_ → Idempotent _≈_ _•_ sel⇒idem sel x = reduce (sel x x) +module _ {p ℓ} {_•_ : Op₂ A} (_≈_ : Rel A ℓ) + {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}} + module _ {ℓ} {f : Op₁ A} (_≈_ : Rel A ℓ) where reflexive∧selfInverse⇒involutive : Reflexive _≈_ → @@ -29,6 +65,7 @@ module _ {ℓ} {f : Op₁ A} (_≈_ : Rel A ℓ) where Involutive _≈_ f reflexive∧selfInverse⇒involutive refl inv _ = inv refl + ------------------------------------------------------------------------ -- DEPRECATED NAMES ------------------------------------------------------------------------ diff --git a/src/Algebra/Consequences/Setoid.agda b/src/Algebra/Consequences/Setoid.agda index a6c7d252a7..57689ace7e 100644 --- a/src/Algebra/Consequences/Setoid.agda +++ b/src/Algebra/Consequences/Setoid.agda @@ -16,7 +16,7 @@ module Algebra.Consequences.Setoid {a ℓ} (S : Setoid a ℓ) where open Setoid S renaming (Carrier to A) open import Algebra.Core open import Algebra.Definitions _≈_ -open import Data.Sum.Base using (inj₁; inj₂) +open import Data.Sum.Base using (map₂) open import Data.Product.Base using (_,_) open import Function.Base using (_$_; id; _∘_) open import Function.Definitions @@ -100,20 +100,28 @@ module _ {f : Op₁ A} (self : SelfInverse f) where module _ {_∙_ : Op₂ A} (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 @@ -157,21 +165,13 @@ module _ {_∙_ : Op₂ A} (comm : Commutative _∙_) {e : A} where comm∧almostCancelˡ⇒almostCancelʳ : AlmostLeftCancellative e _∙_ → AlmostRightCancellative e _∙_ - comm∧almostCancelˡ⇒almostCancelʳ 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ˡ 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 ------------------------------------------------------------------------ -- Group-like structures diff --git a/src/Algebra/Definitions.agda b/src/Algebra/Definitions.agda index 62528e5b70..d468ce943d 100644 --- a/src/Algebra/Definitions.agda +++ b/src/Algebra/Definitions.agda @@ -16,7 +16,6 @@ {-# OPTIONS --cubical-compatible --safe #-} open import Relation.Binary.Core using (Rel; _Preserves_⟶_; _Preserves₂_⟶_⟶_) -open import Relation.Nullary.Negation.Core using (¬_) module Algebra.Definitions {a ℓ} {A : Set a} -- The underlying set @@ -26,6 +25,7 @@ module Algebra.Definitions open import Algebra.Core using (Op₁; Op₂) open import Data.Product.Base using (_×_; ∃-syntax) open import Data.Sum.Base using (_⊎_) +open import Relation.Unary using (Pred; ∁) ------------------------------------------------------------------------ -- Properties of operations @@ -37,10 +37,10 @@ Congruent₂ : Op₂ A → Set _ Congruent₂ ∙ = ∙ Preserves₂ _≈_ ⟶ _≈_ ⟶ _≈_ LeftCongruent : Op₂ A → Set _ -LeftCongruent _∙_ = ∀ {x} → (x ∙_) Preserves _≈_ ⟶ _≈_ +LeftCongruent _∙_ = ∀ {x} → Congruent₁ (x ∙_) RightCongruent : Op₂ A → Set _ -RightCongruent _∙_ = ∀ {x} → (_∙ x) Preserves _≈_ ⟶ _≈_ +RightCongruent _∙_ = ∀ {x} → Congruent₁ (_∙ x) Associative : Op₂ A → Set _ Associative _∙_ = ∀ x y z → ((x ∙ y) ∙ z) ≈ (x ∙ (y ∙ z)) @@ -140,20 +140,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 2062c33237..0a4dda8fdd 100644 --- a/src/Algebra/Properties/CancellativeCommutativeSemiring.agda +++ b/src/Algebra/Properties/CancellativeCommutativeSemiring.agda @@ -12,29 +12,36 @@ 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 Data.Sum.Base using (_⊎_; [_,_]′; map₂) 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 +open CancellativeCommutativeSemiring R renaming (Carrier to A) -*-almostCancelʳ : AlmostRightCancellative _≈_ 0# _*_ -*-almostCancelʳ = comm∧almostCancelˡ⇒almostCancelʳ *-comm *-cancelˡ-nonZero +private + variable + x y : A -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 -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 +module _ (_≟_ : Decidable _≈_) where + + 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 2.3 + +*-almostCancelʳ = *-cancelʳ-nonZero +{-# WARNING_ON_USAGE *-almostCancelʳ +"Warning: *-almostCancelʳ was deprecated in v2.3. +Please use Algebra.Structures.IsCancellativeCommutativeSemiring.*-cancelʳ-nonZero instead." +#-} diff --git a/src/Data/Integer/Properties.agda b/src/Data/Integer/Properties.agda index 8db99652a0..6d09ae2e06 100644 --- a/src/Data/Integer/Properties.agda +++ b/src/Data/Integer/Properties.agda @@ -44,7 +44,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 5cadc91273..037489d580 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 @@ -50,6 +47,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 @@ -914,10 +916,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ʳ-≡ o m n {{≢-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 943e2eedf0..d04293ae1f 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 @@ -172,9 +171,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 ∘′ ≃⇒≡ @@ -861,14 +860,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ℚᵘ @@ -1096,14 +1095,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 df70346f53..0bbda20f8f 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 @@ -62,6 +61,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 @@ -764,7 +764,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) @@ -792,8 +792,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) ⟨ @@ -805,12 +805,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