rw?? won't match `n + 1` with `n.succ`

Stream: mathlib4

[Jakub Nowak]

Maybe we could include special casing for this, like in match pattern?

In the below code, shift+click on List.range (n + 1), it won't find List.range n ++ [n] as possible rewrite. It does, if you replace n + 1 with n.succ.

import Mathlib

example : List.range (n + 1) = List.range n ++ [n] := List.range_succ

example : List.range (n + 1) = List.range n ++ [n] := by
  rw??

[Jakub Nowak]

Or maybe it's API issue and we should have List.range (n + 1) = List.range n ++ [n] instead of List.range n.succ = List.range n ++ [n] in the API, because simp simplifies n.succ to n + 1.

[Jakub Nowak]

Btw, rw? is able to find List.range_succ, so it seems rw? can see past defeq but rw?? doesn't?

[Jovan Gerbscheid]

This is certainly an API issue. I would not expect to matchn + 1 with n.succ, because this requires unfolding Nat.add.

However, Nat.add gets special treatment by some metaprogramming functions, which is why the rewrite works in the first place.

The discrimination tree used by rw?? does not treat Nat.succ or Nat.add specially in this regard, so they are indexed as different patterns.

[Jovan Gerbscheid]

I have now created lean#11768 to replace the range_succ lemmas by range_add_one

[Jakub Nowak]

That's wrong PR number I think? Now it's ok. :)

[Jakub Nowak]

I think the naming convention in mathlib is to write succ in the name of the theorem, yet use n + 1 in the statement? Maybe name it to range_succ' and after the deprecated range_succ is deleted we can rename range_succ' to range_succ?

[Jovan Gerbscheid]

See the other Zulip conversation that I linked in the PR: #mathlib4 > Naming convention: succ vs. add_one @ 💬

My conclusion is that we want to move away from succ in the name.

[Jakub Nowak]

Ah, yeah, I saw that conversation before, but forgot about it.