rewriter oddity

Stream: general

[Chris B]

I ran into this while showing someone the natural numbers game; am I wrong in thinking one (or all) of these should succeed? Both the rewrites fail, and so does library_search. The version of pow_zero in core works, as does the one in NNG. I'm on mathlib cd29ede, lean 3.16.5c

example (a b : nat) : a * (b ^ 0) = a := by library_search

example (a b : nat) : a * (b ^ 0) = (a * 1) := by library_search

example (a b : nat) : a * (b ^ 0) = a :=
begin
  intros,
  rw pow_zero,
  sorry
end

example (a b : nat) : a * (b ^ 0) = a :=
begin
  intros,
  rw pow_zero b,
  sorry
end

[Shing Tak Lam]

wrt. the rewrites, I think you need nat.pow_zero, not pow_zero.

[Bryan Gin-ge Chen]

Here's the first error message if you have set_option pp.notation false and set_option pp.implicit true:

rewrite tactic failed, did not find instance of the pattern in the target expression
  @pow nat nat (@monoid.has_pow nat nat.monoid) b 0
state:
a b : nat
⊢ @eq nat (@has_mul.mul nat nat.has_mul a (@pow nat nat nat.has_pow b 0)) a

So Lean is having trouble unifying @pow nat nat (@monoid.has_pow nat nat.monoid) b 0 (required by src#pow_zero, in algebra.group_power) with @pow nat nat nat.has_pow b 0, whereas src#nat.pow_zero (in core) works.

[Chris B]

Thank you both. The type of pow_zero says it's generic over instances of monoid and #print instances monoid shows that there's a nat.monoid in the environment. I don't really know anything about how lean handles typeclass instances internally, but am I wrong to think that src#pow_zero should succeed here?

[Mario Carneiro]

it should not succeed

[Mario Carneiro]

the problem is that there are two power functions, monoid.pow and nat.pow, and they look the same

[Mario Carneiro]

if you use power on nats you get nat.pow, otherwise you get monoid.pow

[Mario Carneiro]

and only the nat.pow_* theorems work on nat.pow unless you first rewrite with nat.pow_eq_pow

[Kevin Buzzard]

This is something which could be fixed but which would just be painful to fix, right?

[Chris B]

Wow, what a bummer. Is that kind of overloading common in mathlib?

[Chris B]

Thanks for the explanation though.

[Johan Commelin]

Chris B said:

Wow, what a bummer. Is that kind of overloading common in mathlib?

No, this issue with nat.pow is sort of unique. At some point we'll have the courage to fix it.

[Kevin Buzzard]

When the number of people reporting it every month on Zulip becomes too much to bear :-)

[Kevin Buzzard]

Is nat.pow still in core?

[Mario Carneiro]

The issue with nat.pow is also similar to coe : nat -> int vs coe : nat -> A

[Mario Carneiro]

It is in core. Did we determine that it had a GMP implementation in C++?

[Johan Commelin]

Yes, I think it does

[Mario Carneiro]

it doesn't

[Mario Carneiro]

but gcd does? crazy

[Kevin Buzzard]

The coe issue burnt @Ashvni Narayanan only yesterday, with maps from nat to int to with_top int

[Johan Commelin]

Mario Carneiro said:

it doesn't

Then we should give it one, right?

[Mario Carneiro]

looks pretty easy

[Johan Commelin]

If you speak GMP

[Ashvni Narayanan]

Kevin Buzzard said:

The coe issue burnt Ashvni Narayanan only yesterday, with maps from nat to int to with_top int

Yeah, I was trying to show

lemma val_int_power (a : K) (nz : a ≠ 0) : ∀ n : ℤ, v(a^n) = (n : with_top ℤ)*v(a) :=

for a discrete valuation field K. Finally used this

lemma with_top.sub_add_eq_zero (n : ℕ) : ((-n : ℤ) : with_top ℤ) + (n : with_top ℤ) = 0 :=

so it worked out okay.