Binary leaf trees are free magmas

freemagma

module Set

%default total

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

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

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'

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

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


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

class MySemigroup c => MyMonoid c where
  Zero : c
  zeroLeftNeutral : (c1 : c) -> Zero <++> c1 ~= c1
  zeroRightNeutral : (c1 : c) -> c1 <++> Zero ~= c1

zerosLeftNeutral : MyMonoid c => (z, x : c) -> (z ~= Zero) -> z <++> x ~= x
zerosLeftNeutral {c} z x zZero =
  let foo : (Zero <++> x ~= x) = zeroLeftNeutral x
      bar = plusPreservesEqL {c} {c2=x} zZero
  in trns {c} bar foo

zerosRightNeutral : MyMonoid c => (z, x : c) -> (z ~= Zero) -> x <++> z ~= x
zerosRightNeutral {c} z x zZero =
  let foo : (x <++> Zero ~= x) = zeroRightNeutral x
      bar = plusPreservesEqR {c} {c1=x} zZero
  in trns {c} bar foo

-- The free magma over a type.
-- TODO Rename this.
data Sem : Type -> Type where
  SSingle : (x : s) -> Sem s
  SPlus : (x,y : Sem s) -> Sem s

instance Set c => Set (Sem c) where
  (~=) (SSingle x) (SSingle y) = x ~= y
  (~=) (SSingle x) (SPlus y z) = Void
  (~=) (SPlus x z) (SSingle y) = Void
  (~=) (SPlus x z) (SPlus y w) = (x ~= y, z ~= w)
  rfl {x = (SSingle x)} = rfl {c}
  rfl {x = (SPlus x y)} = (rfl {c = Sem c}, rfl {c = Sem c})
  symm {x = (SSingle x)} {y = (SSingle y)} xy = symm {c} xy
  symm {x = (SSingle x)} {y = (SPlus y z)} xy = absurd xy
  symm {x = (SPlus x z)} {y = (SSingle y)} xy = absurd xy
  symm {x = (SPlus ps qs)} {y = (SPlus rs ss)} (psrs, qsss) = (symm {c=Sem c} psrs, symm {c=Sem c} qsss)
  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 w)} xy yz = absurd yz
  trns {x = (SSingle x)} {y = (SPlus y w)} {z = z} xy yz = absurd xy
  trns {x = (SPlus x w)} {y = (SSingle y)} {z = z} xy yz = absurd xy
  trns {x = (SPlus x1 x2)} {y = (SPlus y1 y2)} {z = (SSingle z)} xy yz = absurd yz
  trns {x = (SPlus x1 x2)} {y = (SPlus y1 y2)} {z = (SPlus z1 z2)} (x1y1, x2y2) (y1z1, y2z2) =
    (trns {c=Sem c} x1y1 y1z1, trns {c=Sem c} x2y2 y2z2)

instance Set c => Magma (Sem c) where
  (<++>) xs ys = SPlus 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

evalS : Magma s => Sem s -> s
evalS (SSingle x) = x
evalS (SPlus x y) = evalS x <++> evalS y

evalSRespectsMagma : Magma c => RespectsMagma {n=c} evalS
evalSRespectsMagma {c} x y = rfl {c}

evalSIsFunction : Magma c => IsFunction evalS {b=c}
evalSIsFunction (SSingle x) (SSingle y) xy = xy
evalSIsFunction (SSingle x) (SPlus y z) xy = absurd xy
evalSIsFunction (SPlus x y) (SSingle z) xy = absurd xy
evalSIsFunction {c} (SPlus x1 x2) (SPlus y1 y2) (x1y1, x2y2) =
  let foo = evalSIsFunction x1 y1 x1y1
      bar = evalSIsFunction x2 y2 x2y2
  in plusPreservesEq {c} foo bar

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

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

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

||| fmSplit actually splits its argument.
fmSplitSplits : Magma n => (f : c -> n) -> f ~~= fmSplit f . SSingle
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.
fmSplitRespectsMagma : (Set c, Magma n) => (f : c -> n) -> RespectsMagma {m = Sem c} (fmSplit f)
fmSplitRespectsMagma {n} f (SSingle x) (SSingle y) = rfl {c=n}
fmSplitRespectsMagma {n} f (SSingle x) (SPlus y1 y2) = rfl {c=n}
fmSplitRespectsMagma {n} f (SPlus x1 x2) (SSingle y) = rfl {c=n}
fmSplitRespectsMagma {n} f (SPlus x1 x2) (SPlus 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.
fmSplitIsFunction : (Set c, Magma n) => (f : c -> n) -> IsFunction f -> IsFunction (fmSplit f)
fmSplitIsFunction {c = c} {n = n} f fIsFun (SSingle x) (SSingle y) xy = fIsFun x y xy
fmSplitIsFunction {c = c} {n = n} f fIsFun (SSingle x) (SPlus y1 y2) xy = absurd xy
fmSplitIsFunction {c = c} {n = n} f fIsFun (SPlus x1 x2) (SSingle y) xy = absurd xy
fmSplitIsFunction {c = c} {n = n} f fIsFun (SPlus x1 x2) (SPlus 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 `Sem c` to `n` that splits `f` is equivalent to
||| `fmSplit f`.
fmSplitUnique : (Set c, Magma n) =>
                (f : c -> n) ->
                (g : Sem c -> n) ->
                RespectsMagma g ->
                f ~~= g . SSingle -> fmSplit f ~~= g
fmSplitUnique {c} {n} f g gRespMag gSplits (SSingle x) = gSplits x
fmSplitUnique {c} {n} f g gRespMag gSplits (SPlus 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