Prove simple theorems in Haskell in automated way

Question

I would like to prove in Haskell, whether in vanilla Haskell or using some libraries / tools, some simple theorems such as:

and [n*(n+1)/2 == sum [0..n] | n <- [0..]]

Is there a simple enough (ie. fully automated) way to prove such theorems involving integers in Haskell? I am not really interested in the proof itself, or a counterexample, but merely a yes/no answer.

There's this publication which doesn't seem practically usable; other than that most of everything else seems to be rather complex, ie. involving a completely separate language and not concerning Haskell.

Answer 1

SMT (satisfiablity-modulo-theories) solvers can provide an (almost-) push-button solution for at least a subset of such problems, especially for those that use machine-arithmetic, IEEE-floats, etc., where efficient decision procedures do exist. There's also good support for arrays and data-types, along with reasoning about arithmetic with mixed types.

There are several Haskell libraries built on-top-of SMT solvers to access these features. So, the answer to your question is a qualified "yes." If you squint the right way, then you can code and prove properties of many Haskell functions using SMT-solvers.

I say "squint" because you'll have to modify your functions to work with symbolic values. This translation depends on the exact problem you're working on and what library you use. I'm most familiar with SBV, so my answer below uses that system.

For non-recursive functions that work on numbers (i.e., machine integers, reals, floats, unbounded integers etc.), the translation is relatively easy. Things get hairy when you have algebraic types, but support is there for most common data structures. You can see many examples at SBV's hackage documentation.

Where things get tricky is recursion: Both recursive functions and recursive data-types are problematic for SMT solving. While the underlying solvers do support such definitions, proof-support is (at least for the time being) rather weak. The main reason is that any interesting property of a recursive definition will need to use induction, and SMT solvers do not perform induction out-of-the-box.

However, for a certain subset of problems, you can make quite a bit of progress. SBV supports several programming idioms and proof tricks that let you do inductive proofs over naturals. Since you mentioned sum in your question, here's an example based on that.¹

First some preliminaries:

module Example where

import Data.SBV
import Data.SBV.Tools.NaturalInduction

This simply brings SBV in scope, and the induction tactic. Let's recursively define summing numbers up to an arbitrary natural n:

sumToN :: SInteger -> SInteger
sumToN = smtFunction "sumToN" $ \n -> ite (n .== 0) 0 (n + sumToN (n-1))

Of course, in regular Haskell you'd write this simply as sum [1..n]. Alas, that definition won't do when we want to prove it for all n. This is the "symbolic transformation" you need to do. Since Haskell's if-then-else takes a boolean as an argument, we use ite instead, which does the same thing but over symbolic test values.² Also note how we tell the solver to not expand this definition by explicitly marking it as an smtFunction. Unless you mark functions this way, SBV will unroll them at each call site, and that won't work here since n is symbolic and thus the recursive call will never terminate.

Now we can write a little helper:

check :: (SInteger -> SInteger) -> IO ThmResult
check f = inductNat $ \n -> (sumToN_spec n, f n)
  where sumToN_spec :: SInteger -> SInteger
        sumToN_spec n = (n * (n+1)) `sEDiv` 2

This simply calls SBV's inductNat function, which itself takes a split-predicate: That is, a function that takes a natural number and evaluates the "left-hand-side" (which you can think of as the specification), and the "right-hand-side" (which you can think of as the implementation). The spec is defined right there as the usual formula. (The function sEDiv is symbolic euclidian division, which is equivalent to regular division when the divisor is positive.³)

We can now check if our definition is good:

*Example> check sumToN
Q.E.D.

And voila, we have our proof.

It's instructive to see what happens if we make a mistake. Let's write a buggy version of our function:

sumToN_bad :: SInteger -> SInteger
sumToN_bad n = ite (n .== 123) 0 (sumToN n)

We introduced a point-failure: A corner case bug if you will: The function will work for all values except 123. Note that the above looks exactly what you'd write in Haskell, aside for the use of ite: Since it's not recursive we can let SBV unroll it in all call-sites. (Notice we didn't call smtFunction. We could've; but we didn't need to.) We now have:

*Example> check sumToN_bad
Falsifiable. Counter-example:
  P(0)   =       (0,0) :: (Integer, Integer)
  P(k)   = (7503,7503) :: (Integer, Integer)
  P(k+1) =    (7626,0) :: (Integer, Integer)
  k      =         122 :: Integer

We get a full-account of the induction proof. The base case (i.e., 0) passes. The proof is also true all the way up to 122, but spec and the implementation diverge at k+1 = 123. Note how difficult it would be for a test based approach to catch this bug: It'd have to use 123 as its test value. But an SMT solver can easily identify such corner cases.

Of course, this doesn't mean the SMT solver will be able to complete all such proofs. SMT solving is not a panacea, it's merely another tool to use in verification. It's entirely possible that it will loop-forever, since decision procedures for recursive definitions is necessarily incomplete. My experience, however, is that they work well in most practical cases, and hopefully SMT-solvers will continue to improve to make such problems even more amenable to these sorts of techniques. At the cost of more user-involvement, a better approach is to use a proper theorem prover (such as Isabelle, Coq, ACL2 etc.), and use SMT-solvers as engines in proof discovery, allowing you to discharge many proof-obligations (especially those involving arithmetic) automatically.

---

¹ SBV will call to Microsoft's z3 SMT solver by default. See https://github.com/Z3Prover/z3. SBV can also use other SMT solvers as well (such as cvc5, yices, etc.), though support for z3 is the most robust. Make sure you installed z3 and its executable is in your path before you use SBV.

² One can use rebindable syntax in GHC to allow if to be used, but I find that approach more confusing than helpful.

³ We use euclidian division instead of the regular Haskell division, since SMT solvers deal with it much better. SBV supports both variants.

Answer 2

Look at Agda [1][2]

I think that it's exactly what you are looking for.

I recommend using its emacs mode for autocompletion and hole/interactive programming. [2]/quick-guide.html

A very good introduction is plfa [3], also [2]/tutorial-list.html

[1] https://en.wikipedia.org/wiki/Agda_(programming_language)

[2] https://agda.readthedocs.io/en/v2.6.0.1/getting-started/what-is-agda.html

[3] https://plfa.github.io/

Answer 3

On top of everyone else, don't forget that the Curry-Howard correspondence also gives you a way to prove theorems.

Say you want to prove that $B \wedge (A \vee (B \rightarrow A)) \rightarrow A$. Here's the proof:

-- The statement of the theorem...
proof :: (b, Either a (b -> a)) -> a
-- ...and the proof.
proof (b, Left a) = a
proof (b, Right f) = f b