Free magmas and semigroups

Magmas

-- Construction of the free magma over an arbitrary type.

module Magma
import Set

%default total
%access public

infixl 6 <++>
class Set c => Magma c where
  (<++>) : c -> c -> c
  total
  plusPreservesEq : {c1,c2,c1',c2':c} -> c1 ~= c1' -> c2 ~= c2' -> c1 <++> c2 ~= c1' <++> c2'

abstract
plusPreservesEqL : Magma c => {c1,c1',c2:c} -> c1 ~= c1' -> c1 <++> c2 ~= c1' <++> c2
plusPreservesEqL {c} {c2} c1c1' = plusPreservesEq {c} c1c1' (rfl {c} {x=c2})

abstract
plusPreservesEqR : Magma c => {c1,c2,c2':c} -> c2 ~= c2' -> c1 <++> c2 ~= c1 <++> c2'
plusPreservesEqR {c} {c1} c2c2' = plusPreservesEq {c} (rfl {c} {x=c1}) c2c2'

-- The free magma over a type.
data FreeMagma : Type -> Type where
  MagSingle : (x : s) -> FreeMagma s
  MagPlus : (x,y : FreeMagma s) -> FreeMagma s

instance Set c => Set (FreeMagma c) where
  (~=) (MagSingle x) (MagSingle y) = x ~= y
  (~=) (MagSingle x) (MagPlus y z) = Void
  (~=) (MagPlus x z) (MagSingle y) = Void
  (~=) (MagPlus x z) (MagPlus y w) = (x ~= y, z ~= w)
  rfl {x = (MagSingle x)} = rfl {c}
  rfl {x = (MagPlus x y)} = (rfl {c = FreeMagma c}, rfl {c = FreeMagma c})
  symm {x = (MagSingle x)} {y = (MagSingle y)} xy = symm {c} xy
  symm {x = (MagSingle x)} {y = (MagPlus y z)} xy = absurd xy
  symm {x = (MagPlus x z)} {y = (MagSingle y)} xy = absurd xy
  symm {x = (MagPlus ps qs)} {y = (MagPlus rs ss)} (psrs, qsss) = (symm {c=FreeMagma c} psrs, symm {c=FreeMagma c} qsss)
  trns {x = (MagSingle x)} {y = (MagSingle y)} {z = (MagSingle z)} xy yz = trns {c} xy yz
  trns {x = (MagSingle x)} {y = (MagSingle y)} {z = (MagPlus z w)} xy yz = absurd yz
  trns {x = (MagSingle x)} {y = (MagPlus y w)} {z = z} xy yz = absurd xy
  trns {x = (MagPlus x w)} {y = (MagSingle y)} {z = z} xy yz = absurd xy
  trns {x = (MagPlus x1 x2)} {y = (MagPlus y1 y2)} {z = (MagSingle z)} xy yz = absurd yz
  trns {x = (MagPlus x1 x2)} {y = (MagPlus y1 y2)} {z = (MagPlus z1 z2)} (x1y1, x2y2) (y1z1, y2z2) =
    (trns {c=FreeMagma c} x1y1 y1z1, trns {c=FreeMagma c} x2y2 y2z2)

instance Set c => Magma (FreeMagma c) where
  (<++>) xs ys = MagPlus xs ys
  plusPreservesEq c1c1' c2c2' = (c1c1', c2c2')

RespectsMagma : (Magma m, Magma n) => (m -> n) -> Type
RespectsMagma {m} f = (x, y : m) -> f (x <++> y) ~= f x <++> f y

respectCompositional : (Magma m, Magma n, Magma o) =>
                       {f : n -> o} -> {g : m -> n} ->
                       IsFunction f -> RespectsMagma f ->
                       IsFunction g -> RespectsMagma g ->
                       RespectsMagma (f . g)
respectCompositional {o} {g} funF rf funG rg x y =
  let foo = rg x y
      bar = funF (g (x <++> y)) (g x <++> g y) foo
      baz = rf (g x) (g y)
  in trns {c=o} bar baz

{-
The functions fmSplit, fmSplitSplits, fmSplitRespectsMagma, fmSplitIsFunction,
and fmSplitUnique together prove that for any Set c, FreeMagma c is the free magma
over c.
-}

||| Any function from a type `c` to a magma `n` can be split into
||| a function, `MagSingle`, from `c` to `FreeMagma c` followed by a unique
||| magma morphism from `FreeMagma c` to `n`. `fmSplit` produces the function
||| from `FreeMagma c` to `n`.
fmSplit : Magma n => (f : c -> n) -> (FreeMagma c -> n)
fmSplit f (MagSingle x) = f x
fmSplit f (MagPlus x y) = fmSplit f x <++> fmSplit f y

||| fmSplit actually splits its argument.
abstract
fmSplitSplits : Magma n => (f : c -> n) -> f ~~= fmSplit f . MagSingle
fmSplitSplits {n} f x = rfl {c=n}

||| The result of `fmSplit` respects the magmas. Together with `fmSplitIsFunction`,
||| this proves the result of `fmSplit` is a magma morphism.
abstract
fmSplitRespectsMagma : (Set c, Magma n) => (f : c -> n) -> RespectsMagma {m = FreeMagma c} (fmSplit f)
fmSplitRespectsMagma {n} f (MagSingle x) (MagSingle y) = rfl {c=n}
fmSplitRespectsMagma {n} f (MagSingle x) (MagPlus y1 y2) = rfl {c=n}
fmSplitRespectsMagma {n} f (MagPlus x1 x2) (MagSingle y) = rfl {c=n}
fmSplitRespectsMagma {n} f (MagPlus x1 x2) (MagPlus y1 y2) = rfl {c=n}

||| The result of `fmSplit` is a function. Together with `fmSplitRespectsMagma`, this
||| shows that the result of `fmSplit` is a magma morphism.
abstract
fmSplitIsFunction : (Set c, Magma n) => (f : c -> n) -> IsFunction f -> IsFunction (fmSplit f)
fmSplitIsFunction {c = c} {n = n} f fIsFun (MagSingle x) (MagSingle y) xy = fIsFun x y xy
fmSplitIsFunction {c = c} {n = n} f fIsFun (MagSingle x) (MagPlus y1 y2) xy = absurd xy
fmSplitIsFunction {c = c} {n = n} f fIsFun (MagPlus x1 x2) (MagSingle y) xy = absurd xy
fmSplitIsFunction {c = c} {n = n} f fIsFun (MagPlus x1 x2) (MagPlus y1 y2) (x1y1, x2y2)
    = let hx1EQhy1 : (fmSplit f x1 ~= fmSplit f y1) = fmSplitIsFunction f fIsFun x1 y1 x1y1
          hx2EQhy2 : (fmSplit f x2 ~= fmSplit f y2) = fmSplitIsFunction f fIsFun x2 y2 x2y2
          foo : (fmSplit f (x1 <++> x2) ~= fmSplit f x1 <++> fmSplit f x2) = fmSplitRespectsMagma {c} {n} f x1 x2
          baz : (fmSplit f x1 <++> fmSplit f x2 ~= fmSplit f y1 <++> fmSplit f y2) =
            plusPreservesEq {c=n} hx1EQhy1 hx2EQhy2
          quux : (fmSplit f y1 <++> fmSplit f y2 ~= fmSplit f (y1 <++> y2))
               = symm {c=n} $ fmSplitRespectsMagma f y1 y2
          in trns {c=n} (trns {c=n} foo baz) quux

||| Any magma morphism from `FreeMagma c` to `n` that splits `f` is equivalent to
||| `fmSplit f`. The theorem is in fact slighly stronger -- the morphism does
||| not need to have been proven a "function" first.
abstract
fmSplitUnique : (Set c, Magma n) =>
                (f : c -> n) ->
                (g : FreeMagma c -> n) ->
                RespectsMagma g ->
                f ~~= g . MagSingle -> fmSplit f ~~= g
fmSplitUnique {c} {n} f g gRespMag gSplits (MagSingle x) = gSplits x
fmSplitUnique {c} {n} f g gRespMag gSplits (MagPlus x1 x2) =
  let x1unique : (fmSplit f x1 ~= g x1) = fmSplitUnique {c} {n} f g gRespMag gSplits x1
      x2unique : (fmSplit f x2 ~= g x2) = fmSplitUnique {c} {n} f g gRespMag gSplits x2
      pp : (fmSplit f x1 <++> fmSplit f x2 ~= g x1 <++> g x2) = plusPreservesEq {c=n} x1unique x2unique
      yeah : (g x1 <++> g x2 ~= g (x1 <++> x2)) = symm {c=n} $ gRespMag x1 x2
  in trns {c=n} pp yeah

||| The free magma over a magma can be collapsed down to the underlying
||| magma. In particular, `evalMag` is the unique morphism from
||| `FreeMagma s` to `s` that retracts `MagSingle`.
evalMag : Magma s => FreeMagma s -> s
evalMag = fmSplit {n=s} id

evalMagRespectsMagma : Magma c => (x,y:FreeMagma c) -> evalMag x <++> evalMag y ~= evalMag (x <++> y)
evalMagRespectsMagma {c} x y = fmSplitRespectsMagma {c} id x y

evalMagIsFunction : Magma c => IsFunction {b=c} evalMag
evalMagIsFunction {c} = fmSplitIsFunction {c} {n=c} id idIsFunction

---------- Example -----------

instance Magma Additive where
  (<++>) = (<+>)
  plusPreservesEq c1c1' c2c2' = rewrite c1c1' in rewrite c2c2' in Refl

Semigroups

module Semigroup
import Set
import Magma

%default total
%access public

class Magma c => MySemigroup c where
  plusAssoc : (c1,c2,c3:c) -> c1 <++> (c2 <++> c3) ~= c1 <++> c2 <++> c3

||| The free semigroup over a type (i.e., a type of nonempty lists)
data FreeSem : Type -> Type where
  SSingle : (x : c) -> FreeSem c
  SPlus : (x : c) -> (xs : FreeSem c) -> FreeSem c

instance Set c => Set (FreeSem c) where
  (SSingle x) ~= (SSingle y) = x ~= y
  (SSingle y) ~= (SPlus x xs) = Void
  (SPlus x xs) ~= (SSingle y) = Void
  (SPlus x xs) ~= (SPlus y ys) = (x ~= y, xs ~= ys)
  rfl {x = (SSingle x)} = rfl {c}
  rfl {x = (SPlus x xs)} = (rfl {c}, rfl {x=xs})
  symm {x = (SSingle x)} {y = (SSingle y)} xy = symm {c} xy
  symm {x = (SSingle x)} {y = (SPlus y xs)} xy = absurd xy
  symm {x = (SPlus x xs)} {y = (SSingle y)} xy = absurd xy
  symm {x = (SPlus x xs)} {y = (SPlus y z)} (xy, xsys) = (symm {c} xy, symm {c=FreeSem c} xsys)
  trns {x = (SSingle x)} {y = (SSingle y)} {z = (SSingle z)} xy yz = trns {c} xy yz
  trns {x = (SSingle x)} {y = (SSingle y)} {z = (SPlus z xs)} xy yz = absurd yz
  trns {x = (SSingle x)} {y = (SPlus y xs)} {z = z} xy yz = absurd xy
  trns {x = (SPlus x xs)} {y = (SSingle y)} {z = z} xy yz = absurd xy
  trns {x = (SPlus x xs)} {y = (SPlus y w)} {z = (SSingle z)} xy yz = absurd yz
  trns {x = (SPlus x xs)} {y = (SPlus y w)} {z = (SPlus z s)} (xy,xsys) (yz,yszs) =
    (trns {c} xy yz, trns {c=FreeSem c} xsys yszs)

sPlus : FreeSem c -> FreeSem c -> FreeSem c
sPlus (SSingle x) xs = SPlus x xs
sPlus (SPlus x xs) ys = SPlus x (xs `sPlus` ys)

abstract
plusPreservesEqFS : Set c => {c1,c1',c2,c2' : FreeSem c} -> c1 ~= c1' -> c2 ~= c2' -> sPlus c1 c2 ~= sPlus c1' c2'
plusPreservesEqFS {c1 = (SSingle x)} {c1'=(SSingle y)} {c2 = c2} {c2'=c2p} c1c1' c2c2' = (c1c1', c2c2')
plusPreservesEqFS {c1 = (SSingle x)} {c1'=(SPlus y xs)} {c2 = c2} {c2'=c2p} c1c1' c2c2' = absurd c1c1'
plusPreservesEqFS {c1 = (SPlus x xs)} {c1'=(SSingle y)} {c2 = c2} {c2'=c2p} c1c1' c2c2' = absurd c1c1'
plusPreservesEqFS {c1 = (SPlus x xs)} {c1'=(SPlus y ys)} {c2 = c2} {c2'=c2p} (xy, xsys) c2c2p =
  let foo = plusPreservesEqFS {c1=xs} {c1'=ys} {c2} {c2'=c2p} xsys c2c2p
  in (xy, foo)

instance Set c => Magma (FreeSem c) where
  (<++>) = sPlus
  plusPreservesEq = plusPreservesEqFS {c}

private
plusAssocFS : Set c => {c1,c2,c3 : FreeSem c} ->
              c1 <++> (c2 <++> c3) ~= c1 <++> c2 <++> c3

plusAssocFS {c} {c1 = (SSingle x)} = (rfl {c}, rfl {c=FreeSem c})
plusAssocFS {c} {c1 = (SPlus x xs)} = (rfl {c}, plusAssocFS {c})

instance Set c => MySemigroup (FreeSem c) where
  plusAssoc {c1} {c2} {c3} = plusAssocFS {c} {c1} {c2} {c3}

-- The functions `fsSplit`, `fsSplitSplits`, `fsSplitRespectsSem`, `fsSplitIsFunction`,
-- and `fsSplitUnique` together prove that `FreeSem c` with injection `SSingle`
-- is the free semigroup for a set `c`.

||| Any function from a type `c` to a semigroup `n` can be split into
||| a function, `MagSingle`, from `c` to `FreeSem c` followed by a unique
||| homomorphism from `FreeSem c` to `n`. `fsSplit` produces the function
||| from `FreeSem c` to `n`.
fsSplit : Magma s => (f : c -> s) -> (FreeSem c -> s)
fsSplit f (SSingle x) = f x
fsSplit f (SPlus x xs) = f x <++> fsSplit f xs

||| fmSplit actually splits its argument.
fsSplitSplits : Magma s => (f : c -> s) -> f ~~= fsSplit f . SSingle
fsSplitSplits {s} f x = rfl {c=s}

||| The result of `fsSplit` respects the semigroups. Together with `fsSplitIsFunction`,
||| this proves the result of `fsSplit` is a homomorphism.
fsSplitRespectsSem : (Set c, MySemigroup s) => (f : c -> s) -> RespectsMagma {m = FreeSem c} (fsSplit f)
fsSplitRespectsSem {s} f (SSingle x) (SSingle y) = rfl {c=s}
fsSplitRespectsSem {s} f (SSingle x) (SPlus y1 y2) = rfl {c=s}
fsSplitRespectsSem {s} f (SPlus x1 x2) y =
  let
      foo : (fsSplit f (x2 <++> y) ~= fsSplit f x2 <++> fsSplit f y)
          = fsSplitRespectsSem {s} f x2 y

      bar : ( f x1 <++> fsSplit f (x2 <++> y) ~= f x1 <++> (fsSplit f x2 <++> fsSplit f y) )
          = plusPreservesEqR {c=s} {c1=f x1} {c2=fsSplit f (x2 <++> y)} {c2'=fsSplit f x2 <++> fsSplit f y} foo

      baz = plusAssoc (f x1) (fsSplit f x2) (fsSplit f y)
  in trns {c=s} bar baz

||| The result of `fsSplit` is a well-defined function. Together with
||| `fsSplitRespectsSem`, this proves it is a homomorphism.
fsSplitIsFunction : (Set c, Magma s) => (f : c -> s) -> IsFunction f ->
                    (x,y : FreeSem c) -> x ~= y -> fsSplit f x ~= fsSplit f y
fsSplitIsFunction f fIsFun (SSingle x) (SSingle y) xy = fIsFun x y xy
fsSplitIsFunction f fIsFun (SSingle x) (SPlus y xs) xy = absurd xy
fsSplitIsFunction f fIsFun (SPlus x xs) (SSingle y) xy = absurd xy
fsSplitIsFunction {s} f fIsFun (SPlus x xs) (SPlus y ys) (xy, xsys) =
  let foo = fIsFun x y xy
      bar = fsSplitIsFunction f fIsFun xs ys xsys
  in plusPreservesEq {c=s} foo bar

||| The morphism produced by `fsSplit` is unique.
fsSplitUnique : (Set c, MySemigroup n) =>
                (f : c -> n) ->
                (g : FreeSem c -> n) ->
                RespectsMagma g ->
                f ~~= g . SSingle -> fsSplit f ~~= g
fsSplitUnique f g gRespMag gSplitsf (SSingle x) = gSplitsf x
fsSplitUnique {n} f g gRespMag gSplitsf (SPlus x xs) =
  let
      foo : (fsSplit f xs ~= g xs)
          = fsSplitUnique f g gRespMag gSplitsf xs
      bar : (g (SSingle x) <++> g xs ~= g (SSingle x <++> xs))
          = symm {c=n} $ gRespMag (SSingle x) xs
      baz : (f x ~= g (SSingle x))
          = gSplitsf x
      quux : (f x <++> fsSplit f xs ~= g (SSingle x) <++> g xs)
          = plusPreservesEq {c=n} baz foo
  in trns {c=n} quux bar

||| The free semigroup over a semigroup can be collapsed down to the
||| underlying semigroup. `evalS` is the (unique) retraction of
||| `SSingle`.
evalS : MySemigroup c => FreeSem c -> c
evalS {c} = fsSplit {s=c} id

evalSIsFunction : MySemigroup c => IsFunction (evalS {c})
evalSIsFunction {c} x y xy = fsSplitIsFunction {c} id idIsFunction x y xy

||| We can take the free magma to the free semigroup in a unique
||| way that factors `SSingle`. That is, by the properties of `fmSplit`,
||| `canonS` is a morphism, `canonS . MagSingle ~~= SSingle`, and
||| `canonS` is the only such morphism. What does this mean, and why is
||| it useful? The equivalence above just says that if we take a
||| single value, form it into an expression with MagSingle, and pass that
||| expression to `canonS`, then we will get the same expression we would
||| get by applying `SSingle` to the value. The fact that it is a morphism
||| means that adding two expressions adds (appends) the `canonS` results.
||| Uniqueness means there's only one way to do it; the result of `canonS`
||| is completely determined by algebraic properties, and not by any details
||| of its implementation.
canonS : Set c => FreeMagma c -> FreeSem c
canonS = fmSplit SSingle

SSingleIsFunction : Set s => (x, y : s) -> x ~= y -> SSingle x ~= SSingle y
SSingleIsFunction x y xy = xy

canonSWorks_lem1 : MySemigroup s => id ~~= fsSplit {s} id . fmSplit {n=FreeSem s} SSingle . MagSingle
canonSWorks_lem1 {s} x = rfl {c=s}  -- This must be proof by computation. Spooky.

||| Applying `canonS` to an expression (represented by a free magma) is guaranteed
||| to produce an expression (represented by a free semigroup) that evaluates to
||| the same thing.
abstract
canonSWorks : MySemigroup s => (fm : FreeMagma s) -> evalMag fm ~= evalS (canonS fm)
canonSWorks {s} fm =
  -- The length of this function makes me sad. Maybe there is some way to clean it up.
  let
     -- Why do we need this horrible thing?
     huh : (Set s) = %instance
     resp : (RespectsMagma (fsSplit id . fmSplit {c=s} SSingle))
          = respectCompositional {f=fsSplit id} {g=fmSplit {c=s} SSingle}
              (fsSplitIsFunction {c=s} id (\x,y,xy=>xy))
              (fsSplitRespectsSem id)
              (fmSplitIsFunction SSingle SSingleIsFunction)  -- g is well-defined
              (fmSplitRespectsMagma SSingle)
     foo  : (fmSplit id ~~= fsSplit id . fmSplit SSingle)
          = fmSplitUnique {c=s} {n=s} id (fsSplit id . fmSplit SSingle) resp canonSWorks_lem1
  in foo fm

solveSemigroup : MySemigroup a => (xs, ys : FreeMagma a) -> {default Refl canonSame : canonS xs = canonS ys} ->
                            evalMag xs ~= evalMag ys
solveSemigroup {a} {canonSame} xs ys =
  let fooxs = canonSWorks {s=a} xs
      fooys = symm {c=a} $ canonSWorks {s=a} ys
  in ?solveSemigroup_rhs

testing : MySemigroup s => (x,y,z,w,p:s) ->
          x <++> (y <++> (z <++> p) <++> w) ~= x <++> y <++> (z <++> (p <++> w))
testing {s} x y z w p = 
  -- Why do I need this???
  let huh : (Set s) = %instance
  in solveSemigroup
          (MagSingle x <++> ((MagSingle y <++> (MagSingle z <++> MagSingle p)) <++> MagSingle w))
          ((MagSingle x <++> MagSingle y) <++> (MagSingle z <++> (MagSingle p <++> MagSingle w)))

testing2 : MySemigroup s => (x,y,z,w,p:s) ->
          x <++> (y <++> (z <++> p) <++> w) ~= x <++> y <++> (z <++> (p <++> w))
testing2 x y z w p = solveSemigroup
          (MagSingle x `MagPlus` ((MagSingle y `MagPlus` (MagSingle z `MagPlus` MagSingle p)) `MagPlus` MagSingle w))
          ((MagSingle x `MagPlus` MagSingle y) `MagPlus` (MagSingle z `MagPlus` (MagSingle p `MagPlus` MagSingle w)))

---------- Proofs ----------

solveSemigroup_rhs = proof
  intro a,xs,ys
  intro
  intro
  rewrite canonSame 
  intros
  exact trns {c=a} fooxs fooys

Set basics

-- We consider pretty much everything up to some arbitrary equivalence relation.

module Set

%default total
%access public

infixl 4 ~=
class Set c where
  (~=) : (x,y:c) -> Type

  rfl : {x:c} -> x ~= x
  symm : {x,y:c} -> x ~= y -> y ~= x
  trns : {x,y,z:c} -> x ~= y -> y ~= z -> x ~= z

infix 5 ~~=
||| Equivalence of functions
(~~=) : Set b => (a -> b) -> (a -> b) -> Type
(~~=) {a} f g = (x : a) -> f x ~= g x

IsFunction : (Set a, Set b) => (a -> b) -> Type
IsFunction {a} {b} f = (x, y : a) -> x ~= y -> f x ~= f y

idIsFunction : Set a => (x,y:a) -> (x ~= y) -> id x ~= id y
idIsFunction x y xy = xy

functionsCompose : (Set a, Set b, Set c) =>
                   {f : b -> c} ->
                   {g : a -> b} ->
                   IsFunction f ->
                   IsFunction g ->
                   IsFunction (f . g)
functionsCompose {g} fIsFun gIsFun x y xy = fIsFun (g x) (g y) (gIsFun x y xy)

abstract
eqPreservesEq : Set c -> (x,y,c1,c2:c) -> x ~= c1 -> y ~= c2 -> c1 ~= c2 -> x ~= y
eqPreservesEq {c} setc x y c1 c2 xc1 yc2 c1c2 =
  let xc2 : (x ~= c2) = trns {c} xc1 c1c2
      c2y : (c2 ~= y) = symm {c} yc2
  in trns {c} xc2 c2y

----------------  Demos   ----------------

instance Set t => Set (Maybe t) where
  (~=) Nothing Nothing = ()
  (~=) Nothing (Just x) = Void
  (~=) (Just x) Nothing = Void
  (~=) (Just x) (Just y) = (x~=y)
  rfl {x = Nothing} = ()
  rfl {x = (Just x)} = rfl {c=t}
  symm {x = Nothing} {y = Nothing} xy = ()
  symm {x = Nothing} {y = (Just x)} xy = absurd xy
  symm {x = (Just x)} {y = Nothing} xy = absurd xy
  symm {x = (Just x)} {y = (Just y)} xy = symm {c=t} xy
  trns {x = Nothing} {y = Nothing} {z = Nothing} xy yz = ()
  trns {x = Nothing} {y = Nothing} {z = (Just x)} xy yz = absurd yz
  trns {x = Nothing} {y = (Just x)} {z = z} xy yz = absurd xy
  trns {x = (Just x)} {y = Nothing} {z = z} xy yz = absurd xy
  trns {x = (Just x)} {y = (Just y)} {z = Nothing} xy yz = absurd yz
  trns {x = (Just x)} {y = (Just y)} {z = (Just z)} xy yz = trns {c=t} xy yz

instance Set Nat where
  (~=) = (~=~)
  rfl = Refl
  symm = sym
  trns = trans

instance Set Additive where
  (~=) = (~=~)
  rfl = Refl
  symm = sym
  trns = trans