simp and vector notation

Stream: general

[Joseph Myers]

If you use the ![] vector notation to define a vector, then simp can extract elements 0 and 1 from that vector, but not any subsequent elements. Should there be bit0 and bit1 lemmas to allow simp to extract any constant-number element from a vector defined with this notation? This shows up in geometry when you use that notation to define a triangle with an explicit list of vertices, and then simp can only extract the first two vertices.

import data.matrix.notation

variables {α : Type*} (a b c d e : α)

-- These examples work.
example : ![a, b, c, d, e] 0 = a := by simp
example : ![a, b, c, d, e] 1 = b := by simp

-- These only work with `rfl`, not with `by simp`.
example : ![a, b, c, d, e] 2 = c := by simp
example : ![a, b, c, d, e] 3 = d := by simp
example : ![a, b, c, d, e] 4 = e := by simp

[Johan Commelin]

Sounds good to me

[Joseph Myers]

Done. See #4491. It ended up taking me 140 lines of Lean to get simp to handle this in general (including cases where the numeral exceeds the length of the list and is interpreted mod that length), and two of the simp lemmas there are proved by simp but for some reason it doesn't work without them being marked as simp lemmas, which I don't understand.