# Zulip Chat Archive

## 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))`

?

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

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'm asking the same question

#### 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`

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

: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

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

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