The Coq mailing list

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

On 08/09/2016 07:56 AM, Daniel de Rauglaudre wrote:
>   (x mod 3)%Z =
>   (((x mod 3 - - x mod 3) mod 3 - (- x mod 3 - x mod 3) mod 3) mod 3)%Z

Here is the proof (I am sure it can be automated (I remember a paper by 
John Harrison
automating this kind of stuff)

Anyway here is the vintage Coq proof:

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.
set (u := - x mod 3).
set (v := x mod 3).
rewrite <-Zminus_mod.
replace (v -u - (u - v)) with (2 * (v - u)) by lia.
rewrite Zmult_mod.
unfold v, u.
rewrite <-Zminus_mod.
replace (x -- x) with (2 * x) by lia.
rewrite <- Zmult_mod.
replace (2 * (2 * x)) with (4 * x) by lia.
rewrite Zmult_mod.
replace (4 mod 3) with 1.
replace (1 * (x mod 3)) with (x mod 3) by lia.
rewrite Zmod_mod.
trivial.
replace 4 with (3 + 1) by lia.
rewrite Zplus_mod.
rewrite Z_mod_same_full.
replace (0 + (1 mod 3)) with (1 mod 3) by lia.
rewrite Zmod_mod.
rewrite Zmod_small; lia.
Qed.