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 ;)
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.
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.
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.
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)
Jason Gross (Aug 02 2023 at 19:57):Where are the %| and %% notations from, and what are they defined as?
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: Oct 05 2023 at 02:01 UTC