Stream: math-comp users

Topic: equation manipulation


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

view this post on Zulip Paolo Giarrusso (Sep 27 2020 at 23:12):

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

view this post on Zulip Paolo Giarrusso (Sep 27 2020 at 23:13):

IIRC, the name stands for linear integer arithmetic.

view this post on Zulip Paolo Giarrusso (Sep 27 2020 at 23:13):

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

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

view this post on Zulip Paolo Giarrusso (Sep 27 2020 at 23:15):

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

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

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

view this post on Zulip Paolo Giarrusso (Sep 27 2020 at 23:20):

Separately see also https://coq.inria.fr/distrib/current/refman/addendum/ring.html

view this post on Zulip vlj (Sep 28 2020 at 07:05):

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

view this post on Zulip Paolo Giarrusso (Sep 28 2020 at 10:48):

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

view this post on Zulip Paolo Giarrusso (Sep 28 2020 at 10:48):

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


Last updated: Feb 08 2023 at 04:04 UTC