[ bug ] Fix use of + in lemma preconditions in favour of ∧ (bis) (#2578)

* fix: knock-ons from #2168

* fix: knock-ons from #2168

* fix: knock-ons from #2168

* fix: more names cf. #2168

* fix: knock-ons

* add: deprecations

Author: jamesmckinna

CHANGELOG.md

@@ -32,6 +32,14 @@ Deprecated names
   _∤∤_    ↦  _∦_
   ```
 
+* In `Algebra.Module.Consequences
+  ```agda
+  *ₗ-assoc+comm⇒*ᵣ-assoc      ↦  *ₗ-assoc∧comm⇒*ᵣ-assoc
+  *ₗ-assoc+comm⇒*ₗ-*ᵣ-assoc   ↦  *ₗ-assoc∧comm⇒*ₗ-*ᵣ-assoc
+  *ᵣ-assoc+comm⇒*ₗ-assoc      ↦  *ᵣ-assoc∧comm⇒*ₗ-assoc
+  *ₗ-assoc+comm⇒*ₗ-*ᵣ-assoc   ↦  *ₗ-assoc∧comm⇒*ₗ-*ᵣ-assoc
+  ```
+
 * In `Algebra.Properties.Magma.Divisibility`:
   ```agda
   ∣∣-sym       ↦  ∥-sym

src/Algebra/Construct/NaturalChoice/MinMaxOp.agda

@@ -59,7 +59,7 @@ open import Algebra.Construct.NaturalChoice.MaxOp maxOp public
   (x ⊓ y) ⊔ (x ⊓ z) ∎
 
 ⊓-distribʳ-⊔ : _⊓_ DistributesOverʳ _⊔_
-⊓-distribʳ-⊔ = comm+distrˡ⇒distrʳ ⊔-cong ⊓-comm ⊓-distribˡ-⊔
+⊓-distribʳ-⊔ = comm∧distrˡ⇒distrʳ ⊔-cong ⊓-comm ⊓-distribˡ-⊔
 
 ⊓-distrib-⊔ : _⊓_ DistributesOver _⊔_
 ⊓-distrib-⊔ = ⊓-distribˡ-⊔ , ⊓-distribʳ-⊔
@@ -76,7 +76,7 @@ open import Algebra.Construct.NaturalChoice.MaxOp maxOp public
   (x ⊔ y) ⊓ (x ⊔ z) ∎
 
 ⊔-distribʳ-⊓ : _⊔_ DistributesOverʳ _⊓_
-⊔-distribʳ-⊓ = comm+distrˡ⇒distrʳ ⊓-cong ⊔-comm ⊔-distribˡ-⊓
+⊔-distribʳ-⊓ = comm∧distrˡ⇒distrʳ ⊓-cong ⊔-comm ⊔-distribˡ-⊓
 
 ⊔-distrib-⊓ : _⊔_ DistributesOver _⊓_
 ⊔-distrib-⊓ = ⊔-distribˡ-⊓ , ⊔-distribʳ-⊓

src/Algebra/Module/Consequences.agda

@@ -40,20 +40,20 @@ module _ (_≈ᴬ_ : Rel {a} A ℓa) (S : Setoid c ℓ) where
     private
       _*ᵣ_ = flip _*ₗ_
 
-    *ₗ-assoc+comm⇒*ᵣ-assoc :
+    *ₗ-assoc∧comm⇒*ᵣ-assoc :
       L.RightCongruent _≈ᴬ_ _*ₗ_ →
       L.Associative _*_ _*ₗ_ → Commutative _*_ → R.Associative _*_ _*ᵣ_
-    *ₗ-assoc+comm⇒*ᵣ-assoc *ₗ-congʳ *ₗ-assoc *-comm m x y = begin
+    *ₗ-assoc∧comm⇒*ᵣ-assoc *ₗ-congʳ *ₗ-assoc *-comm m x y = begin
       (m *ᵣ x) *ᵣ y  ≈⟨ refl ⟩
       y *ₗ (x *ₗ m)  ≈⟨ *ₗ-assoc _ _ _ ⟨
       (y * x) *ₗ m   ≈⟨ *ₗ-congʳ (*-comm y x) ⟩
       (x * y) *ₗ m   ≈⟨ refl ⟩
       m *ᵣ (x * y)   ∎
 
-    *ₗ-assoc+comm⇒*ₗ-*ᵣ-assoc :
+    *ₗ-assoc∧comm⇒*ₗ-*ᵣ-assoc :
       L.RightCongruent _≈ᴬ_ _*ₗ_ →
       L.Associative _*_ _*ₗ_ → Commutative _*_ → B.Associative _*ₗ_ _*ᵣ_
-    *ₗ-assoc+comm⇒*ₗ-*ᵣ-assoc *ₗ-congʳ *ₗ-assoc *-comm x m y = begin
+    *ₗ-assoc∧comm⇒*ₗ-*ᵣ-assoc *ₗ-congʳ *ₗ-assoc *-comm x m y = begin
       ((x *ₗ m) *ᵣ y)  ≈⟨ refl ⟩
       (y *ₗ (x *ₗ m))  ≈⟨ *ₗ-assoc _ _ _ ⟨
       ((y * x) *ₗ m)   ≈⟨ *ₗ-congʳ (*-comm y x) ⟩
@@ -66,23 +66,56 @@ module _ (_≈ᴬ_ : Rel {a} A ℓa) (S : Setoid c ℓ) where
     private
       _*ₗ_ = flip _*ᵣ_
 
-    *ᵣ-assoc+comm⇒*ₗ-assoc :
+    *ᵣ-assoc∧comm⇒*ₗ-assoc :
       R.LeftCongruent _≈ᴬ_ _*ᵣ_ →
       R.Associative _*_ _*ᵣ_ → Commutative _*_ → L.Associative _*_ _*ₗ_
-    *ᵣ-assoc+comm⇒*ₗ-assoc *ᵣ-congˡ *ᵣ-assoc *-comm x y m = begin
+    *ᵣ-assoc∧comm⇒*ₗ-assoc *ᵣ-congˡ *ᵣ-assoc *-comm x y m = begin
       ((x * y) *ₗ m)   ≈⟨ refl ⟩
       (m *ᵣ (x * y))   ≈⟨ *ᵣ-congˡ (*-comm x y) ⟩
       (m *ᵣ (y * x))   ≈⟨ *ᵣ-assoc _ _ _ ⟨
       ((m *ᵣ y) *ᵣ x)  ≈⟨ refl ⟩
       (x *ₗ (y *ₗ m))  ∎
 
-    *ᵣ-assoc+comm⇒*ₗ-*ᵣ-assoc :
+    *ᵣ-assoc∧comm⇒*ₗ-*ᵣ-assoc :
       R.LeftCongruent _≈ᴬ_ _*ᵣ_ →
       R.Associative _*_ _*ᵣ_ → Commutative _*_ → B.Associative _*ₗ_ _*ᵣ_
-    *ᵣ-assoc+comm⇒*ₗ-*ᵣ-assoc *ᵣ-congˡ *ᵣ-assoc *-comm x m y = begin
+    *ᵣ-assoc∧comm⇒*ₗ-*ᵣ-assoc *ᵣ-congˡ *ᵣ-assoc *-comm x m y = begin
       ((x *ₗ m) *ᵣ y)  ≈⟨ refl ⟩
       ((m *ᵣ x) *ᵣ y)  ≈⟨ *ᵣ-assoc _ _ _ ⟩
       (m *ᵣ (x * y))   ≈⟨ *ᵣ-congˡ (*-comm x y) ⟩
       (m *ᵣ (y * x))   ≈⟨ *ᵣ-assoc _ _ _ ⟨
       ((m *ᵣ y) *ᵣ x)  ≈⟨ refl ⟩
       (x *ₗ (m *ᵣ y))  ∎
+
+
+------------------------------------------------------------------------
+-- DEPRECATED NAMES
+------------------------------------------------------------------------
+-- Please use the new names as continuing support for the old names is
+-- not guaranteed.
+
+-- Version 2.3
+
+*ₗ-assoc+comm⇒*ᵣ-assoc = *ₗ-assoc∧comm⇒*ᵣ-assoc
+{-# WARNING_ON_USAGE *ₗ-assoc+comm⇒*ᵣ-assoc
+"Warning: *ₗ-assoc+comm⇒*ᵣ-assoc was deprecated in v2.3.
+Please use *ₗ-assoc∧comm⇒*ᵣ-assoc instead."
+#-}
+
+*ₗ-assoc+comm⇒*ₗ-*ᵣ-assoc = *ₗ-assoc∧comm⇒*ₗ-*ᵣ-assoc
+{-# WARNING_ON_USAGE *ₗ-assoc+comm⇒*ₗ-*ᵣ-assoc
+"Warning: *ₗ-assoc+comm⇒*ₗ-*ᵣ-assoc was deprecated in v2.3.
+Please use *ₗ-assoc∧comm⇒*ₗ-*ᵣ-assoc instead."
+#-}
+
+*ᵣ-assoc+comm⇒*ₗ-assoc = *ᵣ-assoc∧comm⇒*ₗ-assoc
+{-# WARNING_ON_USAGE *ᵣ-assoc+comm⇒*ₗ-assoc
+"Warning: *ᵣ-assoc+comm⇒*ₗ-assoc was deprecated in v2.3.
+Please use *ᵣ-assoc∧comm⇒*ₗ-assoc instead."
+#-}
+
+*ᵣ-assoc+comm⇒*ₗ-*ᵣ-assoc = *ᵣ-assoc∧comm⇒*ₗ-*ᵣ-assoc
+{-# WARNING_ON_USAGE *ᵣ-assoc+comm⇒*ₗ-*ᵣ-assoc
+"Warning: *ᵣ-assoc+comm⇒*ₗ-*ᵣ-assoc was deprecated in v2.3.
+Please use *ᵣ-assoc∧comm⇒*ₗ-*ᵣ-assoc instead."
+#-}

src/Algebra/Module/Structures/Biased.agda

@@ -48,12 +48,12 @@ module _ (commutativeSemiring : CommutativeSemiring r ℓr) where
         ; *ᵣ-distribˡ = *ₗ-distribʳ
         ; *ᵣ-identityʳ = *ₗ-identityˡ
         ; *ᵣ-assoc =
-          *ₗ-assoc+comm⇒*ᵣ-assoc _≈_ ≈ᴹ-setoid *ₗ-congʳ *ₗ-assoc *-comm
+          *ₗ-assoc∧comm⇒*ᵣ-assoc _≈_ ≈ᴹ-setoid *ₗ-congʳ *ₗ-assoc *-comm
         ; *ᵣ-zeroˡ = *ₗ-zeroʳ
         ; *ᵣ-distribʳ = *ₗ-distribˡ
         }
       ; *ₗ-*ᵣ-assoc =
-        *ₗ-assoc+comm⇒*ₗ-*ᵣ-assoc _≈_ ≈ᴹ-setoid *ₗ-congʳ *ₗ-assoc *-comm
+        *ₗ-assoc∧comm⇒*ₗ-*ᵣ-assoc _≈_ ≈ᴹ-setoid *ₗ-congʳ *ₗ-assoc *-comm
       }
 
     isSemimodule : IsSemimodule commutativeSemiring ≈ᴹ +ᴹ 0ᴹ *ₗ (flip *ₗ)
@@ -81,13 +81,13 @@ module _ (commutativeSemiring : CommutativeSemiring r ℓr) where
         ; *ₗ-distribʳ = *ᵣ-distribˡ
         ; *ₗ-identityˡ = *ᵣ-identityʳ
         ; *ₗ-assoc =
-          *ᵣ-assoc+comm⇒*ₗ-assoc _≈_ ≈ᴹ-setoid *ᵣ-congˡ *ᵣ-assoc *-comm
+          *ᵣ-assoc∧comm⇒*ₗ-assoc _≈_ ≈ᴹ-setoid *ᵣ-congˡ *ᵣ-assoc *-comm
         ; *ₗ-zeroʳ = *ᵣ-zeroˡ
         ; *ₗ-distribˡ = *ᵣ-distribʳ
         }
       ; isPrerightSemimodule = isPrerightSemimodule
       ; *ₗ-*ᵣ-assoc =
-        *ᵣ-assoc+comm⇒*ₗ-*ᵣ-assoc _≈_ ≈ᴹ-setoid *ᵣ-congˡ *ᵣ-assoc *-comm
+        *ᵣ-assoc∧comm⇒*ₗ-*ᵣ-assoc _≈_ ≈ᴹ-setoid *ᵣ-congˡ *ᵣ-assoc *-comm
       }
 
     isSemimodule : IsSemimodule commutativeSemiring ≈ᴹ +ᴹ 0ᴹ (flip *ᵣ) *ᵣ

src/Algebra/Properties/CancellativeCommutativeSemiring.agda

@@ -22,7 +22,7 @@ open import Algebra.Consequences.Setoid setoid
 open import Relation.Binary.Reasoning.Setoid setoid
 
 *-almostCancelʳ : AlmostRightCancellative _≈_ 0# _*_
-*-almostCancelʳ = comm+almostCancelˡ⇒almostCancelʳ *-comm *-cancelˡ-nonZero
+*-almostCancelʳ = comm∧almostCancelˡ⇒almostCancelʳ *-comm *-cancelˡ-nonZero
 
 xy≈0⇒x≈0∨y≈0 : Decidable _≈_ → ∀ {x y} → x * y ≈ 0# → x ≈ 0# ⊎ y ≈ 0#
 xy≈0⇒x≈0∨y≈0 _≟_ {x} {y} xy≈0 with x ≟ 0# | y ≟ 0#

src/Data/Rational/Unnormalised/Properties.agda

@@ -746,7 +746,7 @@ neg⇒nonZero (mkℚᵘ (-[1+ _ ]) _) = _
 +-identityˡ p = ≃-reflexive (+-identityˡ-≡ p)
 
 +-identityʳ-≡ : RightIdentity _≡_ 0ℚᵘ _+_
-+-identityʳ-≡ = comm+idˡ⇒idʳ +-comm-≡ {e = 0ℚᵘ} +-identityˡ-≡
++-identityʳ-≡ = comm∧idˡ⇒idʳ +-comm-≡ {e = 0ℚᵘ} +-identityˡ-≡
 
 +-identityʳ : RightIdentity _≃_ 0ℚᵘ _+_
 +-identityʳ p = ≃-reflexive (+-identityʳ-≡ p)
@@ -1104,7 +1104,7 @@ p≤q⇒0≤q-p {p} {q} p≤q = begin
 *-identityˡ-≡ p@record{} = ↥↧≡⇒≡ (ℤ.*-identityˡ (↥ p)) (ℕ.+-identityʳ (↧ₙ p))
 
 *-identityʳ-≡ : RightIdentity _≡_ 1ℚᵘ _*_
-*-identityʳ-≡ = comm+idˡ⇒idʳ *-comm-≡ {e = 1ℚᵘ} *-identityˡ-≡
+*-identityʳ-≡ = comm∧idˡ⇒idʳ *-comm-≡ {e = 1ℚᵘ} *-identityˡ-≡
 
 *-identity-≡ : Identity _≡_ 1ℚᵘ _*_
 *-identity-≡ = *-identityˡ-≡ , *-identityʳ-≡
@@ -1144,7 +1144,7 @@ p≤q⇒0≤q-p {p} {q} p≤q = begin
 *-zeroˡ p@record{} = *≡* refl
 
 *-zeroʳ : RightZero _≃_ 0ℚᵘ _*_
-*-zeroʳ = Consequences.comm+zeˡ⇒zeʳ ≃-setoid *-comm *-zeroˡ
+*-zeroʳ = Consequences.comm∧zeˡ⇒zeʳ ≃-setoid *-comm *-zeroˡ
 
 *-zero : Zero _≃_ 0ℚᵘ _*_
 *-zero = *-zeroˡ , *-zeroʳ
@@ -1171,7 +1171,7 @@ invertible⇒≄ {p} {q} (1/p-q , 1/x*x≃1 , x*1/x≃1) p≃q = 0≄1 (begin
   in *≡* eq where open ℤ-solver
 
 *-distribʳ-+ : _DistributesOverʳ_ _≃_ _*_ _+_
-*-distribʳ-+ = Consequences.comm+distrˡ⇒distrʳ ≃-setoid +-cong *-comm *-distribˡ-+
+*-distribʳ-+ = Consequences.comm∧distrˡ⇒distrʳ ≃-setoid +-cong *-comm *-distribˡ-+
 
 *-distrib-+ : _DistributesOver_ _≃_ _*_ _+_
 *-distrib-+ = *-distribˡ-+ , *-distribʳ-+