## Stream: Coq users

### Topic: Why lia can't prove `m <= M / n -> n * m <= M`

#### Daniel Hilst Selli (Feb 04 2022 at 03:48):

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?

#### Paolo Giarrusso (Feb 04 2022 at 04:09):

lia = linear integer arithmetic.

#### Paolo Giarrusso (Feb 04 2022 at 04:09):

there are nia and psatz for this scenario, but nia does little and psatz requires a special external solver

#### Paolo Giarrusso (Feb 04 2022 at 04:10):

Lia has some docs in the manual, but they're probably not too helpful.

#### Paolo Giarrusso (Feb 04 2022 at 04:11):

as a hint, lia is (claimed to be) a complete decision procedure for Presburger arithmetic.

#### Frédéric Besson (Feb 04 2022 at 09:03):

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.

#### Daniel Hilst Selli (Feb 04 2022 at 11:51):

Also I think I need to understand Positivstellensatz refutations to understand lia

#### Daniel Hilst Selli (Feb 04 2022 at 11:53):

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

#### Paolo Giarrusso (Feb 04 2022 at 11:57):

@Daniel Hilst Selli I don't think you need "Positivstellennsatz", AFAIK that's an implementation technique which you can happily ignore

#### Paolo Giarrusso (Feb 04 2022 at 11:57):

@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

#### Paolo Giarrusso (Feb 04 2022 at 11:58):

(also those docs are years old, best check https://coq.inria.fr/refman/coq-tacindex.html#cap-l)

#### Daniel Hilst Selli (Feb 04 2022 at 11:58):

Sorry the newbie question but what exactly means to be linear for lia, having `/\ \/ ~ + - * < > >= <=` operators?

#### Paolo Giarrusso (Feb 04 2022 at 11:59):

"linear" excludes `*`

#### Daniel Hilst Selli (Feb 04 2022 at 11:59):

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

#### Daniel Hilst Selli (Feb 04 2022 at 12:00):

So linear is only `+ ` (and `-`because it's another kind of `+`)

#### Paolo Giarrusso (Feb 04 2022 at 12:00):

that can only be considered linear if `a` is ignored

#### Paolo Giarrusso (Feb 04 2022 at 12:01):

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`

#### Daniel Hilst Selli (Feb 04 2022 at 12:02):

I didn't know about Presburger arithmetic, so lia can solve Presburger arithmetic, that's right?e

yes

#### Daniel Hilst Selli (Feb 04 2022 at 12:03):

Okay, thanks Paolo! I will take a look into it

#### Paolo Giarrusso (Feb 04 2022 at 12:03):

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 :-)

#### Daniel Hilst Selli (Feb 04 2022 at 12:04):

to be honest I'm always using lia in trial error way, and when it does't work I stay stuck on a subgoal

#### Daniel Hilst Selli (Feb 04 2022 at 12:04):

Yeah I know about having to unfold :) it's possible to automate this with the pre hook, pretty cool indeed

#### Daniel Hilst Selli (Feb 04 2022 at 12:06):

and about `psazt` I never used it I will take a look at it too, thanks again

#### Paolo Giarrusso (Feb 04 2022 at 12:06):

some "trial and error" is common, but this helps have an idea

#### Daniel Hilst Selli (Feb 04 2022 at 12:09):

Yeah the problem is not the trial and error, is getting stuck with no idea in the error case, which is quite common here :)

#### Daniel Hilst Selli (Feb 04 2022 at 12:09):

I like to have at last an intuition about things

Last updated: Jan 29 2023 at 01:02 UTC