list.map_id' with weaker hypothesis

Stream: Is there code for X?

[Kayla Thomas]

Is there an existing version of docs#list.map_id' with a weaker hypothesis? Something like:

example
  {α : Type}
  {f : α → α}
  (l : list α)
  (h : ∀ (x : α), x ∈ l → f x = x) :
  list.map f l = l := sorry

I can prove it, just curious why I didn't see it already I guess.

[Junyan Xu]

It follows relatively easily from docs#list.map_congr and docs#list.map_id; maybe that's why.

[Kayla Thomas]

Hmm. I wonder if there is an advantage to having list.map_id' be what it is instead of the above version.

[Kayla Thomas]

Since I think the current version follows from the above version?

[Junyan Xu]

Indeed, if you replace docs#list.map_id' by your more general version, it should be straightforward to fix anything that breaks. But the file it's in was already ported ...

[Junyan Xu]

I traced docs#list.map_id' back to this commit by the father of Lean. It was moved to mathlib from Lean core in 2017.

[Eric Wieser]

Kayla Thomas said:

Hmm. I wonder if there is an advantage to having list.map_id' be what it is instead of the above version.

It doesn't scale well to add another lemma to mathlib for every existing lemma about map combined with congr

[Kayla Thomas]

I was thinking along the lines of whether the existing list.map_id' could be replaced.

[Eric Wieser]

Ah sorry, I should have clicked list.map_id', it doesn't have the statement I expected. I think your version would probably be good as a replacement. Is docs4#List.map_id' the same?

[Eric Wieser]

Although I think a better statement might be list.map_eq_self_iff : List.map f l = l ↔ ∀ (x : α), x ∈ l → f x = x

[Kayla Thomas]

No problem. Yes, they look the same.

[Eric Wieser]

Note that port-status#data/list/basic says the file is not only ported, but also out of sync

[Eric Wieser]

So it might not be a good idea to add any more changes in mathlib3 until we're resynced the existing changes

[Kayla Thomas]

Ok.

[Floris van Doorn]

Eric Wieser said:

Although I think a better statement might be list.map_eq_self_iff : List.map f l = l ↔ ∀ (x : α), x ∈ l → f x = x

Which is very similar to docs#list.map_eq_map_iff

[Kayla Thomas]

Is it odd that there is both docs#list.map_congr and docs#list.map_eq_map_iff ?

[Kayla Thomas]

Maybe docs#list.map_congr could be removed, since it appears to be just one direction of docs#list.map_eq_map_iff ?

[Kayla Thomas]

Just to note, I've never tried to make a PR to mathlib or used lean4 much.

[Floris van Doorn]

list.map_congr could be removed, but I think the status quo is fine. list.map_congr might be easier to find by guessing the name. Note also that these two lemmas are consecutive in the file, and that list.map_eq_map_iff uses list.map_congr in its proof, so not much is gained by removing list.map_congr