Primality for binary natural numbers #

This file defines versions of Nat.minFac and Nat.Prime for Num and PosNum. 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 decide, 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.

source

def PosNum.minFacAux (n : PosNum) :

ℕ → PosNum → PosNum

Auxiliary function for computing the smallest prime factor of a PosNum. Unlike Nat.minFacAux, 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.

Equations