------------------------------------------------------------------------
-- The Agda standard library
--
-- Relations between properties of functions, such as associativity and
-- commutativity (specialised to propositional equality)
------------------------------------------------------------------------

{-# OPTIONS --cubical-compatible --safe #-}

module Algebra.Consequences.Propositional
  {a} {A : Set a} where

open import Data.Sum.Base using (inj₁; inj₂)
open import Relation.Binary.Core using (Rel)
open import Relation.Binary.Bundles using (Setoid)
open import Relation.Binary.Definitions using (Symmetric; Total)
open import Relation.Binary.PropositionalEquality
open import Relation.Unary using (Pred)

open import Algebra.Core
open import Algebra.Definitions {A = A} _≡_
import Algebra.Consequences.Setoid (setoid A) as Base

------------------------------------------------------------------------
-- Re-export all proofs that don't require congruence or substitutivity

open Base public
  hiding
  ( 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
  )

------------------------------------------------------------------------
-- Group-like structures

module _ {_•_ _⁻¹ ε} where

  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 : Associative _•_  Identity ε _•_ 
                              LeftInverse ε _⁻¹ _•_ 
                               x y  (x  y)  ε  y  (x ⁻¹)
  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ʳ _+_ 
                                RightIdentity 0# _+_  RightInverse 0# -_ _+_ 
                                LeftZero 0# _*_
  assoc+distribʳ+idʳ+invʳ⇒zeˡ =
    Base.assoc+distribʳ+idʳ+invʳ⇒zeˡ (cong₂ _+_) (cong₂ _*_)

  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₂ _*_)

------------------------------------------------------------------------
-- 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⇒sym[distribˡ] :  x  Symmetric  y z  (x  (y  z))  ((x  y)  (x  z)))
  comm⇒sym[distribˡ] = Base.comm⇒sym[distribˡ] (cong₂ _◦_) •-comm

------------------------------------------------------------------------
-- Selectivity

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

  sel⇒idem : Selective _•_  Idempotent _•_
  sel⇒idem = Base.sel⇒idem _≡_

------------------------------------------------------------------------
-- Middle-Four Exchange

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

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

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

  identity+middleFour⇒comm : {_+_ : Op₂ A} {e : A}  Identity e _+_ 
                             _•_ MiddleFourExchange _+_ 
                             Commutative _•_
  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) 
                   Symmetric  a b  P (f a b))
  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