Is this provable without using native_decide?

Stream: new members

[Kevin Cheung]

Is the following provable without using native_decide? I tried simp, decide, and norm_num so far.

import Mathlib

example : (Nat.factorization 28) 2 = 2 := by
  native_decide

EDIT: Added import.

[Yaël Dillies]

You would get quicker help if your code snippet was a #mwe :wink:

[Kevin Cheung]

Is the edited version now a #mwe? I don't know how to make it more minimal.

[Yaël Dillies]

Sure that's now a MWE. You can make it more minimal (in particular to avoid me having to wait a minute for the imports to load on my Windows machine) by running #min_imports at the bottom of your file (after having changed example with lemma blah)

[Kevin Cheung]

I see. I saw on the #mwe page that it was ok to use "import Mathlib" and the example there does use it. So I thought that was fine.

[Yaël Dillies]

It's fine if like Kevin Buzzard you have bought the latest mac :sweat_smile:

[Yaël Dillies]

I will let you take it from there:

import Mathlib.Data.Nat.Factorization.Defs

namespace Nat
variable {p n k : ℕ}

lemma factorization_eq_iff (hp : p.Prime) (hn : n ≠ 0) :
    n.factorization p = k ↔ p ^ k ∣ n ∧ ¬ p ^ (k + 1) ∣ n where
  mp := by rintro rfl; exact ⟨ordProj_dvd .., pow_succ_factorization_not_dvd hn hp⟩
  mpr := by
    rintro ⟨h, h'⟩
    sorry

example : Nat.factorization 28 2 = 2 := by
  rw [Nat.factorization_eq_iff prime_two (by norm_num)]; constructor <;> decide

end Nat

[Kevin Cheung]

Good to know. Perhaps the #mwe page could highlight that?

[Kevin Cheung]

The lemma seems like something that could be added to Mathlib.

[Kevin Cheung]

Thanks for the starting point. I'll try to complete it.

[Kevin Cheung]

Here is the completed proof. Thanks @Yaël Dillies .

import Mathlib.Data.Nat.Factorization.Basic

namespace Nat
variable {p n k : ℕ}

lemma factorization_eq_iff (hp : p.Prime) (hn : n ≠ 0) :
    n.factorization p = k ↔ p ^ k ∣ n ∧ ¬ p ^ (k + 1) ∣ n where
  mp := by rintro rfl; exact ⟨ord_proj_dvd .., pow_succ_factorization_not_dvd hn hp⟩
  mpr := by
    rintro ⟨h, h'⟩
    have (k : ℕ) := @Prime.pow_dvd_iff_le_factorization p k n hp hn
    rw [this] at h'
    exact Nat.le_antisymm (Nat.le_of_not_lt h') ((this k).mp h)

example : Nat.factorization 28 2 = 2 := by
  rw [Nat.factorization_eq_iff prime_two (by norm_num)]; constructor <;> decide

end Nat

[Yaël Dillies]

See also #new members > How to show value of padicValNat @ 💬

[Kevin Cheung]

Thanks. My proof looks so long in comparison.

[Yaël Dillies]

That's mathlib's fault, not yours :smile:

[Yaël Dillies]

We should burninate docs#padicValNat in favour of docs#Nat.factorization. Probably something @Paul Lezeau and I will do soon