The Coq mailing list

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

> 
> Lemma can_be_brute_forced : forall (n : nat), n < 10 -> n mod 10 = (n ^
> 5) mod 10.

Another alternative is to use the maths that explain why this holds.

Here is a proof in ssreflect.

It is based on fermat little theorem:

Lemma fermat_little a p : prime p -> a ^ p = a %[mod p].

and the chinese remainder theorem:

Lemma chinese_remainder m1 m2 x y :
       coprime m1 m2 ->
       (x == y %[mod m1 * m2]) = (x == y %[mod m1]) && (x == y %[mod m2])

The proof is then

Lemma avoid_brute_forced n : n ^ 5 = n %[mod 10].
Proof.
apply/eqP.
rewrite (chinese_remainder (_ : coprime 5 2)) // fermat_little // eqxx.
rewrite (_ : n ^ 5 = n * (n ^ 2) ^ 2) /=; last by rewrite expnS -expnM.
by rewrite -modnMmr !fermat_little // modnMmr mulnn fermat_little.
Qed.

but you can get much more

Lemma gen_avoid_brute_forced  n p : p != 2 -> prime p -> n ^ p = n %[mod
p.*2].
Proof.
move=> /eqP H2 Hp; apply/eqP.
have Op : odd p by  case: (even_prime Hp).
rewrite -muln2 (chinese_remainder (_ : coprime p 2)); last by rewrite
coprimen2.
rewrite fermat_little // eqxx /=.
apply/eqP.
elim: {p H2 Hp}_.+1 {-2}p (ltnSn p) Op => // k IH [|[|p]] // Hp Op.
rewrite /= negbK in Op.
rewrite ltnS in Hp.
rewrite 2!expnS mulnA mulnn.
rewrite -modnMml !fermat_little // modnMml.
by rewrite -modnMmr !IH ?(leq_trans _ Hp) // modnMmr mulnn fermat_little.
Qed.

--
Laurent