Can Vector.map_cons be simp

Stream: mathlib4

[Alex Keizer]

In the spirit of Chesterson's fence, is there a strong reason why Vector.map_nil is marked @[simp], but Vector.map_cons isn't?

/-- A `nil` vector maps to a `nil` vector. -/
@[simp]
theorem map_nil (f : α → β) : map f nil = nil :=
  rfl
#align vector.map_nil Vector.map_nil

/-- `map` is natural with respect to `cons`. -/
theorem map_cons (f : α → β) (a : α) : ∀ v : Vector α n, map f (cons a v) = cons (f a) (map f v)
  | ⟨_, _⟩ => rfl
#align vector.map_cons Vector.map_cons

It seems to me that you usually want the map to be unfolded if you know that it's being applied to a vector with more than one element

I noticed that neither List.map_nil nor List.map_cons is marked simp either

[Yaël Dillies]

Is docs4#List.map tagged simp?

[Yaël Dillies]

Nope, then I'm surprised Vector.map_cons, List.map_nil, List.map_cons are not tagged simp.

[Alex Keizer]

So my intuition that we want these kinds of rewrite to be simp is correct? Then I'll make that change (I'm working on a PR to add some Vector theorems)

[Yaël Dillies]

Yes, unless you see a lot of breakage when doing so (but I'm not expecting that to happen).

[Gabriel Ebner]

There are a couple of reasons why you might not want to mark something as simp. One disadvantage of marking map_cons as simp is that it duplicates the function. If you have map (f ....) [1,2,3,4] then map_cons would turn this into [f ... 1, f ... 2, f ... 3, f ... 4]. And if f` is big, then the resulting goal state can easily become huge and hard to read.

[Gabriel Ebner]

Another reason is that the simp lemma destroys structure and prevents other simp lemmas from doing something more useful (a form of nonconfluence). This is why we've removed and_assoc etc. from the simp set. Another one that annoys me greatly is Set.mem_image, which I always have to disable because what I actually want is Set.ball_image_iff.