Semigroup solver thing

monoidsolverthing

module Mon
import Set

%default total
%access public

data MonBit a = MkMonBit a | MonZero
data Mon a = MkMon (Sem (MonBit a))

evalM' : MyMonoid a => Sem (MonBit a) -> a
evalM' (SSingle (MkMonBit x)) = x
evalM' (SSingle MonNeutral) = Zero
evalM' (SPlus x y) = evalM' x <++> evalM' y

evalM : MyMonoid a => Mon a -> a
evalM (MkMon s) = evalM' s

data MonCanonS a = MCZero | MCSem (Sem a)

evalMC : MyMonoid m => MonCanonS m -> m
evalMC MCZero = Zero
evalMC (MCSem x) = evalS x

instance MyMonoid c => Set (MonCanonS c) where
  (~=) x y = evalMC x ~= evalMC y
  rfl = rfl {c}
  symm = symm {c}
  trns = trns {c}

instance MyMonoid c => Magma (MonCanonS c) where
  (<++>) MCZero y = y
  (<++>) x MCZero = x
  (<++>) (MCSem x) (MCSem y) = MCSem (SPlus x y)
  plusPreservesEqL {c1 = MCZero} {c1'=MCZero} c1c1' = rfl {c}
  plusPreservesEqL {c1 = MCZero} {c1'=(MCSem c1')} {c2 = MCZero} c1c1' = c1c1'
  plusPreservesEqL {c1 = (MCSem x)} {c1'=(MCSem y)} {c2=MCZero} c1c1' = c1c1'
  plusPreservesEqL {c1 = MCZero} {c1'=(MCSem c1')} {c2 = (MCSem x)} c1c1' =
     symm {c} $ zerosLeftNeutral (evalS c1') (evalS x) (symm {c} c1c1')
  plusPreservesEqL {c1 = (MCSem c1)} {c1'=MCZero} {c2 = MCZero} c1Zero = c1Zero
  plusPreservesEqL {c1 = (MCSem c1)} {c1'=MCZero} {c2 = (MCSem x)} c1Zero =
     zerosLeftNeutral (evalS c1) (evalS x) c1Zero
  plusPreservesEqL {c1 = (MCSem c1)} {c1'=(MCSem c1')} {c2=(MCSem c2)} c1c1' =
     plusPreservesEqL {c} {c2=evalS c2} c1c1'

  plusPreservesEqR {c1 = c1} {c2 = MCZero} {c2'=MCZero} c2c2' = rfl {c}
  plusPreservesEqR {c1 = MCZero} {c2 = MCZero} {c2'=(MCSem c2')} c2c2' = c2c2'
  plusPreservesEqR {c1 = (MCSem c1)} {c2 = MCZero} {c2'=(MCSem c2')} c2c2' =
     symm {c} $ zerosRightNeutral {c} _ (evalS c1) (symm {c} c2c2')
  plusPreservesEqR {c1 = MCZero} {c2 = (MCSem x)} {c2'=c2p} c2c2' = c2c2'
  plusPreservesEqR {c1 = (MCSem c1)} {c2 = (MCSem c2)} {c2'=MCZero} c2c2' =
     zerosRightNeutral {c} (evalS c2) (evalS c1) c2c2'
  plusPreservesEqR {c1 = (MCSem c1)} {c2 = (MCSem c2)} {c2'=(MCSem c2')} c2c2' =
     plusPreservesEqR {c} {c1=evalS c1} c2c2'

evalMCMorphism : MyMonoid m => (x,y:MonCanonS m) -> evalMC x <++> evalMC y ~= evalMC (x <++> y)
evalMCMorphism {m} MCZero y = zeroLeftNeutral {c=m} _
evalMCMorphism {m = m} MCZero MCZero = zeroLeftNeutral {c=m} _
evalMCMorphism {m = m} (MCSem x) MCZero = zeroRightNeutral {c=m} _
evalMCMorphism (MCSem x) (MCSem y) = rfl {c=m}

canonMS' : MyMonoid a => Sem (MonBit a) -> MonCanonS a
canonMS' (SSingle (MkMonBit x)) = MCSem (SSingle x)
canonMS' (SSingle MonZero) = MCZero
canonMS' (SPlus x y) = canonMS' x <++> canonMS' y

canonMS : MyMonoid a => Mon a -> MonCanonS a
canonMS (MkMon x) = canonMS' x

cmsWorks' : MyMonoid a => (xs : Sem (MonBit a)) -> evalM' xs ~= evalMC (canonMS' xs)
cmsWorks' {a} (SSingle (MkMonBit x)) = rfl {c=a}
cmsWorks' {a} (SSingle MonZero) = rfl {c=a}
cmsWorks' {a} (SPlus x y) with (cmsWorks' x, cmsWorks' y)
  cmsWorks' {a} (SPlus x y) | (xw, yw) =
    let foo = plusPreservesEq {c=a} xw yw
        bar = evalMCMorphism {m=a} (canonMS' x) (canonMS' y)
    in trns {c=a} foo bar

cmsWorks : MyMonoid a => (xs : Mon a) -> evalM xs ~= evalMC (canonMS xs)
cmsWorks {a = a} (MkMon xs) = cmsWorks' {a} xs

solveMonoid : MyMonoid a => (xs, ys : Mon a) -> {auto canonSame : canonMS xs = canonMS ys} ->
                            evalM xs ~= evalM ys
solveMonoid {a} {canonSame} xs ys =
  let fooxs = cmsWorks xs
      fooys = symm {c=a} $ cmsWorks ys
  in ?solveMonoid_rhs


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

Mon.solveMonoid_rhs = proof
  compute
  intro a,xs,ys
  intro
  intro
  rewrite canonSame
  intros
  exact trns {c=a} fooxs fooys

semsolversimple

-- The class definitions are based closely on ones Franck Selma uses in the Idris ring solver-in-progress.
-- The rest of the code is quite unrelated.
module Set
import Classes.Verified

%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

{-
OUCH!
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
  -}

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

infixl 6 <++>
class Set c => Magma c where
  (<++>) : c -> c -> c

  -- Users must define either plusPreservesEq or both plusPreservesEqL and
  -- plusPreservesEqR
  total
  plusPreservesEqL : {c1,c1',c2:c} -> c1 ~= c1' -> c1 <++> c2 ~= c1' <++> c2

  total
  plusPreservesEqR : {c1,c2,c2':c} -> c2 ~= c2' -> c1 <++> c2 ~= c1 <++> c2'

total
plusPreservesEq : Magma c => {c1,c2,c1',c2':c} -> c1 ~= c1' -> c2 ~= c2' -> c1 <++> c2 ~= c1' <++> c2'
plusPreservesEq {c} {c1} {c2} {c1'} {c2'} c1c1' c2c2' =
  let lefty : (c1 <++> c2 ~= c1' <++> c2) = plusPreservesEqL {c} c1c1'
      righty : (c1' <++> c2 ~= c1' <++> c2') = plusPreservesEqR {c} c2c2'
  in trns {c} lefty righty

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

data Sem : Type -> Type where
  SSingle : (x : s) -> Sem s
  SPlus : (x,y : Sem s) -> Sem s

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

data SemCanon : Type -> Type where
  SCSingle : (x : s) -> SemCanon s
  SCPlus : (xs : SemCanon s) -> (y : s) -> SemCanon s

evalSC : MySemigroup s => SemCanon s -> s
evalSC (SCSingle x) = x
evalSC (SCPlus xs y) = evalSC xs <++> y

instance MySemigroup s => Set (SemCanon s) where
  x ~= y = evalSC x ~= evalSC y
  rfl = rfl {c=s}
  symm = symm {c=s}
  trns = trns {c=s}

scPlus : SemCanon s -> SemCanon s -> SemCanon s
scPlus xs (SCSingle x) = xs `SCPlus` x
scPlus xs (SCPlus x y) = (xs `scPlus` x) `SCPlus` y

mutual
  plusPreservesEqLSC : MySemigroup s => {c1,c1',c2:SemCanon s} ->
                       c1 ~= c1' -> (c1 `scPlus` c2) ~= (c1' `scPlus` c2)

  plusPreservesEqLSC {c1} {c1'} {c2} c1c1' =
    let
      foo : (evalSC (c1 `scPlus` c2) ~= evalSC c1 <++> evalSC c2)
          = evalSCMorphism {s} c1 c2
      bar : (evalSC c1 <++> evalSC c2 ~= evalSC c1' <++> evalSC c2)
          = plusPreservesEqL {c=s} {c2=evalSC c2} c1c1'
      baz : (evalSC (c1 `scPlus` c2) ~= evalSC c1' <++> evalSC c2)
          = trns {c=s} foo bar
      quux : (evalSC c1' <++> evalSC c2 ~= evalSC (c1' `scPlus` c2))
           = symm {c=s} $ evalSCMorphism {s} c1' c2
      in trns {c=s} baz quux

  evalSCMorphism : MySemigroup s => (xs,ys : SemCanon s) -> evalSC (xs `scPlus` ys) ~= evalSC xs <++> evalSC ys
  evalSCMorphism {s} xs (SCSingle x) = rfl {c=s}
  evalSCMorphism {s} xs (SCPlus x y) =
    let
        foo : (evalSC (xs `scPlus` x) ~= evalSC xs <++> evalSC x) = evalSCMorphism xs x
        bar : (evalSC (xs `scPlus` x) <++> y ~= (evalSC xs <++> evalSC x) <++> y)
                = plusPreservesEqL {c=s} {c2=y} foo
        baz : (evalSC xs <++> evalSC x <++> y ~= evalSC xs <++> (evalSC x <++> y))
                = symm {c=s} $ plusAssoc (evalSC xs) (evalSC x) y
    in trns {c=s} bar baz

instance MySemigroup s => Magma (SemCanon s) where
  (<++>) = scPlus
  plusPreservesEqL c1c1' = plusPreservesEqLSC {s} c1c1'

  plusPreservesEqR {c1} {c2} {c2'} c2c2' =
    let foo = evalSCMorphism c1 c2
        bar = plusPreservesEqR {c1=evalSC c1} c2c2'
        baz = symm {c=s} $ evalSCMorphism {s} c1 c2'
        quux = trns {c=s} {y=evalSC c1 <++> evalSC c2'} {z=evalSC (scPlus c1 c2')} bar baz
    in trns {c=s} {y=evalSC c1 <++> evalSC c2} foo quux
  
canonS : MySemigroup s => Sem s -> SemCanon s
canonS (SSingle x) = SCSingle x
canonS (SPlus xs ys) = canonS xs <++> canonS ys

canonSMorphism : MySemigroup s => (xs, ys : Sem s) -> canonS (xs `SPlus` ys) ~= canonS xs <++> canonS ys
canonSMorphism {s} xs ys = rfl {c=s}

scWorks : MySemigroup s => (sm : Sem s) -> evalS sm ~= evalSC (canonS sm)
scWorks {s} (SSingle x) = rfl {c=s}
scWorks (SPlus x y) =
  let 
    xWorks = scWorks x
    yWorks = scWorks y
    xyhuh = plusPreservesEq {c=s} xWorks yWorks
    foo = evalSCMorphism (canonS x) (canonS y)
    bar = symm {c=s} foo
  in trns {c=s} {y=evalSC (canonS x) <++> evalSC (canonS y)}
                {z=evalSC (scPlus (canonS x) (canonS y))} xyhuh bar

-- Sometimes plain old equality is good enough, and we don't need general
-- equivalences. For these situations, we offer a plain version. This will
-- need a nicer interface

data Wrap a = MkWrap a
unwrap : Wrap a -> a
unwrap (MkWrap x) = x

instance VerifiedSemigroup s => Set (Wrap s) where
  (~=) = (~=~)
  rfl = Refl
  symm = sym
  trns = trans

instance VerifiedSemigroup s => Magma (Wrap s) where
  (<++>) (MkWrap x) (MkWrap y) = MkWrap (x <+> y)
  plusPreservesEqL c1c1' = rewrite sym c1c1' in Refl
  plusPreservesEqR c2c2' = cong c2c2'

instance VerifiedSemigroup s => MySemigroup (Wrap s) where
  plusAssoc (MkWrap x1) (MkWrap x2) (MkWrap x3) =
    cong $ semigroupOpIsAssociative x1 x2 x3

testing : MySemigroup s => (x,y,z,w,p:s) ->
          x <++> (y <++> (z <++> p) <++> w) ~= x <++> y <++> z <++> p <++> w
testing x y z w p = scWorks $
          SSingle x `SPlus` ((SSingle y `SPlus` (SSingle z `SPlus` SSingle p)) `SPlus` SSingle w)

instance VerifiedSemigroup Additive where
  semigroupOpIsAssociative (getAdditive x) (getAdditive y) (getAdditive z)
    = cong $ plusAssociative x y z

testingWrap : VerifiedSemigroup s => (x,y,z,w,p:s) ->
          x <+> (y <+> (z <+> p) <+> w) = x <+> y <+> z <+> p <+> w
testingWrap x y z w p =
   let foo = scWorks $
          SSingle (MkWrap x) `SPlus` ((SSingle (MkWrap y) `SPlus` (SSingle (MkWrap z) `SPlus` SSingle (MkWrap p))) `SPlus` SSingle (MkWrap w))
   in cong {f=unwrap} foo

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

instance Magma Nat where
  (<++>) = (+)
  plusPreservesEqL c1c1' = rewrite c1c1' in Refl
  plusPreservesEqR c2c2' = rewrite c2c2' in Refl

instance MySemigroup Nat where
  plusAssoc = plusAssociative

instance MyMonoid Nat where
  Zero = Z
  zeroLeftNeutral = plusZeroLeftNeutral
  zeroRightNeutral = plusZeroRightNeutral

I've added a solveSemigroup function just like solveMonoid, with essentially the same implementation. The API for the semigroup solver seems close to okay, although it could be improved. The one for the monoid solver is really quite awful, as is the "wrapped" interface.