The Coq mailing list

[Vincent Laporte <vincent.laporte AT gmail.com>]

> Is there a simple way to do that?

Hi,

Here is a method (Frédéric Besson taught it to me). Dealing with
division and modulo directly is indeed painful. However, these
operations can be completely specified in terms of multiplications,
additions, and less-than relations (see the Z_div_mod_full lemma).
Moreover, when the divisor is a constant (in your case, 3), these
specifications are linear. Therefore, your goal can be automatically
changed into an equivalent one that is linear (hence solved by lia).

Here is the code (tested with Coq 8.5pl2).

Require Import Psatz.
Import ZArith.

Ltac elim_mod :=
repeat match goal with
| |- context[Z.modulo ?a ?b] =>
  unfold Z.modulo at 1;
  generalize (Z_div_mod_full a b);
  unfold Remainder;
  destruct (Z.div_eucl a b)
end.

Goal forall x, (x mod 3)%Z =
          (((x mod 3 - - x mod 3) mod 3 - (- x mod 3 - x mod 3) mod 3)
mod 3)%Z.
intros.
elim_mod.
lia.
Qed.

Cheers,
--
Vincent.