data.num.prime

# Primality for binary natural numbers #

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.

def pos_num.min_fac_aux (n : pos_num) :

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.

Equations
theorem pos_num.min_fac_aux_to_nat {fuel : } {n k : pos_num} (h : < fuel + (k.bit1)) :

Returns the smallest prime factor of n ≠ 1.

Equations
@[simp]
@[simp]
def pos_num.prime (n : pos_num) :
Prop

Primality predicate for a pos_num.

Equations
Instances for pos_num.prime
@[protected, instance]
Equations
def num.min_fac  :

Returns the smallest prime factor of n ≠ 1.

Equations
@[simp]
theorem num.min_fac_to_nat (n : num) :
@[simp]
def num.prime (n : num) :
Prop

Primality predicate for a num.

Equations
Instances for num.prime
@[protected, instance]
Equations