------------------------------------------------------------------------
-- The Agda standard library
--
-- Relations between properties of functions, such as associativity and
-- commutativity, when the underlying relation is a setoid
------------------------------------------------------------------------

{-# OPTIONS --cubical-compatible --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.Base using (inj₁; inj₂)
open import Data.Product using (_,_)
open import Function.Base 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 setoid

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     

  comm+almostCancelˡ⇒almostCancelʳ : AlmostLeftCancellative e _•_ 
                                     AlmostRightCancellative e _•_
  comm+almostCancelˡ⇒almostCancelʳ cancelˡ-nonZero {x} y z x≉e yx≈zx =
    cancelˡ-nonZero 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 _•_ 
                                     AlmostLeftCancellative e _•_
  comm+almostCancelʳ⇒almostCancelˡ cancelʳ-nonZero {x} y z x≉e xy≈xz =
    cancelʳ-nonZero y z x≉e $ begin
      y  x ≈⟨ comm y x 
      x  y ≈⟨ xy≈xz 
      x  z ≈⟨ comm x z 
      z  x 

------------------------------------------------------------------------
-- 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