Stream: Is there code for X?
Topic: A vector range
Bolton Bailey (Dec 02 2020 at 22:58):
Is there code for a vector range analogous to the list.range function? If not, should this be added to vector.lean?
/-- Vector form of range function -/ def vector_range (k : ℕ) : vector ℕ k := ⟨list.range k, by simp⟩
Yakov Pechersky (Dec 02 2020 at 23:05):
It doesn't currently. I've played around with it for quite some bit. What do you plan to do with it? I've found that working in lists usually ended up being easier.
Bolton Bailey (Dec 02 2020 at 23:30):
This function was useful for me when I wanted to represent a vector of powers of a polynomial variable, which I do using the expression
def powers_of_τ : vector (mv_polynomial vars F) m := vector.map (λ i, X_poly^i) (vector_range m)
In this case I want to use vector rather than list because later I want to take the dot product of this vector with another vector of polynomials, which I do using
* and then calling
sum. I suppose I could convert everything to lists and use
list.map₂, but this seems less clean and I think I would later need to prove that these two lists are the same length. This actually raises another point: Is there code for taking the dot product of vectors of ring elements?
Yakov Pechersky (Dec 02 2020 at 23:31):
Might be easier to do this in
fin n \to R
Yakov Pechersky (Dec 02 2020 at 23:32):
Because if you're going to reason about sum, it's going to be some unwieldy thing about
foldr or something like it, and you'll be juggling lemmas about associativity and identity elements. In
fin n \to R, you can use all the existing
big_operators lemmas about fintypes and fin.
Bolton Bailey (Dec 03 2020 at 10:02):
That sounds great. What are are these
big_operators you are talking about?
big_operators does not come up in a search of the lean documentation.
Reid Barton (Dec 03 2020 at 10:04):
Last updated: May 16 2021 at 05:21 UTC