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.

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
  • 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
    source
    theorem PosNum.minFacAux_to_nat {fuel : ℕ} {n : PosNum} {k : PosNum} (h : (↑n).sqrt < fuel + ↑k.bit1) :
    ↑(n.minFacAux fuel k) = (↑n).minFacAux ↑k.bit1
    source
    def PosNum.minFac :
    PosNum → PosNum

    Returns the smallest prime factor of n ≠ 1.

    Equations
    • x.minFac = match x with | PosNum.one => 1 | a.bit0 => 2 | n.bit1 => n.bit1.minFacAux (↑n) 1
    Instances For
      source
      @[simp]
      theorem PosNum.minFac_to_nat (n : PosNum) :
      ↑n.minFac = (↑n).minFac
      source
      def PosNum.Prime (n : PosNum) :
      Prop

      Primality predicate for a PosNum.

      Equations
      Instances For
        source
        instance PosNum.decidablePrime :
        DecidablePred PosNum.Prime
        Equations
        source
        def Num.minFac :
        Num → PosNum

        Returns the smallest prime factor of n ≠ 1.

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

          Primality predicate for a Num.

          Equations
          Instances For
            source
            instance Num.decidablePrime :
            DecidablePred Num.Prime
            Equations