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 ?

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

IIRC, the name stands for *linear* integer arithmetic.

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

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.

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

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

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

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

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

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

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

Last updated: Jul 15 2024 at 20:02 UTC