Stream: Coq users

Topic: Tactics for modular arithmetic


view this post on Zulip 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?

view this post on Zulip Wolf Honore (Jun 17 2020 at 20:09):

The Z.mod_small lemma from ZArith plus lia should be able to solve that.

view this post on Zulip Wolf Honore (Jun 17 2020 at 20:09):

Assuming x is Z

view this post on Zulip 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...

view this post on Zulip 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.

view this post on Zulip Cody Roux (Jun 17 2020 at 20:34):

Ooooh! Thanks Anton.

view this post on Zulip 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 :)

view this post on Zulip 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.

view this post on Zulip Karl Palmskog (Jun 17 2020 at 20:38):

the hammer tactic (the plugin part) doesn't do all that well on arithmetic goals if I recall correctly

view this post on Zulip Bas Spitters (Jun 17 2020 at 20:58):

How does scrush compare to the more recent sauto ?

view this post on Zulip 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

view this post on Zulip Bas Spitters (Jun 18 2020 at 14:33):

Any experience combining scrush with math-comp? I know this was a problem before.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Karl Palmskog (Jun 18 2020 at 15:00):

I think lia4mathcomp is to be considered legacy now

view this post on Zulip 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

view this post on Zulip Bas Spitters (Jun 18 2020 at 15:07):

@Karl Palmskog I guess we'll need your standardization committee again :-)

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip Anton Trunov (Jun 18 2020 at 15:12):

The lucky Coq 8.13, we all count on you :)

view this post on Zulip 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

view this post on Zulip Anton Trunov (Jun 18 2020 at 15:14):

we hack around, as we always do ;)


Last updated: Jan 31 2023 at 13:02 UTC