Some kind of issue with `testBit_shiftLeft` as `grind` lemma

Stream: lean4

[Wrenna Robson]

The following works:

@[grind =]
theorem testBit_shiftRight_shiftLeft_add {n j k : ℕ} (x : ℕ) : (x >>> n <<< (n + k)).testBit j =
    (decide (n + k ≤ j) && x.testBit (j - k)) := by
  rcases le_or_gt (n + k) j with h | h
  · simp only [testBit_shiftLeft]
    grind
  · grind

However, this does not.

@[grind =]
theorem testBit_shiftRight_shiftLeft_add {n j k : ℕ} (x : ℕ) : (x >>> n <<< (n + k)).testBit j =
    (decide (n + k ≤ j) && x.testBit (j - k)) := by
  rcases le_or_gt (n + k) j with h | h
  · grind
  · grind

This is despite testBit_shiftLeft being a grind lemma. I wonder if there's something misfiring here? I seem to keep encountering odd hiccups with shiftLeft and grind in particular.

[Wrenna Robson]

I will file this as an issue if it actually is one, but I just want to check I'm not missing something.

[Henrik Böving]

Both of these work on live https://live.lean-lang.org/#codez=JYWwDg9gTgLgBAWQIYwBYBtgCMBQOACA2gOZTAB2AJnALwC6OaAptEyHDEwM4wBCwMAPpdUwAGYwASsGKohI8TAAyTCYKSVqAb3JwAVnADWcAFxxAqIQBfOAAoAHqYsBKR/bgA+T3F0AeP7d0AaiMnJwA6Th5+eAMaHDgE20omAGNgZIC4YONAEyJ9FwAyArg7CO4+AVsDAFoQlxMaOCwAT3i4KBSkLm44dCZBaEFieBsgkP04AHcBVDhZgB85toB2uFIKShW1sio8InWqWgZmVnZIivlRCWlZS8UVNQ1KAHI4HQnjMytbBy/6n48Xl8/lGWTqZSilVibQSNmSaQyoOycDyekKxVK52iVTgtUMoVMjRabQ6XR6fQGUCGIzG+Im0zQczgi1QWy4oDAcAg5HQzTghAAcigIRdhFdlKoYAxEtsNlsDpQgA

[Wrenna Robson]

Hmm, interesting! To be clear I'm on just-updated Mathlib, I think on .27rc1

[Wrenna Robson]

Did we make a change here recently?

[Henrik Böving]

Leo makes half a dozen changes on grind on a daily basis

[Wrenna Robson]

Ha. I meant "one that might obviously touch this fairly niche area" but yeah if it's some subtle improvement I guess it won't be obvious.

[Wrenna Robson]

It's very cool how often I have an issue with grind and by the time I've found it it's already actually been fixed

[Wrenna Robson]

Hmm. In fact they seem to work there on latest Mathlib... which is what I am using on my machine. In both cases #version gives the same output.

[Wrenna Robson]

So possibly I have made some local definition that is causing my issue!

[Wrenna Robson]

Thanks

[Wrenna Robson]

Hmm, OK. Some MWEs.

namespace Nat

@[grind =]
theorem testBit_shiftRight_shiftLeft_add {n j k : Nat} (x : Nat) : (x >>> n <<< (n + k)).testBit j =
    (decide (n + k ≤ j) && x.testBit (j - k)) := by
  grind

theorem toNat_testBit_zero {x : Nat} : (x.testBit 0).toNat = x % 2 := by grind

end Nat

This works.

However, this does not (why does this change anything?!)

namespace Nat

theorem toNat_testBit_zero {x : Nat} : (x.testBit 0).toNat = x % 2 := by grind

@[grind =]
theorem testBit_shiftRight_shiftLeft_add {n j k : Nat} (x : Nat) : (x >>> n <<< (n + k)).testBit j =
    (decide (n + k ≤ j) && x.testBit (j - k)) := by
  grind

end Nat

However, this works again.

import Mathlib

namespace Nat

theorem toNat_testBit_zero {x : Nat} : (x.testBit 0).toNat = x % 2 := by grind

@[grind =]
theorem testBit_shiftRight_shiftLeft_add {n j k : Nat} (x : Nat) : (x >>> n <<< (n + k)).testBit j =
    (decide (n + k ≤ j) && x.testBit (j - k)) := by
  grind

end Nat

[Wrenna Robson]

So the ordering of my theorem after a non-grind theorem suddenly means grind is taking a while (appears to timeout). However, something happens in Mathlib that makes this not an issue.

[Wrenna Robson]

This is strange behaviour, right?

[Wrenna Robson]

It doesn't seem to matter what the theorem is, mind.

[Henrik Böving]

Probably some local definition cache is poisoned, feel free to report the mathlib free version as an issue.

[Wrenna Robson]

Can you confirm you do get the same issue as me (on the non-Mathlib copy?)

[Wrenna Robson]

Filed as lean4#11697