norm_num for deciding primality?

Stream: new members

[Kevin Cheung]

In the documentation https://github.com/leanprover-community/mathlib4/blob/24fce2d2db1a7ed39c8c5bdaf300d2ddfc83313f/Mathlib/Data/Nat/Prime/Defs.lean#L142-L142, there is this sentence: "If you need to prove that a particular number is prime, in any case you should not use by decide, but rather by norm_num, which is much faster."

However, I have the following and norm_num is underlined with red squiggly line saying the goal is unsolved.

import Mathlib.Data.Nat.Prime.Basic
import Mathlib.Tactic.Normnum

example : Nat.Prime 3 := by decide

example : Nat.Prime 3 := by norm_num

Is there a more powerful version of norm_num that needs to be imported? If so, what would that be?

[Kyle Miller]

Import Mathlib.Tactic.Normnum.Prime, which has the norm num extension for primality.

[Kevin Cheung]

Thanks!

[Kevin Cheung]

Strange. When I perform a search for "Mathlib.Tactic.Normnum.Prime" at https://leanprover-community.github.io/mathlib4_docs/search.html?sitesearch=https%3A%2F%2Fleanprover-community.github.io%2Fmathlib4_docs&q=mathlib.tactic.normnum.prime I got no results.

[Ruben Van de Velde]

It's a file

[Kevin Cheung]

I see. My bad.

[Kyle Miller]

It's worth browsing the Mathlib/Tactic/Normnum folder to see what norm num plugins are available

[Kevin Cheung]

Thanks for the tip.