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: Feb 08 2023 at 04:04 UTC