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

Last updated: Jan 31 2023 at 13:02 UTC