Stream: new members

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

YH (Dec 16 2019 at 21:00):

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 (Dec 16 2019 at 21:08):

Are there lemmas about that mention vector_zero?

Johan Commelin (Dec 16 2019 at 21:08):

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

Johan Commelin (Dec 16 2019 at 21:09):

So...

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


YH (Dec 16 2019 at 21:12):

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 (Dec 16 2019 at 21:17):

length_eq_zero

Joe (Dec 16 2019 at 21:17):

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


Joe (Dec 16 2019 at 21:17):

You can find this using library_search

Joe (Dec 16 2019 at 21:18):

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

Joe (Dec 16 2019 at 21:19):

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

Joe (Dec 16 2019 at 21:22):

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