Documentation

Mathlib.Data.Num.Prime

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.

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
  • n.minFacAux 0 x = n
  • n.minFacAux fuel.succ x = if n < x.bit1 * x.bit1 then n else if x.bit1 n then x.bit1 else n.minFacAux fuel x.succ
Instances For
    theorem PosNum.minFacAux_to_nat {fuel : } {n : PosNum} {k : PosNum} (h : (↑n).sqrt < fuel + k.bit1) :
    (n.minFacAux fuel k) = (↑n).minFacAux k.bit1

    Returns the smallest prime factor of n ≠ 1.

    Equations
    • PosNum.one.minFac = 1
    • a.bit0.minFac = 2
    • n.bit1.minFac = n.bit1.minFacAux (↑n) 1
    Instances For
      @[simp]
      theorem PosNum.minFac_to_nat (n : PosNum) :
      n.minFac = (↑n).minFac

      Primality predicate for a PosNum.

      Equations
      Instances For
        Equations

        Returns the smallest prime factor of n ≠ 1.

        Equations
        Instances For
          @[simp]
          theorem Num.minFac_to_nat (n : Num) :
          n.minFac = (↑n).minFac
          def Num.Prime (n : Num) :

          Primality predicate for a Num.

          Equations
          Instances For
            Equations