diff --git a/CHANGELOG.md b/CHANGELOG.md index 0e50316b36..25065935ce 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -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 @@ -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 @@ -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`: diff --git a/src/Algebra/Consequences/Base.agda b/src/Algebra/Consequences/Base.agda index 446a82d868..574ad48a16 100644 --- a/src/Algebra/Consequences/Base.agda +++ b/src/Algebra/Consequences/Base.agda @@ -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." +#-} diff --git a/src/Algebra/Consequences/Propositional.agda b/src/Algebra/Consequences/Propositional.agda index 1adcb12afc..5c10a9e4cc 100644 --- a/src/Algebra/Consequences/Propositional.agda +++ b/src/Algebra/Consequences/Propositional.agda @@ -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ˡ @@ -35,10 +49,7 @@ open Base public ; assoc+id+invˡ⇒invʳ-unique ; comm+distrˡ⇒distrʳ ; comm+distrʳ⇒distrˡ - ; comm⇒sym[distribˡ] ; subst+comm⇒sym - ; wlog - ; sel⇒idem ) ------------------------------------------------------------------------ @@ -46,43 +57,43 @@ open Base public 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 @@ -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." +#-} diff --git a/src/Algebra/Consequences/Setoid.agda b/src/Algebra/Consequences/Setoid.agda index f90a801fe4..66e441a9e0 100644 --- a/src/Algebra/Consequences/Setoid.agda +++ b/src/Algebra/Consequences/Setoid.agda @@ -37,9 +37,9 @@ open import Algebra.Consequences.Base public module _ {_∙_ : Op₂ A} (cong : Congruent₂ _∙_) where - comm+assoc⇒middleFour : Commutative _∙_ → Associative _∙_ → + comm∧assoc⇒middleFour : Commutative _∙_ → Associative _∙_ → _∙_ MiddleFourExchange _∙_ - comm+assoc⇒middleFour comm assoc w x y z = begin + comm∧assoc⇒middleFour comm assoc w x y z = begin (w ∙ x) ∙ (y ∙ z) ≈⟨ assoc w x (y ∙ z) ⟩ w ∙ (x ∙ (y ∙ z)) ≈⟨ cong refl (sym (assoc x y z)) ⟩ w ∙ ((x ∙ y) ∙ z) ≈⟨ cong refl (cong (comm x y) refl) ⟩ @@ -47,19 +47,19 @@ module _ {_∙_ : Op₂ A} (cong : Congruent₂ _∙_) where w ∙ (y ∙ (x ∙ z)) ≈⟨ sym (assoc w y (x ∙ z)) ⟩ (w ∙ y) ∙ (x ∙ z) ∎ - identity+middleFour⇒assoc : {e : A} → Identity e _∙_ → + identity∧middleFour⇒assoc : {e : A} → Identity e _∙_ → _∙_ MiddleFourExchange _∙_ → Associative _∙_ - identity+middleFour⇒assoc {e} (identityˡ , identityʳ) middleFour x y z = begin + identity∧middleFour⇒assoc {e} (identityˡ , identityʳ) middleFour x y z = begin (x ∙ y) ∙ z ≈⟨ cong refl (sym (identityˡ z)) ⟩ (x ∙ y) ∙ (e ∙ z) ≈⟨ middleFour x y e z ⟩ (x ∙ e) ∙ (y ∙ z) ≈⟨ cong (identityʳ x) refl ⟩ x ∙ (y ∙ z) ∎ - identity+middleFour⇒comm : {_+_ : Op₂ A} {e : A} → Identity e _+_ → + identity∧middleFour⇒comm : {_+_ : Op₂ A} {e : A} → Identity e _+_ → _∙_ MiddleFourExchange _+_ → Commutative _∙_ - identity+middleFour⇒comm {_+_} {e} (identityˡ , identityʳ) middleFour x y + identity∧middleFour⇒comm {_+_} {e} (identityˡ , identityʳ) middleFour x y = begin x ∙ y ≈⟨ sym (cong (identityˡ x) (identityʳ y)) ⟩ (e + x) ∙ (y + e) ≈⟨ middleFour e x y e ⟩ @@ -72,7 +72,7 @@ module _ {_∙_ : Op₂ A} (cong : Congruent₂ _∙_) where module _ {f : Op₁ A} (self : SelfInverse f) where selfInverse⇒involutive : Involutive f - selfInverse⇒involutive = reflexive+selfInverse⇒involutive _≈_ refl self + selfInverse⇒involutive = reflexive∧selfInverse⇒involutive _≈_ refl self selfInverse⇒congruent : Congruent _≈_ _≈_ f selfInverse⇒congruent {x} {y} x≈y = sym (self (begin @@ -100,15 +100,15 @@ 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∧cancelˡ⇒cancelʳ : LeftCancellative _∙_ → RightCancellative _∙_ + comm∧cancelˡ⇒cancelʳ cancelˡ x y z eq = cancelˡ x 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ˡ : RightCancellative _∙_ → LeftCancellative _∙_ + comm∧cancelʳ⇒cancelˡ cancelʳ x y z eq = cancelʳ x y z $ begin y ∙ x ≈⟨ comm y x ⟩ x ∙ y ≈⟨ eq ⟩ x ∙ z ≈⟨ comm x z ⟩ @@ -119,54 +119,54 @@ module _ {_∙_ : Op₂ A} (comm : Commutative _∙_) where module _ {_∙_ : Op₂ A} (comm : Commutative _∙_) {e : A} where - comm+idˡ⇒idʳ : LeftIdentity e _∙_ → RightIdentity e _∙_ - comm+idˡ⇒idʳ idˡ x = begin + 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 + comm∧idʳ⇒idˡ : RightIdentity e _∙_ → LeftIdentity e _∙_ + comm∧idʳ⇒idˡ idʳ x = begin e ∙ x ≈⟨ comm e x ⟩ x ∙ e ≈⟨ idʳ x ⟩ x ∎ - comm+idˡ⇒id : LeftIdentity e _∙_ → Identity e _∙_ - comm+idˡ⇒id idˡ = idˡ , comm+idˡ⇒idʳ idˡ + comm∧idˡ⇒id : LeftIdentity e _∙_ → Identity e _∙_ + comm∧idˡ⇒id idˡ = idˡ , comm∧idˡ⇒idʳ idˡ - comm+idʳ⇒id : RightIdentity e _∙_ → Identity e _∙_ - comm+idʳ⇒id idʳ = comm+idʳ⇒idˡ idʳ , idʳ + comm∧idʳ⇒id : RightIdentity e _∙_ → Identity e _∙_ + comm∧idʳ⇒id idʳ = comm∧idʳ⇒idˡ idʳ , idʳ - comm+zeˡ⇒zeʳ : LeftZero e _∙_ → RightZero e _∙_ - comm+zeˡ⇒zeʳ zeˡ x = begin + 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 + comm∧zeʳ⇒zeˡ : RightZero e _∙_ → LeftZero e _∙_ + comm∧zeʳ⇒zeˡ zeʳ x = begin e ∙ x ≈⟨ comm e x ⟩ x ∙ e ≈⟨ zeʳ x ⟩ e ∎ - comm+zeˡ⇒ze : LeftZero e _∙_ → Zero e _∙_ - comm+zeˡ⇒ze zeˡ = zeˡ , comm+zeˡ⇒zeʳ zeˡ + comm∧zeˡ⇒ze : LeftZero e _∙_ → Zero e _∙_ + comm∧zeˡ⇒ze zeˡ = zeˡ , comm∧zeˡ⇒zeʳ zeˡ - comm+zeʳ⇒ze : RightZero e _∙_ → Zero e _∙_ - comm+zeʳ⇒ze zeʳ = comm+zeʳ⇒zeˡ zeʳ , zeʳ + comm∧zeʳ⇒ze : RightZero e _∙_ → Zero e _∙_ + comm∧zeʳ⇒ze zeʳ = comm∧zeʳ⇒zeˡ zeʳ , zeʳ - comm+almostCancelˡ⇒almostCancelʳ : AlmostLeftCancellative e _∙_ → + comm∧almostCancelˡ⇒almostCancelʳ : AlmostLeftCancellative e _∙_ → AlmostRightCancellative e _∙_ - comm+almostCancelˡ⇒almostCancelʳ cancelˡ-nonZero x y z x≉e yx≈zx = + 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ˡ : AlmostRightCancellative e _∙_ → + comm∧almostCancelʳ⇒almostCancelˡ : AlmostRightCancellative e _∙_ → AlmostLeftCancellative e _∙_ - comm+almostCancelʳ⇒almostCancelˡ cancelʳ-nonZero x y z x≉e xy≈xz = + 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 ⟩ @@ -178,30 +178,30 @@ module _ {_∙_ : Op₂ A} (comm : Commutative _∙_) {e : A} where module _ {_∙_ : Op₂ A} {_⁻¹ : Op₁ A} {e} (comm : Commutative _∙_) where - comm+invˡ⇒invʳ : LeftInverse e _⁻¹ _∙_ → RightInverse e _⁻¹ _∙_ - comm+invˡ⇒invʳ invˡ x = begin + 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 : LeftInverse e _⁻¹ _∙_ → Inverse e _⁻¹ _∙_ - comm+invˡ⇒inv invˡ = invˡ , comm+invˡ⇒invʳ invˡ + comm∧invˡ⇒inv : LeftInverse e _⁻¹ _∙_ → Inverse e _⁻¹ _∙_ + comm∧invˡ⇒inv invˡ = invˡ , comm∧invˡ⇒invʳ invˡ - comm+invʳ⇒invˡ : RightInverse e _⁻¹ _∙_ → LeftInverse e _⁻¹ _∙_ - comm+invʳ⇒invˡ invʳ x = begin + comm∧invʳ⇒invˡ : RightInverse e _⁻¹ _∙_ → LeftInverse e _⁻¹ _∙_ + comm∧invʳ⇒invˡ invʳ x = begin (x ⁻¹) ∙ x ≈⟨ comm (x ⁻¹) x ⟩ x ∙ (x ⁻¹) ≈⟨ invʳ x ⟩ e ∎ - comm+invʳ⇒inv : RightInverse e _⁻¹ _∙_ → Inverse e _⁻¹ _∙_ - comm+invʳ⇒inv invʳ = comm+invʳ⇒invˡ invʳ , invʳ + comm∧invʳ⇒inv : RightInverse e _⁻¹ _∙_ → Inverse e _⁻¹ _∙_ + comm∧invʳ⇒inv invʳ = comm∧invʳ⇒invˡ invʳ , invʳ module _ {_∙_ : Op₂ A} {_⁻¹ : Op₁ A} {e} (cong : Congruent₂ _∙_) where - assoc+id+invʳ⇒invˡ-unique : Associative _∙_ → + 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 + 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 ⁻¹)) ⟩ @@ -209,10 +209,10 @@ module _ {_∙_ : Op₂ A} {_⁻¹ : Op₁ A} {e} (cong : Congruent₂ _∙_) wh e ∙ (y ⁻¹) ≈⟨ idˡ (y ⁻¹) ⟩ y ⁻¹ ∎ - assoc+id+invˡ⇒invʳ-unique : Associative _∙_ → + 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 + 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 ⟩ @@ -228,25 +228,25 @@ module _ {_∙_ _◦_ : Op₂ A} (∙-comm : Commutative _∙_) where - comm+distrˡ⇒distrʳ : _∙_ DistributesOverˡ _◦_ → _∙_ DistributesOverʳ _◦_ - comm+distrˡ⇒distrʳ distrˡ x y z = begin + 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 + 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+distrˡ⇒distr : _∙_ DistributesOverˡ _◦_ → _∙_ DistributesOver _◦_ - comm+distrˡ⇒distr distrˡ = distrˡ , comm+distrˡ⇒distrʳ distrˡ + comm∧distrˡ⇒distr : _∙_ DistributesOverˡ _◦_ → _∙_ DistributesOver _◦_ + comm∧distrˡ⇒distr distrˡ = distrˡ , comm∧distrˡ⇒distrʳ distrˡ - comm+distrʳ⇒distr : _∙_ DistributesOverʳ _◦_ → _∙_ DistributesOver _◦_ - comm+distrʳ⇒distr distrʳ = comm+distrʳ⇒distrˡ distrʳ , distrʳ + comm∧distrʳ⇒distr : _∙_ DistributesOverʳ _◦_ → _∙_ DistributesOver _◦_ + comm∧distrʳ⇒distr distrʳ = comm∧distrʳ⇒distrˡ distrʳ , distrʳ comm⇒sym[distribˡ] : ∀ x → Symmetric (λ y z → (x ◦ (y ∙ z)) ≈ ((x ◦ y) ∙ (x ◦ z))) comm⇒sym[distribˡ] x {y} {z} prf = begin @@ -262,11 +262,11 @@ module _ {_∙_ _◦_ : Op₂ A} (◦-comm : Commutative _◦_) where - distrib+absorbs⇒distribˡ : _∙_ Absorbs _◦_ → + distrib∧absorbs⇒distribˡ : _∙_ Absorbs _◦_ → _◦_ Absorbs _∙_ → _◦_ DistributesOver _∙_ → _∙_ DistributesOverˡ _◦_ - distrib+absorbs⇒distribˡ ∙-absorbs-◦ ◦-absorbs-∙ (◦-distribˡ-∙ , ◦-distribʳ-∙) x y z = begin + distrib∧absorbs⇒distribˡ ∙-absorbs-◦ ◦-absorbs-∙ (◦-distribˡ-∙ , ◦-distribʳ-∙) x y z = begin x ∙ (y ◦ z) ≈⟨ ∙-cong (∙-absorbs-◦ _ _) refl ⟨ (x ∙ (x ◦ y)) ∙ (y ◦ z) ≈⟨ ∙-cong (∙-cong refl (◦-comm _ _)) refl ⟩ (x ∙ (y ◦ x)) ∙ (y ◦ z) ≈⟨ ∙-assoc _ _ _ ⟩ @@ -284,10 +284,10 @@ module _ {_+_ _*_ : Op₂ A} (*-cong : Congruent₂ _*_) 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ˡ +-assoc distribʳ idʳ invʳ x = begin + 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 _ _ _) ⟩ @@ -296,10 +296,10 @@ module _ {_+_ _*_ : Op₂ A} (0# * x) + ((0# * x)⁻¹) ≈⟨ invʳ _ ⟩ 0# ∎ - 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ʳ +-assoc distribˡ idʳ invʳ x = begin + 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 _ _ _) ⟩ @@ -316,10 +316,130 @@ module _ {p} {f : Op₂ A} {P : Pred A p} (comm : Commutative f) where - subst+comm⇒sym : Symmetric (λ a b → P (f a b)) - subst+comm⇒sym = ≈-subst P (comm _ _) + 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 + wlog r-total = Bin.wlog r-total subst∧comm⇒sym + + +------------------------------------------------------------------------ +-- 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+cancelˡ⇒cancelʳ = comm∧cancelˡ⇒cancelʳ +{-# WARNING_ON_USAGE comm+cancelˡ⇒cancelʳ +"Warning: comm+cancelˡ⇒cancelʳ was deprecated in v2.0. +Please use comm∧cancelˡ⇒cancelʳ instead." +#-} +comm+cancelʳ⇒cancelˡ = comm∧cancelʳ⇒cancelˡ +{-# WARNING_ON_USAGE comm+cancelʳ⇒cancelˡ +"Warning: comm+cancelʳ⇒cancelˡ was deprecated in v2.0. +Please use comm∧cancelʳ⇒cancelˡ instead." +#-} +comm+idˡ⇒idʳ = comm∧idˡ⇒idʳ +{-# WARNING_ON_USAGE comm+idˡ⇒idʳ +"Warning: comm+idˡ⇒idʳ was deprecated in v2.0. +Please use comm∧idˡ⇒idʳ instead." +#-} +comm+idʳ⇒idˡ = comm∧idʳ⇒idˡ +{-# WARNING_ON_USAGE comm+idʳ⇒idˡ +"Warning: comm+idʳ⇒idˡ was deprecated in v2.0. +Please use comm∧idʳ⇒idˡ instead." +#-} +comm+zeˡ⇒zeʳ = comm∧zeˡ⇒zeʳ +{-# WARNING_ON_USAGE comm+zeˡ⇒zeʳ +"Warning: comm+zeˡ⇒zeʳ was deprecated in v2.0. +Please use comm∧zeˡ⇒zeʳ instead." +#-} +comm+zeʳ⇒zeˡ = comm∧zeʳ⇒zeˡ +{-# WARNING_ON_USAGE comm+zeʳ⇒zeˡ +"Warning: comm+zeʳ⇒zeˡ was deprecated in v2.0. +Please use comm∧zeʳ⇒zeˡ instead." +#-} +comm+almostCancelˡ⇒almostCancelʳ = comm∧almostCancelˡ⇒almostCancelʳ +{-# WARNING_ON_USAGE comm+almostCancelˡ⇒almostCancelʳ +"Warning: comm+almostCancelˡ⇒almostCancelʳ was deprecated in v2.0. +Please use comm∧almostCancelˡ⇒almostCancelʳ instead." +#-} +comm+almostCancelʳ⇒almostCancelˡ = comm∧almostCancelʳ⇒almostCancelˡ +{-# WARNING_ON_USAGE comm+almostCancelʳ⇒almostCancelˡ +"Warning: comm+almostCancelʳ⇒almostCancelˡ was deprecated in v2.0. +Please use comm∧almostCancelʳ⇒almostCancelˡ instead." +#-} +comm+invˡ⇒invʳ = comm∧invˡ⇒invʳ +{-# WARNING_ON_USAGE comm+invˡ⇒invʳ +"Warning: comm+invˡ⇒invʳ was deprecated in v2.0. +Please use comm∧invˡ⇒invʳ instead." +#-} +comm+invʳ⇒invˡ = comm∧invʳ⇒invˡ +{-# WARNING_ON_USAGE comm+invʳ⇒invˡ +"Warning: comm+invʳ⇒invˡ was deprecated in v2.0. +Please use comm∧invʳ⇒invˡ instead." +#-} +comm+invˡ⇒inv = comm∧invˡ⇒inv +{-# WARNING_ON_USAGE comm+invˡ⇒inv +"Warning: comm+invˡ⇒inv was deprecated in v2.0. +Please use comm∧invˡ⇒inv instead." +#-} +comm+invʳ⇒inv = comm∧invʳ⇒inv +{-# WARNING_ON_USAGE comm+invʳ⇒inv +"Warning: comm+invʳ⇒inv was deprecated in v2.0. +Please use comm∧invʳ⇒inv 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." +#-} diff --git a/src/Algebra/Lattice/Properties/BooleanAlgebra.agda b/src/Algebra/Lattice/Properties/BooleanAlgebra.agda index 450527ddc0..702e9fa1c8 100644 --- a/src/Algebra/Lattice/Properties/BooleanAlgebra.agda +++ b/src/Algebra/Lattice/Properties/BooleanAlgebra.agda @@ -57,7 +57,7 @@ open DistribLatticeProperties distributiveLattice public x ∎ ∧-identityˡ : LeftIdentity ⊤ _∧_ -∧-identityˡ = comm+idʳ⇒idˡ ∧-comm ∧-identityʳ +∧-identityˡ = comm∧idʳ⇒idˡ ∧-comm ∧-identityʳ ∧-identity : Identity ⊤ _∧_ ∧-identity = ∧-identityˡ , ∧-identityʳ @@ -69,7 +69,7 @@ open DistribLatticeProperties distributiveLattice public x ∎ ∨-identityˡ : LeftIdentity ⊥ _∨_ -∨-identityˡ = comm+idʳ⇒idˡ ∨-comm ∨-identityʳ +∨-identityˡ = comm∧idʳ⇒idˡ ∨-comm ∨-identityʳ ∨-identity : Identity ⊥ _∨_ ∨-identity = ∨-identityˡ , ∨-identityʳ @@ -83,7 +83,7 @@ open DistribLatticeProperties distributiveLattice public ⊥ ∎ ∧-zeroˡ : LeftZero ⊥ _∧_ -∧-zeroˡ = comm+zeʳ⇒zeˡ ∧-comm ∧-zeroʳ +∧-zeroˡ = comm∧zeʳ⇒zeˡ ∧-comm ∧-zeroʳ ∧-zero : Zero ⊥ _∧_ ∧-zero = ∧-zeroˡ , ∧-zeroʳ @@ -97,7 +97,7 @@ open DistribLatticeProperties distributiveLattice public ⊤ ∎ ∨-zeroˡ : LeftZero ⊤ _∨_ -∨-zeroˡ = comm+zeʳ⇒zeˡ ∨-comm ∨-zeroʳ +∨-zeroˡ = comm∧zeʳ⇒zeˡ ∨-comm ∨-zeroʳ ∨-zero : Zero ⊤ _∨_ ∨-zero = ∨-zeroˡ , ∨-zeroʳ @@ -377,7 +377,7 @@ module XorRing (x ∧ (y ∨ z)) ∧ ¬ x ∎ ∧-distribʳ-⊕ : _∧_ DistributesOverʳ _⊕_ - ∧-distribʳ-⊕ = comm+distrˡ⇒distrʳ ⊕-cong ∧-comm ∧-distribˡ-⊕ + ∧-distribʳ-⊕ = comm∧distrˡ⇒distrʳ ⊕-cong ∧-comm ∧-distribˡ-⊕ ∧-distrib-⊕ : _∧_ DistributesOver _⊕_ ∧-distrib-⊕ = ∧-distribˡ-⊕ , ∧-distribʳ-⊕ diff --git a/src/Algebra/Lattice/Structures/Biased.agda b/src/Algebra/Lattice/Structures/Biased.agda index b5e1e6c9fd..5da9714354 100644 --- a/src/Algebra/Lattice/Structures/Biased.agda +++ b/src/Algebra/Lattice/Structures/Biased.agda @@ -82,9 +82,9 @@ record IsDistributiveLatticeʳʲᵐ (∨ ∧ : Op₂ A) : Set (a ⊔ ℓ) where setoid : Setoid a ℓ setoid = record { isEquivalence = isEquivalence } - ∨-distrib-∧ = comm+distrʳ⇒distr setoid ∧-cong ∨-comm ∨-distribʳ-∧ - ∧-distribˡ-∨ = distrib+absorbs⇒distribˡ setoid ∧-cong ∧-assoc ∨-comm ∧-absorbs-∨ ∨-absorbs-∧ ∨-distrib-∧ - ∧-distrib-∨ = comm+distrˡ⇒distr setoid ∨-cong ∧-comm ∧-distribˡ-∨ + ∨-distrib-∧ = comm∧distrʳ⇒distr setoid ∧-cong ∨-comm ∨-distribʳ-∧ + ∧-distribˡ-∨ = distrib∧absorbs⇒distribˡ setoid ∧-cong ∧-assoc ∨-comm ∧-absorbs-∨ ∨-absorbs-∧ ∨-distrib-∧ + ∧-distrib-∨ = comm∧distrˡ⇒distr setoid ∨-cong ∧-comm ∧-distribˡ-∨ isDistributiveLatticeʳʲᵐ : IsDistributiveLattice ∨ ∧ isDistributiveLatticeʳʲᵐ = record @@ -115,8 +115,8 @@ record IsBooleanAlgebraʳ isBooleanAlgebraʳ : IsBooleanAlgebra ∨ ∧ ¬ ⊤ ⊥ isBooleanAlgebraʳ = record { isDistributiveLattice = isDistributiveLattice - ; ∨-complement = comm+invʳ⇒inv setoid ∨-comm ∨-complementʳ - ; ∧-complement = comm+invʳ⇒inv setoid ∧-comm ∧-complementʳ + ; ∨-complement = comm∧invʳ⇒inv setoid ∨-comm ∨-complementʳ + ; ∧-complement = comm∧invʳ⇒inv setoid ∧-comm ∧-complementʳ ; ¬-cong = ¬-cong } diff --git a/src/Algebra/Structures.agda b/src/Algebra/Structures.agda index ed55226d67..237e50a876 100644 --- a/src/Algebra/Structures.agda +++ b/src/Algebra/Structures.agda @@ -264,11 +264,11 @@ record IsGroup (_∙_ : Op₂ A) (ε : A) (_⁻¹ : Op₁ A) : Set (a ⊔ ℓ) w inverseʳ = proj₂ inverse uniqueˡ-⁻¹ : ∀ x y → (x ∙ y) ≈ ε → x ≈ (y ⁻¹) - uniqueˡ-⁻¹ = Consequences.assoc+id+invʳ⇒invˡ-unique + uniqueˡ-⁻¹ = Consequences.assoc∧id∧invʳ⇒invˡ-unique setoid ∙-cong assoc identity inverseʳ uniqueʳ-⁻¹ : ∀ x y → (x ∙ y) ≈ ε → y ≈ (x ⁻¹) - uniqueʳ-⁻¹ = Consequences.assoc+id+invˡ⇒invʳ-unique + uniqueʳ-⁻¹ = Consequences.assoc∧id∧invˡ⇒invʳ-unique setoid ∙-cong assoc identity inverseˡ isInvertibleMagma : IsInvertibleMagma _∙_ ε _⁻¹ diff --git a/src/Algebra/Structures/Biased.agda b/src/Algebra/Structures/Biased.agda index c0c6994e3f..cb730e9ba6 100644 --- a/src/Algebra/Structures/Biased.agda +++ b/src/Algebra/Structures/Biased.agda @@ -36,7 +36,7 @@ record IsCommutativeMonoidˡ (∙ : Op₂ A) (ε : A) : Set (a ⊔ ℓ) where isCommutativeMonoid = record { isMonoid = record { isSemigroup = isSemigroup - ; identity = comm+idˡ⇒id setoid comm identityˡ + ; identity = comm∧idˡ⇒id setoid comm identityˡ } ; comm = comm } where open IsSemigroup isSemigroup @@ -55,7 +55,7 @@ record IsCommutativeMonoidʳ (∙ : Op₂ A) (ε : A) : Set (a ⊔ ℓ) where isCommutativeMonoid = record { isMonoid = record { isSemigroup = isSemigroup - ; identity = comm+idʳ⇒id setoid comm identityʳ + ; identity = comm∧idʳ⇒id setoid comm identityʳ } ; comm = comm } where open IsSemigroup isSemigroup @@ -146,9 +146,9 @@ record IsCommutativeSemiringˡ (+ * : Op₂ A) (0# 1# : A) : Set (a ⊔ ℓ) whe ; *-cong = *.∙-cong ; *-assoc = *.assoc ; *-identity = *.identity - ; distrib = comm+distrʳ⇒distr +.setoid +.∙-cong *.comm distribʳ + ; distrib = comm∧distrʳ⇒distr +.setoid +.∙-cong *.comm distribʳ } - ; zero = comm+zeˡ⇒ze +.setoid *.comm zeroˡ + ; zero = comm∧zeˡ⇒ze +.setoid *.comm zeroˡ } ; *-comm = *.comm } @@ -175,9 +175,9 @@ record IsCommutativeSemiringʳ (+ * : Op₂ A) (0# 1# : A) : Set (a ⊔ ℓ) whe ; *-cong = *.∙-cong ; *-assoc = *.assoc ; *-identity = *.identity - ; distrib = comm+distrˡ⇒distr +.setoid +.∙-cong *.comm distribˡ + ; distrib = comm∧distrˡ⇒distr +.setoid +.∙-cong *.comm distribˡ } - ; zero = comm+zeʳ⇒ze +.setoid *.comm zeroʳ + ; zero = comm∧zeʳ⇒ze +.setoid *.comm zeroʳ } ; *-comm = *.comm } @@ -207,11 +207,11 @@ record IsRingWithoutAnnihilatingZero (+ * : Op₂ A) (-_ : Op₁ A) (0# 1# : A) open * using () renaming (∙-cong to *-cong) zeroˡ : LeftZero 0# * - zeroˡ = assoc+distribʳ+idʳ+invʳ⇒zeˡ setoid + zeroˡ = assoc∧distribʳ∧idʳ∧invʳ⇒zeˡ setoid +-cong *-cong +.assoc (proj₂ distrib) +.identityʳ +.inverseʳ zeroʳ : RightZero 0# * - zeroʳ = assoc+distribˡ+idʳ+invʳ⇒zeʳ setoid + zeroʳ = assoc∧distribˡ∧idʳ∧invʳ⇒zeʳ setoid +-cong *-cong +.assoc (proj₁ distrib) +.identityʳ +.inverseʳ zero : Zero 0# * diff --git a/src/Data/Integer/Properties.agda b/src/Data/Integer/Properties.agda index 43152bceee..01bdfcfe0c 100644 --- a/src/Data/Integer/Properties.agda +++ b/src/Data/Integer/Properties.agda @@ -810,7 +810,7 @@ sign-⊖-≰ = sign-⊖-< ∘ ℕ.≰⇒> +-identityˡ (+ _) = refl +-identityʳ : RightIdentity +0 _+_ -+-identityʳ = comm+idˡ⇒idʳ +-comm +-identityˡ ++-identityʳ = comm∧idˡ⇒idʳ +-comm +-identityˡ +-identity : Identity +0 _+_ +-identity = +-identityˡ , +-identityʳ @@ -904,7 +904,7 @@ distribʳ-⊖-+-neg m n o = begin +-inverseˡ +[1+ n ] = n⊖n≡0 (suc n) +-inverseʳ : RightInverse +0 -_ _+_ -+-inverseʳ = comm+invˡ⇒invʳ +-comm +-inverseˡ ++-inverseʳ = comm∧invˡ⇒invʳ +-comm +-inverseˡ +-inverse : Inverse +0 -_ _+_ +-inverse = +-inverseˡ , +-inverseʳ @@ -1319,7 +1319,7 @@ pred-mono (+≤+ m≤n) = ⊖-monoˡ-≤ 1 m≤n *-identityˡ +[1+ n ] rewrite ℕ.+-identityʳ n = refl *-identityʳ : RightIdentity 1ℤ _*_ -*-identityʳ = comm+idˡ⇒idʳ *-comm *-identityˡ +*-identityʳ = comm∧idˡ⇒idʳ *-comm *-identityˡ *-identity : Identity 1ℤ _*_ *-identity = *-identityˡ , *-identityʳ @@ -1328,7 +1328,7 @@ pred-mono (+≤+ m≤n) = ⊖-monoˡ-≤ 1 m≤n *-zeroˡ _ = refl *-zeroʳ : RightZero 0ℤ _*_ -*-zeroʳ = comm+zeˡ⇒zeʳ *-comm *-zeroˡ +*-zeroʳ = comm∧zeˡ⇒zeʳ *-comm *-zeroˡ *-zero : Zero 0ℤ _*_ *-zero = *-zeroˡ , *-zeroʳ @@ -1469,7 +1469,7 @@ private = refl *-distribˡ-+ : _*_ DistributesOverˡ _+_ -*-distribˡ-+ = comm+distrʳ⇒distrˡ *-comm *-distribʳ-+ +*-distribˡ-+ = comm∧distrʳ⇒distrˡ *-comm *-distribʳ-+ *-distrib-+ : _*_ DistributesOver _+_ *-distrib-+ = *-distribˡ-+ , *-distribʳ-+ diff --git a/src/Data/Nat/Binary/Properties.agda b/src/Data/Nat/Binary/Properties.agda index f83bbfc12c..4f0dc58e73 100644 --- a/src/Data/Nat/Binary/Properties.agda +++ b/src/Data/Nat/Binary/Properties.agda @@ -1077,7 +1077,7 @@ private where open ≡-Reasoning; k = toℕ a; m = toℕ b; n = toℕ c *-distribʳ-+ : _*_ DistributesOverʳ _+_ -*-distribʳ-+ = comm+distrˡ⇒distrʳ *-comm *-distribˡ-+ +*-distribʳ-+ = comm∧distrˡ⇒distrʳ *-comm *-distribˡ-+ *-distrib-+ : _*_ DistributesOver _+_ *-distrib-+ = *-distribˡ-+ , *-distribʳ-+ diff --git a/src/Data/Nat/Binary/Subtraction.agda b/src/Data/Nat/Binary/Subtraction.agda index 48eb4b4ae7..a4d0ba125d 100644 --- a/src/Data/Nat/Binary/Subtraction.agda +++ b/src/Data/Nat/Binary/Subtraction.agda @@ -9,7 +9,7 @@ module Data.Nat.Binary.Subtraction where open import Algebra using (Op₂; Magma) -open import Algebra.Consequences.Propositional using (comm+distrˡ⇒distrʳ) +open import Algebra.Consequences.Propositional using (comm∧distrˡ⇒distrʳ) open import Algebra.Morphism.Consequences using (homomorphic₂-inv) open import Data.Bool.Base using (true; false) open import Data.Nat as ℕ using (ℕ) @@ -237,7 +237,7 @@ x∸y