I trying to prove this simple lemma, it seems reasonable to be
Require Import ZArith. Require Import Lia. Open Scope Z_scope. Lemma foo : forall m n M, m >= 0 -> n > 0 -> m <= M / n -> m * n <= M.
I was expecting lia so solve this easily but for my surprise it doesn't. FIrst question _Is this true in general, I did some property tests, and tried to look for some counter examples but couldn't find one_. Second question _Is there any intuition to help to understand when lia helps and when it doesn't? Any material on how lia works would be helpfull_. And the last question is how to attach these arithmetic problems when lia can't help?
lia = linear integer arithmetic.
there are nia and psatz for this scenario, but nia does little and psatz requires a special external solver
Lia has some docs in the manual, but they're probably not too helpful.
as a hint, lia is (claimed to be) a complete decision procedure for Presburger arithmetic.
To have support for division, you need to set the following:
Ltac Zify.zify_post_hook ::= Z.to_euclidean_division_equations.
If you look at the resulting goal after
zify, you will see that the goal is not linear.
In this case,
nia does the job.
@Paolo Giarrusso I think you're talking about this page https://coq.github.io/doc/V8.11.0/refman/addendum/micromega.html
Also I think I need to understand Positivstellensatz refutations to understand lia
In fact nia works for this goal, I just forgot about
nia at all. I would like to build a intuition on this but that
Positivstellennsatz refutations are complex to me yet, I will try to digest it
@Daniel Hilst Selli I don't think you need "Positivstellennsatz", AFAIK that's an implementation technique which you can happily ignore
@Daniel Hilst Selli if you want to know exactly what
lia is guaranteed to solve, you can read about https://en.wikipedia.org/wiki/Presburger_arithmetic
(also those docs are years old, best check https://coq.inria.fr/refman/coq-tacindex.html#cap-l)
Sorry the newbie question but what exactly means to be linear for lia, having
/\ \/ ~ + - * < > >= <= operators?
I was thinking about linear as linear equations
ax + b
So linear is only
-because it's another kind of
that can only be considered linear if
a is ignored
indeed, that's linear _in_
a is a concrete number, that can be translated into Presburger arithmetic, via
x + x + x + .... + x + b
I didn't know about Presburger arithmetic, so lia can solve Presburger arithmetic, that's right?e
Okay, thanks Paolo! I will take a look into it
beware: that does not mean that
lia can solve all goals involving those things, only that it has reasoning techniques for those operators. For instance,
lia is often not able to
unfold definitions so you might need to do that yourself :-)
to be honest I'm always using lia in trial error way, and when it does't work I stay stuck on a subgoal
Yeah I know about having to unfold :) it's possible to automate this with the pre hook, pretty cool indeed
psazt I never used it I will take a look at it too, thanks again
some "trial and error" is common, but this helps have an idea
Yeah the problem is not the trial and error, is getting stuck with no idea in the error case, which is quite common here :)
I like to have at last an intuition about things
Last updated: Oct 04 2023 at 23:01 UTC