integer division tactic?

Stream: lean4

[Billlie Franch]

I want to ask if there is any useful tactic about integer division in lean4

[Julian Berman]

Can you show an example of a goal you're trying to prove?

[Billlie Franch]

Julian Berman said:

Can you show an example of a goal you're trying to prove?

 example {m n p : ℕ} (coprime_mn : m.coprime n) (prime_p : p.Prime) : m ^ 2 ≠ p * n ^ 2 := by
 sorry

[Ruben Van de Velde]

That's a hard one

[Eric Wieser]

It looks like that's natural division not integer division

[Ruben Van de Velde]

coprime_mn is not needed, is it? I'd just count the multiplicity of p on both sides

[Kevin Buzzard]

You need to rule out m=n=0 somehow

[Kevin Buzzard]

The cool way to do it would be to define core n to be the squarefree part of n (for n>0 this is the unique squarefree t such that n=tm^2) and make enough API for it, including core(ab^2)=core(a), core(p)=p etc

[Kevin Buzzard]

A slightly weird way of doing it with the coprimality assumption would be by proving that m divides pn^2 and hence it divides p and then getting a contradiction in both cases

[Kevin Buzzard]

By the way @Billlie Franch if you think lean tactics are up to solving this kind of questions in one line then I'm afraid you've got a lot to lean about the state of the art with lean tactics...

[Kevin Buzzard]

Would sledgehammer do this in Isabelle?

[Alex Kontorovich]

I'm surprised

import Mathlib.NumberTheory.Padics.PadicVal

theorem padicValNat_ofSquare (n : ℕ) (p : ℕ) (prime_p : p.Prime) (hn : n ≠ 0) :
    Even (padicValNat p (n^2)) := by
  have : Fact (p.Prime) := fact_iff.mpr prime_p
  rw [@padicValNat.pow p n this 2 hn]
  use padicValNat p n
  ring

isn't in mathlib. (Should it be?)

Then apply padicValNat to both sides; one is even, the other odd...

[Alex Kontorovich]

We don't seem to have

theorem padicValNat_mul (n m : ℕ) (hm : m ≠ 0) (hn : n ≠ 0) (p : ℕ) (prime_p : p.Prime) :
    padicValNat p (n * m) = (padicValNat p n) + (padicValNat p m) :=

either? (A bit more annoying to prove, by the looks of it; trying to untangle Part.get (multiplicity p n) (_ : multiplicity.Finite p n)... We do have multiplicity.mul / multiplicity.mul'...)

Should I try to add these?

[Alex J. Best]

We have those, docs#padicValNat.mul, it would be really shocking if we didnt!

import Mathlib

example {m n p : ℕ} (hm : m ≠ 0) (hn : n ≠ 0) (prime_p : p.Prime) : m ^ 2 ≠ p * n ^ 2 := by
  apply_fun (Even <| padicValNat p .)
  simp [*, prime_p.pos.ne', padicValNat.mul (hp := ⟨prime_p⟩), padicValNat.pow (hp := ⟨prime_p⟩),
    parity_simps, padicValNat.self prime_p.one_lt]

[Ruben Van de Velde]

There's docs#Nat.Prime.multiplicity_mul

[Alex Kontorovich]

Not sure how I missed that. I guess it's farther down in the file, after padicValRat is introduced, so I assumed there wasn't more useful padicValNat stuff down below. (Somehow exact? didn't find it either?...) Anyway, thanks!

[Eric Wieser]

padicValNat.mul looks misnamed to be, it should be padicValNat_mul

[Matthew Ballard]

I thought it was namespaced?

[Alex J. Best]

Alex Kontorovich said:

Not sure how I missed that. I guess it's farther down in the file, after padicValRat is introduced, so I assumed there wasn't more useful padicValNat stuff down below. (Somehow exact? didn't find it either?...) Anyway, thanks!

Do you remember what the precise state you called exact on was? It would be good to either debug or understand that failure (there was one in another thread today already that was a timeout, so could be the same thing)

[Alex J. Best]

If its the snippet you posted earlier I guess its just a mismatch between Fact and having the argument explicitly. Maybe we could teach solve_by_elim to try Fact.mk always or something like that?

[Alex Kontorovich]

Yes, that was probably it; it knew p.Prime but not Fact p.Prime! Argh...

[Eric Wieser]

I'd argue that's also a bug: I thought Fact p.Prime was only for instances such as Field (ZMod p)

[Kevin Buzzard]

wait, docs#Nat.Prime.multiplicity_mul has no Fact and neither does the question.

[Eric Wieser]

docs#padicValNat.mul does