## Stream: General

### Topic: nlinarith for Isabelle

#### Wenda Li (Jul 28 2021 at 16:55):

The following problem:

``````theorem
fixes a b c::real
assumes h0: "0 < a ∧ 0 < b ∧ 0 < c"
and h1: "a * (b + c) = 152"
and h2: "b * (c + a) = 162"
and h3: "c * (a + b) = 170"
shows "a * b * c = 720"
``````

can automatically be solved by the `nlinarith` tactic in Lean, where `nlinarith` extends `linarith` by having some pre-processings. In comparison, we do have the `linarith` tactic in Isabelle, while it appears that we don't have the `nlinarith` tactic yet (or do we?).

Maybe we can aim to similarly extend our `linarith` tactic. Any thoughts?

#### Mathias Fleury (Jul 28 2021 at 17:48):

As far as I know there is`arith` that calls linarith, but I have no idea what it does

#### Manuel Eberl (Jul 28 2021 at 18:12):

I wonder what pre-processing that is. That example absolutely doesn't look linear.

#### Wenda Li (Jul 29 2021 at 05:23):

Here is the documented pre-processing steps:

``````An extension of `linarith` with some preprocessing to allow it to solve some nonlinear arithmetic
problems. (Based on Coq's `nra` tactic.) See `linarith` for the available syntax of options,
which are inherited by `nlinarith`; that is, `nlinarith!` and `nlinarith only [h1, h2]` all work as
in `linarith`. The preprocessing is as follows:
* For every subterm `a ^ 2` or `a * a` in a hypothesis or the goal,
the assumption `0 ≤ a ^ 2` or `0 ≤ a * a` is added to the context.
* For every pair of hypotheses `a1 R1 b1`, `a2 R2 b2` in the context, `R1, R2 ∈ {<, ≤, =}`,
the assumption `0 R' (b1 - a1) * (b2 - a2)` is added to the context (non-recursively),
where `R ∈ {<, ≤, =}` is the appropriate comparison derived from `R1, R2`.
``````

I have a rough idea about how it works, but am still quite amazed by the fact that it can solve the example above automatically.

#### Shing Tak Lam (Jul 29 2021 at 12:47):

By the way you can use `set_option trace.linarith true` to see what `(n)linarith` is doing. For your example, `linarith` generates the following facts

``````[a * b * c - 720 < 0,
-c < 0,
-b < 0,
-a < 0,
c * (a + b) - 170 = 0,
b * (c + a) - 162 = 0,
a * (b + c) - 152 = 0]
``````

The pre-processing stage specific to `nlinarith` is run after the general `linarith` pre-precessing, and after running the `nlinarith` specific pre-processing, `nlinarith` has the following facts

``````[a * b * c - 720 < 0,
-c < 0,
-b < 0,
-a < 0,
c * (a + b) - 170 = 0,
b * (c + a) - 162 = 0,
a * (b + c) - 152 = 0,
(a * (b + c) - 152) * (a * (b + c) - 152) = 0,
(b * (c + a) - 162) * (a * (b + c) - 152) = 0,
(b * (c + a) - 162) * (b * (c + a) - 162) = 0,
(c * (a + b) - 170) * (a * (b + c) - 152) = 0,
(c * (a + b) - 170) * (b * (c + a) - 162) = 0,
(c * (a + b) - 170) * (c * (a + b) - 170) = 0,
-a * (a * (b + c) - 152) = 0,
-a * (b * (c + a) - 162) = 0,
-a * (c * (a + b) - 170) = 0,
-(-a * -a) < 0,
-b * (a * (b + c) - 152) = 0,
-b * (b * (c + a) - 162) = 0,
-b * (c * (a + b) - 170) = 0,
-(-b * -a) < 0,
-(-b * -b) < 0,
-c * (a * (b + c) - 152) = 0,
-c * (b * (c + a) - 162) = 0,
-c * (c * (a + b) - 170) = 0,
-(-c * -a) < 0,
-(-c * -b) < 0,
-(-c * -c) < 0,
(a * b * c - 720) * (a * (b + c) - 152) = 0,
(a * b * c - 720) * (b * (c + a) - 162) = 0,
(a * b * c - 720) * (c * (a + b) - 170) = 0,
-((a * b * c - 720) * -a) < 0,
-((a * b * c - 720) * -b) < 0,
-((a * b * c - 720) * -c) < 0,
-((a * b * c - 720) * (a * b * c - 720)) < 0]
``````

#### Wenda Li (Jul 30 2021 at 10:05):

Thank you so much @Shing Tak Lam. The trace information truly helps!

Last updated: Dec 07 2023 at 16:21 UTC