## Stream: general

### Topic: simp and vector notation

#### Joseph Myers (Oct 05 2020 at 20:16):

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 (Oct 05 2020 at 20:18):

Sounds good to me

#### Joseph Myers (Oct 07 2020 at 01:29):

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.

Last updated: Dec 20 2023 at 11:08 UTC