simp attributes in Std

Stream: std4

[Scott Morrison]

In Std.Data.List.Init.Lemmas we add the @[simp] attribute to a lot of definitions:

attribute [simp] get reverseAux eraseIdx map join find? findSome?
  replace elem lookup drop take foldl foldr zipWith unzip range.loop enumFrom
  intersperse isPrefixOf isEqv dropLast iota mapM.loop mapA List.forM forA filterAuxM
  filterMapM.loop List.foldlM firstM anyM allM findM? findSomeM? forIn.loop forIn'.loop
  concat_eq_append append_assoc

Is this really a good idea? I thought that we had decided not to put @[simp] on declarations like these, as it makes for unpredictable unfolding.

[Scott Morrison]

The example where I've recently been annoyed by this reduced to:

set_option autoImplicit true
set_option relaxedAutoImplicit true

example : List.foldl f x (List.zip (a :: as) (b :: bs)) = f (List.foldl f x (List.zip as bs)) (a, b) := by
  simp -- simp made no progress, since we haven't added @[simp] yet
  sorry

attribute [simp] List.foldl

example : List.foldl f x (List.zip (a :: as) (b :: bs)) = f (List.foldl f x (List.zip as bs)) (a, b) := by
  simp only [List.foldl]
  -- Goal is now:
  -- ⊢ List.foldl f (f x (a, b)) (List.zipWith Prod.mk as bs) = f (List.foldl f x (List.zip as bs)) (a, b)
  -- Note that `List.zip` has been replaced with `List.zipWith Prod.mk`!
  sorry

[Scott Morrison]

It would be some work to undo these attributes, but I think it might be a good idea.

[Scott Morrison]

The work in Std is not terrible: std4#260. No idea yet how Mathlib copes or otherwise.

[Scott Morrison]

The corresponding Mathlib PR is now at #7134, but it has a sorry that I would be happy to have help with.

[Alex Keizer]

I can have a look

[Alex Keizer]

Which sorry do you mean, the one in mapIdx_eq_enum_map?

[Scott Morrison]

Awesome, thanks!

[Mario Carneiro]

Most of them seem to be bad ideas, and have been removed slowly. Specifically, putting @[simp] on a non-recursive function defined by pattern matching has different behavior in lean 3 and lean 4 and the lean 4 behavior is undesirable. Maybe some day this will be fixed, but for now we have to write all the equation lemmas we actually want to be @[simp] here by hand

[Eric Wieser]

lean4#2042 is the tracking issue for that behavior change, presumably :+1:ing it if you care is worth something