Issue with `Nat.log2` and `rfl` (not definitionally equal)

Stream: mathlib4

[Geoffrey Irving]

Nat.log2 isn't behaving nicely under kernel evaluation. I've hit issues with Nat.log2 before in this thread. @Joachim Breitner provided some excellent help in that thread, but the new issue seems unrelated.

Here's a minimized test case. It's minimised since all of the Nat.fast_log2 code can be deleted without changing the issue, which is unsurprising as fast_log2 is only there to help native_decide (it's there only in case that's related to the problem). Whether I use Nat.log2 or Nat.fast_log2, native_decide works but rfl and decide do not. The fast_decide tactic defined at https://github.com/girving/interval/blob/main/Interval/Tactic/Decide.lean also does not work.

import Mathlib.Algebra.Order.Group.Nat
import Mathlib.Algebra.Ring.Nat
import Mathlib.Tactic.Cases
import Interval.Tactic.Decide

/-!
### Kernel-friendly version of `Nat.log2`

Necessary to make kernel computations work without timing out. Implementation courtesy of
Joachim Breitner, though I've specialized it considerably:
  https://leanprover.zulipchat.com/#narrow/stream/239415-metaprogramming-.2F-tactics/topic/An.20interval.20tactic.20for.20constant.20real.20inequalities/near/468309472
-/

/-- Inner loop of `Nat.fast_log2` -/
def Nat.fast_log2.go : Nat → Nat → Nat :=
  Nat.rec (fun _ ↦ 0) (fun _ h n ↦ if 2 ≤ n then h (n / 2) + 1 else 0)

/-- Kernel-friendly version of `Nat.log2` -/
@[irreducible]
def Nat.fast_log2 (n : @& ℕ) : ℕ :=
  fast_log2.go n n

/-- `Nat.fast_log2 = Nat.log2` -/
@[simp, csimp] lemma Nat.fast_log2_eq : fast_log2 = log2 := by
  ext n
  rw [fast_log2]
  suffices h : ∀ f n, (h : n ≤ f) → fast_log2.go f n = n.log2 by
    exact h _ _ (le_refl _)
  intro f
  induction' f using Nat.strong_induction_on with f h
  · intro n nf
    rw [fast_log2.go, log2]
    by_cases n0 : n = 0
    · simp only [n0, nonpos_iff_eq_zero, OfNat.ofNat_ne_zero, ↓reduceIte]
      induction' f with f
      · simp only [rec_zero]
      · simp only [nonpos_iff_eq_zero, OfNat.ofNat_ne_zero, ↓reduceIte]
    have n1 : 1 ≤ n := by omega
    generalize hf1 : f - 1 = f1
    have hf : f = f1 + 1 := by omega
    simp only [hf]
    by_cases n2 : 2 ≤ n
    · simp only [n2, ↓reduceIte, add_left_inj]
      apply h
      all_goals omega
    · simp only [n2, ↓reduceIte]

/-!
### log2 doesn't work well with rfl, though
-/

/-- Works -/
lemma good : (1 : ℕ).log2 = 0 := by native_decide

/-- Fails: the left-hand side one is not definitionally equal to the right-hand side -/
lemma nope : (1 : ℕ).log2 = 0 := by rfl

[Robin Arnez]

Well log2 is defined through wellfounded recursion and is naturally irreducible and fast_log2, well you defined it irreducible yourself. Otherwise:

/-- Inner loop of `Nat.fast_log2` -/
def Nat.fast_log2.go : Nat → Nat → Nat :=
  Nat.rec (fun _ ↦ 0) (fun _ h n ↦ if 2 ≤ n then h (n / 2) + 1 else 0)

/-- Kernel-friendly version of `Nat.log2` -/
def Nat.fast_log2 (n : Nat) : Nat :=
  fast_log2.go n n

example : (12345314871384564987352863479352 : ℕ).fast_log2 = 103 := by rfl

[Robin Arnez]

Hmm I'd love if we actually got something like lean4#7965 though; I've seen too many cases now where people decided to rewrite functions to fueled because of these issues