Stream: Coq users

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


view this post on Zulip 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?

view this post on Zulip Paolo Giarrusso (Feb 04 2022 at 04:09):

lia = linear integer arithmetic.

view this post on Zulip 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

view this post on Zulip Paolo Giarrusso (Feb 04 2022 at 04:10):

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

view this post on Zulip Paolo Giarrusso (Feb 04 2022 at 04:11):

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

view this post on Zulip 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.

view this post on Zulip Daniel Hilst Selli (Feb 04 2022 at 11:51):

@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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip Daniel Hilst Selli (Feb 04 2022 at 11:58):

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

view this post on Zulip Paolo Giarrusso (Feb 04 2022 at 11:59):

"linear" excludes *

view this post on Zulip Daniel Hilst Selli (Feb 04 2022 at 11:59):

I was thinking about linear as linear equations ax + b

view this post on Zulip Daniel Hilst Selli (Feb 04 2022 at 12:00):

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

view this post on Zulip Paolo Giarrusso (Feb 04 2022 at 12:00):

that can only be considered linear if a is ignored

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Paolo Giarrusso (Feb 04 2022 at 12:03):

yes

view this post on Zulip Daniel Hilst Selli (Feb 04 2022 at 12:03):

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

view this post on Zulip 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 :-)

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Paolo Giarrusso (Feb 04 2022 at 12:06):

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

view this post on Zulip 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 :)

view this post on Zulip 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