simp normal form

Stream: mathlib4

[Winston Yin]

In #1135 (and often elsewhere), the linter complains that some simp lemmas' LHS can be "simplified" to some other expression. For example, normalize x can be simp-ed to x * ↑(normUnit x). But that doesn't look simpler, and it makes the lemmas a lot less meaningful. What should I do in these cases?

[Kevin Buzzard]

This is presumably mathlib4#1135

[Reid Barton]

In general, I think changing the lemma statement (as in one of the suggestions of the linter) is rarely/never the right thing to do.
I would start by investigating why the lemmas it is using to simplify the LHS are simp lemmas.

[Reid Barton]

(Changing the lemma statement would be sensible for a new lemma, but not for a lemma being ported.)

[Yury G. Kudryashov]

In this case, it's possible that coercion for a GroupWithZeroHom unfolds to something with toFun instead of CoeFun.coe.

[Reid Barton]

I don't understand how the situation wasn't the same in mathlib 3, given

@[simp] lemma normalize_apply (x : α) : normalize x = x * norm_unit x := rfl

@[simp] lemma normalize_zero : normalize (0 : α) = 0 := normalize.map_zero

and then a bunch more lemmas about normalize. How did these pass the simp_nf linter?

[Reid Barton]

In any case, I don't think normalize_apply is a good simp lemma

[Reid Barton]

And indeed normalize is really a monoid_with_zero_hom, but I don't see why that should matter...

[Yaël Dillies]

Agreed. The coercion is a projection, but here we don't want to break the normalize abstraction. This is because the bundling of normalize is an implementation detail.

[Yury G. Kudryashov]

Probably, I was wrong about coercion. About normalize_apply in mathlib3, I think that simp applied lemmas in the reverse order.

[Yury G. Kudryashov]

So, if at some level it can apply both normalize_apply and a more specific lemma about normalize, then it will apply the more specific lemma first.

[Ruben Van de Velde]

I guess we don't have the simp normal form linter in mathlib 3, but it would have fired if we'd had it?

[Reid Barton]

It definitely exists: https://github.com/leanprover-community/mathlib/blob/master/src/tactic/lint/simp.lean#L170
I don't know whether it actually runs, or works.

[Yaël Dillies]

Ruben Van de Velde said:

I guess we don't have the simp normal form linter in mathlib 3, but it would have fired if we'd had it?

Of course we do. I'm sure it bothered you (as any of us) more than once :grinning_face_with_smiling_eyes:

[Ruben Van de Velde]

My memories of mathlib 3 are clearly rapidly fading :innocent:

[Kevin Buzzard]

My understanding (from Mario explaining this to me a few weeks ago) is that the simplifier applies lemmas in what should be interpreted as a random order (which might not be preserved by the port), so if the simp set is not confluent then perhaps it's not impossible that the simp_nf linter might fire in mathlib4 but not in mathlib3?

[Reid Barton]

Is the idea that the simp_nf linter runs with the simp set that's been extended with the new lemma, so if we're lucky(?) then it will trigger on itself, rather than the other lemma triggering?

[Gabriel Ebner]

The difference is not with the linter (it works in both mathlib 3 and 4!). It is with simp itself. In Lean 3, simp tried the lemmas in the order that they were declared/imported in (or in the reverse order, I can never remember). In Lean 4, this is a bit more random (simp will still respect priorities though).

[Yury G. Kudryashov]

So, the proper fix in this case is to give the normalize_apply lemma a lower priority?

[Gabriel Ebner]

That would replicate the Lean 3 behavior, yes.

[Winston Yin]

How do I assign priority to simp lemmas in Lean4? @[simp, priority 1100] doesn't seem to work.

[Mario Carneiro]

@[simp 1100]

[Riccardo Brasca]

Does this work differently for declaration in core? Even modifying the priority in the Lean declaration the linter keeps complaining that the left hand side can be modified, by a simp lemma in core.

[Johan Commelin]

What do people think of the following workflow to systematically deal with simp_nf linting errors? (This issue is holding up several PRs by now. We should resolve it.)

1. make a copy of the statement, add ' to the name
2. in the original statement remove @[simp]
3. in the copy, simplify the LHS, to make the linter happy
4. keep the #align on the original, but don't align the copy.
5. add a -- Porting note: simp_nf copy just before the copied statement

[Riccardo Brasca]

LGTM

[Kevin Buzzard]

I've been out of the loop since before Christmas and haven't seen these new issues. Is the problem with the linter or the lemmas, or are we not sure? What are examples of PRs being held up by this issue?

[Johan Commelin]

mathlib4#1135 by Winston (who started the thread) and mathlib4#966 (data.list.basic)

[Johan Commelin]

There's probably more.

[Yaël Dillies]

Priming the names will bring you trouble, but, if you instead suffix _simp_nf or something like that, it should never conflict

[Kevin Buzzard]

OK so I've had a look at the lint errors in data.list.basic and it seems to me that there are several possibly different issues with the declarations in this file, which simpNF is objecting to. I write them here just to summarise what the main problems seem to be currently.

1) "Left-hand side simplifies". Example: List.modify_head_modify_head. The linter claims that the (lousy) move simp only [List.modifyHead] "simplifies" List.modifyHead g (List.modifyHead f l) to

match
  match l with
  | [] => []
  | a :: l => f a :: l with
| [] => []
| a :: l => g a :: l

No doubt it does. I think that this one might be easy to fix: right now we have

/-- Apply `f` to the head of the list, if it exists. -/
@[simp, inline] def modifyHead (f : α → α) : List α → List α
  | [] => []
  | a :: l => f a :: l

and in Lean 3 the simp attribute attaches simp to the equation lemmas, but in Lean 4 it also attaches simp to the declaration itself, i.e. telling the simplifier "unfold this to a match whenever you see it, please". This is in std. @Mario Carneiro should docs4#List.modifyHead be tagged @[simp] in Lean 4? Similar comments apply to List.filterMap -- this is tagged @[specialize] -- does this somehow imply @[simp]? The most confusing example is List.find? -- simpNF is claiming that List.find? p (a :: l) is being simplified to

  match p a with
| true => some a
| false => List.find? p l

but it doen't seem that List.find? is tagged with @[simp] at all? Another example is List.nthLe_repeat which mentions List.repeat; this declaration is in mathlib4 in Data.List.Basic and tagged with @[simp]. If we're tagging List.repeat with @[simp] then it is true that no simp lemma should mention List.repeat, and List.nthLe_repeat does.

2) "Left-hand side does not simplify". This we've seen before, and it might be a bug in the linter. Example:

example (l : List α) (f : α → β) :
    (l.attach.map fun (i : {i // i ∈ l}) => f i) = l.map f := by simp?

This works fine; the simplfier suggests simp only [attach_map_coe']. And yet simpNF reports on List.attach_map_coe' that the left hand side doesn't simplify. I have seen this issue before and reported it ; @Gabriel Ebner suggested that in this case I ignore the issue and just nolint simpNF. Gabriel is that also true for this example? The declaration is

@[simp]
theorem attach_map_coe' (l : List α) (f : α → β) :
    (l.attach.map fun (i : {i // i ∈ l}) => f i) = l.map f := by
  rw [attach, map_pmap]; exact pmap_eq_map _ _ _ _

3) "simp can prove this". There are two of these. For List.init_cons_of_ne_nil it doesn't actually seem to be true: the claimed proof is the funny-looking simp only [_private.Std.Data.List.Init.Lemmas.0.List.dropLast._eq_3] so I'm wondering if this is a bug in the linter. For the other one, List.indexOf_nil, it is true that simp can prove it by the end of the file. I propose not tagging it with simp.

[Mario Carneiro]

Kevin Buzzard said:

I think that this one might be easy to fix: right now we have

/-- Apply `f` to the head of the list, if it exists. -/
@[simp, inline] def modifyHead (f : α → α) : List α → List α
  | [] => []
  | a :: l => f a :: l

and in Lean 3 the simp attribute attaches simp to the equation lemmas, but in Lean 4 it also attaches simp to the declaration itself, i.e. telling the simplifier "unfold this to a match whenever you see it, please". This is in std. Mario Carneiro should docs4#List.modifyHead be tagged @[simp] in Lean 4?

No it should not. Currently @[simp] on a nonrecursive function unfolds in this unhelpful way, differently to lean 3, and the correct way to reproduce the lean 3 behavior in lean 4 is to remove @[simp] from the definition and add it to the equation lemmas (writing them if necessary).

Similar comments apply to List.filterMap -- this is tagged @[specialize] -- does this somehow imply @[simp]?

No, specialize is an instruction for the compiler, it is unrelated to simp.

The most confusing example is List.find? -- simpNF is claiming that List.find? p (a :: l) is being simplified to

  match p a with
| true => some a
| false => List.find? p l

but it doen't seem that List.find? is tagged with @[simp] at all?

Perhaps the attribute is being applied later? Or it is applied to an equation lemma.

Another example is List.nthLe_repeat which mentions List.repeat; this declaration is in mathlib4 in Data.List.Basic and tagged with @[simp]. If we're tagging List.repeat with @[simp] then it is true that no simp lemma should mention List.repeat, and List.nthLe_repeat does.

With List.repeat, I'm not sure if we should set up the simp lemmas so that repeat immediately unfolds to replicate and then replicate has all the useful lemmas, or whether repeat should not unfold unconditionally but instead it has parallel lemmas to replicate, tagged with @[simp] in the same places.

3) "simp can prove this". There are two of these. For List.init_cons_of_ne_nil it doesn't actually seem to be true: the claimed proof is the funny-looking simp only [_private.Std.Data.List.Init.Lemmas.0.List.dropLast._eq_3] so I'm wondering if this is a bug in the linter. For the other one, List.indexOf_nil, it is true that simp can prove it by the end of the file. I propose not tagging it with simp.

It seems that a private lemma got marked as a global @[simp] lemma somehow?

[Riccardo Brasca]

What about trying a partial solution and changing later if it doesn't work?

I tried to find the private lemma corresponding to _private.Std.Data.List.Init.Lemmas.0.List.dropLast._eq_3 but I didn't find it :(

[Johan Commelin]

@Mario Carneiro Does this mean that we should update std before continuing with fixing linting errors in Data.List.Basic?

[Mario Carneiro]

when a bug occurs upstream, it's best not to block the downstream on that bug unless there is no other choice. In this case you can just use attribute [-simp] and or nolint to move on in Data.List.Basic (in addition to sending a PR to std if I don't get to it in time)

[Patrick Massot]

Johan, Mario is probably busy with https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Scoped.20attribute/near/319162000 which is indeed blocking.

[Reid Barton]

attribute [-simp] only seems to apply locally.

[Yaël Dillies]

attribute [-some_attribute] means the same as Lean 3's local attribute [-some_attribute], because we can't remove attribute globally anymore.

[Reid Barton]

Here is one "fun" case.
Std has @[simp] theorem reverse_map (f : α → β) (l : List α) : (l.map f).reverse = l.reverse.map f
while Mathlib has @[simp] theorem map_reverse (f : α → β) (l : List α) : map f (reverse l) = reverse (map f l)

[Reid Barton]

I don't want to start a discussion about which lemma is "better", except to say that in the context of porting mathlib, the better lemma is the one that proofs in the rest of mathlib expect to exist.

[Reid Barton]

But it seems that attribute [-simp] is not a possible tool to work around the new lemma in Std, and in fact it cannot be worked around at all.

[Reid Barton]

A bigger issue is the stuff related to getLastD because mathlib has no lemmas about that--I created https://github.com/leanprover/std4/pull/75

[Reid Barton]

("Bigger" because in the case of reverse_map/map_reverse, one could reasonably let Std "win" and hope there are no consequences for the rest of mathlib)

[Johan Commelin]

Otoh, a confluent simp set probably needs to be consistent wrt map_<foobar> / <foobar>_map for (almost) all values of <foobar> in mathlib.

[Reid Barton]

Yeah it's not at all clear that there would be no consequences.

[Heather Macbeth]

Std is supposed to be non-opinionated, right? It seems to me that the non-opinionated choice when an attribute is debatable is for Std not to mark with that attribute, and then for a downstream library which wants the attribute to make an alias which does have the attribute.

[Heather Macbeth]

Of course, that only works for lemmas, not for definitions.

[Johan Commelin]

https://github.com/leanprover/std4/pull/76 removes @[simp] from reverse_map in Std.

[Johan Commelin]

I hope these ad-hoc developments in Std aren't going to throw many wrenches in the wheels of the porting process. Because it's quite annoying.

[Mario Carneiro]

It seems reasonable to switch from reverse_map to map_reverse here (it would be better if the other lemma was actually upstreamed though instead of just removing the simp attribute from reverse_map)

[Mario Carneiro]

I'm still unhappy about the getLastD issue, but I won't block the port on it. The obvious solution to not having enough lemmas about getLastD is to add more lemmas about getLastD

[Gabriel Ebner]

Reid Barton said:

I don't want to start a discussion about which lemma is "better", except to say that in the context of porting mathlib, the better lemma is the one that proofs in the rest of mathlib expect to exist.

I fully agree with this statement. Now is not the time to refactor, also not in std4. If std4 bites off pieces of mathlib, then those pieces need to remain mathlib-compatible until the port is done.

[Gabriel Ebner]

We can certainly do xs.getLast h = xs.getLastD after the port is done, but the std4 PR should come with a corresponding mathlib4 PR then.