[Merged by Bors] - feat(data/matrix/notation): simp lemmas for constant-indexed elements

[jsm28]

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].

---

[eric-wieser]

I'm slightly surprised this doesn't already exist!

[jcommelin]

See also #4406, in particular https://github.com/leanprover-community/mathlib/pull/4406/files#diff-0ad6543ff7afc0f24fe40302b8a0b440R84

[jsm28]

Despite the doc string there, I definitely needed the extra argument here to give control over definitional equality for the vector length (otherwise there's a problem comparing a vector of length m + 1 + n with one of length m + n + 1 in cons_join).

[Vierkantor]

My own experience with finvec-like structures tells me that the append in this PR is much more practical than the one in #4406. (Applying eq.rec on data is like the definition of DTT hell.)

[Vierkantor]

Thanks, this looks very useful!

[Vierkantor]

I missed a few spots in copying my remarks, sorry! Apart from that, looks good to me.

[eric-wieser]

Does it make sense to define this instead as:

Suggested change

	def vec_alt0 (hm : m = n + n) (v : fin m → α) (k : fin n) : α :=
	v ⟨(k : ℕ) + k, hm.symm ▸ add_lt_add k.property k.property⟩
	def fin.bit0 (hm : m = n + n) (k : fin n) : fin m :=
	⟨(k : ℕ) + k, hm.symm ▸ add_lt_add k.property k.property⟩

and then using v ∘ fin.bit0?

[jsm28]

I'm not sure what other use there would be for that definition, but if we want it (possibly built on variants adding two different fin values, with or without 1 added as well) then presumably it goes in data.fin.

[eric-wieser]

Or perhaps for consistency with the other bit0 functions,

def fin.bit0 {n : ℕ} (k : fin n) : fin (n + n) :=
⟨(k : ℕ) + k, add_lt_add k.property k.property⟩

/-- `hm` provides control of definitional equality -/
def fin.bit0' {m n : ℕ} (hm : m = n + n) : fin m := fin.cast hm.symm ∘ (fin.bit0 k)

[Vierkantor]

I'm mildly in favour of the fin.bit0/fin.bit0' proposal, but keeping vec_alt0 until we really need fin.bit0 also makes sense to me.

[eric-wieser]

If nothing else, v ∘ fin.bit0 seems like a clearer name to me than vec_alt0.

[eric-wieser]

Also at that point, it seems quite desirable to express it as

def fin.bit0 {n : ℕ} (k : fin n) : fin (bit0 n) :=
⟨bit0 (k : ℕ), _⟩

to make the connection between nat.bit0 and fin.bit0 really clear.

[jsm28]

I don't see any nat.bit0 definition, only _root_.bit0.

As noted above, using bit0 and bit1 in these definitions ends up meaning the subsequent proofs need to unfold bit0 and bit1 in several places; they're simpler if these definitions don't use bit0 and bit1.

[eric-wieser]

How about as a compromise, we introduce fin.bit0, then as a follow-up I'll try re-expressing the proofs to use bit0 k instead of k + k?

[jsm28]

If you use fin.bit0 for vec_alt0, then in the context of these lemmas you should have fin.bit1 for vec_alt1; vec_alt0 and vec_alt1 are exactly analogous, extracting alternate elements of an even-length vector.

However, fin.bit0 and fin.bit1 would not be so clearly analogous to each other when seen on their own. fin.bit0 would map fin n to fin (bit0 n), while fin.bit1 would also map fin n to fin (bit0 n); it would not map to fin (bit1 n), which would be an odd inconsistency in the fin context. But if you make fin.bit0 instead map to the smallest fin type that can hold all the required values, i.e. fin (bit0 n - 1), that's no longer what's wanted for vec_alt0. And if you combine such a function with cast_succ to get back to fin (bit0 n) as needed for vec_alt0, you start needing to special-case n = 0 because fin 0 not fin 1 is correct there.

I think of bit0 and bit1 as being about numerals; those definitions outside the context of numerals don't seem very helpful. I can see more possible use for two-argument versions that might be something like fin.add_cast_add and find.add_add_one_cast_add that map fin m and fin n to fin (m + n) (with an appropriate extra argument for control of definitional equality of types). That could e.g. map row and column indices in some context to indices for diagonals, or generally be relevant for some kind of convolution indexed by fin types. But it also wouldn't work with function composition for defining vec_alt0 and vec_alt1 in any such convenient way as fin.bit0 or fin.bit1.

[Vierkantor]

I'm happy with the changes as-is, although the suggestion to move vec_alt0 to fin.bit0 would be nice for consistency. @urkud @eric-wieser, any suggestions?

[jcommelin]

Thanks 🎉

bors merge

Any slight changes concerning vec_alt0 vs fin.bit0 can be sorted out in a later PR.

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests