------------------------------------------------------------------------
-- The Agda standard library
--
-- Relations between properties of functions, such as associativity and
-- commutativity
------------------------------------------------------------------------

open import Relation.Binary using (Setoid)

module Algebra.FunctionProperties.Consequences
  {a } (S : Setoid a ) where

open Setoid S
open import Algebra.FunctionProperties _≈_
open import Relation.Binary.EqReasoning S
open import Data.Sum using (inj₁; inj₂)
open import Data.Product using (proj₁; proj₂)

------------------------------------------------------------------------
-- Existence of identity elements

comm+idˡ⇒idʳ :  {_•_}  Commutative _•_ 
               {e}  LeftIdentity e _•_  RightIdentity e _•_
comm+idˡ⇒idʳ {_•_} comm {e} idˡ x = begin
  x  e ≈⟨ comm x e 
  e  x ≈⟨ idˡ x 
  x     

comm+idʳ⇒idˡ :  {_•_}  Commutative _•_ 
               {e}  RightIdentity e _•_  LeftIdentity e _•_
comm+idʳ⇒idˡ {_•_} comm {e} idʳ x = begin
  e  x ≈⟨ comm e x 
  x  e ≈⟨ idʳ x 
  x     

------------------------------------------------------------------------
-- Existence of zero elements

comm+zeˡ⇒zeʳ :  {_•_}  Commutative _•_ 
               {e}  LeftZero e _•_  RightZero e _•_
comm+zeˡ⇒zeʳ {_•_} comm {e} zeˡ x = begin
  x  e ≈⟨ comm x e 
  e  x ≈⟨ zeˡ x 
  e     

comm+zeʳ⇒zeˡ :  {_•_}  Commutative _•_ 
               {e}  RightZero e _•_  LeftZero e _•_
comm+zeʳ⇒zeˡ {_•_} comm {e} zeʳ x = begin
  e  x ≈⟨ comm e x 
  x  e ≈⟨ zeʳ x 
  e     

assoc+distribʳ+idʳ+invʳ⇒zeˡ :  {_+_ _*_ -_ 0#} 
                            Congruent₂ _+_  Congruent₂ _*_ 
                            Associative _+_  _*_ DistributesOverʳ _+_ 
                            RightIdentity 0# _+_  RightInverse 0# -_ _+_ 
                            LeftZero 0# _*_
assoc+distribʳ+idʳ+invʳ⇒zeˡ {_+_} {_*_} { -_ } {0#}
  +-cong *-cong +-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ʳ :  {_+_ _*_ -_ 0#} 
                            Congruent₂ _+_  Congruent₂ _*_ 
                            Associative _+_  _*_ DistributesOverˡ _+_ 
                            RightIdentity 0# _+_  RightInverse 0# -_ _+_ 
                            RightZero 0# _*_
assoc+distribˡ+idʳ+invʳ⇒zeʳ {_+_} {_*_} { -_ } {0#}
  +-cong *-cong +-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#                                   

------------------------------------------------------------------------
-- Existence of inverses

comm+invˡ⇒invʳ :  {e _⁻¹ _•_}  Commutative _•_ 
                LeftInverse e _⁻¹ _•_  RightInverse e _⁻¹ _•_
comm+invˡ⇒invʳ {e} {_⁻¹} {_•_} comm invˡ x = begin
  x  (x ⁻¹) ≈⟨ comm x (x ⁻¹) 
  (x ⁻¹)  x ≈⟨ invˡ x 
  e          

comm+invʳ⇒invˡ :  {e _⁻¹ _•_}  Commutative _•_ 
                RightInverse e _⁻¹ _•_  LeftInverse e _⁻¹ _•_
comm+invʳ⇒invˡ {e} {_⁻¹} {_•_} comm invʳ x = begin
  (x ⁻¹)  x ≈⟨ comm (x ⁻¹) x 
  x  (x ⁻¹) ≈⟨ invʳ x 
  e          

------------------------------------------------------------------------
-- Uniqueness of inverses

assoc+id+invʳ⇒invˡ-unique :  {_•_ _⁻¹ ε} 
                           Congruent₂ _•_  Associative _•_ 
                           Identity ε _•_  RightInverse ε _⁻¹ _•_ 
                            x y  (x  y)  ε  x  (y ⁻¹)
assoc+id+invʳ⇒invˡ-unique {_•_} {_⁻¹} {ε} cong assoc id invʳ x y eq =
  begin
    x                ≈⟨ sym (proj₂ id x) 
    x  ε            ≈⟨ cong refl (sym (invʳ y)) 
    x  (y  (y ⁻¹)) ≈⟨ sym (assoc x y (y ⁻¹)) 
    (x  y)  (y ⁻¹) ≈⟨ cong eq refl 
    ε  (y ⁻¹)       ≈⟨ proj₁ id (y ⁻¹) 
    y ⁻¹             

assoc+id+invˡ⇒invʳ-unique :  {_•_ _⁻¹ ε} 
                           Congruent₂ _•_  Associative _•_ 
                           Identity ε _•_  LeftInverse ε _⁻¹ _•_ 
                            x y  (x  y)  ε  y  (x ⁻¹)
assoc+id+invˡ⇒invʳ-unique {_•_} {_⁻¹} {ε} cong assoc id invˡ x y eq =
  begin
    y                ≈⟨ sym (proj₁ id y) 
    ε  y            ≈⟨ cong (sym (invˡ x)) refl 
    ((x ⁻¹)  x)  y ≈⟨ assoc (x ⁻¹) x y 
    (x ⁻¹)  (x  y) ≈⟨ cong refl eq 
    (x ⁻¹)  ε       ≈⟨ proj₂ id (x ⁻¹) 
    x ⁻¹             

------------------------------------------------------------------------
-- Distributivity

comm+distrˡ⇒distrʳ :  {_•_ _◦_}  Congruent₂ _◦_  Commutative _•_ 
                   _•_ DistributesOverˡ _◦_  _•_ DistributesOverʳ _◦_
comm+distrˡ⇒distrʳ {_•_} {_◦_} cong comm 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ˡ :  {_•_ _◦_}  Congruent₂ _◦_  Commutative _•_ 
                   _•_ DistributesOverʳ _◦_  _•_ DistributesOverˡ _◦_
comm+distrʳ⇒distrˡ {_•_} {_◦_} cong comm 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) 

------------------------------------------------------------------------
-- Cancellativity

comm+cancelˡ⇒cancelʳ :  {_•_}  Commutative _•_ 
                     LeftCancellative _•_   RightCancellative _•_
comm+cancelˡ⇒cancelʳ {_•_} comm 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ˡ :  {_•_}  Commutative _•_ 
                     RightCancellative _•_  LeftCancellative _•_
comm+cancelʳ⇒cancelˡ {_•_} comm cancelʳ x {y} {z} eq = cancelʳ y z (begin
  y  x ≈⟨ comm y x 
  x  y ≈⟨ eq 
  x  z ≈⟨ comm x z 
  z  x )

------------------------------------------------------------------------
-- Selectivity implies idempotence

sel⇒idem :  {_•_}  Selective _•_  Idempotent _•_
sel⇒idem sel x with sel x x
... | inj₁ x•x≈x = x•x≈x
... | inj₂ x•x≈x = x•x≈x