refactor(tactic/norm_num): move norm_num extensions (#4822)

#4820 adds the long awaited ability for `norm_num` to be extended in other files. There are two norm_num extensions currently in mathlib: `norm_digits`, which was previously exposed as a standalone tactic, and `eval_prime`, which was a part of `norm_num` and so caused `tactic.norm_num` to depend on `data.nat.prime`. This PR turns both of these into norm_num extensions, and changes the dependencies so that `data.nat.prime` can import `norm_num` rather than the other way around (which required splitting `pnat` primality and gcd facts to their own file).



Co-authored-by: Rob Lewis <rob.y.lewis@gmail.com>

Author: digama0

archive/imo/imo1959_q1.lean

@@ -5,6 +5,7 @@ Authors: Kevin Lacker
 -/
 
 import tactic.ring
+import data.nat.prime
 
 open nat
 

archive/imo/imo1960_q1.lean

@@ -87,7 +87,7 @@ begin
   have := search_up_to_start,
   iterate 82 {
     replace := search_up_to_step this (by norm_num1; refl) (by norm_num1; refl)
-      (by norm_digits; refl) dec_trivial },
+      (by norm_num1; refl) dec_trivial },
   exact search_up_to_end this
 end
 
@@ -100,4 +100,3 @@ by rcases spn with (rfl | rfl); norm_num [problem_predicate, sum_of_squares]
 
 theorem imo1960_q1 (n : ℕ) : problem_predicate n ↔ solution_predicate n :=
 ⟨right_direction, left_direction n⟩
-

archive/imo/imo1969_q1.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kevin Lacker
 -/
 
+import data.nat.prime
 import tactic.linarith
 import tactic.norm_cast
 import tactic.ring
@@ -40,7 +41,7 @@ by exact_mod_cast lt_of_lt_of_le h le_nat_abs
 lemma int_not_prime (a b : ℤ) (c : ℕ) (h1 : 1 < a) (h2 : 1 < b) (h3 : a*b = ↑c) : ¬ prime c :=
 have h4 : (a*b).nat_abs = a.nat_abs * b.nat_abs, from nat_abs_mul a b,
 have h5 : a.nat_abs * b.nat_abs = c, by finish,
-norm_num.not_prime_helper a.nat_abs b.nat_abs c h5 (int_large a h1) (int_large b h2)
+tactic.norm_num.not_prime_helper a.nat_abs b.nat_abs c h5 (int_large a h1) (int_large b h2)
 
 lemma polynomial_not_prime (m n : ℕ) (h1 : 1 < m) : ¬ prime (n^4 + 4*m^4) :=
 have h2 : 1 < of_nat m, from coe_nat_lt.mpr h1,
@@ -66,5 +67,3 @@ begin
   assume n,
   exact polynomial_not_prime (2+b) n h1
 end
-
-

archive/imo/imo1988_q6.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johan Commelin
 -/
 
+import data.nat.prime
 import data.rat.basic
 import order.well_founded
 import tactic.linarith

src/data/nat/digits.lean

@@ -606,51 +606,37 @@ meta def eval_aux (eb : expr) (b : ℕ) :
     return (ic, `(@list.cons ℕ %%er %%el),
       `(digits_succ %%eb %%en %%em %%er %%el %%pe %%pr %%p))
 
-/-- Helper function for the `norm_digits` tactic. -/
-meta def eval : expr → ℕ → expr → ℕ → tactic (expr × expr)
-| eb b en 0 := return (`([] : list ℕ), `(nat.digits_zero %%eb))
-| eb 0 en n := do
-  ic ← mk_instance_cache `(ℕ),
-  (_, pn0) ← norm_num.prove_pos ic en,
-  return (`([%%en] : list ℕ), `(@nat.digits_zero_succ' %%en %%pn0))
-| eb 1 en n := do
-  ic ← mk_instance_cache `(ℕ),
-  (_, pn0) ← norm_num.prove_pos ic en,
-  s ← simp_lemmas.add_simp simp_lemmas.mk `list.repeat,
-  (rhs, p2) ← simplify s [] `(list.repeat 1 %%en),
-  p ← mk_eq_trans `(nat.digits_one %%en) p2,
-  return (rhs, p)
-| eb b en n := do
-  ic ← mk_instance_cache `(ℕ),
-  (_, l, p) ← eval_aux eb b en n ic,
-  p ← mk_app ``and.left [p],
-  return (l, p)
-
-end norm_digits
-
-open tactic
-
 /--
 A tactic for normalizing expressions of the form `nat.digits a b = l` where
 `a` and `b` are numerals.
 
 ```
-example : nat.digits 10 123 = [3,2,1] := by norm_digits
+example : nat.digits 10 123 = [3,2,1] := by norm_num
 ```
 -/
-meta def norm_digits : tactic unit :=
-do `(nat.digits %%eb %%en = %%el') ← target,
+@[norm_num] meta def eval : expr → tactic (expr × expr)
+| `(nat.digits %%eb %%en) := do
   b ← expr.to_nat eb,
   n ← expr.to_nat en,
-  (el, p) ← nat.norm_digits.eval eb b en n,
-  unify el el',
-  exact p
+  if n = 0 then return (`([] : list ℕ), `(nat.digits_zero %%eb))
+  else if b = 0 then do
+    ic ← mk_instance_cache `(ℕ),
+    (_, pn0) ← norm_num.prove_pos ic en,
+    return (`([%%en] : list ℕ), `(@nat.digits_zero_succ' %%en %%pn0))
+  else if b = 1 then do
+    ic ← mk_instance_cache `(ℕ),
+    (_, pn0) ← norm_num.prove_pos ic en,
+    s ← simp_lemmas.add_simp simp_lemmas.mk `list.repeat,
+    (rhs, p2) ← simplify s [] `(list.repeat 1 %%en),
+    p ← mk_eq_trans `(nat.digits_one %%en) p2,
+    return (rhs, p)
+  else do
+    ic ← mk_instance_cache `(ℕ),
+    (_, l, p) ← eval_aux eb b en n ic,
+    p ← mk_app ``and.left [p],
+    return (l, p)
+| _ := failed
 
-run_cmd add_interactive [``norm_digits]
+end norm_digits
 
-add_tactic_doc
-{ name        := "norm_digits",
-  category    := doc_category.tactic,
-  decl_names  := [`tactic.interactive.norm_digits],
-  tags        := ["arithmetic", "decision procedure"] }
 end nat

src/data/nat/prime.lean

@@ -8,6 +8,7 @@ import data.nat.sqrt
 import data.nat.gcd
 import algebra.group_power
 import tactic.wlog
+import tactic.norm_num
 
 /-!
 # Prime numbers
@@ -589,7 +590,7 @@ namespace primes
 instance : has_repr nat.primes := ⟨λ p, repr p.val⟩
 instance : inhabited primes := ⟨⟨2, prime_two⟩⟩
 
-instance coe_nat  : has_coe nat.primes ℕ  := ⟨subtype.val⟩
+instance coe_nat : has_coe nat.primes ℕ := ⟨subtype.val⟩
 
 theorem coe_nat_inj (p q : nat.primes) : (p : ℕ) = (q : ℕ) → p = q :=
 λ h, subtype.eq h
@@ -599,3 +600,170 @@ end primes
 instance monoid.prime_pow {α : Type*} [monoid α] : has_pow α primes := ⟨λ x p, x^p.val⟩
 
 end nat
+
+/-! ### Primality prover -/
+
+namespace tactic
+namespace norm_num
+open norm_num
+
+lemma not_prime_helper (a b n : ℕ)
+  (h : a * b = n) (h₁ : 1 < a) (h₂ : 1 < b) : ¬ nat.prime n :=
+by rw ← h; exact nat.not_prime_mul h₁ h₂
+
+lemma is_prime_helper (n : ℕ)
+  (h₁ : 1 < n) (h₂ : nat.min_fac n = n) : nat.prime n :=
+nat.prime_def_min_fac.2 ⟨h₁, h₂⟩
+
+lemma min_fac_bit0 (n : ℕ) : nat.min_fac (bit0 n) = 2 :=
+by simp [nat.min_fac_eq, show 2 ∣ bit0 n, by simp [bit0_eq_two_mul n]]
+
+/-- A predicate representing partial progress in a proof of `min_fac`. -/
+def min_fac_helper (n k : ℕ) : Prop :=
+0 < k ∧ bit1 k ≤ nat.min_fac (bit1 n)
+
+theorem min_fac_helper.n_pos {n k : ℕ} (h : min_fac_helper n k) : 0 < n :=
+nat.pos_iff_ne_zero.2 $ λ e,
+by rw e at h; exact not_le_of_lt (nat.bit1_lt h.1) h.2
+
+lemma min_fac_ne_bit0 {n k : ℕ} : nat.min_fac (bit1 n) ≠ bit0 k :=
+by rw bit0_eq_two_mul; exact λ e, absurd
+  ((nat.dvd_add_iff_right (by simp [bit0_eq_two_mul n])).2
+    (dvd_trans ⟨_, e⟩ (nat.min_fac_dvd _)))
+  dec_trivial
+
+lemma min_fac_helper_0 (n : ℕ) (h : 0 < n) : min_fac_helper n 1 :=
+begin
+  refine ⟨zero_lt_one, lt_of_le_of_ne _ min_fac_ne_bit0.symm⟩,
+  refine @lt_of_le_of_ne ℕ _ _ _ (nat.min_fac_pos _) _,
+  intro e,
+  have := nat.min_fac_prime _,
+  { rw ← e at this, exact nat.not_prime_one this },
+  { exact ne_of_gt (nat.bit1_lt h) }
+end
+
+lemma min_fac_helper_1 {n k k' : ℕ} (e : k + 1 = k')
+  (np : nat.min_fac (bit1 n) ≠ bit1 k)
+  (h : min_fac_helper n k) : min_fac_helper n k' :=
+begin
+  rw ← e,
+  refine ⟨nat.succ_pos _,
+    (lt_of_le_of_ne (lt_of_le_of_ne _ _ : k+1+k < _)
+      min_fac_ne_bit0.symm : bit0 (k+1) < _)⟩,
+  { rw add_right_comm, exact h.2 },
+  { rw add_right_comm, exact np.symm }
+end
+
+lemma min_fac_helper_2 (n k k' : ℕ) (e : k + 1 = k')
+  (np : ¬ nat.prime (bit1 k)) (h : min_fac_helper n k) : min_fac_helper n k' :=
+begin
+  refine min_fac_helper_1 e _ h,
+  intro e₁, rw ← e₁ at np,
+  exact np (nat.min_fac_prime $ ne_of_gt $ nat.bit1_lt h.n_pos)
+end
+
+lemma min_fac_helper_3 (n k k' c : ℕ) (e : k + 1 = k')
+  (nc : bit1 n % bit1 k = c) (c0 : 0 < c)
+  (h : min_fac_helper n k) : min_fac_helper n k' :=
+begin
+  refine min_fac_helper_1 e _ h,
+  refine mt _ (ne_of_gt c0), intro e₁,
+  rw [← nc, ← nat.dvd_iff_mod_eq_zero, ← e₁],
+  apply nat.min_fac_dvd
+end
+
+lemma min_fac_helper_4 (n k : ℕ) (hd : bit1 n % bit1 k = 0)
+  (h : min_fac_helper n k) : nat.min_fac (bit1 n) = bit1 k :=
+by rw ← nat.dvd_iff_mod_eq_zero at hd; exact
+le_antisymm (nat.min_fac_le_of_dvd (nat.bit1_lt h.1) hd) h.2
+
+lemma min_fac_helper_5 (n k k' : ℕ) (e : bit1 k * bit1 k = k')
+  (hd : bit1 n < k') (h : min_fac_helper n k) : nat.min_fac (bit1 n) = bit1 n :=
+begin
+  refine (nat.prime_def_min_fac.1 (nat.prime_def_le_sqrt.2
+    ⟨nat.bit1_lt h.n_pos, _⟩)).2,
+  rw ← e at hd,
+  intros m m2 hm md,
+  have := le_trans h.2 (le_trans (nat.min_fac_le_of_dvd m2 md) hm),
+  rw nat.le_sqrt at this,
+  exact not_le_of_lt hd this
+end
+
+/-- Given `e` a natural numeral and `d : nat` a factor of it, return `⊢ ¬ prime e`. -/
+meta def prove_non_prime (e : expr) (n d₁ : ℕ) : tactic expr :=
+do let e₁ := reflect d₁,
+  c ← mk_instance_cache `(nat),
+  (c, p₁) ← prove_lt_nat c `(1) e₁,
+  let d₂ := n / d₁, let e₂ := reflect d₂,
+  (c, e', p) ← prove_mul_nat c e₁ e₂,
+  guard (e' =ₐ e),
+  (c, p₂) ← prove_lt_nat c `(1) e₂,
+  return $ `(not_prime_helper).mk_app [e₁, e₂, e, p, p₁, p₂]
+
+/-- Given `a`,`a1 := bit1 a`, `n1` the value of `a1`, `b` and `p : min_fac_helper a b`,
+  returns `(c, ⊢ min_fac a1 = c)`. -/
+meta def prove_min_fac_aux (a a1 : expr) (n1 : ℕ) :
+  instance_cache → expr → expr → tactic (instance_cache × expr × expr)
+| ic b p := do
+  k ← b.to_nat,
+  let k1 := bit1 k,
+  let b1 := `(bit1:ℕ→ℕ).mk_app [b],
+  if n1 < k1*k1 then do
+    (ic, e', p₁) ← prove_mul_nat ic b1 b1,
+    (ic, p₂) ← prove_lt_nat ic a1 e',
+    return (ic, a1, `(min_fac_helper_5).mk_app [a, b, e', p₁, p₂, p])
+  else let d := k1.min_fac in
+  if to_bool (d < k1) then do
+    let k' := k+1, let e' := reflect k',
+    (ic, p₁) ← prove_succ ic b e',
+    p₂ ← prove_non_prime b1 k1 d,
+    prove_min_fac_aux ic e' $ `(min_fac_helper_2).mk_app [a, b, e', p₁, p₂, p]
+  else do
+    let nc := n1 % k1,
+    (ic, c, pc) ← prove_div_mod ic a1 b1 tt,
+    if nc = 0 then
+      return (ic, b1, `(min_fac_helper_4).mk_app [a, b, pc, p])
+    else do
+      (ic, p₀) ← prove_pos ic c,
+      let k' := k+1, let e' := reflect k',
+      (ic, p₁) ← prove_succ ic b e',
+      prove_min_fac_aux ic e' $ `(min_fac_helper_3).mk_app [a, b, e', c, p₁, pc, p₀, p]
+
+/-- Given `a` a natural numeral, returns `(b, ⊢ min_fac a = b)`. -/
+meta def prove_min_fac (ic : instance_cache) (e : expr) : tactic (instance_cache × expr × expr) :=
+match match_numeral e with
+| match_numeral_result.zero := return (ic, `(2:ℕ), `(nat.min_fac_zero))
+| match_numeral_result.one := return (ic, `(1:ℕ), `(nat.min_fac_one))
+| match_numeral_result.bit0 e := return (ic, `(2), `(min_fac_bit0).mk_app [e])
+| match_numeral_result.bit1 e := do
+  n ← e.to_nat,
+  c ← mk_instance_cache `(nat),
+  (c, p) ← prove_pos c e,
+  let a1 := `(bit1:ℕ→ℕ).mk_app [e],
+  prove_min_fac_aux e a1 (bit1 n) c `(1) (`(min_fac_helper_0).mk_app [e, p])
+| _ := failed
+end
+
+/-- Evaluates the `prime` and `min_fac` functions. -/
+@[norm_num] meta def eval_prime : expr → tactic (expr × expr)
+| `(nat.prime %%e) := do
+  n ← e.to_nat,
+  match n with
+  | 0 := false_intro `(nat.not_prime_zero)
+  | 1 := false_intro `(nat.not_prime_one)
+  | _ := let d₁ := n.min_fac in
+    if d₁ < n then prove_non_prime e n d₁ >>= false_intro
+    else do
+      let e₁ := reflect d₁,
+      c ← mk_instance_cache `(nat),
+      (c, p₁) ← prove_lt_nat c `(1) e₁,
+      (c, e₁, p) ← prove_min_fac c e,
+      true_intro $ `(is_prime_helper).mk_app [e, p₁, p]
+  end
+| `(nat.min_fac %%e) := do
+  ic ← mk_instance_cache `(ℕ),
+  prod.snd <$> prove_min_fac ic e
+| _ := failed
+
+end norm_num
+end tactic

src/number_theory/divisors.lean

@@ -5,6 +5,7 @@ Authors: Aaron Anderson
 -/
 import algebra.big_operators.order
 import tactic
+import data.nat.prime
 
 /-!
 # Divisor finsets