How to get simp to fire?

Stream: mathlib4

[Michael Stoll]

Can someone explain this?

import Mathlib

lemma foo {n m : ℕ} [m.AtLeastTwo] : (OfNat.ofNat (α := ZMod n) m).val = m % n :=
  ZMod.val_natCast m

lemma foo' (n : ℕ) {m : ℕ} [m.AtLeastTwo] : (OfNat.ofNat (α := ZMod n) m).val = m % n :=
  ZMod.val_natCast m

lemma foo'' {n : ℕ} (m : ℕ) [m.AtLeastTwo] : (OfNat.ofNat (α := ZMod n) m).val = m % n :=
  ZMod.val_natCast m

example {F} [Field F] (x : F) : x ^ ((3 : ZMod 8).val) = x := by
  -- rw [foo] -- OK
  -- rw [foo'] -- OK
  -- rw [foo''] -- OK
  -- simp only [foo] -- no progress
  -- simp only [@foo] -- no progress
  -- simp only [@foo _] -- OK
  -- simp only [(foo)] -- OK
  -- simp only [@foo (m := 3)] -- OK
  -- simp only [foo'] -- no progress
  -- simp only [foo' _] -- OK
  -- simp only [(foo')] -- no progress
  -- simp only [foo''] -- no progress
  -- simp only [foo'' _] -- OK
  -- simp only [(foo'')] -- OK
  sorry

attribute [simp] foo foo' foo''

example {F} [Field F] (x : F) : x ^ ((3 : ZMod 8).val) = x := by
  -- simp -- no progress
  sorry

lemma bar {n : ℕ} [NeZero n] {m : ℕ} : (OfNat.ofNat (α := Fin n) m).val = m % n := rfl

lemma bar' (n : ℕ) [NeZero n] {m : ℕ} : (OfNat.ofNat (α := Fin n) m).val = m % n := rfl

lemma bar'' {n : ℕ} [NeZero n] (m : ℕ) : (OfNat.ofNat (α := Fin n) m).val = m % n := rfl

example {F} [Field F] (x : F) : x ^ ((3 : Fin 8).val) = x := by
  -- rw [bar] -- OK
  -- rw [bar'] -- OK
  -- rw [bar''] -- OK
  -- simp only [bar] -- no progress
  -- simp only [@bar] -- no progress
  -- simp only [(bar)] -- no progress
  -- simp only [@bar _] -- no progress
  -- simp only [@bar 8] -- no progress
  -- simp only [@bar _ _ 3] -- OK
  -- simp only [bar'] -- no progress
  -- simp only [(bar')] -- no progress
  -- simp only [bar' _] -- no progress
  -- simp only [bar' 8] -- no progress
  -- simp only [bar''] -- no progress
  -- simp only [bar'' _] -- no progress
  -- simp only [bar'' 3] -- OK
  -- simp only [(bar'')] -- no progress
  sorry

I'd like simp to use a variant of foo (and bar) by itself, i.e., by tagging foo with @[simp] and then just using simp without specifying foo explicitly. This seems to be related to whether simp only [foo] works or not, so the secondary question is how to write foo so that this works.

[llllvvuu]

Mathlib-free minimization:

@[simp] theorem bar {n : Nat} (m : Nat) : (OfNat.ofNat (α := Fin n.succ) m).val = m % n.succ := rfl

set_option trace.Meta.Tactic.simp true in
example : ((3 : Fin 8).val) = 3 := by
  -- simp only [bar 3] -- OK
  -- simp only [bar] -- no progress
  sorry

Very interesting. It looks like the lemma is not tried at all

[Alex J. Best]

You need no_index for such ofnat lemmas

@[simp] theorem bar {n : Nat} (m : Nat) : (no_index (OfNat.ofNat (α := Fin n.succ) (no_index m))).val = m % n.succ := rfl

[llllvvuu]

huh, that's interesting (lean4#2867). Looks like only the first no_index is required

[Alex J. Best]

oh yes the second is a typo, i forgot where its meant to go

[Michael Stoll]

I think I tried no_index, but I must have put it in the wrong place.