Representation of exponents

Stream: general

[David Ang]

What's going on in here?

import tactic.ring -- overkill import
variables {R : Type} [comm_ring R] (x : R)
example : x ^ (2048 - 1024) - x ^ 1024 = 0 := by rw [sub_self] -- works
example : x ^ (2049 - 1024) - x ^ 1025 = 0 := by rw [sub_self] -- fails

It seems to me that the natural number exponent is represented differently above a certain threshold?

[Riccardo Brasca]

This

example : x ^ (2049 - 1024) - x ^ 1025 = 0 :=
begin
  change x ^ 1025 - x ^ 1025 = 0,
  rw [sub_self]
end

works, so maybe it is simply that for some reasons Lean gives up on understanding that 2049 - 1024 = 1025 without a little help, but I don't know.

[Mario Carneiro]

Here's a more MWE:

example : bit0 1024 - 1024 = 1024 := by rw [] -- works
example : bit1 1024 - 1024 = 1025 := by rw [] -- fails

rw [] is a way to write "refl with reducible transparency". The surprising one here is the first one, these are not obviously the same and I wouldn't expect weak refl to get it

[Eric Wieser]

It's weird that the presence of x ^ makes rw more likely to succeed:

example : id (2048 - 1024) - id 1024 = 0 := by rw [sub_self] -- fails

[Mario Carneiro]

The representation in all cases is as a chain of bit0 and bit1 applications on 1, so that's not the difference. This representation does preference powers of two though so it's not super surprising that something happens after 1024

[Mario Carneiro]

Given the evidence it sounds like a timeout is occurring during reduction and so the stuff surrounding the match makes a difference