feat: add Nat.maxPowDiv (#5158)

Adds tail recursive definition of maximal `k` such that `p^k | n` for `p, n : Nat` and `csimp` theorem relating it to `Nat.padicValNat`

Mathlib.lean

@@ -1494,6 +1494,7 @@ import Mathlib.Data.Nat.Hyperoperation
 import Mathlib.Data.Nat.Interval
 import Mathlib.Data.Nat.Lattice
 import Mathlib.Data.Nat.Log
+import Mathlib.Data.Nat.MaxPowDiv
 import Mathlib.Data.Nat.ModEq
 import Mathlib.Data.Nat.Multiplicity
 import Mathlib.Data.Nat.Order.Basic

Mathlib/Data/Nat/MaxPowDiv.lean

@@ -0,0 +1,112 @@
+/-
+Copyright (c) 2023 Matthew Robert Ballard. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Matthew Robert Ballard
+-/
+
+import Mathlib.Data.Nat.Pow
+
+/-!
+# The maximal power of one natural number dividing another
+
+Here we introduce `p.maxPowDiv n` which returns the maximal `k : ℕ` for
+which `p ^ k ∣ n` with the convention that `maxPowDiv 1 n = 0` for all `n`.
+
+We prove enough about `maxPowDiv` in this file to show equality with `Nat.padicValNat` in
+`padicValNat.padicValNat_eq_maxPowDiv`.
+
+The implementation of `maxPowDiv` improves on the speed of `padicValNat`.
+-/
+
+namespace Nat
+
+open Nat
+
+/--
+Tail recursive function which returns the largest `k : ℕ` such that `p ^ k ∣ n` for any `p : ℕ`.
+`padicValNat_eq_maxPowDiv` allows the code generator to use this definition for `padicValNat`
+-/
+def maxPowDiv (p n : ℕ) : ℕ :=
+  go 0 p n
+where go (k p n : ℕ) : ℕ :=
+  if h : 1 < p ∧ 0 < n ∧ n % p = 0 then
+    have : n / p < n := by apply Nat.div_lt_self <;> aesop
+    go (k+1) p (n / p)
+  else
+    k
+
+attribute [inherit_doc maxPowDiv] maxPowDiv.go
+
+end Nat
+
+namespace Nat.maxPowDiv
+
+theorem go_eq {k p n : ℕ} :
+    go k p n = if 1 < p ∧ 0 < n ∧ n % p = 0 then go (k+1) p (n / p) else k := by
+  dsimp [go, go._unary]
+  rw [WellFounded.fix_eq]
+  simp
+
+theorem go_succ {k p n : ℕ} : go (k+1) p n = go k p n + 1 := by
+  rw [go_eq]
+  conv_rhs => rw [go_eq]
+  by_cases (1 < p ∧ 0 < n ∧ n % p = 0); swap
+  · simp only [if_neg h]
+  · have : n / p < n := by apply Nat.div_lt_self <;> aesop
+    simp only [if_pos h]
+    apply go_succ
+
+@[simp]
+theorem zero_base {n : ℕ} : maxPowDiv 0 n = 0 := by
+  dsimp [maxPowDiv]
+  rw [maxPowDiv.go_eq]
+  simp
+
+@[simp]
+theorem zero {p : ℕ} : maxPowDiv p 0 = 0 := by
+  dsimp [maxPowDiv]
+  rw [maxPowDiv.go_eq]
+  simp
+
+theorem base_mul_eq_succ {p n : ℕ} (hp : 1 < p) (hn : 0 < n) :
+    p.maxPowDiv (p*n) = p.maxPowDiv n + 1 := by
+  have : 0 < p := lt_trans (b := 1) (by simp) hp
+  dsimp [maxPowDiv]
+  rw [maxPowDiv.go_eq, if_pos, mul_div_right _ this]
+  · apply go_succ
+  · refine ⟨hp, ?_, by simp⟩
+    apply Nat.mul_pos this hn
+
+theorem base_pow_mul {p n exp : ℕ} (hp : 1 < p) (hn : 0 < n) :
+    p.maxPowDiv (p ^ exp * n) = p.maxPowDiv n + exp := by
+  match exp with
+  | 0 => simp
+  | e + 1 =>
+    rw [pow_succ, mul_assoc, mul_comm, mul_assoc, base_mul_eq_succ hp, mul_comm, base_pow_mul hp hn]
+    · ac_rfl
+    · apply Nat.mul_pos hn <| pow_pos (pos_of_gt hp) e
+
+theorem pow_dvd (p n : ℕ) : p ^ (p.maxPowDiv n) ∣ n := by
+  dsimp [maxPowDiv]
+  rw [go_eq]
+  by_cases (1 < p ∧ 0 < n ∧ n % p = 0)
+  · have : n / p < n := by apply Nat.div_lt_self <;> aesop
+    rw [if_pos h]
+    have ⟨c,hc⟩ := pow_dvd p (n / p)
+    rw [go_succ, pow_succ]
+    nth_rw 2 [←mod_add_div' n p]
+    rw [h.right.right, zero_add]
+    exact ⟨c,by nth_rw 1 [hc]; ac_rfl⟩
+  · rw [if_neg h]
+    simp
+
+theorem le_of_dvd {p n pow : ℕ} (hp : 1 < p) (hn : 0 < n) (h : p ^ pow ∣ n) :
+    pow ≤ p.maxPowDiv n := by
+  have ⟨c, hc⟩ := h
+  have : 0 < c := by
+    apply Nat.pos_of_ne_zero
+    intro h'
+    rw [h',mul_zero] at hc
+    exact not_eq_zero_of_lt hn hc
+  simp [hc, base_pow_mul hp this]
+

Mathlib/NumberTheory/Padics/PadicVal.lean

@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2018 Robert Y. Lewis. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Robert Y. Lewis
+Authors: Robert Y. Lewis, Matthew Robert Ballard
 
 ! This file was ported from Lean 3 source module number_theory.padics.padic_val
 ! leanprover-community/mathlib commit 60fa54e778c9e85d930efae172435f42fb0d71f7
@@ -10,6 +10,8 @@ Authors: Robert Y. Lewis
 -/
 import Mathlib.NumberTheory.Divisors
 import Mathlib.RingTheory.Int.Basic
+import Mathlib.Data.Nat.MaxPowDiv
+import Mathlib.Tactic.IntervalCases
 
 /-!
 # p-adic Valuation
@@ -95,6 +97,37 @@ theorem eq_zero_of_not_dvd {n : ℕ} (h : ¬p ∣ n) : padicValNat p n = 0 :=
   eq_zero_iff.2 <| Or.inr <| Or.inr h
 #align padic_val_nat.eq_zero_of_not_dvd padicValNat.eq_zero_of_not_dvd
 
+open Nat.maxPowDiv
+
+theorem maxPowDiv_eq_multiplicity {p n : ℕ} (hp : 1 < p) (hn : 0 < n) :
+    p.maxPowDiv n = multiplicity p n := by
+  apply multiplicity.unique <| pow_dvd p n
+  intro h
+  apply Nat.not_lt.mpr <| le_of_dvd hp hn h
+  simp
+
+theorem maxPowDiv_eq_multiplicity_get {p n : ℕ} (hp : 1 < p) (hn : 0 < n) (h : Finite p n) :
+    p.maxPowDiv n = (multiplicity p n).get h := by
+  rw [PartENat.get_eq_iff_eq_coe.mpr]
+  apply maxPowDiv_eq_multiplicity hp hn|>.symm
+
+/-- Allows for more efficient code for `padicValNat` -/
+@[csimp]
+theorem padicValNat_eq_maxPowDiv : @padicValNat = @maxPowDiv := by
+  ext p n
+  by_cases (1 < p ∧ 0 < n)
+  · dsimp [padicValNat]
+    rw [dif_pos ⟨Nat.ne_of_gt h.1,h.2⟩, maxPowDiv_eq_multiplicity_get h.1 h.2]
+  · simp only [not_and_or,not_gt_eq,le_zero_iff] at h
+    apply h.elim
+    · intro h
+      interval_cases p
+      · simp [Classical.em]
+      · dsimp [padicValNat, maxPowDiv]
+        rw [go_eq, if_neg, dif_neg] <;> simp
+    · intro h
+      simp [h]
+
 end padicValNat
 
 /-- For `p ≠ 1`, the `p`-adic valuation of an integer `z ≠ 0` is the largest natural number `k` such

test/MaxPowDiv.lean

@@ -0,0 +1,4 @@
+import Mathlib.NumberTheory.Padics.PadicVal
+
+/- Previously this would hang -/
+#eval padicValNat 2 (2 ^ 100000)