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?
The Z.mod_small
lemma from ZArith
plus lia
should be able to solve that.
Assuming x is Z
Yep! But I have 15 lemmas with slight variations of this theme, so I was hoping for something like lia
...
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.
Ooooh! Thanks Anton.
@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 :)
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
How does scrush compare to the more recent sauto ?
scrush
is just a thin layer on top of sauto
. It's literally defined as try strivial; ssimpl; sauto
Any experience combining scrush with math-comp? I know this was a problem before.
Lukasz has a CoqHammer branch called mathcomp
. However, this branch doesn't seem aware of things like zify
and https://github.com/pi8027/mczify
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
.
I think lia4mathcomp is to be considered legacy now
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
@Karl Palmskog I guess we'll need your standardization committee again :-)
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)
The support for automation is underway :fingers_crossed: https://github.com/math-comp/math-comp/issues/263#issuecomment-631377939
The lucky Coq 8.13, we all count on you :)
ah, but what do we do until then? Coq 8.13 is likely 6-9 months away
we hack around, as we always do ;)
Last updated: Jan 31 2023 at 13:02 UTC