motive is not type correct

Stream: lean4

[Arien Malec]

I apologize for the lack of an #mwe but I've found it hard to isolate this issue out of context...

import Std.Data.Rat

@[simp] theorem mk_zero: (mkRat 0 n) = 0 := by
  cases n with
  | zero => simp [mkRat]
  | succ n => simp [mkRat, normalize, maybeNormalize, Int.natAbs]; split; rename_i hn; rw [hn]

fails at rw with the error message

tactic 'rewrite' failed, motive is not type correct
case succ.inl
n: Nat
hn: n = 0
⊢ mk 0 (Nat.succ n) = 0

but all the types check AFAIK

[Marcus Rossel]

Could you post the definitions of normalize and maybeNormalize?

[Marcus Rossel]

Ah, it's Rat.normalize and Rat.maybeNormalize.
Using subst hn instead of rw [hn] works here:

import Std.Data.Rat

@[simp] theorem mk_zero: (mkRat 0 n) = 0 := by
  cases n with
  | zero => simp [mkRat]
  | succ n =>
    simp [mkRat, Rat.normalize, Rat.maybeNormalize, Int.natAbs]
    split
    case _ hn => subst hn; rfl
    case _ hn => sorry

[Arien Malec]

(deleted)

[Arien Malec]

Is there a reason why rw fails here?

[Adam Topaz]

I think it's because mk secretly has some additional parameters

[Adam Topaz]

note that simp [hn] also works.

[Arien Malec]

yes, mk has additional parameters -- this explains the error I got while trying to create an #mwe -- thanks!

[James Gallicchio]

There are also many threads on motive not type correct, if you run into further problems maybe give those threads a gander :)