Stream: new members

Topic: Using list.fin_range

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?

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 ?

Mario Carneiro (Aug 05 2020 at 22:35):

that looks like an extensionality lemma to me

Mario Carneiro (Aug 05 2020 at 22:35):

is there anything like list.nth_le_ext?

Mario Carneiro (Aug 05 2020 at 22:36):

list.ext_le

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)


Kevin Buzzard (Aug 05 2020 at 22:39):

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

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


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

oops too slow

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 $M^q$ into $\Lambda (M)$ is multilinear.

Last updated: May 08 2021 at 09:11 UTC