Cody Roux (Jun 17 2020 at 20:05): Cody Roux (Jun 17 2020 at 20:05):Hi all, I'm trying to prove something along the lines of 0 < x < 12 -> x = (x - 1 + 1) mod 12. Any tactics that allow me to do this from stdlib?
Wolf Honore (Jun 17 2020 at 20:09):The Z.mod_small lemma from ZArith plus lia should be able to solve that.
Wolf Honore (Jun 17 2020 at 20:09):Assuming x is Z
Cody Roux (Jun 17 2020 at 20:11):Yep! But I have 15 lemmas with slight variations of this theme, so I was hoping for something like lia...
Anton Trunov (Jun 17 2020 at 20:27):If you are willing to install a plugin (and external solvers it depends on), then I believe coq-hammer will be able to handle those. If you are an opam user:
opam repo add coq-released https://coq.inria.fr/opam/released
opam install coq-hammer
Then scrush tactic should be able to handle those lemmas.
Cody Roux (Jun 17 2020 at 20:34):Ooooh! Thanks Anton.
Anton Trunov (Jun 17 2020 at 20:36):@Cody Roux You are welcome! coq-hammer is an awesome thing, but sometimes seemingly randomly breaks. Please let me know if it breaks for you, I'm curious now :)
Karl Palmskog (Jun 17 2020 at 20:37):just a note that if the only goal is to get the scrush tactic and similar tactics (which call lia), one only needs:
opam install coq-hammer-tactics
and
From Hammer Require Import Tactics.
the hammer tactic (the plugin part) doesn't do all that well on arithmetic goals if I recall correctly
Bas Spitters (Jun 17 2020 at 20:58):How does scrush compare to the more recent sauto ?
Karl Palmskog (Jun 17 2020 at 21:10):scrush is just a thin layer on top of sauto. It's literally defined as try strivial; ssimpl; sauto
Bas Spitters (Jun 18 2020 at 14:33):Any experience combining scrush with math-comp? I know this was a problem before.
Karl Palmskog (Jun 18 2020 at 14:58):Lukasz has a CoqHammer branch called mathcomp. However, this branch doesn't seem aware of things like zify and https://github.com/pi8027/mczify
Anton Trunov (Jun 18 2020 at 14:59):Also, some tactics from this project turned out to be helpful in my experience: https://github.com/amahboubi/lia4mathcomp. E.g. ssrnatify, which is used by ssrlia.
Karl Palmskog (Jun 18 2020 at 15:00):I think lia4mathcomp is to be considered legacy now
Anton Trunov (Jun 18 2020 at 15:02):indeed, it hasn't been updated for a while, but at the time I needed to use lia with mathcomp, I couldn't easily get mczify to compile
Bas Spitters (Jun 18 2020 at 15:07):@Karl Palmskog I guess we'll need your standardization committee again :-)
Karl Palmskog (Jun 18 2020 at 15:09):I think all we need is a decision from MathComp devs (cc: @Cyril Cohen) to officially maintain+package mczify or some enhancement of it (given that this seems to be functionality that many need, and otherwise will get replicated)
Anton Trunov (Jun 18 2020 at 15:11):The support for automation is underway :fingers_crossed: https://github.com/math-comp/math-comp/issues/263#issuecomment-631377939
Anton Trunov (Jun 18 2020 at 15:12):The lucky Coq 8.13, we all count on you :)
Karl Palmskog (Jun 18 2020 at 15:13):ah, but what do we do until then? Coq 8.13 is likely 6-9 months away
Anton Trunov (Jun 18 2020 at 15:14):we hack around, as we always do ;)
Last updated: Jan 31 2023 at 13:02 UTC