Fully applied lemmas

Stream: new members

[Yakov Pechersky]

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

[Yakov Pechersky]

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

[Reid Barton]

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]

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]

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]

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]

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]

oh, id does have a simp lemma

[Yakov Pechersky]

Because there is a list.map_id'.

[Reid Barton]

I don't see it

[Yakov Pechersky]

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]

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

[Yakov Pechersky]

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]

Ah, you meant simp [list.map_id']

[Yakov Pechersky]

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

[Yakov Pechersky]

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]

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

[Yakov Pechersky]

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