How do I show that sum of trivial vector of ℝ is zero?

Stream: new members

[YH]

OK this feels really dumb but I got stuck on showing

lemma ss0 (a : vector ℝ 0): a.val.sum = 0 :=

where vector α n is defined as {l : list α // length l = n}.

[Johan Commelin]

Are there lemmas about that mention vector_zero?

[Johan Commelin]

You would want a lemma that says a.val = []

[Johan Commelin]

So...

begin
  suffices : a.val = [],
  { rw this, sorry },
  library_search
end

[YH]

Didn't find any. But I guess I can prove that anyway.
Now if my goal is length (a.val) = 0 → a.val = nil how do I generalize it so that it is for all list l, length (l) = 0 → l = nil?

[Joe]

length_eq_zero

[Joe]

theorem length_eq_zero {l : list α} : length l = 0 ↔ l = [] :=
⟨eq_nil_of_length_eq_zero, λ h, h.symm ▸ rfl⟩

[Joe]

You can find this using library_search

[Joe]

Though to actually prove this by hand, use induction on the list l.

[Joe]

That is, if l is nil, then nothing to prove; if l is x :: xs, then there is a contradiction.

[Joe]

lemma foo {α : Type*} {l : list α} : length l = 0 → l = nil :=
begin
  intros,
  induction l,
  { refl },
  { contradiction }
end

[YH]

Great thanks.