Zulip Chat Archive

Stream: new members

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


view this post on Zulip 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}.

view this post on Zulip Johan Commelin (Dec 16 2019 at 21:08):

Are there lemmas about that mention vector_zero?

view this post on Zulip Johan Commelin (Dec 16 2019 at 21:08):

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

view this post on Zulip Johan Commelin (Dec 16 2019 at 21:09):

So...

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

view this post on Zulip 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?

view this post on Zulip Joe (Dec 16 2019 at 21:17):

length_eq_zero

view this post on Zulip 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

view this post on Zulip Joe (Dec 16 2019 at 21:17):

You can find this using library_search

view this post on Zulip Joe (Dec 16 2019 at 21:18):

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

view this post on Zulip 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.

view this post on Zulip Joe (Dec 16 2019 at 21:22):

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

view this post on Zulip YH (Dec 16 2019 at 21:23):

Great thanks.


Last updated: May 06 2021 at 22:13 UTC