Symbolic theory proving using SBV and Haskell

Question

I'm using SBV (with Z3 backend) in Haskell to create some theory provers. I want to check if forall x and y with given constrains (like x + y = y + x, where + is a "plus operator", not addition) some other terms are valid. I want to define axioms about the + expression (like associativity, identity etc.) and then check for further equalities, like check if a + (b + c) == (a + c) + b is valid formal a, b and c.

I was trying to accomplish it using something like:

main = do
    let x = forall "x"
    let y = forall "y"
    out <- prove $ (x .== x)
    print "end"

But it seems we cannot use the .== operator on symbolic values. Is this a missing feature or wrong usage? Are we able to do it somehow using SBV?

Answer 1

That sort of reasoning is indeed possible, through the use of uninterpreted sorts and functions. Be warned, however, that reasoning about such structures typically requires quantified axioms, and SMT-solvers are usually not terribly good at reasoning with quantifiers.

Having said that, here's how I would go about it, using SBV.

First, some boiler-plate code to get an uninterpreted type T:

{-# LANGUAGE DeriveDataTypeable #-}

import Data.Generics
import Data.SBV

-- Uninterpreted type T
data T = TBase () deriving (Eq, Ord, Data, Typeable, Read, Show)
instance SymWord T
instance HasKind T
type ST = SBV T

Once you do this, you'll have access to an uninterpreted type T and its symbolic counterpart ST. Let's declare plus and zero, again just uninterpreted constants with the right types:

-- Uninterpreted addition
plus :: ST -> ST -> ST
plus = uninterpret "plus"

-- Uninterpreted zero
zero :: ST
zero = uninterpret "zero"

So far, all we told SBV is that there exists a type T, and a function plus, and a constant zero; expressly being uninterpreted. That is, the SMT solver makes no assumptions other than the fact that they have the given types.

Let's first try to prove that 0+x = x:

bad = prove $ \x -> zero `plus` x .== x

If you try this, you'll get the following response:

*Main> bad
Falsifiable. Counter-example:
  s0 = T!val!0 :: T

What the SMT solver is telling you is that the property does not hold, and here's a value where it doesn't hold. The value T!val!0 is a Z3 specific response; other solvers can return other things. It's essentially an internal identifier for a habitant of the type T; and other than that we know nothing about it. This isn't terribly useful of course, as you don't really know what associations it made for plus and zero, but it is to be expected.

To prove the property, let's tell the SMT solver two more things. First, that plus is commutative. And second, that zero added on the right doesn't do anything. These are done via addAxiom calls. Unfortunately, you have to write your axioms in the SMTLib syntax, as SBV doesn't (at least yet) support axioms written using Haskell. Note also we switch to using the Symbolic monad here:

good = prove $ do
         addAxiom "plus-zero-axioms"
                  [ "(assert (forall ((x T) (y T)) (= (plus x y) (plus y x))))"
                  , "(assert (forall ((x T)) (= (plus x zero) x)))"
                  ]
         x <- free "x"
         return $ zero `plus` x .== x

Note how we told the solver x+y = y+x and x+0 = x, and asked it to prove 0+x = x. Writing axioms this way looks really ugly since you have to use the SMTLib syntax, but that's the current state of affairs. Now we have:

*Main> good
Q.E.D.

Quantified axioms and uninterpreted-types/functions are not the easiest things to use via the SBV interface, but you can get some mileage out of it this way. If you have heavy use of quantifiers in your axioms, it's unlikely that the solver will be able to answer your queries; and will likely respond unknown. It all depends on the solver you use, and how hard the properties to prove are.