vlj (Sep 27 2020 at 20:41): 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
Paolo Giarrusso (Sep 27 2020 at 23:20):Separately see also https://coq.inria.fr/distrib/current/refman/addendum/ring.html
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: Oct 13 2024 at 01:02 UTC