Zulip Chat Archive

Stream: mathlib4

Topic: simp normal form


Winston Yin (Dec 27 2022 at 00:10):

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 (Dec 27 2022 at 00:27):

This is presumably mathlib4#1135

Reid Barton (Dec 27 2022 at 08:00):

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 (Dec 27 2022 at 08:00):

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

Yury G. Kudryashov (Dec 27 2022 at 08:05):

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

Reid Barton (Dec 27 2022 at 08:13):

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 (Dec 27 2022 at 08:13):

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

Reid Barton (Dec 27 2022 at 08:15):

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

Yaël Dillies (Dec 27 2022 at 08:16):

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 (Dec 27 2022 at 08:18):

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

Yury G. Kudryashov (Dec 27 2022 at 08:19):

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 (Dec 27 2022 at 08:25):

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 (Dec 27 2022 at 08:26):

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 (Dec 27 2022 at 08:27):

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 (Dec 27 2022 at 08:47):

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

Kevin Buzzard (Dec 27 2022 at 13:57):

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 (Dec 27 2022 at 16:32):

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 (Dec 27 2022 at 16:44):

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 (Dec 27 2022 at 17:05):

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

Gabriel Ebner (Dec 27 2022 at 17:07):

That would replicate the Lean 3 behavior, yes.

Winston Yin (Dec 27 2022 at 20:38):

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

Mario Carneiro (Dec 27 2022 at 20:47):

@[simp 1100]

Riccardo Brasca (Dec 28 2022 at 13:28):

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 (Dec 29 2022 at 11:13):

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 (Dec 29 2022 at 11:28):

LGTM

Kevin Buzzard (Dec 29 2022 at 11:33):

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 (Dec 29 2022 at 11:37):

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

Johan Commelin (Dec 29 2022 at 11:37):

There's probably more.

Yaël Dillies (Dec 29 2022 at 11:57):

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

Kevin Buzzard (Dec 29 2022 at 18:37):

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 (Dec 29 2022 at 18:56):

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 (Dec 31 2022 at 10:36):

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 (Jan 03 2023 at 14:10):

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

Mario Carneiro (Jan 03 2023 at 21:35):

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 (Jan 03 2023 at 21:37):

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 (Jan 04 2023 at 15:44):

attribute [-simp] only seems to apply locally.

Yaël Dillies (Jan 04 2023 at 15:45):

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

Reid Barton (Jan 04 2023 at 15:45):

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 (Jan 04 2023 at 15:46):

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 (Jan 04 2023 at 15:47):

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 (Jan 04 2023 at 16:02):

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 (Jan 04 2023 at 16:05):

("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 (Jan 04 2023 at 16:10):

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 (Jan 04 2023 at 16:10):

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

Heather Macbeth (Jan 04 2023 at 16:19):

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 (Jan 04 2023 at 16:24):

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

Johan Commelin (Jan 04 2023 at 17:30):

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

Johan Commelin (Jan 04 2023 at 20:54):

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 (Jan 04 2023 at 21:38):

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 (Jan 04 2023 at 21:40):

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 (Jan 04 2023 at 22:28):

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 (Jan 04 2023 at 22:29):

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.


Last updated: Dec 20 2023 at 11:08 UTC