Fun modulo 5

[maxhaslbeck]

Task Authors and Translators

Task was stated by @maxhaslbeck in Isabelle, and translated to Coq by Armaël Guéneau, to Lean by Kevin Kappelmann and to ACL2 by Sebastiaan Joosten.

The sample solution

For this task it is instructive to see that m ^ 5 mod 10 = m if m < 10.
To finish the proof one needs ((a mod b) ^ n) mod b = (a ^ n) mod b which either is in your proof assistant's library or you need to prove it yourself. :)

In Isabelle

The sample solution due to @maxhaslbeck can be found here.

In Coq

The sample solution due to Armaël Guéneau can be found here.

[monadius]

A sample Coq solution is missing: It is just the template Submission.v file.

[monadius]

I would like to see a sample Lean solution for this problem.

[kappelmann]

@monadius here is a Lean solution (credits to Chris)

theorem mod_power_five (n : ℕ) : n % 10 = (n ^ 5) % 10 :=
have h : ∀ (n : zmod 10), n = n ^ 5, from dec_trivial,
(zmod.eq_iff_modeq_nat' (show 0 < 10, from dec_trivial)).1 $
  by rw [h n, nat.cast_pow]

[monadius]

@kappelmann Thank you!