The Coq mailing list

[Laurent Thery <Laurent.Thery AT inria.fr>]

On 08/09/2016 09:42 AM, Laurent Thery wrote:
> Forgot  Zmod was computing ;-)
>
> Anyway an alternative way to automate would be to express the goal only
> in term of (x mod 3) that can have only 3 values 0 1 2 and check them by
> computation.

Here is the comlete alternative proof. I think it is nicer.

Require Import ZArith Psatz.

Open Scope Z_scope.

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.
intro x.
replace (- x mod 3) with ((2 * (x mod 3)) mod 3).
assert (H : x mod 3 = 0 \/ x mod 3 = 1 \/ x mod 3 = 2).
  assert (H1 := Z_mod_lt x 3).
  lia.
destruct H as [H | [H|H]]; rewrite H; trivial.
replace (- x) with (-1 * x) by lia.
rewrite (Zmult_mod (-1)).
trivial.
Qed.