Adding vectors of reals

Stream: new members

[Marcus Rossel]

I tried to define addition on vector ℝ n as follows:

protected def add : Π {n : ℕ}, vector ℝ n → vector ℝ n → vector ℝ n
  | 0       ⟨[], _⟩        ⟨[], _⟩        := nil
  | (m + 1) ⟨hd₁::tl₁, h₁⟩ ⟨hd₂::tl₂, h₂⟩ :=
    let v₁ : vector ℝ m := ⟨tl₁, (by simp [list.length_cons] at h₁; exact h₁)⟩ in
    let v₂ : vector ℝ m := ⟨tl₂, (by simp [list.length_cons] at h₂; exact h₂)⟩ in
    (hd₁ + hd₂) ::ᵥ (add v₁ v₂)

Proving things about this definition isn't very nice though. I always have to obtain the underlying list and then do a case distinction on n and the list:

protected theorem add_comm (v₁ v₂ : vector ℝ n) : v₁ + v₂ = v₂ + v₁ := begin
  cases n,
  obtain ⟨l₁, hl₁⟩ := v₁,
  { cases l₁ ; simp [vector.add] },
  {
    cases l₁,
    ...
  }
end

Is there a way to define add directly over vectors, instead of the lists somehow?

[Kevin Buzzard]

vector is a pretty gnarly dependent type. Why not just use the non-dependent type fin n -> \R instead, like in mathlib? Proving things about the latter definition is really easy. I agree that proving things about your definition isn't very nice, but I am suggesting that you don't bother trying to solve this problem.

[Kevin Buzzard]

See for example docs#vector3

[Eric Wieser]

Does docs#vector.zip_with exist?

[Eric Wieser]

Your add is just zip_with (+)

[Eric Wieser]

And your add_comm follows from docs#list.zip_with_comm