The Coq mailing list

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

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.

Something like

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).
set (u := x mod 3).
admit.
admit.


On 08/09/2016 09:32 AM, Clément Pit--Claudel wrote:
> On 2016-08-09 03:13, Laurent Thery wrote:
> > 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.
>
> I think this part can be replaced with reflexivity. :)