Rename Algebra.FunctionProperties.Consequences to Algebra.Consequences

CHANGELOG.md

@@ -188,6 +188,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
 ----------------
 

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

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

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

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₂; [_,_])