## Stream: general

### Topic: Tactic for nonlinear integer arithmetic

#### Donald Sebastian Leung (Apr 13 2020 at 08:11):

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

#### Kevin Buzzard (Apr 13 2020 at 08:22):

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 (Apr 13 2020 at 08:22):

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

#### Donald Sebastian Leung (Apr 13 2020 at 08:53):

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 (Apr 13 2020 at 09:16):

I thought lia was the strongest

#### Mario Carneiro (Apr 13 2020 at 09:43):

I don't even see any nonlinearity in there though

#### Mario Carneiro (Apr 13 2020 at 09:43):

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

#### Kevin Buzzard (Apr 13 2020 at 09:50):

Ie ring can't do that

#### Mario Carneiro (Apr 13 2020 at 09:55):

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

Last updated: Aug 03 2023 at 10:10 UTC