Commit 2020-10-15 16:28 b01ca810

feat(data/matrix/notation): simp lemmas for constant-indexed elements (#4491) If you use the ![] vector notation to define a vector, then simp can extract elements 0 and 1 from that vector, but not element 2 or subsequent elements. (This shows up in particular in geometry if defining a triangle with a concrete vector of vertices and then subsequently doing things that need to extract a particular vertex.) Add bit0 and bit1 simp lemmas to allow any element indexed by a numeral to be extracted (even when the numeral is larger than the length of the list, such numerals in fin n being interpreted mod n). This ends up quite long; bit0 and bit1 semantics mean extracting alternate elements of the vector in a way that can wrap around to the start of the vector when the numeral is n or larger, so the lemmas need to deal with constructing such a vector of alternate elements. As I've implemented it, some definitions also need an extra hypothesis as an argument to control definitional equalities for the vector lengths, to avoid problems with non-defeq types when stating subsequent lemmas. However, even the example added to test/matrix.lean of extracting element 123456789 of a 5-element vector is processed quite quickly, so this seems efficient enough. Note also that there are two @[simp] lemmas whose proofs are just by simp, but that are in fact needed for simp to complete extracting some elements and that the simp linter does not (at least when used with #lint for this single file) complain about. I'm not sure what's going on there, since I didn't think a lemma that simp can prove should normally need to be marked as @[simp].