Using `sbv` to detect if a fold is commutative

commutative.hs

import Data.SBV

import Control.Applicative ((<$>))
import Prelude hiding (sum, count)

------------------------------------------------------------------------

main :: IO ()
main = do
  x <- satWith z3 { timing = True, smtFile = Just "smt.txt" } program
  print x
  return ()

program :: Symbolic SBool
program = bAnd <$> sequence
  [ commutes n sum
  , commutes n count
  , commutes n mean
--  , commutes n newest
--  , commutes n oldest
  ]
  where
    n = 10 -- how big is the list we try

commutes :: (SymWord a, EqSymbolic b) => Int -> ([SBV a] -> b) -> Symbolic SBool
commutes n f = do
  xs <- mkForallVars n
  let xs' = reverse xs
  return (f xs .== f xs')

------------------------------------------------------------------------
-- !Commutative

-- newest v = latest 1 ~> let fold1 s = v : v ~> s.
newest :: [SReal] -> SReal
newest xs = last xs

-- oldest v = let fold1 s = v : s ~> s.
oldest :: [SReal] -> SReal
oldest xs = head xs

------------------------------------------------------------------------
-- Commutative

-- sum v = let fold s = 0 : v + s ~> s.
sum :: [SReal] -> SReal
sum xs = foldl (+) 0 xs

-- count = let fold c = 0 : c + 1 ~> c.
count :: [SReal] -> SReal
count xs = foldl (\x _ -> x + 1) 0 xs

-- mean v = sum (double v) / count.
mean :: [SReal] -> SReal
mean xs = sum xs / count xs