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?

As far as I know there is`arith`

that calls linarith, but I have no idea what it does

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

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.

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]
```

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

Last updated: Dec 07 2023 at 16:21 UTC