Lean has a wonderful tactic called norm_num which, among many other things, is able to prove divisibility statements about specific numbers. In this kata, you will not use this tactic. Instead, you will teach (a variant of) the simp tactic to decide whether a natural number is divisible by three.

To do this, you can select up to ten lemmas of your choice and call them three_dvd₁, ..., three_dvd₁₀. You should do this in such a way that expressions of the form

lemma check6 : 3 ∣ 6 :=
by basic_simp
lemma check7 : ¬3 ∣ 7 :=
by basic_simp

work as expected. basic_simp is a very naive implementation of a simp-like tactic. It is provided in Preloaded.lean and looks as follows:

meta def basic_simp :=
`[repeat { rw [three_dvd₁] <|> rw [three_dvd₂] <|> rw [three_dvd₃] <|> rw [three_dvd₄] <|>
           rw [three_dvd₅] <|> rw [three_dvd₆] <|> rw [three_dvd₇] <|> rw [three_dvd₈] <|>
           rw [three_dvd₉] <|> rw [three_dvd₁₀] },
  try { exact trivial }]

We use it instead of the actual simp tactic because simp turns out to be slightly too powerful for the purposes of this kata.

Tests

Similar to katas in "normal" programming languages, your lemmas will be tested for a certain set of natural numbers. The example test cases contain only a subset of the full test cases.

Using your lemmas, the simplifier should be able to check divisibility for relatively large numbers relatively quickly. More precisely, the full tests contain

• 26 tests where $0\le n\le 500\; \backslash leq\; n\; \backslash leq\; 50$,
• 9 tests where $0\le n\le 10^{18}0\backslash leq\; n\backslash leq\; 10^\{18\}$.

Within the 20 second time limit, your solution must compile and pass all the tests.

Golf

Can you solve this kata using less than 10 lemmas? What is the smallest number of lemmas you can manage?