On Sun, Mar 16, 2014 at 11:06 AM, Christiaan Baaij
Iavor is working on a branch that allows the constraint solver to call an external solver: https://github.com/ghc/ghc/tree/decision-procedure Currently, it: a) only supports CVC4 (an SMT solver), and b) is slightly out of of line with HEAD. I think the above branch will be able to solve things like: 1 <= n + 1 ~ True
I don't know much about CVC4, but I do know that Presberger arithmetic is decidable-- which means all the addition-based inequalities can be proven automatically. With that in hand, the only things users or other solvers would have to worry about is multiplying two variables together (multiplying a variable by a constant is included in PA) and similar things (like exponentiation). It shouldn't be too hard to copy over the PA solver used in Coq, though I have no idea how hard it'd be to actually hook the solver up to GHC. The other thing to look at is Agda's (semi)ring solver which, iirc, has the same pros and cons as your patch: variable multiplications but no inequalities. Given the undecidability of Peano arithmetic, the only real way forward will require the ability for users to generate proofs manually-- which is still sorely lacking. Or course, we'd like to have solvers to automate away as much of this as possible, but it's known that we can't automate all of it away. -- Live well, ~wren