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

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.

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.

So `lia`

supersedes `ring`

on a signature for integer arithmetic registered for `zify`

?

Ah! I was writing simulatneously.

So ok your answer is "yes".

Assia Mahboubi has marked this topic as resolved.

Last updated: Oct 13 2024 at 01:02 UTC