Assia Mahboubi (Jan 12 2022 at 10:38): 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.
Assia Mahboubi (Jan 12 2022 at 11:11):So ok your answer is "yes".
Notification Bot (Jan 12 2022 at 11:18):Assia Mahboubi has marked this topic as resolved.
Last updated: Oct 03 2023 at 21:01 UTC