nth_rw and equation lemmas

Stream: lean4

[Timo Carlin-Burns]

When using rw to unfold a recursive definition using equation lemmas, it seems to find the first equation lemma whose LHS appears in the goal, and then find the leftmost occurrence of that LHS in the goal. I would've expected it to find the leftmost subexpression in the goal which matches any of the possible equation lemmas. Similarly, I would expect nth_rw n (AKA rw (config := {occs := .pos [n]})) to find the nth subexpression which matches any of the equation lemmas, not just the first equation lemma.

example (x : α) : [x].length = ([] : List α).length + 1 := by
  rw [List.length] -- unsolved goals; rewrites `[].length = 0` instead of `[x].length = [].length + 1`

example (x : α) : [x].length = ([] : List α).length + 1 := by
  rw (config := {occs := .pos [1]}) [List.length] -- same as above

example (x : α) : [x].length = ([] : List α).length + 1 := by
  rw (config := {occs := .pos [2]}) [List.length] -- error; `rw` can't find a second occurence for the `[].length = _` equation

-- Workaround: Use the specific desired equation lemma
example (x : α) : [x].length = ([] : List α).length + 1 := by
  rw [List.length.eq_2] -- success

Should this be fixed?

[Joachim Breitner]

Maybe it should, although it could be non-trivial to achieve with the rw implementation, and since a work-around exist fixing may be not high priority. But certainly worth recording this as an issue against the lean repository.

[Timo Carlin-Burns]

Made an issue at lean4#5026!

[François G. Dorais]

That's an interesting case. However, simp only [List.length] does exactly what you expect (and a tiny bit more mostly harmless stuff in some cases). Is there a reason why you must use rw instead of simp only?

[Timo Carlin-Burns]

In the original example, the user didn't use simp only because they were solving exercises in a book that only taught rw. In regular Lean usage, another reason I can imagine is that simp only repeatedly applies the equation lemmas, which could cause performance issues if there are large terms involved

[François G. Dorais]

Well, I don't know what book but, at an early stage of learning Lean, it might be better to introduce List.length_nil and List.length_cons than relying on equation lemmas for List.length.

[Timo Carlin-Burns]

(Here is the original thread https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Mechanics.20of.20Proof.20--.20Trouble.20rewriting.20factorial.20sometimes.3F/near/459950961)