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 isarith
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 2024 at 16:22 UTC