Zulip Chat Archive

Stream: general

Topic: nth_map


view this post on Zulip 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) :=

view this post on Zulip Patrick Massot (May 13 2018 at 20:59):

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

view this post on Zulip Patrick Massot (May 13 2018 at 20:59):

Am I doing something wrong?

view this post on Zulip 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

view this post on Zulip Patrick Massot (May 13 2018 at 21:01):

And I don't know how to prove it

view this post on Zulip 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)

view this post on Zulip Patrick Massot (May 13 2018 at 21:01):

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

view this post on Zulip Patrick Massot (May 13 2018 at 21:02):

ok

view this post on Zulip Patrick Massot (May 13 2018 at 21:02):

I still don't know how to prove it though

view this post on Zulip Patrick Massot (May 13 2018 at 21:03):

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

view this post on Zulip Mario Carneiro (May 13 2018 at 21:03):

I'm asking the same question

view this post on Zulip Mario Carneiro (May 13 2018 at 21:03):

I would start with nth

view this post on Zulip Mario Carneiro (May 13 2018 at 21:03):

since that avoids the proof argument stuff

view this post on Zulip Patrick Massot (May 13 2018 at 21:03):

I also thought that

view this post on Zulip Patrick Massot (May 13 2018 at 21:03):

But I couldn't even state it :disappointed:

view this post on Zulip Patrick Massot (May 13 2018 at 21:04):

Because f doesn't want an option α

view this post on Zulip 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

view this post on Zulip Mario Carneiro (May 13 2018 at 21:08):

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

view this post on Zulip Patrick Massot (May 13 2018 at 21:09):

:open_mouth:

view this post on Zulip Patrick Massot (May 13 2018 at 21:10):

I was clearly missing that option.map piece

view this post on Zulip Patrick Massot (May 13 2018 at 21:10):

but probably not only that

view this post on Zulip Mario Carneiro (May 13 2018 at 21:10):

option is a functor

view this post on Zulip Kenny Lau (May 13 2018 at 21:10):

is this proven in mathlib / Lean?

view this post on Zulip Mario Carneiro (May 13 2018 at 21:10):

yes, because every monad is a functor

view this post on Zulip Mario Carneiro (May 13 2018 at 21:11):

and option is like the very first monad you write

view this post on Zulip Kenny Lau (May 13 2018 at 21:11):

you mean sentence

view this post on Zulip Mario Carneiro (May 13 2018 at 21:12):

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

view this post on Zulip 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

view this post on Zulip Patrick Massot (May 13 2018 at 21:12):

I still think you could put those two lemmas in mathlib

view this post on Zulip Mario Carneiro (May 13 2018 at 21:14):

I'm doing that now

view this post on Zulip 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

view this post on Zulip Patrick Massot (May 13 2018 at 21:17):

Great

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Patrick Massot (May 13 2018 at 21:20):

and generalizing all the range' lemmas to this case

view this post on Zulip 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