nth_map

Stream: general

[Patrick Massot]

Do we have something like

lemma nth_le_map {α : Type*} {β : Type*} {l : list α} (n : ℕ) (H: n < length l)
  (f : α → β) : nth_le (map f l) n ((length_map f l).symm ▸ H) = f (nth_le l n H) :=

[Patrick Massot]

It feels a bit weird to stick a proof in the middle of the statement

[Patrick Massot]

Am I doing something wrong?

[Mario Carneiro]

One approach I have used in the past is to have two proof arguments, but this makes rewriting produce proof obligations that look superfluous

[Patrick Massot]

And I don't know how to prove it

[Mario Carneiro]

i.e. you would prove nth_le (map f l) n H1 = f (nth_le l n H2)

[Patrick Massot]

You you mean adding (H' : n < length (map f l))?

[Patrick Massot]

ok

[Patrick Massot]

I still don't know how to prove it though

[Patrick Massot]

Why is this not in mathlib? It looks like it would be useful for many proofs

[Mario Carneiro]

I'm asking the same question

[Mario Carneiro]

I would start with nth

[Mario Carneiro]

since that avoids the proof argument stuff

[Patrick Massot]

I also thought that

[Patrick Massot]

But I couldn't even state it :disappointed:

[Patrick Massot]

Because f doesn't want an option α

[Mario Carneiro]

theorem nth_map (f : α → β) : ∀ l n, nth (map f l) n = (nth l n).map f
| []       n     := rfl
| (a :: l) 0     := rfl
| (a :: l) (n+1) := nth_map l n

theorem nth_le_map (f : α → β) {l n} (H1 H2) : nth_le (map f l) n H1 = f (nth_le l n H2) :=
option.some.inj $ by rw [← nth_le_nth, nth_map, nth_le_nth]; refl

[Mario Carneiro]

option.map takes f : A -> B to map f : option A -> option B

[Patrick Massot]

:open_mouth:

[Patrick Massot]

I was clearly missing that option.map piece

[Patrick Massot]

but probably not only that

[Mario Carneiro]

option is a functor

[Kenny Lau]

is this proven in mathlib / Lean?

[Mario Carneiro]

yes, because every monad is a functor

[Mario Carneiro]

and option is like the very first monad you write

[Kenny Lau]

you mean sentence

[Mario Carneiro]

like when learning what monads are and examples, option is always the example

[Patrick Massot]

Thank you very much Mario. I hope this will also be a good reference next time I'll hit this option stuff

[Patrick Massot]

I still think you could put those two lemmas in mathlib

[Mario Carneiro]

I'm doing that now

[Mario Carneiro]

I definitely want more nth and index_of theorems, to make it easier to think of list as finitely supported functions on nat

[Patrick Massot]

Great

[Patrick Massot]

I was going after something like reverse (range' a b) = map (lam x, ...) (range' a b) and stuff like that

[Patrick Massot]

And was also thinking about defining int_range k n same as range' but k is an integer

[Patrick Massot]

and generalizing all the range' lemmas to this case

[Mario Carneiro]

That makes sense. I guess you could define range' generalized to any semiring, although it doesn't have the "consecutivity" property except in nat and int