Tactic for nonlinear integer arithmetic

Stream: general

[Donald Sebastian Leung]

In Coq, there is an incomplete decision procedure nia for nonlinear integer arithmetic. Does a similar tactic exist in Lean?

[Kevin Buzzard]

There is ring/ring_exp and linarithand omega but other than those I think you're on your own. Can you give an example of a goal nia solves?

[Kevin Buzzard]

I'd like to have some kind of a feeling about what we're missing

[Donald Sebastian Leung]

For example, it can solve the equivalent of this goal in Coq immediately:

k : ℕ
hge : fib (succ k) ≥ fib k
h : fib (2 * k) = fib k * (2 * fib (succ k) - fib k)
h0 : fib (succ (2 * k)) =
     fib k * fib k + fib (succ k) * fib (succ k)
⊢ fib (succ (2 * k)) + fib (2 * k) =
fib (succ k) * (2 * (fib (succ k) + fib k) - fib (succ k)) ∧
fib (succ (2 * k)) + fib (2 * k) + fib (succ (2 * k)) =
fib (succ k) * fib (succ k) +
(fib (succ k) + fib k) * (fib (succ k) + fib k)

[Kenny Lau]

I thought lia was the strongest

[Mario Carneiro]

I don't even see any nonlinearity in there though

[Mario Carneiro]

ring could do that (or at least, if it did grobner basis stuff)

[Kevin Buzzard]

Ie ring can't do that

[Mario Carneiro]

I should make a wrapper around ring like ring_hyp a1 * h1 + a2 * h2 where it multiplies the hypotheses (which are equations) by the coefficients and uses ring to prove that they add up to the equation in the goal. That would give it the same power as a grobner basis tactic except you have to provide the coefficients yourself