Can't get lean to unify equality

Stream: lean4

[Sebastian Widua]

I'm starting to think I'm crazy.
When I do this

def log2_rem (x : Nat) : Nat × Nat :=
  if h_zero : x = 0 then
    (0, 0)
  else if 2 ∣ x then
    have : x / 2 < x := Nat.half_lt_self h_zero
    let (exp, rest) := log2_rem (x / 2)
    (exp+1, rest)
  else (0, x)

theorem log2_rem_eq (x : Nat) : log2_rem x =
 (if h_zero : x = 0 then
    (0, 0)
  else if 2 ∣ x then
    have : x / 2 < x := Nat.half_lt_self h_zero
    let (exp, rest) := log2_rem (x / 2)
    (exp+1, rest)
  else (0, x)) := rfl

I get the error

type mismatch
  rfl
has type
  log2_rem x = log2_rem x : Prop
but is expected to have type
  log2_rem x =
    if h_zero : x = 0 then (0, 0)
    else
      if 2 ∣ x then
        let_fun this := (_ : x / 2 < x);
        match log2_rem (x / 2) with
        | (exp, rest) => (exp + 1, rest)
      else (0, x) : Prop

even though it's literally just the code copy-pasted

[Eric Wieser]

It's not the same code copy-pasted, because log2_rem in the first example is a self-reference to a thing that doesn't exist yet

[Eric Wieser]

The proof of log2_rem_eq should be rw [log2_rem], because Lean generates an unfolding lemma that does what you want

[Sebastian Widua]

Eric Wieser said:

It's not the same code copy-pasted, because log2_rem in the first example is a self-reference to a thing that doesn't exist yet

oh is this because I used well-founded recursion here? Good to know

[Eric Wieser]

Exactly!