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

@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

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

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

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: Oct 13 2024 at 01:02 UTC