simp attributes in Std

Stream: batteries

[Kim 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.

[Kim 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

[Kim Morrison]

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

[Kim Morrison]

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

[Kim 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?

[Kim 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

[Yury G. Kudryashov]

Unrelated to previously discussed @[simp] attributes: @Mario Carneiro, what do you think about adding @[simp] to docs#List.length_pos and docs#List.drop_eq_nil_iff_le (and possibly changing assumptions length l > 0 to l ≠ [] in other lemmas)?

[Mario Carneiro]

That sounds okay to me, although the proof is in the quality of the mathlib bump PR

[Yury G. Kudryashov]

Why docs#List.headD_eq_head? is a simp lemma in this direction?

[Yury G. Kudryashov]

With this lemma, we can never have headD in a simp normal form. In fact, I would reverse LHS with RHS.

[Mario Carneiro]

It means headD is never a simp normal form, so theorems don't have to be stated about it

[Mario Carneiro]

There is a bit of combinatorial multiplication of foo? / foo! / foo / fooD / fooI definitions for lots of partial functions

[Mario Carneiro]

and we don't want to have to write out the foo? API 4-5 times

[Yury G. Kudryashov]

Is there a uniform rule that applies to all foos?

[Yury G. Kudryashov]

BTW, fooI is usually defeq foo!

[Mario Carneiro]

usually fooD a = foo?.getD a and fooI = foo?.getD default

[Mario Carneiro]

and foo! and fooI are defeq

[Mario Carneiro]

the relationship between foo? and foo (the latter being a proof-taking function) depends on how the hypothesis is stated

[Yury G. Kudryashov]

Is there a rule about simp-normal form that applies to many foos?

[Mario Carneiro]

I'm not sure we have a consistent rule in all cases, but I think it is reasonable to try to avoid fooD in favor of Option.getD

[Yury G. Kudryashov]

E.g., we simplify headD but docs#List.getD_eq_get? is not a simp lemma.

[Mario Carneiro]

maybe it should be?

[Yury G. Kudryashov]

It's in core. I have no opinion here, other than predictable simp-normal forms are better than unpredictable.

[Mario Carneiro]

I don't think the FRO will disagree on that point

[Yury G. Kudryashov]

On "predictable is better than unpredictable" or "fooD vs Option.getD (foo? ..)"?

[Mario Carneiro]

The former. The latter I don't expect people to have much opinion on but you can use the former as a justification for it

[Yury G. Kudryashov]

@Kim Morrison I replied in std4#769

[Yury G. Kudryashov]

I won't be able to do anything Std/Mathlib-related in the next 10-12h.