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?

"linear" excludes `*`

I was thinking about linear as linear equations `ax + b`

So linear is only `+ `

(and `-`

because it's another kind of `+`

)

that can only be considered linear if `a`

is ignored

indeed, that's linear _in_ `x`

; if `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

yes

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

and about `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: Jun 15 2024 at 08:01 UTC