mathlib3 documentation

data.nat.prime_norm_num

Primality prover #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file provides a norm_num extention to prove that natural numbers are prime.

source
theorem tactic.norm_num.is_prime_helper (n : ℕ) (h₁ : 1 < n) (h₂ : n.min_fac = n) :
nat.prime n
source
theorem tactic.norm_num.min_fac_bit0 (n : ℕ) :
(bit0 n).min_fac = 2
source
def tactic.norm_num.min_fac_helper (n k : ℕ) :
Prop

A predicate representing partial progress in a proof of min_fac.

Equations
source
theorem tactic.norm_num.min_fac_helper.n_pos {n k : ℕ} (h : tactic.norm_num.min_fac_helper n k) :
0 < n
source
theorem tactic.norm_num.min_fac_ne_bit0 {n k : ℕ} :
(bit1 n).min_fac ≠ bit0 k
source
theorem tactic.norm_num.min_fac_helper_0 (n : ℕ) (h : 0 < n) :
tactic.norm_num.min_fac_helper n 1
source
theorem tactic.norm_num.min_fac_helper_1 {n k k' : ℕ} (e : k + 1 = k') (np : (bit1 n).min_fac ≠ bit1 k) (h : tactic.norm_num.min_fac_helper n k) :
tactic.norm_num.min_fac_helper n k'
source
theorem tactic.norm_num.min_fac_helper_2 (n k k' : ℕ) (e : k + 1 = k') (np : ¬nat.prime (bit1 k)) (h : tactic.norm_num.min_fac_helper n k) :
tactic.norm_num.min_fac_helper n k'
source
theorem tactic.norm_num.min_fac_helper_3 (n k k' c : ℕ) (e : k + 1 = k') (nc : bit1 n % bit1 k = c) (c0 : 0 < c) (h : tactic.norm_num.min_fac_helper n k) :
tactic.norm_num.min_fac_helper n k'
source
theorem tactic.norm_num.min_fac_helper_4 (n k : ℕ) (hd : bit1 n % bit1 k = 0) (h : tactic.norm_num.min_fac_helper n k) :
(bit1 n).min_fac = bit1 k
source
theorem tactic.norm_num.min_fac_helper_5 (n k k' : ℕ) (e : bit1 k * bit1 k = k') (hd : bit1 n < k') (h : tactic.norm_num.min_fac_helper n k) :
(bit1 n).min_fac = bit1 n
source
meta def tactic.norm_num.prove_non_prime (e : expr) (n d₁ : ℕ) :
tactic expr

Given e a natural numeral and d : nat a factor of it, return ⊢ ¬ prime e.

source
meta def tactic.norm_num.prove_min_fac_aux (a a1 : expr) (n1 : ℕ) :
tactic.instance_cache → expr → expr → tactic (tactic.instance_cache × expr × expr)

Given a,a1 := bit1 a, n1 the value of a1, b and p : min_fac_helper a b, returns (c, ⊢ min_fac a1 = c).

source
meta def tactic.norm_num.prove_min_fac (ic : tactic.instance_cache) (e : expr) :
tactic (tactic.instance_cache × expr × expr)

Given a a natural numeral, returns (b, ⊢ min_fac a = b).

source
def tactic.norm_num.factors_helper (n p : ℕ) (l : list ℕ) :
Prop

A partial proof of factors. Asserts that l is a sorted list of primes, lower bounded by a prime p, which multiplies to n.

Equations
source
theorem tactic.norm_num.factors_helper_nil (a : ℕ) :
tactic.norm_num.factors_helper 1 a list.nil
source
theorem tactic.norm_num.factors_helper_cons' (n m a b : ℕ) (l : list ℕ) (h₁ : b * m = n) (h₂ : a ≤ b) (h₃ : b.min_fac = b) (H : tactic.norm_num.factors_helper m b l) :
tactic.norm_num.factors_helper n a (b :: l)
source
theorem tactic.norm_num.factors_helper_cons (n m a b : ℕ) (l : list ℕ) (h₁ : b * m = n) (h₂ : a < b) (h₃ : b.min_fac = b) (H : tactic.norm_num.factors_helper m b l) :
tactic.norm_num.factors_helper n a (b :: l)
source
theorem tactic.norm_num.factors_helper_sn (n a : ℕ) (h₁ : a < n) (h₂ : n.min_fac = n) :
tactic.norm_num.factors_helper n a [n]
source
theorem tactic.norm_num.factors_helper_same (n m a : ℕ) (l : list ℕ) (h : a * m = n) (H : tactic.norm_num.factors_helper m a l) :
tactic.norm_num.factors_helper n a (a :: l)
source
theorem tactic.norm_num.factors_helper_same_sn (a : ℕ) :
tactic.norm_num.factors_helper a a [a]
source
theorem tactic.norm_num.factors_helper_end (n : ℕ) (l : list ℕ) (H : tactic.norm_num.factors_helper n 2 l) :
n.factors = l
source
meta def tactic.norm_num.prove_factors_aux  :
tactic.instance_cache → expr → expr → ℕ → ℕ → tactic (tactic.instance_cache × expr × expr)

Given n and a natural numerals, returns (l, ⊢ factors_helper n a l).

source
meta def tactic.norm_num.eval_prime  :
expr → tactic (expr × expr)

Evaluates the prime and min_fac functions.