[Haskell-cafe] is there a way to prove the equivalence of these two implementations of (Prelude) break function?

[Thomas Hartman]

Here's two implementations of break, a snappy one from the prelude,
and a slow stupid stateful one.

They are quickchecked to be identical.

Is there a way to prove they are identical mathematically? What are
the techniques involved? Or to transform one to the other?

import Control.Monad.State
import Test.QuickCheck

tThis = take 5 . show .  mybreak (>4000000) $ [1..10^7]
tPrel = take 5 . show .  prelbreak (>4000000) $ [1..10^7]


prelbreak p xs = (takeWhile (not . p) xs,dropWhile (not . p) xs) --
fast, more or less as implemented in prelude iiuc

mybreak p xs =  evalState (brk p) ([],xs) -- stateful, slow
brk p = do
      (notsat,remaining) <- get
      case remaining of
        [] -> return (notsat,remaining)
        (r:rs) -> if p r
                    then return (notsat,remaining)
                    else do put (notsat++[r],rs) -- ++ is probaby a
major reason
                            brk p