simp and matching on `OfNat.ofNat`.

Stream: lean4

[Joachim Breitner]

In the following example, I can use rw but not simp. Is that expected? How can I express a rewrite rule that applies to literals?

set_option pp.numericTypes true
set_option pp.coercions true

inductive Foo where | mk : Foo

instance : OfNat Foo n where
  ofNat := Foo.mk

def f : Foo → Prop := fun _ => True

theorem f_lit (n : Nat) : f (OfNat.ofNat n) = True := rfl

example : f 42 := by
  fail_if_success simp only [f_lit] -- does not work
  rw [f_lit]; trivial -- works

[Matthew Ballard]

no_index?

[Joachim Breitner]

Ah, I have to put the no_index outside the OfNat.ofNat. Ok, fair enough.

Thanks!

[Eric Wieser]

lean4#2867 tracks removing the no_index requirement (and hopefully improving performance as a result)

[Matthew Ballard]

Note: this workaround is the cause of problems like simp trying a theorem 50k times but never unifying.

[Matthew Ballard]

And I am only now :+1:ing today... :man_facepalming: