From 302638eb4a59a4fc2dbd3c5ff63c64dbf4f7c7be Mon Sep 17 00:00:00 2001 From: = Date: Wed, 15 Jan 2020 11:50:15 +0800 Subject: [PATCH 1/3] Rename `Algebra.FunctionProperties.Consequences` to `Algebra.Consequences` --- CHANGELOG.md | 18 +- src/Algebra/Consequences/Base.agda | 22 ++ src/Algebra/Consequences/Propositional.agda | 106 ++++++++++ src/Algebra/Consequences/Setoid.agda | 197 ++++++++++++++++++ .../FunctionProperties/Consequences.agda | 188 +---------------- .../FunctionProperties/Consequences/Core.agda | 17 +- .../Consequences/Propositional.agda | 101 +-------- src/Algebra/Properties/BooleanAlgebra.agda | 2 +- src/Algebra/Structures.agda | 2 +- src/Data/Nat/Properties.agda | 2 +- 10 files changed, 363 insertions(+), 292 deletions(-) create mode 100644 src/Algebra/Consequences/Base.agda create mode 100644 src/Algebra/Consequences/Propositional.agda create mode 100644 src/Algebra/Consequences/Setoid.agda diff --git a/CHANGELOG.md b/CHANGELOG.md index 800fe707bd..5cd89d44d5 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -185,6 +185,22 @@ Non-backwards compatible changes * In `Codata.Colist`, replaced all the uses of `Data.BoundedVec` with the more up to date `Data.Vec.Bounded`. +Deprecated modules +------------------ + +The following modules have been renamed as part of a drive to improve +consistency across the library. The deprecated modules still exist and +therefore all existing code should still work, however use of the new names +is encouraged. Automated warnings are attached to deprecated modules to +discourage their use. + +* In `Algebra`: + ``` + Algebra.FunctionProperties.Consequences.Core ↦ Algebra.Consequences.Base + Algebra.FunctionProperties.Consequences.Propositional ↦ Algebra.Consequences.Propositional + Algebra.FunctionProperties.Consequences ↦ Algebra.Conseqeunces.Setoid + ``` + Deprecated names ---------------- @@ -675,4 +691,4 @@ Version 2.6.1 changes * Added new definitions in `Relation.Binary.Core`: ```agda DecidableEquality A = Decidable {A = A} _≡_ - ``` \ No newline at end of file + ``` diff --git a/src/Algebra/Consequences/Base.agda b/src/Algebra/Consequences/Base.agda new file mode 100644 index 0000000000..914aaf2cec --- /dev/null +++ b/src/Algebra/Consequences/Base.agda @@ -0,0 +1,22 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Lemmas relating algebraic definitions (such as associativity and +-- commutativity) that don't the equality relation to be a setoid. +------------------------------------------------------------------------ + +{-# OPTIONS --without-K --safe #-} + +module Algebra.Consequences.Base + {a} {A : Set a} where + +open import Algebra.Core +open import Algebra.Definitions +open import Data.Sum.Base +open import Relation.Binary.Core + +sel⇒idem : ∀ {ℓ} {_•_ : Op₂ A} (_≈_ : Rel A ℓ) → + Selective _≈_ _•_ → Idempotent _≈_ _•_ +sel⇒idem _ sel x with sel x x +... | inj₁ x•x≈x = x•x≈x +... | inj₂ x•x≈x = x•x≈x diff --git a/src/Algebra/Consequences/Propositional.agda b/src/Algebra/Consequences/Propositional.agda new file mode 100644 index 0000000000..a353dc5bfc --- /dev/null +++ b/src/Algebra/Consequences/Propositional.agda @@ -0,0 +1,106 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Relations between properties of functions, such as associativity and +-- commutativity (specialised to propositional equality) +------------------------------------------------------------------------ + +{-# OPTIONS --without-K --safe #-} + +module Algebra.Consequences.Propositional + {a} {A : Set a} where + +open import Data.Sum using (inj₁; inj₂) +open import Relation.Binary using (Rel; Setoid; Symmetric; Total) +open import Relation.Binary.PropositionalEquality +open import Relation.Unary using (Pred) + +open import Algebra.Core +open import Algebra.Definitions {A = A} _≡_ +import Algebra.Consequences.Setoid (setoid A) as Base + +------------------------------------------------------------------------ +-- Re-export all proofs that don't require congruence or substitutivity + +open Base public + hiding + ( assoc+distribʳ+idʳ+invʳ⇒zeˡ + ; assoc+distribˡ+idʳ+invʳ⇒zeʳ + ; assoc+id+invʳ⇒invˡ-unique + ; assoc+id+invˡ⇒invʳ-unique + ; comm+distrˡ⇒distrʳ + ; comm+distrʳ⇒distrˡ + ; comm⇒sym[distribˡ] + ; subst+comm⇒sym + ; wlog + ; sel⇒idem + ) + +------------------------------------------------------------------------ +-- Group-like structures + +module _ {_•_ _⁻¹ ε} where + + assoc+id+invʳ⇒invˡ-unique : Associative _•_ → Identity ε _•_ → + RightInverse ε _⁻¹ _•_ → + ∀ x y → (x • y) ≡ ε → x ≡ (y ⁻¹) + assoc+id+invʳ⇒invˡ-unique = Base.assoc+id+invʳ⇒invˡ-unique (cong₂ _) + + assoc+id+invˡ⇒invʳ-unique : Associative _•_ → Identity ε _•_ → + LeftInverse ε _⁻¹ _•_ → + ∀ x y → (x • y) ≡ ε → y ≡ (x ⁻¹) + assoc+id+invˡ⇒invʳ-unique = Base.assoc+id+invˡ⇒invʳ-unique (cong₂ _) + +------------------------------------------------------------------------ +-- Ring-like structures + +module _ {_+_ _*_ -_ 0#} where + + assoc+distribʳ+idʳ+invʳ⇒zeˡ : Associative _+_ → _*_ DistributesOverʳ _+_ → + RightIdentity 0# _+_ → RightInverse 0# -_ _+_ → + LeftZero 0# _*_ + assoc+distribʳ+idʳ+invʳ⇒zeˡ = + Base.assoc+distribʳ+idʳ+invʳ⇒zeˡ (cong₂ _+_) (cong₂ _*_) + + assoc+distribˡ+idʳ+invʳ⇒zeʳ : Associative _+_ → _*_ DistributesOverˡ _+_ → + RightIdentity 0# _+_ → RightInverse 0# -_ _+_ → + RightZero 0# _*_ + assoc+distribˡ+idʳ+invʳ⇒zeʳ = + Base.assoc+distribˡ+idʳ+invʳ⇒zeʳ (cong₂ _+_) (cong₂ _*_) + +------------------------------------------------------------------------ +-- Bisemigroup-like structures + +module _ {_•_ _◦_ : Op₂ A} (•-comm : Commutative _•_) where + + comm+distrˡ⇒distrʳ : _•_ DistributesOverˡ _◦_ → _•_ DistributesOverʳ _◦_ + comm+distrˡ⇒distrʳ = Base.comm+distrˡ⇒distrʳ (cong₂ _) •-comm + + comm+distrʳ⇒distrˡ : _•_ DistributesOverʳ _◦_ → _•_ DistributesOverˡ _◦_ + comm+distrʳ⇒distrˡ = Base.comm+distrʳ⇒distrˡ (cong₂ _) •-comm + + comm⇒sym[distribˡ] : ∀ x → Symmetric (λ y z → (x ◦ (y • z)) ≡ ((x ◦ y) • (x ◦ z))) + comm⇒sym[distribˡ] = Base.comm⇒sym[distribˡ] (cong₂ _◦_) •-comm + +------------------------------------------------------------------------ +-- Selectivity + +module _ {_•_ : Op₂ A} where + + sel⇒idem : Selective _•_ → Idempotent _•_ + sel⇒idem = Base.sel⇒idem _≡_ + +------------------------------------------------------------------------ +-- Without Loss of Generality + +module _ {p} {P : Pred A p} where + + subst+comm⇒sym : ∀ {f} (f-comm : Commutative f) → + Symmetric (λ a b → P (f a b)) + subst+comm⇒sym = Base.subst+comm⇒sym {P = P} subst + + wlog : ∀ {f} (f-comm : Commutative f) → + ∀ {r} {_R_ : Rel _ r} → Total _R_ → + (∀ a b → a R b → P (f a b)) → + ∀ a b → P (f a b) + wlog = Base.wlog {P = P} subst diff --git a/src/Algebra/Consequences/Setoid.agda b/src/Algebra/Consequences/Setoid.agda new file mode 100644 index 0000000000..176e6dc9a4 --- /dev/null +++ b/src/Algebra/Consequences/Setoid.agda @@ -0,0 +1,197 @@ +------------------------------------------------------------------------ +-- The Agda standard library +-- +-- Relations between properties of functions, such as associativity and +-- commutativity, when the underlying relation is a setoid +------------------------------------------------------------------------ + +{-# OPTIONS --without-K --safe #-} + +open import Relation.Binary using (Rel; Setoid; Substitutive; Symmetric; Total) + +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 using (inj₁; inj₂) +open import Data.Product using (_,_) +import Relation.Binary.Consequences as Bin +open import Relation.Binary.Reasoning.Setoid S +open import Relation.Unary using (Pred) + +------------------------------------------------------------------------ +-- Re-exports + +-- Export base lemmas that don't require the setoidd + +open import Algebra.Consequences.Base public + +------------------------------------------------------------------------ +-- Magma-like structures + +module _ {_•_ : Op₂ A} (comm : Commutative _•_) where + + comm+cancelˡ⇒cancelʳ : LeftCancellative _•_ → RightCancellative _•_ + comm+cancelˡ⇒cancelʳ cancelˡ {x} y z eq = cancelˡ x (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ʳ y z (begin + y • x ≈⟨ comm y x ⟩ + x • y ≈⟨ eq ⟩ + x • z ≈⟨ comm x z ⟩ + z • x ∎) + +------------------------------------------------------------------------ +-- Monoid-like structures + +module _ {_•_ : Op₂ A} (comm : Commutative _•_) {e : A} where + + comm+idˡ⇒idʳ : LeftIdentity e _•_ → RightIdentity e _•_ + comm+idˡ⇒idʳ idˡ x = begin + x • e ≈⟨ comm x e ⟩ + e • x ≈⟨ idˡ x ⟩ + x ∎ + + comm+idʳ⇒idˡ : RightIdentity e _•_ → LeftIdentity e _•_ + comm+idʳ⇒idˡ idʳ x = begin + e • x ≈⟨ comm e x ⟩ + x • e ≈⟨ idʳ x ⟩ + x ∎ + + comm+zeˡ⇒zeʳ : LeftZero e _•_ → RightZero e _•_ + comm+zeˡ⇒zeʳ zeˡ x = begin + x • e ≈⟨ comm x e ⟩ + e • x ≈⟨ zeˡ x ⟩ + e ∎ + + comm+zeʳ⇒zeˡ : RightZero e _•_ → LeftZero e _•_ + comm+zeʳ⇒zeˡ zeʳ x = begin + e • x ≈⟨ comm e x ⟩ + x • e ≈⟨ zeʳ x ⟩ + e ∎ + +------------------------------------------------------------------------ +-- Group-like structures + +module _ {_•_ : Op₂ A} {_⁻¹ : Op₁ A} {e} (comm : Commutative _•_) where + + comm+invˡ⇒invʳ : LeftInverse e _⁻¹ _•_ → RightInverse e _⁻¹ _•_ + comm+invˡ⇒invʳ invˡ x = begin + x • (x ⁻¹) ≈⟨ comm x (x ⁻¹) ⟩ + (x ⁻¹) • x ≈⟨ invˡ x ⟩ + e ∎ + + comm+invʳ⇒invˡ : RightInverse e _⁻¹ _•_ → LeftInverse e _⁻¹ _•_ + comm+invʳ⇒invˡ invʳ x = begin + (x ⁻¹) • x ≈⟨ comm (x ⁻¹) x ⟩ + x • (x ⁻¹) ≈⟨ invʳ x ⟩ + e ∎ + +module _ {_•_ : Op₂ A} {_⁻¹ : Op₁ A} {e} (cong : Congruent₂ _•_) where + + assoc+id+invʳ⇒invˡ-unique : Associative _•_ → + Identity e _•_ → RightInverse e _⁻¹ _•_ → + ∀ x y → (x • y) ≈ e → x ≈ (y ⁻¹) + assoc+id+invʳ⇒invˡ-unique assoc (idˡ , idʳ) invʳ x y eq = begin + x ≈⟨ sym (idʳ x) ⟩ + x • e ≈⟨ cong refl (sym (invʳ y)) ⟩ + x • (y • (y ⁻¹)) ≈⟨ sym (assoc x y (y ⁻¹)) ⟩ + (x • y) • (y ⁻¹) ≈⟨ cong eq refl ⟩ + e • (y ⁻¹) ≈⟨ idˡ (y ⁻¹) ⟩ + y ⁻¹ ∎ + + assoc+id+invˡ⇒invʳ-unique : Associative _•_ → + Identity e _•_ → LeftInverse e _⁻¹ _•_ → + ∀ x y → (x • y) ≈ e → y ≈ (x ⁻¹) + assoc+id+invˡ⇒invʳ-unique assoc (idˡ , idʳ) invˡ x y eq = begin + y ≈⟨ sym (idˡ y) ⟩ + e • y ≈⟨ cong (sym (invˡ x)) refl ⟩ + ((x ⁻¹) • x) • y ≈⟨ assoc (x ⁻¹) x y ⟩ + (x ⁻¹) • (x • y) ≈⟨ cong refl eq ⟩ + (x ⁻¹) • e ≈⟨ idʳ (x ⁻¹) ⟩ + x ⁻¹ ∎ + +---------------------------------------------------------------------- +-- Bisemigroup-like structures + +module _ {_•_ _◦_ : Op₂ A} + (◦-cong : Congruent₂ _◦_) + (•-comm : Commutative _•_) + where + + comm+distrˡ⇒distrʳ : _•_ DistributesOverˡ _◦_ → _•_ DistributesOverʳ _◦_ + comm+distrˡ⇒distrʳ distrˡ x y z = begin + (y ◦ z) • x ≈⟨ •-comm (y ◦ z) x ⟩ + x • (y ◦ z) ≈⟨ distrˡ x y z ⟩ + (x • y) ◦ (x • z) ≈⟨ ◦-cong (•-comm x y) (•-comm x z) ⟩ + (y • x) ◦ (z • x) ∎ + + comm+distrʳ⇒distrˡ : _•_ DistributesOverʳ _◦_ → _•_ DistributesOverˡ _◦_ + comm+distrʳ⇒distrˡ distrˡ x y z = begin + x • (y ◦ z) ≈⟨ •-comm x (y ◦ z) ⟩ + (y ◦ z) • x ≈⟨ distrˡ x y z ⟩ + (y • x) ◦ (z • x) ≈⟨ ◦-cong (•-comm y x) (•-comm z x) ⟩ + (x • y) ◦ (x • z) ∎ + + comm⇒sym[distribˡ] : ∀ x → Symmetric (λ y z → (x ◦ (y • z)) ≈ ((x ◦ y) • (x ◦ z))) + comm⇒sym[distribˡ] x {y} {z} prf = begin + x ◦ (z • y) ≈⟨ ◦-cong refl (•-comm z y) ⟩ + x ◦ (y • z) ≈⟨ prf ⟩ + (x ◦ y) • (x ◦ z) ≈⟨ •-comm (x ◦ y) (x ◦ z) ⟩ + (x ◦ z) • (x ◦ y) ∎ + +---------------------------------------------------------------------- +-- Ring-like structures + +module _ {_+_ _*_ : Op₂ A} + {_⁻¹ : Op₁ A} {0# : A} + (+-cong : Congruent₂ _+_) + (*-cong : Congruent₂ _*_) + where + + assoc+distribʳ+idʳ+invʳ⇒zeˡ : Associative _+_ → _*_ DistributesOverʳ _+_ → + RightIdentity 0# _+_ → RightInverse 0# _⁻¹ _+_ → + LeftZero 0# _*_ + assoc+distribʳ+idʳ+invʳ⇒zeˡ +-assoc distribʳ idʳ invʳ x = begin + 0# * x ≈⟨ sym (idʳ _) ⟩ + (0# * x) + 0# ≈⟨ +-cong refl (sym (invʳ _)) ⟩ + (0# * x) + ((0# * x) + ((0# * x)⁻¹)) ≈⟨ sym (+-assoc _ _ _) ⟩ + ((0# * x) + (0# * x)) + ((0# * x)⁻¹) ≈⟨ +-cong (sym (distribʳ _ _ _)) refl ⟩ + ((0# + 0#) * x) + ((0# * x)⁻¹) ≈⟨ +-cong (*-cong (idʳ _) refl) refl ⟩ + (0# * x) + ((0# * x)⁻¹) ≈⟨ invʳ _ ⟩ + 0# ∎ + + assoc+distribˡ+idʳ+invʳ⇒zeʳ : Associative _+_ → _*_ DistributesOverˡ _+_ → + RightIdentity 0# _+_ → RightInverse 0# _⁻¹ _+_ → + RightZero 0# _*_ + assoc+distribˡ+idʳ+invʳ⇒zeʳ +-assoc distribˡ idʳ invʳ x = begin + x * 0# ≈⟨ sym (idʳ _) ⟩ + (x * 0#) + 0# ≈⟨ +-cong refl (sym (invʳ _)) ⟩ + (x * 0#) + ((x * 0#) + ((x * 0#)⁻¹)) ≈⟨ sym (+-assoc _ _ _) ⟩ + ((x * 0#) + (x * 0#)) + ((x * 0#)⁻¹) ≈⟨ +-cong (sym (distribˡ _ _ _)) refl ⟩ + (x * (0# + 0#)) + ((x * 0#)⁻¹) ≈⟨ +-cong (*-cong refl (idʳ _)) refl ⟩ + ((x * 0#) + ((x * 0#)⁻¹)) ≈⟨ invʳ _ ⟩ + 0# ∎ + +------------------------------------------------------------------------ +-- Without Loss of Generality + +module _ {p} {f : Op₂ A} {P : Pred A p} + (≈-subst : Substitutive _≈_ p) + (comm : Commutative f) + where + + subst+comm⇒sym : Symmetric (λ a b → P (f a b)) + subst+comm⇒sym = ≈-subst P (comm _ _) + + wlog : ∀ {r} {_R_ : Rel _ r} → Total _R_ → + (∀ a b → a R b → P (f a b)) → + ∀ a b → P (f a b) + wlog r-total = Bin.wlog r-total subst+comm⇒sym diff --git a/src/Algebra/FunctionProperties/Consequences.agda b/src/Algebra/FunctionProperties/Consequences.agda index 8aa15f81e1..9337494c39 100644 --- a/src/Algebra/FunctionProperties/Consequences.agda +++ b/src/Algebra/FunctionProperties/Consequences.agda @@ -1,8 +1,7 @@ ------------------------------------------------------------------------ -- The Agda standard library -- --- Relations between properties of functions, such as associativity and --- commutativity +-- This module is DEPRECATED. ------------------------------------------------------------------------ {-# OPTIONS --without-K --safe #-} @@ -12,184 +11,9 @@ open import Relation.Binary using (Rel; Setoid; Substitutive; Symmetric; Total) module Algebra.FunctionProperties.Consequences {a ℓ} (S : Setoid a ℓ) where -open Setoid S renaming (Carrier to A) +{-# WARNING_ON_IMPORT +"Algebra.FunctionProperties.Consequences was deprecated in v1.3. +Use Algebra.Consequences.Setoid instead." +#-} -open import Algebra.Core -open import Algebra.Definitions _≈_ -open import Data.Sum using (inj₁; inj₂) -open import Data.Product using (_,_) -import Relation.Binary.Consequences as Bin -open import Relation.Binary.Reasoning.Setoid S -open import Relation.Unary using (Pred) - ------------------------------------------------------------------------- --- Re-export core properties - -open import Algebra.FunctionProperties.Consequences.Core public - ------------------------------------------------------------------------- --- Magma-like structures - -module _ {_•_ : Op₂ A} (comm : Commutative _•_) where - - comm+cancelˡ⇒cancelʳ : LeftCancellative _•_ → RightCancellative _•_ - comm+cancelˡ⇒cancelʳ cancelˡ {x} y z eq = cancelˡ x (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ʳ y z (begin - y • x ≈⟨ comm y x ⟩ - x • y ≈⟨ eq ⟩ - x • z ≈⟨ comm x z ⟩ - z • x ∎) - ------------------------------------------------------------------------- --- Monoid-like structures - -module _ {_•_ : Op₂ A} (comm : Commutative _•_) {e : A} where - - comm+idˡ⇒idʳ : LeftIdentity e _•_ → RightIdentity e _•_ - comm+idˡ⇒idʳ idˡ x = begin - x • e ≈⟨ comm x e ⟩ - e • x ≈⟨ idˡ x ⟩ - x ∎ - - comm+idʳ⇒idˡ : RightIdentity e _•_ → LeftIdentity e _•_ - comm+idʳ⇒idˡ idʳ x = begin - e • x ≈⟨ comm e x ⟩ - x • e ≈⟨ idʳ x ⟩ - x ∎ - - comm+zeˡ⇒zeʳ : LeftZero e _•_ → RightZero e _•_ - comm+zeˡ⇒zeʳ zeˡ x = begin - x • e ≈⟨ comm x e ⟩ - e • x ≈⟨ zeˡ x ⟩ - e ∎ - - comm+zeʳ⇒zeˡ : RightZero e _•_ → LeftZero e _•_ - comm+zeʳ⇒zeˡ zeʳ x = begin - e • x ≈⟨ comm e x ⟩ - x • e ≈⟨ zeʳ x ⟩ - e ∎ - ------------------------------------------------------------------------- --- Group-like structures - -module _ {_•_ : Op₂ A} {_⁻¹ : Op₁ A} {e} (comm : Commutative _•_) where - - comm+invˡ⇒invʳ : LeftInverse e _⁻¹ _•_ → RightInverse e _⁻¹ _•_ - comm+invˡ⇒invʳ invˡ x = begin - x • (x ⁻¹) ≈⟨ comm x (x ⁻¹) ⟩ - (x ⁻¹) • x ≈⟨ invˡ x ⟩ - e ∎ - - comm+invʳ⇒invˡ : RightInverse e _⁻¹ _•_ → LeftInverse e _⁻¹ _•_ - comm+invʳ⇒invˡ invʳ x = begin - (x ⁻¹) • x ≈⟨ comm (x ⁻¹) x ⟩ - x • (x ⁻¹) ≈⟨ invʳ x ⟩ - e ∎ - -module _ {_•_ : Op₂ A} {_⁻¹ : Op₁ A} {e} (cong : Congruent₂ _•_) where - - assoc+id+invʳ⇒invˡ-unique : Associative _•_ → - Identity e _•_ → RightInverse e _⁻¹ _•_ → - ∀ x y → (x • y) ≈ e → x ≈ (y ⁻¹) - assoc+id+invʳ⇒invˡ-unique assoc (idˡ , idʳ) invʳ x y eq = begin - x ≈⟨ sym (idʳ x) ⟩ - x • e ≈⟨ cong refl (sym (invʳ y)) ⟩ - x • (y • (y ⁻¹)) ≈⟨ sym (assoc x y (y ⁻¹)) ⟩ - (x • y) • (y ⁻¹) ≈⟨ cong eq refl ⟩ - e • (y ⁻¹) ≈⟨ idˡ (y ⁻¹) ⟩ - y ⁻¹ ∎ - - assoc+id+invˡ⇒invʳ-unique : Associative _•_ → - Identity e _•_ → LeftInverse e _⁻¹ _•_ → - ∀ x y → (x • y) ≈ e → y ≈ (x ⁻¹) - assoc+id+invˡ⇒invʳ-unique assoc (idˡ , idʳ) invˡ x y eq = begin - y ≈⟨ sym (idˡ y) ⟩ - e • y ≈⟨ cong (sym (invˡ x)) refl ⟩ - ((x ⁻¹) • x) • y ≈⟨ assoc (x ⁻¹) x y ⟩ - (x ⁻¹) • (x • y) ≈⟨ cong refl eq ⟩ - (x ⁻¹) • e ≈⟨ idʳ (x ⁻¹) ⟩ - x ⁻¹ ∎ - ----------------------------------------------------------------------- --- Bisemigroup-like structures - -module _ {_•_ _◦_ : Op₂ A} - (◦-cong : Congruent₂ _◦_) - (•-comm : Commutative _•_) - where - - comm+distrˡ⇒distrʳ : _•_ DistributesOverˡ _◦_ → _•_ DistributesOverʳ _◦_ - comm+distrˡ⇒distrʳ distrˡ x y z = begin - (y ◦ z) • x ≈⟨ •-comm (y ◦ z) x ⟩ - x • (y ◦ z) ≈⟨ distrˡ x y z ⟩ - (x • y) ◦ (x • z) ≈⟨ ◦-cong (•-comm x y) (•-comm x z) ⟩ - (y • x) ◦ (z • x) ∎ - - comm+distrʳ⇒distrˡ : _•_ DistributesOverʳ _◦_ → _•_ DistributesOverˡ _◦_ - comm+distrʳ⇒distrˡ distrˡ x y z = begin - x • (y ◦ z) ≈⟨ •-comm x (y ◦ z) ⟩ - (y ◦ z) • x ≈⟨ distrˡ x y z ⟩ - (y • x) ◦ (z • x) ≈⟨ ◦-cong (•-comm y x) (•-comm z x) ⟩ - (x • y) ◦ (x • z) ∎ - - comm⇒sym[distribˡ] : ∀ x → Symmetric (λ y z → (x ◦ (y • z)) ≈ ((x ◦ y) • (x ◦ z))) - comm⇒sym[distribˡ] x {y} {z} prf = begin - x ◦ (z • y) ≈⟨ ◦-cong refl (•-comm z y) ⟩ - x ◦ (y • z) ≈⟨ prf ⟩ - (x ◦ y) • (x ◦ z) ≈⟨ •-comm (x ◦ y) (x ◦ z) ⟩ - (x ◦ z) • (x ◦ y) ∎ - ----------------------------------------------------------------------- --- Ring-like structures - -module _ {_+_ _*_ : Op₂ A} - {_⁻¹ : Op₁ A} {0# : A} - (+-cong : Congruent₂ _+_) - (*-cong : Congruent₂ _*_) - where - - assoc+distribʳ+idʳ+invʳ⇒zeˡ : Associative _+_ → _*_ DistributesOverʳ _+_ → - RightIdentity 0# _+_ → RightInverse 0# _⁻¹ _+_ → - LeftZero 0# _*_ - assoc+distribʳ+idʳ+invʳ⇒zeˡ +-assoc distribʳ idʳ invʳ x = begin - 0# * x ≈⟨ sym (idʳ _) ⟩ - (0# * x) + 0# ≈⟨ +-cong refl (sym (invʳ _)) ⟩ - (0# * x) + ((0# * x) + ((0# * x)⁻¹)) ≈⟨ sym (+-assoc _ _ _) ⟩ - ((0# * x) + (0# * x)) + ((0# * x)⁻¹) ≈⟨ +-cong (sym (distribʳ _ _ _)) refl ⟩ - ((0# + 0#) * x) + ((0# * x)⁻¹) ≈⟨ +-cong (*-cong (idʳ _) refl) refl ⟩ - (0# * x) + ((0# * x)⁻¹) ≈⟨ invʳ _ ⟩ - 0# ∎ - - assoc+distribˡ+idʳ+invʳ⇒zeʳ : Associative _+_ → _*_ DistributesOverˡ _+_ → - RightIdentity 0# _+_ → RightInverse 0# _⁻¹ _+_ → - RightZero 0# _*_ - assoc+distribˡ+idʳ+invʳ⇒zeʳ +-assoc distribˡ idʳ invʳ x = begin - x * 0# ≈⟨ sym (idʳ _) ⟩ - (x * 0#) + 0# ≈⟨ +-cong refl (sym (invʳ _)) ⟩ - (x * 0#) + ((x * 0#) + ((x * 0#)⁻¹)) ≈⟨ sym (+-assoc _ _ _) ⟩ - ((x * 0#) + (x * 0#)) + ((x * 0#)⁻¹) ≈⟨ +-cong (sym (distribˡ _ _ _)) refl ⟩ - (x * (0# + 0#)) + ((x * 0#)⁻¹) ≈⟨ +-cong (*-cong refl (idʳ _)) refl ⟩ - ((x * 0#) + ((x * 0#)⁻¹)) ≈⟨ invʳ _ ⟩ - 0# ∎ - ------------------------------------------------------------------------- --- Without Loss of Generality - -module _ {p} {f : Op₂ A} {P : Pred A p} - (≈-subst : Substitutive _≈_ p) - (comm : Commutative f) - where - - subst+comm⇒sym : Symmetric (λ a b → P (f a b)) - subst+comm⇒sym = ≈-subst P (comm _ _) - - wlog : ∀ {r} {_R_ : Rel _ r} → Total _R_ → - (∀ a b → a R b → P (f a b)) → - ∀ a b → P (f a b) - wlog r-total = Bin.wlog r-total subst+comm⇒sym +open import Algebra.Consequences.Setoid S public diff --git a/src/Algebra/FunctionProperties/Consequences/Core.agda b/src/Algebra/FunctionProperties/Consequences/Core.agda index d95c0cb747..fe7df6f770 100644 --- a/src/Algebra/FunctionProperties/Consequences/Core.agda +++ b/src/Algebra/FunctionProperties/Consequences/Core.agda @@ -1,8 +1,7 @@ ------------------------------------------------------------------------ -- The Agda standard library -- --- Relations between properties of functions, such as associativity and --- commutativity (only those that don't require any sort of setoid) +-- This module is DEPRECATED. ------------------------------------------------------------------------ {-# OPTIONS --without-K --safe #-} @@ -10,13 +9,9 @@ module Algebra.FunctionProperties.Consequences.Core {a} {A : Set a} where -open import Algebra.Core -open import Algebra.Definitions -open import Data.Sum -open import Relation.Binary +{-# WARNING_ON_IMPORT +"Algebra.FunctionProperties.Consequences.Core was deprecated in v1.3. +Use Algebra.Consequences.Base instead." +#-} -sel⇒idem : ∀ {ℓ} {_•_ : Op₂ A} (_≈_ : Rel A ℓ) → - Selective _≈_ _•_ → Idempotent _≈_ _•_ -sel⇒idem _ sel x with sel x x -... | inj₁ x•x≈x = x•x≈x -... | inj₂ x•x≈x = x•x≈x +open import Algebra.Consequences.Base public diff --git a/src/Algebra/FunctionProperties/Consequences/Propositional.agda b/src/Algebra/FunctionProperties/Consequences/Propositional.agda index 204a1a8e2c..8d68750adf 100644 --- a/src/Algebra/FunctionProperties/Consequences/Propositional.agda +++ b/src/Algebra/FunctionProperties/Consequences/Propositional.agda @@ -1,8 +1,7 @@ ------------------------------------------------------------------------ -- The Agda standard library -- --- Relations between properties of functions, such as associativity and --- commutativity (specialised to propositional equality) +-- This module is DEPRECATED. ------------------------------------------------------------------------ {-# OPTIONS --without-K --safe #-} @@ -10,97 +9,9 @@ module Algebra.FunctionProperties.Consequences.Propositional {a} {A : Set a} where -open import Data.Sum using (inj₁; inj₂) -open import Relation.Binary using (Rel; Setoid; Symmetric; Total) -open import Relation.Binary.PropositionalEquality -open import Relation.Unary using (Pred) +{-# WARNING_ON_IMPORT +"Algebra.FunctionProperties.Consequences.Propositional was deprecated in v1.3. +Use Algebra.Consequences.Propositional instead." +#-} -open import Algebra.Core -open import Algebra.Definitions {A = A} _≡_ -import Algebra.FunctionProperties.Consequences (setoid A) as FP⇒ - ------------------------------------------------------------------------- --- Re-export all proofs that don't require congruence or substitutivity - -open FP⇒ public - hiding - ( assoc+distribʳ+idʳ+invʳ⇒zeˡ - ; assoc+distribˡ+idʳ+invʳ⇒zeʳ - ; assoc+id+invʳ⇒invˡ-unique - ; assoc+id+invˡ⇒invʳ-unique - ; comm+distrˡ⇒distrʳ - ; comm+distrʳ⇒distrˡ - ; comm⇒sym[distribˡ] - ; subst+comm⇒sym - ; wlog - ; sel⇒idem - ) - ------------------------------------------------------------------------- --- Group-like structures - -module _ {_•_ _⁻¹ ε} where - - assoc+id+invʳ⇒invˡ-unique : Associative _•_ → Identity ε _•_ → - RightInverse ε _⁻¹ _•_ → - ∀ x y → (x • y) ≡ ε → x ≡ (y ⁻¹) - assoc+id+invʳ⇒invˡ-unique = FP⇒.assoc+id+invʳ⇒invˡ-unique (cong₂ _) - - assoc+id+invˡ⇒invʳ-unique : Associative _•_ → Identity ε _•_ → - LeftInverse ε _⁻¹ _•_ → - ∀ x y → (x • y) ≡ ε → y ≡ (x ⁻¹) - assoc+id+invˡ⇒invʳ-unique = FP⇒.assoc+id+invˡ⇒invʳ-unique (cong₂ _) - ------------------------------------------------------------------------- --- Ring-like structures - -module _ {_+_ _*_ -_ 0#} where - - assoc+distribʳ+idʳ+invʳ⇒zeˡ : Associative _+_ → _*_ DistributesOverʳ _+_ → - RightIdentity 0# _+_ → RightInverse 0# -_ _+_ → - LeftZero 0# _*_ - assoc+distribʳ+idʳ+invʳ⇒zeˡ = - FP⇒.assoc+distribʳ+idʳ+invʳ⇒zeˡ (cong₂ _+_) (cong₂ _*_) - - assoc+distribˡ+idʳ+invʳ⇒zeʳ : Associative _+_ → _*_ DistributesOverˡ _+_ → - RightIdentity 0# _+_ → RightInverse 0# -_ _+_ → - RightZero 0# _*_ - assoc+distribˡ+idʳ+invʳ⇒zeʳ = - FP⇒.assoc+distribˡ+idʳ+invʳ⇒zeʳ (cong₂ _+_) (cong₂ _*_) - ------------------------------------------------------------------------- --- Bisemigroup-like structures - -module _ {_•_ _◦_ : Op₂ A} (•-comm : Commutative _•_) where - - comm+distrˡ⇒distrʳ : _•_ DistributesOverˡ _◦_ → _•_ DistributesOverʳ _◦_ - comm+distrˡ⇒distrʳ = FP⇒.comm+distrˡ⇒distrʳ (cong₂ _) •-comm - - comm+distrʳ⇒distrˡ : _•_ DistributesOverʳ _◦_ → _•_ DistributesOverˡ _◦_ - comm+distrʳ⇒distrˡ = FP⇒.comm+distrʳ⇒distrˡ (cong₂ _) •-comm - - comm⇒sym[distribˡ] : ∀ x → Symmetric (λ y z → (x ◦ (y • z)) ≡ ((x ◦ y) • (x ◦ z))) - comm⇒sym[distribˡ] = FP⇒.comm⇒sym[distribˡ] (cong₂ _◦_) •-comm - ------------------------------------------------------------------------- --- Selectivity - -module _ {_•_ : Op₂ A} where - - sel⇒idem : Selective _•_ → Idempotent _•_ - sel⇒idem = FP⇒.sel⇒idem _≡_ - ------------------------------------------------------------------------- --- Without Loss of Generality - -module _ {p} {P : Pred A p} where - - subst+comm⇒sym : ∀ {f} (f-comm : Commutative f) → - Symmetric (λ a b → P (f a b)) - subst+comm⇒sym = FP⇒.subst+comm⇒sym {P = P} subst - - wlog : ∀ {f} (f-comm : Commutative f) → - ∀ {r} {_R_ : Rel _ r} → Total _R_ → - (∀ a b → a R b → P (f a b)) → - ∀ a b → P (f a b) - wlog = FP⇒.wlog {P = P} subst +open import Algebra.Consequences.Propositional {A = A} public diff --git a/src/Algebra/Properties/BooleanAlgebra.agda b/src/Algebra/Properties/BooleanAlgebra.agda index b412f61247..74c2b2d3d9 100644 --- a/src/Algebra/Properties/BooleanAlgebra.agda +++ b/src/Algebra/Properties/BooleanAlgebra.agda @@ -18,7 +18,7 @@ import Algebra.Properties.DistributiveLattice as DistribLatticeProperties open import Algebra.Core open import Algebra.Structures _≈_ open import Algebra.Definitions _≈_ -open import Algebra.FunctionProperties.Consequences setoid +open import Algebra.Consequences.Setoid setoid open import Relation.Binary.Reasoning.Setoid setoid open import Relation.Binary open import Function.Base diff --git a/src/Algebra/Structures.agda b/src/Algebra/Structures.agda index e69ea8b6a1..49eeb0207c 100644 --- a/src/Algebra/Structures.agda +++ b/src/Algebra/Structures.agda @@ -22,7 +22,7 @@ module Algebra.Structures open import Algebra.Core open import Algebra.Definitions _≈_ -import Algebra.FunctionProperties.Consequences as Consequences +import Algebra.Consequences.Setoid as Consequences open import Data.Product using (_,_; proj₁; proj₂) open import Level using (_⊔_) diff --git a/src/Data/Nat/Properties.agda b/src/Data/Nat/Properties.agda index 748400db6e..d959ee834b 100644 --- a/src/Data/Nat/Properties.agda +++ b/src/Data/Nat/Properties.agda @@ -14,7 +14,7 @@ module Data.Nat.Properties where open import Axiom.UniquenessOfIdentityProofs open import Algebra.Bundles open import Algebra.Morphism -open import Algebra.FunctionProperties.Consequences.Propositional +open import Algebra.Consequences.Propositional open import Data.Bool.Base using (Bool; false; true; T) open import Data.Bool.Properties using (T?) open import Data.Empty From 7cc299451268f39b41592f095a56af696d79af29 Mon Sep 17 00:00:00 2001 From: = Date: Fri, 17 Jan 2020 16:54:38 +0800 Subject: [PATCH 2/3] Fix double public import bug --- src/Algebra/Construct/LiftedChoice.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Algebra/Construct/LiftedChoice.agda b/src/Algebra/Construct/LiftedChoice.agda index a8f9b104b8..b6f5093610 100644 --- a/src/Algebra/Construct/LiftedChoice.agda +++ b/src/Algebra/Construct/LiftedChoice.agda @@ -10,7 +10,7 @@ open import Algebra module Algebra.Construct.LiftedChoice where -open import Algebra.FunctionProperties.Consequences +open import Algebra.Consequences.Base open import Relation.Binary open import Relation.Nullary using (¬_; yes; no) open import Data.Sum as Sum using (_⊎_; inj₁; inj₂; [_,_]) From cc05ff17904f964052635b55f8b7b8ce8289062d Mon Sep 17 00:00:00 2001 From: = Date: Fri, 17 Jan 2020 17:05:23 +0800 Subject: [PATCH 3/3] Fixed deprecation warnings --- src/Algebra/Structures/Biased.agda | 2 +- src/Data/Nat/Binary/Properties.agda | 2 +- src/Data/Rational/Properties.agda | 2 +- src/Data/Rational/Unnormalised/Properties.agda | 2 +- 4 files changed, 4 insertions(+), 4 deletions(-) diff --git a/src/Algebra/Structures/Biased.agda b/src/Algebra/Structures/Biased.agda index 2c06b3df24..fe3f5b8877 100644 --- a/src/Algebra/Structures/Biased.agda +++ b/src/Algebra/Structures/Biased.agda @@ -17,7 +17,7 @@ module Algebra.Structures.Biased open import Algebra.Core open import Algebra.Definitions _≈_ open import Algebra.Structures _≈_ -import Algebra.FunctionProperties.Consequences as Consequences +import Algebra.Consequences.Setoid as Consequences open import Data.Product using (_,_; proj₁; proj₂) open import Level using (_⊔_) diff --git a/src/Data/Nat/Binary/Properties.agda b/src/Data/Nat/Binary/Properties.agda index e057eb8e16..fe8a94c495 100644 --- a/src/Data/Nat/Binary/Properties.agda +++ b/src/Data/Nat/Binary/Properties.agda @@ -11,7 +11,7 @@ module Data.Nat.Binary.Properties where open import Algebra.Bundles open import Algebra.Morphism.Structures import Algebra.Morphism.MonoidMonomorphism as MonoidMonomorphism -open import Algebra.FunctionProperties.Consequences.Propositional +open import Algebra.Consequences.Propositional open import Data.Nat.Binary.Base open import Data.Nat as ℕ using (ℕ; z≤n; s≤s) import Data.Nat.Properties as ℕₚ diff --git a/src/Data/Rational/Properties.agda b/src/Data/Rational/Properties.agda index a59605db88..2ef9f4fedd 100644 --- a/src/Data/Rational/Properties.agda +++ b/src/Data/Rational/Properties.agda @@ -8,6 +8,7 @@ module Data.Rational.Properties where +open import Algebra.Consequences.Propositional open import Algebra.Morphism open import Algebra.Bundles import Algebra.Morphism.MonoidMonomorphism as MonoidMonomorphisms @@ -45,7 +46,6 @@ open import Relation.Nullary.Product using (_×-dec_) open import Algebra.Definitions {A = ℚ} _≡_ open import Algebra.Structures {A = ℚ} _≡_ -open import Algebra.FunctionProperties.Consequences.Propositional private infix 4 _≢0 diff --git a/src/Data/Rational/Unnormalised/Properties.agda b/src/Data/Rational/Unnormalised/Properties.agda index fa05645f32..208fe47989 100644 --- a/src/Data/Rational/Unnormalised/Properties.agda +++ b/src/Data/Rational/Unnormalised/Properties.agda @@ -9,7 +9,7 @@ module Data.Rational.Unnormalised.Properties where open import Algebra -open import Algebra.FunctionProperties.Consequences.Propositional +open import Algebra.Consequences.Propositional open import Data.Nat using (suc) import Data.Nat.Properties as ℕ open import Data.Integer as ℤ using (ℤ; +0; +[1+_]; 0ℤ; 1ℤ)