Using list.fin_range

Stream: new members

[Zhangir Azerbayev]

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]

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]

that looks like an extensionality lemma to me

[Mario Carneiro]

is there anything like list.nth_le_ext?

[Mario Carneiro]

list.ext_le

[Mario Carneiro]

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]

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

[Mario Carneiro]

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]

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

[Reid Barton]

oops too slow

[Zhangir Azerbayev]

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