Zulip Chat Archive

Stream: new members

Topic: Using list.fin_range


view this post on Zulip Zhangir Azerbayev (Aug 05 2020 at 19:24):

I need to prove the following lemma.

lemma {q : nat} :  list.fin_range q.succ  =  0 :: list.map fin.succ (list.fin_range q)

There are very few lemmas about list.fin_range, so it seems inevitable that any proof would have to work with the underlying list.pmap. Induction on q hasn't worked for me because that approach requires splitting the last element of a list from the rest. I've also tried hitting the goal with ext but that hasn't given me anything I can figure out how to work with. Does anyone have suggestions for how to proceed?

view this post on Zulip Kevin Buzzard (Aug 05 2020 at 22:32):

I thought

lemma list.eq_of_nth_le_eq (α : Type) (A B : list α) (n : ) (hAn : n = A.length) (hBn : n = B.length)
(h :  (i : ) (hi : i < n), A.nth_le i (hAn  hi) = B.nth_le i (hBn  hi)) : A = B :=
begin
  sorry
end

might help, but I didn't prove that and even with it I couldn't make much progress. I'm not great at this stuff. @Mario Carneiro ?

view this post on Zulip Mario Carneiro (Aug 05 2020 at 22:35):

that looks like an extensionality lemma to me

view this post on Zulip Mario Carneiro (Aug 05 2020 at 22:35):

is there anything like list.nth_le_ext?

view this post on Zulip Mario Carneiro (Aug 05 2020 at 22:36):

list.ext_le

view this post on Zulip Mario Carneiro (Aug 05 2020 at 22:38):

lemma list.eq_of_nth_le_eq (α : Type) (A B : list α) (n : ) (hAn : n = A.length) (hBn : n = B.length)
(h :  (i : ) (hi : i < n), A.nth_le i (hAn  hi) = B.nth_le i (hBn  hi)) : A = B :=
list.ext_le (hAn.symm.trans hBn) $ λ i h1 h2, h i (by rwa hAn)

view this post on Zulip Kevin Buzzard (Aug 05 2020 at 22:39):

only problem is that it doesn't help ;-)

view this post on Zulip Mario Carneiro (Aug 05 2020 at 22:50):

namespace list

theorem pmap_map {α β γ} {p : β  Prop} (g :  b, p b  γ) (f : α  β)
  (l H) : pmap g (map f l) H = pmap (λ a h, g (f a) h) l (λ a h, H _ (mem_map_of_mem _ h)) :=
by induction l; [refl, simp only [*, pmap, map]]; split; refl

example {q : nat} : fin_range q.succ = 0 :: map fin.succ (fin_range q) :=
begin
  unfold fin_range,
  rw [map_pmap],
  simp_rw [range_succ_eq_map],
  rw [pmap],
  congr' 1,
  rw pmap_map,
  apply pmap_congr,
  intros, refl,
end

end list

view this post on Zulip Reid Barton (Aug 05 2020 at 22:50):

I think a better strategy should be to use the fact that list.map fin.val is injective and use range_succ_eq_map

view this post on Zulip Reid Barton (Aug 05 2020 at 22:50):

oops too slow

view this post on Zulip Zhangir Azerbayev (Aug 06 2020 at 00:20):

Thank you @Mario Carneiro ! With that we have a sorry-free proof that the canonical map from MqM^q into Λ(M)\Lambda (M) is multilinear.


Last updated: May 08 2021 at 09:11 UTC