Skip to content

Commit

Permalink
[fixes #2168] Change names in Algebra.Consequences.* to reflect `st…
Browse files Browse the repository at this point in the history 
…yle-guide` conventions (#2206)

* fixes issue #2168

* added more names for deprecation, plus `hiding` them in `Propositional`
  • Loading branch information
@jamesmckinna
jamesmckinna authored Nov 25, 2023
1 parent afdc679 commit e822675
Show file tree
Hide file tree
Showing 13 changed files with 383 additions and 141 deletions.
70 changes: 54 additions & 16 deletions CHANGELOG.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1276,6 +1276,44 @@ Deprecated modules
Deprecated names
----------------

* In `Algebra.Consequences.Propositional`:
```agda
comm+assoc⇒middleFour ↦ comm∧assoc⇒middleFour
identity+middleFour⇒assoc ↦ identity∧middleFour⇒assoc
identity+middleFour⇒comm ↦ identity∧middleFour⇒comm
comm+distrˡ⇒distrʳ ↦ comm∧distrˡ⇒distrʳ
comm+distrʳ⇒distrˡ ↦ comm∧distrʳ⇒distrˡ
assoc+distribʳ+idʳ+invʳ⇒zeˡ ↦ assoc∧distribʳ∧idʳ∧invʳ⇒zeˡ
assoc+distribˡ+idʳ+invʳ⇒zeʳ ↦ assoc∧distribˡ∧idʳ∧invʳ⇒zeʳ
assoc+id+invʳ⇒invˡ-unique ↦ assoc∧id∧invʳ⇒invˡ-unique
assoc+id+invˡ⇒invʳ-unique ↦ assoc∧id∧invˡ⇒invʳ-unique
subst+comm⇒sym ↦ subst∧comm⇒sym
```

* In `Algebra.Consequences.Setoid`:
```agda
comm+assoc⇒middleFour ↦ comm∧assoc⇒middleFour
identity+middleFour⇒assoc ↦ identity∧middleFour⇒assoc
identity+middleFour⇒comm ↦ identity∧middleFour⇒comm
comm+cancelˡ⇒cancelʳ ↦ comm∧cancelˡ⇒cancelʳ
comm+cancelʳ⇒cancelˡ ↦ comm∧cancelʳ⇒cancelˡ
comm+almostCancelˡ⇒almostCancelʳ ↦ comm∧almostCancelˡ⇒almostCancelʳ
comm+almostCancelʳ⇒almostCancelˡ ↦ comm∧almostCancelʳ⇒almostCancelˡ
comm+idˡ⇒idʳ ↦ comm∧idˡ⇒idʳ
comm+idʳ⇒idˡ ↦ comm∧idʳ⇒idˡ
comm+zeˡ⇒zeʳ ↦ comm∧zeˡ⇒zeʳ
comm+zeʳ⇒zeˡ ↦ comm∧zeʳ⇒zeˡ
comm+invˡ⇒invʳ ↦ comm∧invˡ⇒invʳ
comm+invʳ⇒invˡ ↦ comm∧invʳ⇒invˡ
comm+distrˡ⇒distrʳ ↦ comm∧distrˡ⇒distrʳ
comm+distrʳ⇒distrˡ ↦ comm∧distrʳ⇒distrˡ
assoc+distribʳ+idʳ+invʳ⇒zeˡ ↦ assoc∧distribʳ∧idʳ∧invʳ⇒zeˡ
assoc+distribˡ+idʳ+invʳ⇒zeʳ ↦ assoc∧distribˡ∧idʳ∧invʳ⇒zeʳ
assoc+id+invʳ⇒invˡ-unique ↦ assoc∧id∧invʳ⇒invˡ-unique
assoc+id+invˡ⇒invʳ-unique ↦ assoc∧id∧invˡ⇒invʳ-unique
subst+comm⇒sym ↦ subst∧comm⇒sym
```

* In `Algebra.Construct.Zero`:
```agda
rawMagma ↦ Algebra.Construct.Terminal.rawMagma
Expand Down Expand Up @@ -2177,21 +2215,21 @@ Additions to existing modules

* Added new proof to `Algebra.Consequences.Base`:
```agda
reflexive+selfInverse⇒involutive : Reflexive _≈_ → SelfInverse _≈_ f → Involutive _≈_ f
reflexive∧selfInverse⇒involutive : Reflexive _≈_ → SelfInverse _≈_ f → Involutive _≈_ f
```

* Added new proofs to `Algebra.Consequences.Propositional`:
```agda
comm+assoc⇒middleFour : Commutative _∙_ → Associative _∙_ → _∙_ MiddleFourExchange _∙_
identity+middleFour⇒assoc : Identity e _∙_ → _∙_ MiddleFourExchange _∙_ → Associative _∙_
identity+middleFour⇒comm : Identity e _+_ → _∙_ MiddleFourExchange _+_ → Commutative _∙_
comm∧assoc⇒middleFour : Commutative _∙_ → Associative _∙_ → _∙_ MiddleFourExchange _∙_
identity∧middleFour⇒assoc : Identity e _∙_ → _∙_ MiddleFourExchange _∙_ → Associative _∙_
identity∧middleFour⇒comm : Identity e _+_ → _∙_ MiddleFourExchange _+_ → Commutative _∙_
```

* Added new proofs to `Algebra.Consequences.Setoid`:
```agda
comm+assoc⇒middleFour : Congruent₂ _∙_ → Commutative _∙_ → Associative _∙_ → _∙_ MiddleFourExchange _∙_
identity+middleFour⇒assoc : Congruent₂ _∙_ → Identity e _∙_ → _∙_ MiddleFourExchange _∙_ → Associative _∙_
identity+middleFour⇒comm : Congruent₂ _∙_ → Identity e _+_ → _∙_ MiddleFourExchange _+_ → Commutative _∙_
comm∧assoc⇒middleFour : Congruent₂ _∙_ → Commutative _∙_ → Associative _∙_ → _∙_ MiddleFourExchange _∙_
identity∧middleFour⇒assoc : Congruent₂ _∙_ → Identity e _∙_ → _∙_ MiddleFourExchange _∙_ → Associative _∙_
identity∧middleFour⇒comm : Congruent₂ _∙_ → Identity e _+_ → _∙_ MiddleFourExchange _+_ → Commutative _∙_
involutive⇒surjective : Involutive f → Surjective f
selfInverse⇒involutive : SelfInverse f → Involutive f
Expand All @@ -2201,15 +2239,15 @@ Additions to existing modules
selfInverse⇒injective : SelfInverse f → Injective f
selfInverse⇒bijective : SelfInverse f → Bijective f
comm+idˡ⇒id : Commutative _∙_ → LeftIdentity e _∙_ → Identity e _∙_
comm+idʳ⇒id : Commutative _∙_ → RightIdentity e _∙_ → Identity e _∙_
comm+zeˡ⇒ze : Commutative _∙_ → LeftZero e _∙_ → Zero e _∙_
comm+zeʳ⇒ze : Commutative _∙_ → RightZero e _∙_ → Zero e _∙_
comm+invˡ⇒inv : Commutative _∙_ → LeftInverse e _⁻¹ _∙_ → Inverse e _⁻¹ _∙_
comm+invʳ⇒inv : Commutative _∙_ → RightInverse e _⁻¹ _∙_ → Inverse e _⁻¹ _∙_
comm+distrˡ⇒distr : Commutative _∙_ → _∙_ DistributesOverˡ _◦_ → _∙_ DistributesOver _◦_
comm+distrʳ⇒distr : Commutative _∙_ → _∙_ DistributesOverʳ _◦_ → _∙_ DistributesOver _◦_
distrib+absorbs⇒distribˡ : Associative _∙_ → Commutative _◦_ → _∙_ Absorbs _◦_ → _◦_ Absorbs _∙_ → _◦_ DistributesOver _∙_ → _∙_ DistributesOverˡ _◦_
comm∧idˡ⇒id : Commutative _∙_ → LeftIdentity e _∙_ → Identity e _∙_
comm∧idʳ⇒id : Commutative _∙_ → RightIdentity e _∙_ → Identity e _∙_
comm∧zeˡ⇒ze : Commutative _∙_ → LeftZero e _∙_ → Zero e _∙_
comm∧zeʳ⇒ze : Commutative _∙_ → RightZero e _∙_ → Zero e _∙_
comm∧invˡ⇒inv : Commutative _∙_ → LeftInverse e _⁻¹ _∙_ → Inverse e _⁻¹ _∙_
comm∧invʳ⇒inv : Commutative _∙_ → RightInverse e _⁻¹ _∙_ → Inverse e _⁻¹ _∙_
comm∧distrˡ⇒distr : Commutative _∙_ → _∙_ DistributesOverˡ _◦_ → _∙_ DistributesOver _◦_
comm∧distrʳ⇒distr : Commutative _∙_ → _∙_ DistributesOverʳ _◦_ → _∙_ DistributesOver _◦_
distrib∧absorbs⇒distribˡ : Associative _∙_ → Commutative _◦_ → _∙_ Absorbs _◦_ → _◦_ Absorbs _∙_ → _◦_ DistributesOver _∙_ → _∙_ DistributesOverˡ _◦_
```

* Added new functions to `Algebra.Construct.DirectProduct`:
Expand Down
17 changes: 15 additions & 2 deletions src/Algebra/Consequences/Base.agda
View file
Original file line number Diff line number Diff line change
Expand Up @@ -23,8 +23,21 @@ module _ {ℓ} {_•_ : Op₂ A} (_≈_ : Rel A ℓ) where

module _ {ℓ} {f : Op₁ A} (_≈_ : Rel A ℓ) where

reflexive+selfInverse⇒involutive : Reflexive _≈_ →
reflexive∧selfInverse⇒involutive : Reflexive _≈_ →
SelfInverse _≈_ f →
Involutive _≈_ f
reflexive+selfInverse⇒involutive refl inv _ = inv refl
reflexive∧selfInverse⇒involutive refl inv _ = inv refl

------------------------------------------------------------------------
-- DEPRECATED NAMES
------------------------------------------------------------------------
-- Please use the new names as continuing support for the old names is
-- not guaranteed.

-- Version 2.0

reflexive+selfInverse⇒involutive = reflexive∧selfInverse⇒involutive
{-# WARNING_ON_USAGE reflexive+selfInverse⇒involutive
"Warning: reflexive+selfInverse⇒involutive was deprecated in v2.0.
Please use reflexive∧selfInverse⇒involutive instead."
#-}
123 changes: 97 additions & 26 deletions src/Algebra/Consequences/Propositional.agda
View file
Original file line number Diff line number Diff line change
Expand Up @@ -26,7 +26,21 @@ import Algebra.Consequences.Setoid (setoid A) as Base

open Base public
hiding
( comm+assoc⇒middleFour
( comm∧assoc⇒middleFour
; identity∧middleFour⇒assoc
; identity∧middleFour⇒comm
; 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
-- plus all the deprecated versions of the above
; comm+assoc⇒middleFour
; identity+middleFour⇒assoc
; identity+middleFour⇒comm
; assoc+distribʳ+idʳ+invʳ⇒zeˡ
Expand All @@ -35,54 +49,51 @@ open Base public
; 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 ε _∙_ →
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 = Base.assoc∧id∧invʳ⇒invˡ-unique (cong₂ _)

assoc+id+invˡ⇒invʳ-unique : Associative _∙_ → Identity ε _∙_ →
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₂ _)
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ʳ _+_ →
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ˡ =
Base.assoc∧distribʳ∧idʳ∧invʳ⇒zeˡ (cong₂ _+_) (cong₂ _*_)

assoc+distribˡ+idʳ+invʳ⇒zeʳ : Associative _+_ → _*_ DistributesOverˡ _+_ →
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₂ _*_)
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+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
Expand All @@ -100,31 +111,91 @@ module _ {_∙_ : Op₂ A} where

module _ {_∙_ : Op₂ A} where

comm+assoc⇒middleFour : Commutative _∙_ → Associative _∙_ →
comm∧assoc⇒middleFour : Commutative _∙_ → Associative _∙_ →
_∙_ MiddleFourExchange _∙_
comm+assoc⇒middleFour = Base.comm+assoc⇒middleFour (cong₂ _∙_)
comm∧assoc⇒middleFour = Base.comm∧assoc⇒middleFour (cong₂ _∙_)

identity+middleFour⇒assoc : {e : A} → Identity e _∙_ →
identity∧middleFour⇒assoc : {e : A} → Identity e _∙_ →
_∙_ MiddleFourExchange _∙_ →
Associative _∙_
identity+middleFour⇒assoc = Base.identity+middleFour⇒assoc (cong₂ _∙_)
identity∧middleFour⇒assoc = Base.identity∧middleFour⇒assoc (cong₂ _∙_)

identity+middleFour⇒comm : {_+_ : Op₂ A} {e : A} → Identity e _+_ →
identity∧middleFour⇒comm : {_+_ : Op₂ A} {e : A} → Identity e _+_ →
_∙_ MiddleFourExchange _+_ →
Commutative _∙_
identity+middleFour⇒comm = Base.identity+middleFour⇒comm (cong₂ _∙_)
identity∧middleFour⇒comm = Base.identity∧middleFour⇒comm (cong₂ _∙_)

------------------------------------------------------------------------
-- Without Loss of Generality

module _ {p} {P : Pred A p} where

subst+comm⇒sym : ∀ {f} (f-comm : Commutative f) →
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
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


------------------------------------------------------------------------
-- DEPRECATED NAMES
------------------------------------------------------------------------
-- Please use the new names as continuing support for the old names is
-- not guaranteed.

-- Version 2.0

comm+assoc⇒middleFour = comm∧assoc⇒middleFour
{-# WARNING_ON_USAGE comm+assoc⇒middleFour
"Warning: comm+assoc⇒middleFour was deprecated in v2.0.
Please use comm∧assoc⇒middleFour instead."
#-}
identity+middleFour⇒assoc = identity∧middleFour⇒assoc
{-# WARNING_ON_USAGE identity+middleFour⇒assoc
"Warning: identity+middleFour⇒assoc was deprecated in v2.0.
Please use identity∧middleFour⇒assoc instead."
#-}
identity+middleFour⇒comm = identity∧middleFour⇒comm
{-# WARNING_ON_USAGE identity+middleFour⇒comm
"Warning: identity+middleFour⇒comm was deprecated in v2.0.
Please use identity∧middleFour⇒comm instead."
#-}
comm+distrˡ⇒distrʳ = comm∧distrˡ⇒distrʳ
{-# WARNING_ON_USAGE comm+distrˡ⇒distrʳ
"Warning: comm+distrˡ⇒distrʳ was deprecated in v2.0.
Please use comm∧distrˡ⇒distrʳ instead."
#-}
comm+distrʳ⇒distrˡ = comm∧distrʳ⇒distrˡ
{-# WARNING_ON_USAGE comm+distrʳ⇒distrˡ
"Warning: comm+distrʳ⇒distrˡ was deprecated in v2.0.
Please use comm∧distrʳ⇒distrˡ instead."
#-}
assoc+distribʳ+idʳ+invʳ⇒zeˡ = assoc∧distribʳ∧idʳ∧invʳ⇒zeˡ
{-# WARNING_ON_USAGE assoc+distribʳ+idʳ+invʳ⇒zeˡ
"Warning: assoc+distribʳ+idʳ+invʳ⇒zeˡ was deprecated in v2.0.
Please use assoc∧distribʳ∧idʳ∧invʳ⇒zeˡ instead."
#-}
assoc+distribˡ+idʳ+invʳ⇒zeʳ = assoc∧distribˡ∧idʳ∧invʳ⇒zeʳ
{-# WARNING_ON_USAGE assoc+distribˡ+idʳ+invʳ⇒zeʳ
"Warning: assoc+distribˡ+idʳ+invʳ⇒zeʳ was deprecated in v2.0.
Please use assoc∧distribˡ∧idʳ∧invʳ⇒zeʳ instead."
#-}
assoc+id+invʳ⇒invˡ-unique = assoc∧id∧invʳ⇒invˡ-unique
{-# WARNING_ON_USAGE assoc+id+invʳ⇒invˡ-unique
"Warning: assoc+id+invʳ⇒invˡ-unique was deprecated in v2.0.
Please use assoc∧id∧invʳ⇒invˡ-unique instead."
#-}
assoc+id+invˡ⇒invʳ-unique = assoc∧id∧invˡ⇒invʳ-unique
{-# WARNING_ON_USAGE assoc+id+invˡ⇒invʳ-unique
"Warning: assoc+id+invˡ⇒invʳ-unique was deprecated in v2.0.
Please use assoc∧id∧invˡ⇒invʳ-unique instead."
#-}
subst+comm⇒sym = subst∧comm⇒sym
{-# WARNING_ON_USAGE subst+comm⇒sym
"Warning: subst+comm⇒sym was deprecated in v2.0.
Please use subst∧comm⇒sym instead."
#-}
Loading

0 comments on commit e822675

Please sign in to comment.