Zulip Chat Archive

Stream: general

Topic: simp and vector notation


view this post on Zulip 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

view this post on Zulip Johan Commelin (Oct 05 2020 at 20:18):

Sounds good to me

view this post on Zulip 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