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?
Z.mod_small lemma from
lia should be able to solve that.
Assuming x is
Yep! But I have 15 lemmas with slight variations of this theme, so I was hoping for something like
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
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
From Hammer Require Import Tactics.
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
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