Primality for binary natural numbers #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
This file defines versions of nat.min_fac and nat.prime for num and pos_num. As with other
num definitions, they are not intended for general use (nat should be used instead of num in
most cases) but they can be used in contexts where kernel computation is required, such as proofs
by rfl and dec_trivial, as well as in #reduce.
The default decidable instance for nat.prime is optimized for VM evaluation, so it should be
preferred within #eval or in tactic execution, while for proofs the norm_num tactic can be used
to construct primality and non-primality proofs more efficiently than kernel computation.
Nevertheless, sometimes proof by computational reflection requires natural number computations, and
num implements algorithms directly on binary natural numbers for this purpose.
Auxiliary function for computing the smallest prime factor of a pos_num. Unlike
nat.min_fac_aux, we use a natural number fuel variable that is set to an upper bound on the
number of iterations. It is initialized to the number n we are determining primality for. Even
though this is exponential in the input (since it is a nat, not a num), it will get lazily
evaluated during kernel reduction, so we will only require about sqrt n unfoldings, for the
sqrt n iterations of the loop.