{-# OPTIONS_GHC -Wunused-imports #-}

-- | Partially ordered monoids.

module Agda.Utils.POMonoid where

import Agda.Utils.PartialOrd

-- | Partially ordered semigroup.
--
-- Law: composition must be monotone.
--
-- @
--   related x POLE x' && related y POLE y' ==>
--   related (x <> y) POLE (x' <> y')
-- @

class (PartialOrd a, Semigroup a) => POSemigroup a where

-- | Partially ordered monoid.
--
-- Law: composition must be monotone.
--
-- @
--   related x POLE x' && related y POLE y' ==>
--   related (x <> y) POLE (x' <> y')
-- @

class (PartialOrd a, Semigroup a, Monoid a) => POMonoid a where

-- | Completing POMonoids with inverses to form a Galois connection.
--
-- Law: composition and inverse composition form a Galois connection.
--
-- @
--   related (inverseCompose p x) POLE y <==> related x POLE (p <> y)
-- @

class POMonoid a => LeftClosedPOMonoid a where
  inverseCompose :: a -> a -> a


-- | @hasLeftAdjoint x@ checks whether
--   @x^-1 := x `inverseCompose` mempty@ is such that
--   @x `inverseCompose` y == x^-1 <> y@ for any @y@.
hasLeftAdjoint :: LeftClosedPOMonoid a => a -> Bool
hasLeftAdjoint :: forall a. LeftClosedPOMonoid a => a -> Bool
hasLeftAdjoint a
x = a -> PartialOrdering -> a -> Bool
forall a. PartialOrd a => a -> PartialOrdering -> a -> Bool
related (a -> a -> a
forall a. LeftClosedPOMonoid a => a -> a -> a
inverseCompose a
x a
forall a. Monoid a => a
mempty a -> a -> a
forall a. Semigroup a => a -> a -> a
<> a
x) PartialOrdering
POLE a
forall a. Monoid a => a
mempty
  -- It is enough to check the above, because of the following proof:
  -- I will write _\_ for `inverseCompose`, id for mempty, and _._ for (<>).
  -- Assume (*) x^-1 . x <= id, as checked.
  -- Show x^-1 . y <=> x \ y
  --
  -- 1. (>=)
     -- id     <= x . (x \ id)      (galois)
     -- id . y <= x . (x \ id) . y
     -- y      <= x . (x \ id) . y
     -- x \ y  <= (x \ id) . y      (galois)
     -- x^-1 . y >= x \ y           qed
  --
  -- 2. (<=)
     --        y <=        x . (x \ y)   (galois)
     -- x^-1 . y <= x^-1 . x . (x \ y)
     --          <= id       . (x \ y)   (*)
     --          <= x \ y
     -- x^-1 . y <= x \ y                qed