## Stream: math-comp users

### Topic: equation manipulation

#### vlj (Sep 27 2020 at 20:41):

Hi,
I'm having some troubles proving "basic" lemma involving equations on natural. For instance I want to prove that `1 <= a %/b -> a - a %/b * b <= a - b.`. Unfortunately lia doesn't work, I think that's because it's not just equation manipulation.
Currently I'm trying to use lia to transform the equation step by step to have something like `a - a %/b * b = a - b + smth` using lia but it looks unreliable. Is there a more standard way of doing ?

#### Paolo Giarrusso (Sep 27 2020 at 23:12):

lia is only guaranteed to work when multiplication is not involved.

#### Paolo Giarrusso (Sep 27 2020 at 23:13):

IIRC, the name stands for linear integer arithmetic.

#### Paolo Giarrusso (Sep 27 2020 at 23:13):

(2*a is still linear in a since it expands to a + a)

#### Paolo Giarrusso (Sep 27 2020 at 23:14):

however, the relevant manual chapter mentions the non-linear variant, nia. I’ve never used it, especially with math-comp, but that seems the relevant direction.

#### Paolo Giarrusso (Sep 27 2020 at 23:15):

(lia does handle inequalities, again with the above restrictions)

#### Paolo Giarrusso (Sep 27 2020 at 23:18):

Also maybe relevant is psatz, but I don’t understand the details on the algorithm https://coq.inria.fr/distrib/current/refman/addendum/micromega.html#psatz-a-proof-procedure-for-non-linear-arithmetic

#### Paolo Giarrusso (Sep 27 2020 at 23:18):

The details on nia and nra are easier https://coq.inria.fr/distrib/current/refman/addendum/micromega.html#nra-a-proof-procedure-for-non-linear-arithmetic

#### vlj (Sep 28 2020 at 07:05):

@Paolo Giarrusso thanks !!! Nia was enough to prove what I wanted with a single line.

#### Paolo Giarrusso (Sep 28 2020 at 10:48):

oh cool! sounds like it does more than the manual describes!

#### Paolo Giarrusso (Sep 28 2020 at 10:48):

(or maybe I understood the manual even less than I thought)

Last updated: Jul 15 2024 at 20:02 UTC