Zulip Chat Archive

Stream: new members

Topic: Fully applied lemmas


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?

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.

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.

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.

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]

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?

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)

Reid Barton (Nov 25 2020 at 00:19):

oh, id does have a simp lemma

Yakov Pechersky (Nov 25 2020 at 00:19):

Because there is a list.map_id'.

Reid Barton (Nov 25 2020 at 00:20):

I don't see it

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'

Reid Barton (Nov 25 2020 at 00:20):

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

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

Yakov Pechersky (Nov 25 2020 at 00:23):

Ah, you meant simp [list.map_id']

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]

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.

Reid Barton (Nov 25 2020 at 00:26):

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

Yakov Pechersky (Nov 25 2020 at 00:28):

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


Last updated: Dec 20 2023 at 11:08 UTC