Stream: Coq users

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


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

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

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

view this post on Zulip Assia Mahboubi (Jan 12 2022 at 11:10):

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

view this post on Zulip Assia Mahboubi (Jan 12 2022 at 11:11):

Ah! I was writing simulatneously.

view this post on Zulip Assia Mahboubi (Jan 12 2022 at 11:11):

So ok your answer is "yes".

view this post on Zulip Notification Bot (Jan 12 2022 at 11:18):

Assia Mahboubi has marked this topic as resolved.


Last updated: Feb 09 2023 at 00:03 UTC