positive type-level naturals

[wren ng thornton]

On Sun, Mar 16, 2014 at 11:06 AM, Christiaan Baaij
<christiaan.baaij at gmail.com> wrote:
> 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