[ refactor ] Restate, and use, the definitions of Monotonic etc. operations

CHANGELOG.md

@@ -152,6 +152,21 @@ New modules
 Additions to existing modules
 -----------------------------
 
+* In `Algebra.Consequences.Base`:
+  ```agda
+  module Congruence (_≈_ : Rel A ℓ) (cong : Congruent₂ _≈_ _∙_) (refl : Reflexive _≈_)
+  where
+    ∙-congˡ : LeftCongruent _≈_ _∙_
+    ∙-congʳ : RightCongruent _≈_ _∙_
+  ```
+
+* In `Algebra.Consequences.Setoid`:
+  ```agda
+  module Congruence (cong : Congruent₂ _≈_ _∙_) where
+    ∙-congˡ : LeftCongruent _≈_ _∙_
+    ∙-congʳ : RightCongruent _≈_ _∙_
+  ```
+
 * In `Algebra.Construct.Pointwise`:
   ```agda
   isNearSemiring                  : IsNearSemiring _≈_ _+_ _*_ 0# →
@@ -232,13 +247,28 @@ Additions to existing modules
   filter-↭ : ∀ (P? : Pred.Decidable P) → xs ↭ ys → filter P? xs ↭ filter P? ys
   ```
 
+* In `Relation.Binary.Consequences`:
+  ```agda
+  mono₂⇒monoˡ : Reflexive ≤₁ → Monotonic₂ ≤₁ ≤₂ ≤₃ f → LeftMonotonic ≤₂ ≤₃ f
+  mono₂⇒monoˡ : Reflexive ≤₂ → Monotonic₂ ≤₁ ≤₂ ≤₃ f → RightMonotonic ≤₁ ≤₃ f
+  monoˡ∧monoʳ⇒mono₂ : Transitive ≤₃ →
+                      LeftMonotonic ≤₂ ≤₃ f → RightMonotonic ≤₁ ≤₃ f →
+                      Monotonic₂ ≤₁ ≤₂ ≤₃ f
+  ```
+
 * In `Relation.Binary.Construct.Add.Infimum.Strict`:
   ```agda
   <₋-accessible-⊥₋ : Acc _<₋_ ⊥₋
   <₋-accessible[_] : Acc _<_ x → Acc _<₋_ [ x ]
   <₋-wellFounded   : WellFounded _<_ → WellFounded _<₋_
   ```
 
+* In `Relation.Binary.Definitions`:
+  ```agda
+  LeftMonotonic  : Rel B ℓ₁ → Rel C ℓ₂ → (A → B → C) → Set _
+  RightMonotonic : Rel A ℓ₁ → Rel C ℓ₂ → (A → B → C) → Set _
+  ```
+
 * In `Relation.Nullary.Decidable.Core`:
   ```agda
   ⊤-dec : Dec {a} ⊤

src/Algebra/Consequences/Base.agda

@@ -11,22 +11,35 @@ module Algebra.Consequences.Base
   {a} {A : Set a} where
 
 open import Algebra.Core using (Op₁; Op₂)
-open import Algebra.Definitions
-  using (Selective; Idempotent; SelfInverse; Involutive)
+import Algebra.Definitions as Definitions
+  using (Congruent₂; LeftCongruent; RightCongruent
+        ; Selective; Idempotent; SelfInverse; Involutive)
 open import Data.Sum.Base using (_⊎_; reduce)
+open import Relation.Binary.Consequences
+  using (mono₂⇒monoˡ; mono₂⇒monoʳ)
 open import Relation.Binary.Core using (Rel)
 open import Relation.Binary.Definitions using (Reflexive)
 
-module _ {ℓ} {_•_ : Op₂ A} (_≈_ : Rel A ℓ) where
+module Congruence {ℓ} {_∙_ : Op₂ A} (_≈_ : Rel A ℓ) (open Definitions _≈_)
+                  (cong : Congruent₂ _∙_) (refl : Reflexive _≈_)
+  where
 
-  sel⇒idem : Selective _≈_ _•_ → Idempotent _≈_ _•_
+  ∙-congˡ : LeftCongruent _∙_
+  ∙-congˡ {x} = mono₂⇒monoˡ _ _≈_ _≈_ (refl {x = x}) cong x
+
+  ∙-congʳ : RightCongruent _∙_
+  ∙-congʳ {x} = mono₂⇒monoʳ _≈_ _ _≈_ (refl {x = x}) cong x
+
+module _ {ℓ} {_∙_ : Op₂ A} (_≈_ : Rel A ℓ) (open Definitions _≈_) where
+
+  sel⇒idem : Selective _∙_ → Idempotent _∙_
   sel⇒idem sel x = reduce (sel x x)
 
-module _ {ℓ} {f : Op₁ A} (_≈_ : Rel A ℓ) where
+module _ {ℓ} {f : Op₁ A} (_≈_ : Rel A ℓ) (open Definitions _≈_) where
 
   reflexive∧selfInverse⇒involutive : Reflexive _≈_ →
-                                     SelfInverse _≈_ f →
-                                     Involutive _≈_ f
+                                     SelfInverse f →
+                                     Involutive f
   reflexive∧selfInverse⇒involutive refl inv _ = inv refl
 
 ------------------------------------------------------------------------

src/Algebra/Consequences/Propositional.agda

@@ -10,6 +10,7 @@
 module Algebra.Consequences.Propositional
   {a} {A : Set a} where
 
+open import Algebra.Core using (Op₁; Op₂)
 open import Data.Sum.Base using (inj₁; inj₂)
 open import Relation.Binary.Core using (Rel)
 open import Relation.Binary.Bundles using (Setoid)
@@ -19,7 +20,6 @@ open import Relation.Binary.PropositionalEquality.Core
 open import Relation.Binary.PropositionalEquality.Properties
   using (setoid)
 open import Relation.Unary using (Pred)
-open import Algebra.Core using (Op₁; Op₂)
 
 open import Algebra.Definitions {A = A} _≡_
 import Algebra.Consequences.Setoid (setoid A) as Base

src/Algebra/Consequences/Setoid.agda

@@ -13,55 +13,66 @@ open import Relation.Binary.Definitions
 
 module Algebra.Consequences.Setoid {a ℓ} (S : Setoid a ℓ) where
 
-open Setoid S renaming (Carrier to A)
+import Algebra.Consequences.Base as Base
 open import Algebra.Core
-open import Algebra.Definitions _≈_
 open import Data.Sum.Base using (inj₁; inj₂)
 open import Data.Product.Base using (_,_)
 open import Function.Base using (_$_; id; _∘_)
 open import Function.Definitions
 import Relation.Binary.Consequences as Bin
 open import Relation.Binary.Core using (Rel)
-open import Relation.Binary.Reasoning.Setoid S
 open import Relation.Unary using (Pred)
 
+open Setoid S renaming (Carrier to A)
+open import Algebra.Definitions _≈_
+open import Relation.Binary.Reasoning.Setoid S
+
 ------------------------------------------------------------------------
 -- Re-exports
 
 -- Export base lemmas that don't require the setoid
 
-open import Algebra.Consequences.Base public
+open Base public
+  hiding (module Congruence)
+
+-- Export congruence lemmas using reflexivity
+
+module Congruence {_∙_ : Op₂ A} (cong : Congruent₂ _∙_) where
+
+  open Base.Congruence _≈_ cong refl public
 
 ------------------------------------------------------------------------
 -- MiddleFourExchange
 
 module _ {_∙_ : Op₂ A} (cong : Congruent₂ _∙_) where
 
+  open Congruence cong
+
   comm∧assoc⇒middleFour : Commutative _∙_ → Associative _∙_ →
                           _∙_ MiddleFourExchange _∙_
   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) ⟩
-    w ∙ ((y ∙ x) ∙ z) ≈⟨ cong refl (assoc y x z) ⟩
-    w ∙ (y ∙ (x ∙ z)) ≈⟨ sym (assoc w y (x ∙ z)) ⟩
+    w ∙ (x ∙ (y ∙ z)) ≈⟨ ∙-congˡ (assoc x y z) ⟨
+    w ∙ ((x ∙ y) ∙ z) ≈⟨ ∙-congˡ (∙-congʳ (comm x y)) ⟩
+    w ∙ ((y ∙ x) ∙ z) ≈⟨ ∙-congˡ (assoc y x z) ⟩
+    w ∙ (y ∙ (x ∙ z)) ≈⟨ assoc w y (x ∙ z) ⟨
     (w ∙ y) ∙ (x ∙ z) ∎
 
   identity∧middleFour⇒assoc : {e : A} → Identity e _∙_ →
                               _∙_ MiddleFourExchange _∙_ →
                               Associative _∙_
   identity∧middleFour⇒assoc {e} (identityˡ , identityʳ) middleFour x y z = begin
-    (x ∙ y) ∙ z       ≈⟨ cong refl (sym (identityˡ z)) ⟩
+    (x ∙ y) ∙ z       ≈⟨ ∙-congˡ (identityˡ z) ⟨
     (x ∙ y) ∙ (e ∙ z) ≈⟨ middleFour x y e z ⟩
-    (x ∙ e) ∙ (y ∙ z) ≈⟨ cong (identityʳ x) refl ⟩
+    (x ∙ e) ∙ (y ∙ z) ≈⟨ ∙-congʳ (identityʳ x) ⟩
     x ∙ (y ∙ z)       ∎
 
   identity∧middleFour⇒comm : {_+_ : Op₂ A} {e : A} → Identity e _+_ →
                              _∙_ MiddleFourExchange _+_ →
                              Commutative _∙_
   identity∧middleFour⇒comm {_+_} {e} (identityˡ , identityʳ) middleFour x y
     = begin
-    x ∙ y             ≈⟨ sym (cong (identityˡ x) (identityʳ y)) ⟩
+    x ∙ y             ≈⟨ cong (identityˡ x) (identityʳ y) ⟨
     (e + x) ∙ (y + e) ≈⟨ middleFour e x y e ⟩
     (e + y) ∙ (x + e) ≈⟨ cong (identityˡ y) (identityʳ x) ⟩
     y ∙ x             ∎
@@ -198,25 +209,27 @@ module _ {_∙_ : Op₂ A} {_⁻¹ : Op₁ A} {e} (comm : Commutative _∙_) whe
 
 module _ {_∙_ : Op₂ A} {_⁻¹ : Op₁ A} {e} (cong : Congruent₂ _∙_) where
 
+  open Congruence cong
+
   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 ⟩
+    x                ≈⟨ idʳ x ⟨
+    x ∙ e            ≈⟨ ∙-congˡ (invʳ y) ⟨
+    x ∙ (y ∙ (y ⁻¹)) ≈⟨ assoc x y (y ⁻¹) ⟨
+    (x ∙ y) ∙ (y ⁻¹) ≈⟨ ∙-congʳ eq ⟩
     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 ⟩
+    y                ≈⟨ idˡ y ⟨
+    e ∙ y            ≈⟨ ∙-congʳ (invˡ x) ⟨
     ((x ⁻¹) ∙ x) ∙ y ≈⟨ assoc (x ⁻¹) x y ⟩
-    (x ⁻¹) ∙ (x ∙ y) ≈⟨ cong refl eq ⟩
+    (x ⁻¹) ∙ (x ∙ y) ≈⟨ ∙-congˡ eq ⟩
     (x ⁻¹) ∙ e       ≈⟨ idʳ (x ⁻¹) ⟩
     x ⁻¹             ∎
 
@@ -228,6 +241,8 @@ module _ {_∙_ _◦_ : Op₂ A}
          (∙-comm : Commutative _∙_)
          where
 
+  open Congruence ◦-cong renaming (∙-congˡ to ◦-congˡ)
+
   comm∧distrˡ⇒distrʳ :  _∙_ DistributesOverˡ _◦_ → _∙_ DistributesOverʳ _◦_
   comm∧distrˡ⇒distrʳ distrˡ x y z = begin
     (y ◦ z) ∙ x       ≈⟨ ∙-comm (y ◦ z) x ⟩
@@ -250,7 +265,7 @@ module _ {_∙_ _◦_ : Op₂ A}
 
   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 ◦ (z ∙ y)       ≈⟨ ◦-congˡ (∙-comm z y) ⟩
     x ◦ (y ∙ z)       ≈⟨ prf ⟩
     (x ◦ y) ∙ (x ◦ z) ≈⟨ ∙-comm (x ◦ y) (x ◦ z) ⟩
     (x ◦ z) ∙ (x ◦ y) ∎
@@ -262,16 +277,18 @@ module _ {_∙_ _◦_ : Op₂ A}
          (◦-comm  : Commutative _◦_)
          where
 
+  open Congruence ∙-cong
+
   distrib∧absorbs⇒distribˡ : _∙_ Absorbs _◦_ →
                              _◦_ Absorbs _∙_ →
                              _◦_ DistributesOver _∙_ →
                              _∙_ DistributesOverˡ _◦_
   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 ◦ z)                    ≈⟨ ∙-congʳ (∙-absorbs-◦ _ _) ⟨
+    (x ∙ (x ◦ y)) ∙ (y ◦ z)        ≈⟨  ∙-congʳ (∙-congˡ (◦-comm _ _)) ⟩
     (x ∙ (y ◦ x)) ∙ (y ◦ z)        ≈⟨  ∙-assoc _ _ _ ⟩
-    x ∙ ((y ◦ x) ∙ (y ◦ z))        ≈⟨ ∙-cong refl (◦-distribˡ-∙ _ _ _) ⟨
-    x ∙ (y ◦ (x ∙ z))              ≈⟨ ∙-cong (◦-absorbs-∙ _ _) refl ⟨
+    x ∙ ((y ◦ x) ∙ (y ◦ z))        ≈⟨ ∙-congˡ (◦-distribˡ-∙ _ _ _) ⟨
+    x ∙ (y ◦ (x ∙ z))              ≈⟨ ∙-congʳ (◦-absorbs-∙ _ _) ⟨
     (x ◦ (x ∙ z)) ∙ (y ◦ (x ∙ z))  ≈⟨ ◦-distribʳ-∙ _ _ _ ⟨
     (x ∙ y) ◦ (x ∙ z)              ∎
 
@@ -284,27 +301,31 @@ module _ {_+_ _*_ : Op₂ A}
          (*-cong : Congruent₂ _*_)
          where
 
+  open Congruence +-cong renaming (∙-congˡ to +-congˡ; ∙-congʳ to +-congʳ)
+
+  open Congruence *-cong renaming (∙-congˡ to *-congˡ; ∙-congʳ to *-congʳ)
+
   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                                 ≈⟨ idʳ _ ⟨
+    (0# * x) + 0#                          ≈⟨ +-congˡ (invʳ _) ⟨
+    (0# * x) + ((0# * x)  + ((0# * x)⁻¹))  ≈⟨ +-assoc _ _ _ ⟨
+    ((0# * x) +  (0# * x)) + ((0# * x)⁻¹)  ≈⟨ +-congʳ (distribʳ _ _ _) ⟨
+    ((0# + 0#) * x) + ((0# * x)⁻¹)         ≈⟨ +-congʳ (*-congʳ (idʳ _)) ⟩
     (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#                                ≈⟨ idʳ _ ⟨
+     (x * 0#) + 0#                         ≈⟨ +-congˡ (invʳ _) ⟨
+     (x * 0#) + ((x * 0#) + ((x * 0#)⁻¹))  ≈⟨ +-assoc _ _ _ ⟨
+     ((x * 0#) + (x * 0#)) + ((x * 0#)⁻¹)  ≈⟨ +-congʳ (distribˡ _ _ _) ⟨
+     (x * (0# + 0#)) + ((x * 0#)⁻¹)        ≈⟨ +-congʳ (*-congˡ (idʳ _)) ⟩
      ((x * 0#) + ((x * 0#)⁻¹))             ≈⟨ invʳ _ ⟩
      0#                                    ∎
 

src/Algebra/Definitions.agda

@@ -15,8 +15,7 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Relation.Binary.Core using (Rel; _Preserves_⟶_; _Preserves₂_⟶_⟶_)
-open import Relation.Nullary.Negation.Core using (¬_)
+open import Relation.Binary.Core using (Rel)
 
 module Algebra.Definitions
   {a ℓ} {A : Set a}   -- The underlying set
@@ -26,21 +25,24 @@ module Algebra.Definitions
 open import Algebra.Core using (Op₁; Op₂)
 open import Data.Product.Base using (_×_; ∃-syntax)
 open import Data.Sum.Base using (_⊎_)
+open import Relation.Binary.Definitions using (Monotonic₁; Monotonic₂)
+open import Relation.Nullary.Negation.Core using (¬_)
+
 
 ------------------------------------------------------------------------
 -- Properties of operations
 
 Congruent₁ : Op₁ A → Set _
-Congruent₁ f = f Preserves _≈_ ⟶ _≈_
+Congruent₁ = Monotonic₁ _≈_ _≈_
 
 Congruent₂ : Op₂ A → Set _
-Congruent₂ ∙ = ∙ Preserves₂ _≈_ ⟶ _≈_ ⟶ _≈_
+Congruent₂ = Monotonic₂ _≈_ _≈_ _≈_
 
 LeftCongruent : Op₂ A → Set _
-LeftCongruent _∙_ = ∀ {x} → (x ∙_) Preserves _≈_ ⟶ _≈_
+LeftCongruent _∙_ = ∀ {x} → Congruent₁ (x ∙_)
 
 RightCongruent : Op₂ A → Set _
-RightCongruent _∙_ = ∀ {x} → (_∙ x) Preserves _≈_ ⟶ _≈_
+RightCongruent _∙_ = ∀ {x} → Congruent₁ (_∙ x)
 
 Associative : Op₂ A → Set _
 Associative _∙_ = ∀ x y z → ((x ∙ y) ∙ z) ≈ (x ∙ (y ∙ z))

src/Algebra/Structures.agda

@@ -54,13 +54,14 @@ record IsMagma (∙ : Op₂ A) : Set (a ⊔ ℓ) where
 
   setoid : Setoid a ℓ
   setoid = record { isEquivalence = isEquivalence }
-
+{-
   ∙-congˡ : LeftCongruent ∙
   ∙-congˡ y≈z = ∙-cong refl y≈z
 
   ∙-congʳ : RightCongruent ∙
   ∙-congʳ y≈z = ∙-cong y≈z refl
-
+-}
+  open Consequences.Congruence setoid ∙-cong public
 
 record IsCommutativeMagma (∙ : Op₂ A) : Set (a ⊔ ℓ) where
   field

src/Data/Fin/Properties.agda

@@ -902,7 +902,7 @@ pinch-surjective _       zero    = zero , λ { refl → refl }
 pinch-surjective zero    (suc j) = suc (suc j) , λ { refl → refl }
 pinch-surjective (suc i) (suc j) = map suc (λ {f refl → cong suc (f refl)}) (pinch-surjective i j)
 
-pinch-mono-≤ : ∀ (i : Fin n) → (pinch i) Preserves _≤_ ⟶ _≤_
+pinch-mono-≤ : ∀ (i : Fin n) → Monotonic₁ _≤_ _≤_ (pinch i)
 pinch-mono-≤ 0F      {0F}    {k}     0≤n = z≤n
 pinch-mono-≤ 0F      {suc j} {suc k} j≤k = ℕ.s≤s⁻¹ j≤k
 pinch-mono-≤ (suc i) {0F}    {k}     0≤n = z≤n