# Zulip Chat Archive

## 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 `linarith`

and `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: Dec 20 2023 at 11:08 UTC