wlog not working

Stream: general

[Chris Birkbeck]

So I wanted to PR the following

lemma gcd_self_pow (p n m : ℕ) : (p ^ n).gcd (p ^ m) = p ^ (min n m) :=
begin
  wlog h : n ≤ m,
  rw [min_eq_left h],
  apply gcd_eq_left,
  exact pow_dvd_pow p h,
end

and my idea was to put this in data/nat/gcd but in there the wlog doesn't work (specifically it still asks for me to prove the m ≤ n case). Is there some specific import that will get it working? where I was working I had import number_theory.padics.padic_val which does make it work, but I can't add it to data/nat/gcd as I think it becomes circular. I could just change the proof, but I have other things with wlog which give me the same problems so I wanted to see if there is an easy fix.

[Yakov Pechersky]

There's the swap_var tactic which is much weaker but can be used wherever

[Wrenna Robson]

You might need to do this:
wlog h : n ≤ m using [n m, m n]?

[Wrenna Robson]

You need to tell wlog about the symmetry

[Chris Birkbeck]

Wrenna Robson said:

You might need to do this:
wlog h : n ≤ m using [n m, m n]?

No, it seems this gives me three goals instead :( (it asks to also prove n ≤ m ∨ m ≤ n)

[Wrenna Robson]

I suspect ultimately that is the issue yes.

[Wrenna Robson]

I suspect in your context you don't have that?

[Chris Birkbeck]

Well it seems with the correct imports the proof I have above works. I could just prove it without the wlog but I wanted to see if it was easy to get this one working

[Wrenna Robson]

I don't understand how you don't but there it is.

[Chris Birkbeck]

Chris Birkbeck said:

Wrenna Robson said:

You might need to do this:
wlog h : n ≤ m using [n m, m n]?

No, it seems this gives me three goals instead :( (it asks to also prove n ≤ m ∨ m ≤ n)

The problem isnt the specific 0extra goal it adds, its that it adds goals at all

[Wrenna Robson]

Yeah I never use wlog tbh

[Wrenna Robson]

Cursed tactic

[Eric Wieser]

It looks like the actual important import is ring_theory.int.basic

[Ruben Van de Velde]

import data.nat.gcd
instance : is_commutative nat nat.gcd := sorry
instance : is_associative nat nat.gcd := sorry
lemma gcd_self_pow (p n m : ℕ) : (p ^ n).gcd (p ^ m) = p ^ (min n m) :=
begin
  wlog h : n ≤ m,
  rw [min_eq_left h],
  apply nat.gcd_eq_left,
  exact pow_dvd_pow p h,
end

works

[Ruben Van de Velde]

Which is automatic from the gcd_monoid instance in r.i.b, I guess

[Eric Wieser]

Yeah exactly, it needs the docs#nat.gcd_monoid instance in that file

[Ruben Van de Velde]

instance : is_commutative nat nat.gcd := ⟨nat.gcd_comm⟩
instance : is_associative nat nat.gcd := ⟨nat.gcd_assoc⟩

easiest sorries of the day

[Eric Wieser]

I guess we could provide that commutativity instance earlier

[Eric Wieser]

Does it actually need both instances?

[Ruben Van de Velde]

I didn't check

[Eric Wieser]

Looks like it does

[Eric Wieser]

I guess it uses ac_refl somewhere

[Ruben Van de Velde]

Yeah

[Chris Birkbeck]

Oh nice that does work. Would adding those instances before the lemma be fine then? We could put the lemma somewhere else, it just seemed that this was the natural place to have it

[Chris Birkbeck]

(or just prove it without wlog...)

[Eric Wieser]

Is this property true in all gcd_monoids?

[Eric Wieser]

Yes, I think it is, stated as

(p ^ n).gcd (p ^ m) = normalize p ^ (min n m)

[Chris Birkbeck]

I can prove

lemma gcd_self_pow [R : Type*] [cancel_comm_monoid_with_zero R] [normalized_gcd_monoid R]
  (p : R) (n m : ℕ) : gcd (p ^ n) (p ^ m) = normalize (p ^ (min n m)) :=

Ill think more about how to change normalized_gcd_monoid for gcd_monoid

[Eric Wieser]

I suspect that's all you need to prove