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?

Smack

Your prove line is equivalent to prove (forall "x" .== forall "x"). I never used SBV, but this looks wrong to me. – Fluent

You are right. Anyway I was even unable to compile it because we cannot use .== on symbolic (without formal "x" should be also a symbolic value) – Smack

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.

Phalangeal

That is a really great answer. If I could I would uproot it man times, thanks! :) You've mentioned that SMT-solvers are not good at resolving this kind of problems. IS there any "other" type of solvers that is specialised in this domain? – Smack

If you have heavy use of quantifiers and "deep" mathematical theorems, you pretty much have to resort to using traditional theorem provers, such as Isabelle, HOL, or Coq. While these are "manual," (i.e., you have to develop the proof yourself), they have made tremendous progress in the last decade or so that they will be able to discharge many proof goals with little effort. But they are not push-button tools like SMT-solvers are; so some manual work will be needed. This answer seems appropriate for further reading: mathoverflow.net/questions/8260/… – Phalangeal

I've got yet another small question regarding this topic. I wanted to use this solver in my own type-checker. I do not think using HOL or Coq in a type checker of other language is a good decision (It feels awkward at last). I have heavy use of quantifiers (lets say the language is similar to Haskell in some way). I was planning to use Z3, but after your answer I'm not sure if that is a good solution. Would you have any further suggestions to me regarding this topic? I would be very thankful for any hint than would help me choose the best solution here :) – Smack

Answer 2

Your use of the API isn't quite right. The simplest way to prove mathematical equalities would be to use simple functions. For instance, associativity over unbounded Integers can be expressed this way:

prove $ \x y z -> x + (y + z) .== (x + y) + (z :: SInteger)

If you need a more programmatic interface (and sometimes you will), then you can use the Symbolic monad, thusly:

plusAssoc = prove $ do x <- sInteger "x"
                       y <- sInteger "y"
                       z <- sInteger "z"
                       return $ x + (y + z) .== (x + y) + z

I'd recommend browsing through many of the examples provided in the hackage site to get familiar with the API: https://hackage.haskell.org/package/sbv

Phalangeal

Thank you very much for the reply. Unfortunately I cannot use this interface, because I do not want to run the proves on integers. I want to run them on my own "types" and my own functions (like +, which for the type A will be defined associative, but without 0 element, etc). In fact that is what I'm trying to code right now. If you've got any hints regarding this, I would be very thankful if you share it with me! :) – Smack

Best way to do that would be to use uninterpreted functions. Sorry for the late reply here; please contact me if you still have issues. – Phalangeal