Stream: General

Topic: nlinarith for Isabelle


view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Manuel Eberl (Jul 28 2021 at 18:12):

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

view this post on Zulip 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.

view this post on Zulip 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]

view this post on Zulip Wenda Li (Jul 30 2021 at 10:05):

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


Last updated: Mar 28 2024 at 12:29 UTC