nonconfluent simp `Fin.succ_zero_eq_one`

Stream: lean4

[Jovan Gerbscheid]

I came across an example like this where I would expect simp to apply the simp lemma Fin.cases_succ. However, it first applies Fin.succ_zero_eq_one, turning 0.succ into 1, so that Fin.cases_succ doesn't work anymore.

example : Fin.cases False (fun _ => True) (Fin.succ (0 : Fin 1)) := by
  simp --only [Fin.cases_succ]
-- unsolved goals
-- ⊢ Fin.cases False (fun x => True) 1

Is there a way to fix this? Or is the only way to add copies of Fin.cases_succ for the special case of 1 and 2 (since there is also Fin.succ_one_eq_two)

[Kim Morrison]

Yes, I think adding the extra copies is required.

(Although I am a bit surprised the confluence checker isn't detecting this one, it seems like it should...)

I think succ_zero_eq_one is probably a good simp lemma, although Lean itself compiles fine without it. We can see at lean#6292 what the downstream fallout is.

[Kim Morrison]

After I installed some new simprocs for Fin, there are only two failures in Mathlib from removing these simp lemmas, and they are easy to work around... Still uncertain whether it is a good idea to remove.

[Jovan Gerbscheid]

The lemma pred_succ on the other hand does come with the lemma pred_one.

And I think your PR #6295 adding simprocs for Fin, makes the simp lemma succ_zero_eq_one redundant?

[Jovan Gerbscheid]

How does the confluence checker work? Does it try to find critical pairs?

[Kim Morrison]

Jovan Gerbscheid said:

And I think your PR #6295 adding simprocs for Fin, makes the simp lemma succ_zero_eq_one redundant?

No, the simproc will only fire for "ground" values of n.

[Kim Morrison]

Jovan Gerbscheid said:

How does the confluence checker work? Does it try to find critical pairs?

Yes. The confluence checker is in lean#5717, unfortunately still not merged. (My fault, we keep accumulating non-confluence problems faster than I fix them. ...)