How to show value of padicValNat

Stream: new members

[Sabbir Rahman]

[updated statement to fix order of arguments]
How to show the following simple fact

import Mathlib

example : padicValNat 3 48 = 1:= by
  sorry

this is my first time trying out padicValNat so I could be missing easy stuff.

[Edward van de Meent]

this is false, as evidenced by using native_decide

[Edward van de Meent]

i.e.

import Mathlib

example : padicValNat 48 3 = 0:= by
  native_decide

[Mario Carneiro]

does decide not work?

[Edward van de Meent]

no, i think because Nat.find doesn't have a reducible definition?

[Sabbir Rahman]

ah I see I had flipped the order of 48 and 3

[Sabbir Rahman]

thanks for native_decide solution, but as the tactic warns, this adds compiler to trusted. any way to avoid that?

[Mario Carneiro]

maybe we should replace uses of Nat.find with Nat.findBounded where possible

[Mario Carneiro]

where Nat.findBounded has a constructive upper limit and is defined by recursion on nat

[Mario Carneiro]

my guess is that essentially all uses of Nat.find are actually expressible with Nat.findBounded

[Edward van de Meent]

maybe we could/should redefine Nat.find via partial_fixpoint?

[Mario Carneiro]

does that help?

[Mario Carneiro]

it's not a partial function, and I think the fixpoint combinator used by partial_fixpoint is strictly harder to deal with in the kernel than Acc.rec

[Mario Carneiro]

(BTW I tried using with_unfolding_all decide here, but it still doesn't work because that forces unfolding of proofs and the proof of well foundedness in this case uses some axiom)

[Mario Carneiro]

hm, seems the alternative definition used for csimp works better in decide:

import Mathlib.NumberTheory.Padics.PadicVal.Basic

example : padicValNat 3 48 = 1 := by
  simp [padicValNat.padicValNat_eq_maxPowDiv]
  with_unfolding_all decide

[Edward van de Meent]

:hmm:

[Edward van de Meent]

maybe we should add this as a Decidable instance then?

[Mario Carneiro]

well no, it's a terrible decision procedure

[Mario Carneiro]

well not terrible but it would need modification first

[Mario Carneiro]

this should just have a norm_num extension

[Mario Carneiro]

especially since it's easier to verify the result than to calculate it

[Mario Carneiro]

it's a bit annoying that the definitional property of padicValNat isn't a theorem?

For p ≠ 1, the p-adic valuation of a natural n ≠ 0 is the largest natural number k such that p^k divides n.

The closest I can find is docs#padicValNat_dvd_iff

[Mario Carneiro]

I assume you can get at this theorem via multiplicity

[Mario Carneiro]

Here's a better proof, which should be roughly how the norm_num extension works:

theorem foo {p n k} (hp : p ≠ 1) (hn : 0 < n) :
    padicValNat p n = k ↔ p ^ k ∣ n ∧ ¬p ^ (k + 1) ∣ n := by
  rw [padicValNat_def' hp hn, (Nat.finiteMultiplicity_iff.2 ⟨hp, hn⟩).multiplicity_eq_iff]

example : padicValNat 3 48 = 1 :=
  (foo (by decide) (by decide)).2 (by decide)

[Yaël Dillies]

Mario Carneiro said:

where Nat.findBounded has a constructive upper limit and is defined by recursion on nat

You mean docs#Nat.findGreatest ? EDIT: No, but same vibes

[Yaël Dillies]

See also https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Is.20this.20provable.20without.20using.20native_decide.3F