simp usually reduces Fin n literals, but not n itself

[nomeata]

Very conveniently, simp knows about Fin n literals, and reduces them mod n:

example (n : Fin 25) (P : Fin 25 → Prop): P (26) := by
  simp
  guard_target = P 1

It does not do that for n itself, though:

/-- error: simp made no progress -/
#guard_msgs in
example (n : Fin 25) (P : Fin 25 → Prop): P (25) := by
  simp

I expect this to simplify to P 0.

Note that it also doesn't change 0 to n:

/-- error: simp made no progress -/
#guard_msgs in
example (n : Fin 25) (P : Fin 25 → Prop): P 0 := by
  simp

It would be desirable if simp would consistently reduce all Fin n literals (with concrete n) modulo n.

This came up in the equational_theories project.

Versions

"4.12.0-nightly-2024-10-03"

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

[b-mehta]

Out of curiosity, would a similar fix to this one be appropriate for https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/simproc.20for.20Fin as well? Or are the fixes there the correct way to proceed

[nomeata]

I'm not an expert on the API design here. I'd say that whenever a simp rule works it should be used over a simproc. I'm not sure about the conclusion of that thread - did someone find a simp lemma that works?

[b-mehta]

I'd say that whenever a simp rule works it should be used over a simproc.

I think this answers my question!

I'm not sure about the conclusion of that thread - did someone find a simp lemma that works?

It is somewhat implicit in that thread, but the addition which works is

import Mathlib.Data.Fin.Basic

@[simp]
theorem coe_ofNat_of_lt (m n : ℕ) [NeZero m] (h : n < m) :
    ((no_index (OfNat.ofNat n) : Fin m) : ℕ) = OfNat.ofNat n := by
  rwa [Fin.coe_ofNat_eq_mod, Nat.mod_eq_of_lt]

example : ((3 : Fin 4) : Nat) = 3 := by
  simp

[nomeata]

If the discrimnation tree behaviour is ok here (I assume it will be tried on every Fin-to-Nat coercion), then yes, looks plausible.