Wenda Li (Jul 28 2021 at 16:55): 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 isarith 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]
Thank you so much @Shing Tak Lam. The trace information truly helps!
Last updated: Dec 21 2024 at 12:33 UTC