1{-# LANGUAGE CPP #-}
2-- | Partially ordered monoids.
3
4module Agda.Utils.POMonoid where
5
6#if __GLASGOW_HASKELL__ < 804
7import Data.Semigroup
8#endif
9
10import Agda.Utils.PartialOrd
11
12-- | Partially ordered semigroup.
13--
14-- Law: composition must be monotone.
15--
16-- @
17--   related x POLE x' && related y POLE y' ==>
18--   related (x <> y) POLE (x' <> y')
19-- @
20
21class (PartialOrd a, Semigroup a) => POSemigroup a where
22
23-- | Partially ordered monoid.
24--
25-- Law: composition must be monotone.
26--
27-- @
28--   related x POLE x' && related y POLE y' ==>
29--   related (x <> y) POLE (x' <> y')
30-- @
31
32class (PartialOrd a, Semigroup a, Monoid a) => POMonoid a where
33
34-- | Completing POMonoids with inverses to form a Galois connection.
35--
36-- Law: composition and inverse composition form a Galois connection.
37--
38-- @
39--   related (inverseCompose p x) POLE y <==> related x POLE (p <> y)
40-- @
41
42class POMonoid a => LeftClosedPOMonoid a where
43  inverseCompose :: a -> a -> a
44
45
46-- | @hasLeftAdjoint x@ checks whether
47--   @x^-1 := x `inverseCompose` mempty@ is such that
48--   @x `inverseCompose` y == x^-1 <> y@ for any @y@.
49hasLeftAdjoint :: LeftClosedPOMonoid a => a -> Bool
50hasLeftAdjoint x = related (inverseCompose x mempty <> x) POLE mempty
51  -- It is enough to check the above, because of the following proof:
52  -- I will write _\_ for `inverseCompose`, id for mempty, and _._ for (<>).
53  -- Assume (*) x^-1 . x <= id, as checked.
54  -- Show x^-1 . y <=> x \ y
55  --
56  -- 1. (>=)
57     -- id     <= x . (x \ id)      (galois)
58     -- id . y <= x . (x \ id) . y
59     -- y      <= x . (x \ id) . y
60     -- x \ y  <= (x \ id) . y      (galois)
61     -- x^-1 . y >= x \ y           qed
62  --
63  -- 2. (<=)
64     --        y <=        x . (x \ y)   (galois)
65     -- x^-1 . y <= x^-1 . x . (x \ y)
66     --          <= id       . (x \ y)   (*)
67     --          <= x \ y
68     -- x^-1 . y <= x \ y                qed
69