## Stream: Coq users

### Topic: ✔ specification of the lia tactic on non-linear problems

#### Assia Mahboubi (Jan 12 2022 at 10:38):

Hi,
although the name of the `lia` tactic stands for "Linear Integer Arithmetic", the tactic in fact is more powerful than that, and it is actually able to solve some non linear goals. E.g.:

``````Require Import Psatz.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Lemma nonlinear (n m : nat) : 2 * m  * n + m * m + n * n = (m + n) * (n + m).
lia.
Qed.
``````

What is the actual contour of non linear problems `lia` is supposed to solve? @Frédéric Besson @Laurent Théry

#### Laurent Théry (Jan 12 2022 at 10:46):

My understanding (as user) is that `lia` is using ring for simplification so that's why your goal is proved by lia. I think it also does some ad-hoc linearisation. @Frédéric Besson will know more about this.

#### Frédéric Besson (Jan 12 2022 at 11:10):

The first step is to run `zify`: your goal is injected into Z. The next step is to develop polynomials, somehow `ring_simplify`. Then, there is some non-linear reasoning to accumulate positivity constraints that are lost by the injection into Z (think proving `forall n m:nat, n * m >= 0`). At this stage the purely linear reasoning kicks in.

As @Laurent Théry said, `lia` subsumes `zify; ring` that is sufficient for your goal.

#### Assia Mahboubi (Jan 12 2022 at 11:10):

So `lia` supersedes `ring` on a signature for integer arithmetic registered for `zify` ?

#### Assia Mahboubi (Jan 12 2022 at 11:11):

Ah! I was writing simulatneously.

#### Notification Bot (Jan 12 2022 at 11:18):

Assia Mahboubi has marked this topic as resolved.

Last updated: May 18 2024 at 10:02 UTC