The Coq mailing list

[Daniel de Rauglaudre <daniel.de_rauglaudre AT inria.fr>]

Thanks for all your ideas. I eventually find a solution that I like.

>   (x mod 3)%Z =
>   (((x mod 3 - - x mod 3) mod 3 - (- x mod 3 - x mod 3) mod 3) mod 3)%Z

My solution

    (* eliminating the "(-n) mod 3" *)
    destruct (Z.eq_dec (n mod 3) 0) as [Hx| Hx].
     rewrite Hx.
     apply Zdiv.Z_mod_zero_opp_full in Hx; rewrite Hx; reflexivity.

     rewrite Zdiv.Z_mod_nz_opp_full; [ | assumption ].
     (* now, there are only "n mod 3" as variable *)
     rewrite <- Z.mod_mod at 1; [ | intros; discriminate ].
     (* beginning of the trick *)
     rewrite <- Z.mod_add with (b := (n mod 3)%Z); [ | intros; discriminate ].
     rewrite <- Z.mod_add with (b := (-2)%Z); [ | intros; discriminate ].
     f_equal; ring.

It ends with a "ring", what I wanted to do.

I prepare it by adding what is required inside the first "mod 3" using
Z.mod_add to make the two expressions equal.

When I have this kind of equality to prove and the expressions are
complicated, I can do a "f_equal; ring_simplify" before the Z.mod_add
to see what has to be added.

-- 
Daniel de Rauglaudre
http://pauillac.inria.fr/~ddr/