fixing maxPowDiv

Stream: mathlib4

[Cookie Guy]

So I was working on a proof which required me to calculate various p-adic valuations. Sadly, p-adic valuations are noncomputable, butthankfully, mathlib provides padicValNat.maxPowDiv_eq_multiplicity ... : p.maxPowDiv n = multiplicity p n

however, even after rewriting to maxPowDiv, lean still doesnt seem to work nicely with it, for example
lean cant prove example : Nat.maxPowDiv 5 125 = 3 := by rfl, looking into maxPowDiv, I see the definition

def maxPowDiv (p n : ℕ) : ℕ :=
  go 0 p n
where go (k p n : ℕ) : ℕ :=
  if 1 < p ∧ 0 < n ∧ n % p = 0 then
    go (k+1) p (n / p)
  else
    k
  termination_by n
  decreasing_by apply Nat.div_lt_self <;> tauto

it seems that the decreasing_by proof makes it a bit less to reduce in the kernel, so as an experiment, i try giving it fuel instead

def maxPowDiv' (p n : ℕ) : ℕ := go n 0 p n
where go (fuel : ℕ) (k p n : ℕ) : ℕ :=
  match fuel with
  | 0 => k
  | fuel' + 1 =>
    if 1 < p ∧ 0 < n ∧ n % p = 0 then
      go fuel' (k + 1) p (n / p)
    else
      k

and suddenly we can do
example : maxPowDiv' 5 125 = 3 := by rfl

I am wondering if there is no reason apart from deprecation to not change to this definition for its nicer kernel properties?

[Yury G. Kudryashov]

I have a branch that tries to migrate to a similar definition, but I have no time to polish it for a review.

[Yury G. Kudryashov]

Let me open a draft PR.

[Yury G. Kudryashov]

See #34711

[Yury G. Kudryashov]

Do you want to take over that PR? If yes, then probably the way to go is to create a branch in your fork based on my PR, then open a PR to master, and mention my PR.

[Cookie Guy]

Ok, that sounds good.

I was also thinking about creating a simproc for padicValNat to reduce using maxPowDvd, so let me work on creating that too

[Yury G. Kudryashov]

We use norm_num for simplifying functions about numbers.

[Yury G. Kudryashov]

I.e., you should probably write a norm_num plugin instead of a simproc.

[Yury G. Kudryashov]

But the first PR should include just #34711 + cleanup:

• make linters happy (probably, by removing some simp attrs)
• add missing docstrings, if any
• restore old defs and lemmas, probably as deprecated aliases.

Any work on meta code for computing padicValNat should go into a PR stacked on top of the first one.

[Yuyang Zhao]

After lean4#7965 fuel is no longer needed.

[Yuyang Zhao]

import Mathlib

attribute [local semireducible] Nat.maxPowDiv.go

example : Nat.maxPowDiv 5 125 = 3 := by rfl

[Yury G. Kudryashov]

I wrote #34711 before that, then I was too lazy to adjust the proofs to a non-fuel def.

[Yury G. Kudryashov]

@Cookie Guy Are you going to work on this? If no, then I may have a go next weekend.

[Yury G. Kudryashov]

How can I check (other than @[semireducible] being accepted w/o a warning) that lean4#7965 worked on a definition? Is it visible in the #print output?

[Yury G. Kudryashov]

Answering myself by looking at the source: it uses WellFounded.Nat.fix instead of a generic well-founded fixpoint function.