# Zulip Chat Archive

## 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: May 17 2021 at 22:15 UTC