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: Jun 24 2024 at 00:02 UTC