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 ;)

view this post on Zulip Felipe Lisboa (Aug 02 2023 at 14:03):

Trying to prove:

Lemma dvdS_modnS d m: d > 0 -> (d %| m.+1) -> (m %% d).+1 = d.

Any tips? Tried to go through existing lemmas of modn and dvdn, but couldn't solve it.

view this post on Zulip Pierre Jouvelot (Aug 02 2023 at 16:51):

I came up with this solution, but I'm confident that a simpler one exists ;)

Lemma add_sub a b c : a = b + c -> c = a - b.
Proof. by move=> ->; rewrite addnC -subnBA // subnn subn0. Qed.

Lemma dvdS_modnS d m: d > 0 -> (d %| m.+1) -> (m %% d).+1 = d.
Proof.
move=> lt0d /dvdnP [k] m1k.
move/eqP: (divn_eq m d).
set m' := m %/ d; set m'' := m %% d.
rewrite -eqSS -addnS m1k => /eqP /add_sub.
rewrite -mulnBl => m''1.
move: (ltn_pmod m lt0d).
rewrite {}m''1 -{2}(mul1n d) leq_mul2r eqn0Ngt lt0d //= leq_eqVlt => /orP [/eqP ->|];
                                                                  first by rewrite mul1n.
by rewrite ltnS leqn0 subn_eq0 leqNgt ltn_divLR // m1k leqnn.
Qed.

view this post on Zulip Jason Gross (Aug 02 2023 at 19:54):

If you From Coq Require Import Lia ZArith Zify., there's the Z.to_euclidean_division_equations tactic which replaces mod and div with complete equations specifying their behavior, after which nia can often solve goals. Because nia is not complete, when proving a goal about mod, you will often need to assert the equation that holds of the corresponding quotient, though nia can often solve both the assertion and the main goal. (That is, it may be that Z.to_euclidean_division_equations; nia fails, but assert (foo / bar = baz); Z.to_euclidean_division_equations; nia succeeds.) You can also do Ltac zify_convert_to_euclidean_division_equations_flag ::= constr:(true). to get Z.to_euclidean_division_equations to run automatically.

view this post on Zulip Jason Gross (Aug 02 2023 at 19:56):

Currently, Z.to_euclidean_division_equations doesn't support Z.divide (I didn't need support for that when I wrote it), though we'd be happy to accept a pull request supporting it. (In fact, I think we just want match goal with | [ H : Z.divide _ _ |- _ ] => destruct H end, and add a tactic doing that to to_euclidean_division_equations in theories/omega/PreOmega.v)

view this post on Zulip Jason Gross (Aug 02 2023 at 19:57):

Where are the %| and %% notations from, and what are they defined as?

view this post on Zulip Pierre Jouvelot (Aug 02 2023 at 20:09):

Jason Gross said:

Where are the %| and %% notations from, and what are they defined as?

These are mathcomp operators, for "divides" and "modulo" (see https://math-comp.github.io/htmldoc/mathcomp.ssreflect.div.html).


Last updated: Jun 24 2024 at 00:02 UTC