max recursion depth reached on `simp [getElem]`

Stream: lean4

[David Renshaw]

def a : Array Nat := #[1,2,3,4,5]

example : a[2] = 3 := by
  simp [getElem]
  -- tactic 'simp' failed, nested error:
  -- maximum recursion depth has been reached

What is going on here?

[David Renshaw]

(I know that rfl or decide close the goal. I want to understand why this simp seems to get in an infinite loop.)

[Eric Wieser]

I think it's because there is a lemma that turns get back into getElem

[Eric Wieser]

Try doing simp only [getElem] followed by simp? to find it

[Kim Morrison]

Does set_option diagnostics true show you the theorems involved in the infinite loop?

[David Renshaw]

[reduction] unfolded declarations (max: 57, num: 2): ▼
  List.rec ↦ 57
  List.concat ↦ 30
[reduction] unfolded reducible declarations (max: 57, num: 2): ▼
  List.casesOn ↦ 57
  outParam ↦ 24

[David Renshaw]

Eric Wieser said:

Try doing simp only [getElem] followed by simp? to find it

Ah. The simp theorem Array.get_eq_getElem is doing it.

[David Renshaw]

The reason that I was adding getElem was that simp does not close the goal (which seems a bit surprising to me).

[David Renshaw]

This works:

  simp only [getElem, Array.get, List.get]

[Kim Morrison]

@David Renshaw, the original problem will be solved after lean#4765 "feat: simprocs for #[1,2,3,4,5][2] ".