Zulip Chat Archive

Stream: new members

Topic: Fully applied lemmas


view this post on Zulip Yakov Pechersky (Nov 24 2020 at 23:45):

Why are lemmas like list.map_id stated in fully applied form, as opposed to using funext?

view this post on Zulip Yakov Pechersky (Nov 24 2020 at 23:46):

If I have list.map (list.map id) l for some l : list (list a), that doesn't simplify currently.

view this post on Zulip Reid Barton (Nov 25 2020 at 00:01):

Because the normal thing to do with a function is apply it to something, and often the right hand side should be simplified more after being applied to something.

view this post on Zulip Reid Barton (Nov 25 2020 at 00:02):

Sometimes we do have both versions, as in https://github.com/leanprover-community/mathlib/blob/7e66984cb1cd5b4262d8dd0ee775cd212e56c9e7/src/data/equiv/basic.lean#L180 and following.

view this post on Zulip Yakov Pechersky (Nov 25 2020 at 00:11):

I understand -- but what would be the downside of providing a @[simp] lemma list.map_id'' : list.map (@id a) = id also/instead? The current list.map_id does two simplifcation steps, [list.map_id'', id.def]

view this post on Zulip Yakov Pechersky (Nov 25 2020 at 00:12):

In other words, should a "lawful" map lemma be stated in applied or not-applied form? Should list.map_id'' be added to mathlib?

view this post on Zulip Reid Barton (Nov 25 2020 at 00:18):

Seems like a reasonable addition, though it would be nonconfluent if marked simp (and I'm not sure why it needs two 's)

view this post on Zulip Reid Barton (Nov 25 2020 at 00:19):

oh, id does have a simp lemma

view this post on Zulip Yakov Pechersky (Nov 25 2020 at 00:19):

Because there is a list.map_id'.

view this post on Zulip Reid Barton (Nov 25 2020 at 00:20):

I don't see it

view this post on Zulip Yakov Pechersky (Nov 25 2020 at 00:20):

theorem map_id' {f : α  α} (h :  x, f x = x) (l : list α) : map f l = l :=
by induction l; [refl, simp only [*, map]]; split; refl

docs#list.map_id'

view this post on Zulip Reid Barton (Nov 25 2020 at 00:20):

oh, it's somewhere else. In fact, doesn't it solve your problem?

view this post on Zulip Yakov Pechersky (Nov 25 2020 at 00:23):

import data.list

example {α : Type*} {l : list (list α)} : list.map (list.map id) l = l :=
by simp
/-
simplify tactic failed to simplify
state:
α : Type ?,
l : list (list α)
⊢ list.map (list.map id) l = l
-/

@[simp] lemma list.map_id'' {α : Type*} : list.map (@id α) = id :=
by { funext, exact list.map_id _ }

example {α : Type*} {l : list (list α)} : list.map (list.map id) l = l :=
by simp
-- that is now fine

view this post on Zulip Yakov Pechersky (Nov 25 2020 at 00:23):

Ah, you meant simp [list.map_id']

view this post on Zulip Yakov Pechersky (Nov 25 2020 at 00:24):

I see. Well, I guess then I'm just surprised list.map_id' isn't tagged with @[simp]

view this post on Zulip Yakov Pechersky (Nov 25 2020 at 00:25):

If there's no reason not to tag it, that's a simple change. If there is a reason not to tag it, just trying to understand what the reason would be.

view this post on Zulip Reid Barton (Nov 25 2020 at 00:26):

Your map_id'' seems like a better candidate for a simp lemma

view this post on Zulip Yakov Pechersky (Nov 25 2020 at 00:28):

:frown: is_lawful_functor.id_map is also in fully applied form


Last updated: May 10 2021 at 18:22 UTC