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 ;)
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.
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.
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
)
Where are the %|
and %%
notations from, and what are they defined as?
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