## Stream: general

### Topic: nth_map

#### Patrick Massot (May 13 2018 at 20:59):

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 (May 13 2018 at 20:59):

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

#### Patrick Massot (May 13 2018 at 20:59):

Am I doing something wrong?

#### Mario Carneiro (May 13 2018 at 21:01):

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 (May 13 2018 at 21:01):

And I don't know how to prove it

#### Mario Carneiro (May 13 2018 at 21:01):

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

#### Patrick Massot (May 13 2018 at 21:01):

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

ok

#### Patrick Massot (May 13 2018 at 21:02):

I still don't know how to prove it though

#### Patrick Massot (May 13 2018 at 21:03):

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

#### Mario Carneiro (May 13 2018 at 21:03):

I would start with nth

#### Mario Carneiro (May 13 2018 at 21:03):

since that avoids the proof argument stuff

#### Patrick Massot (May 13 2018 at 21:03):

I also thought that

#### Patrick Massot (May 13 2018 at 21:03):

But I couldn't even state it :disappointed:

#### Patrick Massot (May 13 2018 at 21:04):

Because f doesn't want an option α

#### Mario Carneiro (May 13 2018 at 21:08):

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 (May 13 2018 at 21:08):

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

:open_mouth:

#### Patrick Massot (May 13 2018 at 21:10):

I was clearly missing that option.map piece

#### Patrick Massot (May 13 2018 at 21:10):

but probably not only that

#### Mario Carneiro (May 13 2018 at 21:10):

option is a functor

#### Kenny Lau (May 13 2018 at 21:10):

is this proven in mathlib / Lean?

#### Mario Carneiro (May 13 2018 at 21:10):

yes, because every monad is a functor

#### Mario Carneiro (May 13 2018 at 21:11):

and option is like the very first monad you write

#### Kenny Lau (May 13 2018 at 21:11):

you mean sentence

#### Mario Carneiro (May 13 2018 at 21:12):

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

#### Patrick Massot (May 13 2018 at 21:12):

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

#### Patrick Massot (May 13 2018 at 21:12):

I still think you could put those two lemmas in mathlib

#### Mario Carneiro (May 13 2018 at 21:14):

I'm doing that now

#### Mario Carneiro (May 13 2018 at 21:15):

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

Great

#### Patrick Massot (May 13 2018 at 21:18):

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

#### Patrick Massot (May 13 2018 at 21:20):

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

#### Patrick Massot (May 13 2018 at 21:20):

and generalizing all the range' lemmas to this case

#### Mario Carneiro (May 13 2018 at 22:56):

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

Last updated: May 08 2021 at 10:12 UTC