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,
zify; ring that is sufficient for your goal.
ring on a signature for integer arithmetic registered for
Ah! I was writing simulatneously.
So ok your answer is "yes".
Assia Mahboubi has marked this topic as resolved.
Last updated: Oct 03 2023 at 21:01 UTC