Zulip Chat Archive

Stream: mathlib4

Topic: need help placating simpNF linter


Kevin Buzzard (Oct 30 2022 at 14:30):

In mathlib4#523 I port the parts of core Lean 3 init.data.bool.basic and init.data.bool.lemmas which didn't make the cut in Lean 4. Everything's compiling but I have a linter error, with the simpNF linter complaining that my port of the core Lean 3 lemma cond_a_a (defined here) is problematic: my port is

theorem cond_a_a.{u} {α : Type u} (b : Bool) (a : α) : cond b a a = a := by cases b <;> simp

and the linter says

 /- The `simpNF` linter reports:
SOME SIMP LEMMAS ARE NOT IN SIMP-NORMAL FORM.
see note [simp-normal form] for tips how to debug this.
https://leanprover-community.github.io/mathlib_docs/notes.html#simp-normal%20form -/
#check @Bool.cond_a_a /- Left-hand side simplifies from
  bif b then a else a
to
  match b with
| true => a
| false => a
using
  simp only [cond]
Try to change the left-hand side to the simplified term!
 -/

This doesn't make much sense to me: presumably I am not supposed to be doing a match in the statement of a lemma? (or am I?) What should I do to placate the linter? The lemma has such a horrible name and is never used explicitly in mathlib but I can quite believe that the simplifier might use it here and there.

Kevin Buzzard (Oct 30 2022 at 14:32):

PS if this lemma survives, how about cond_self as a name?

Kevin Buzzard (Oct 30 2022 at 14:37):

OK so

@[simp]
theorem cond_self.{u} {α : Type u} (b : Bool) (a : α) :
    ( match b with
      | true => a
      | false => a)
    = a := by cases b <;> simp

does placate the linter, which now then immediately complains about the next lemma involving xor.

Updated question then: should the core Lean 3 line

attribute [simp] cond bor band bnot bxor

here simply be deleted in mathlib4?

Yakov Pechersky (Oct 30 2022 at 14:38):

How about just not tagging it with @[simp]?

Yakov Pechersky (Oct 30 2022 at 14:38):

Or adding it to the nolints

Kevin Buzzard (Oct 30 2022 at 14:38):

You mean not tagging cond with simp or not tagging cond_a_a with simp?

Yakov Pechersky (Oct 30 2022 at 14:38):

Not tagging cond_a_a with simp

Kevin Buzzard (Oct 30 2022 at 14:40):

Well then the simplifier won't be able to prove it (I checked) so we might get random breakage down the line.

Mario Carneiro (Oct 30 2022 at 14:41):

It sounds like cond is marked as simp, which seems wrong

Mario Carneiro (Oct 30 2022 at 14:41):

who did that?

Kevin Buzzard (Oct 30 2022 at 14:41):

I faithfully ported the lean 3 tag to lean 4 in the same PR (see my third post above)

Mario Carneiro (Oct 30 2022 at 14:41):

marking cond as simp will make that match expression appear in any cond lemma

Mario Carneiro (Oct 30 2022 at 14:41):

ah yeah

Mario Carneiro (Oct 30 2022 at 14:42):

remove cond there

Mario Carneiro (Oct 30 2022 at 14:42):

Actually I think this needs to be fixed in lean 4, the meaning of @[simp] on definitions by pattern matching has changed

Kevin Buzzard (Oct 30 2022 at 14:43):

I'm afraid I know very little about the simplifier and in particular about any differences between lean 3 and lean 4's conventions on simp. I can confirm that deleting

attribute [simp] cond or and not xor

fixes 7 issues which the simpNF linter is whining about in that PR.

Mario Carneiro (Oct 30 2022 at 14:44):

Although putting @[simp] on recursive definitions works as you expect (they only are unfolded if one of the match arms applies), putting @[simp] on nonrecursive definitions, even if they use the equation compiler, will unfold directly to a match expression

Kevin Buzzard (Oct 30 2022 at 14:45):

@[macro_inline] def or (x y : Bool) : Bool :=
  match x with
  | true  => true
  | false => y

In Lean 3 or this has a @[simp] tag. Should it have one in Lean 4?

Kevin Buzzard (Oct 30 2022 at 14:45):

Another example linter error:

#check Bool.xor_true /- Left-hand side simplifies from
  xor b true
to
  match b, true with
| true, false => true
| false, true => true
| x, x_1 => false
using
  simp only [xor, forall_const]
Try to change the left-hand side to the simplified term!

Mario Carneiro (Oct 30 2022 at 14:46):

Right now, it will break things to do so. What I have been doing for the list definitions is to manually write the equations and mark them as simp instead

Mario Carneiro (Oct 30 2022 at 14:46):

so in this case, @[simp] theorem : or true y = true and @[simp] theorem : or false y = y

Kevin Buzzard (Oct 30 2022 at 14:46):

I've made the PR, if you like you could comment there on what I should be doing. You'll have to give me a few more clues than "manually write the equations" -- maybe do one or two for me and I'll do the rest?

Kevin Buzzard (Oct 30 2022 at 14:47):

Oh sorry, you just gave me the clues as I was writing that.

Kevin Buzzard (Oct 30 2022 at 14:47):

Thanks -- I'll give this a go.

Mario Carneiro (Oct 30 2022 at 14:49):

You can see me doing a bunch of this here, those lemmas that aren't in the attribute [simp] block are exactly the equation lemmas for nonrecursive list functions defined by pattern matching

Kevin Buzzard (Oct 30 2022 at 14:51):

gaargh do we have #print prefix yet? I don't know the names of the equation lemmas :-/

Mario Carneiro (Oct 30 2022 at 14:51):

(by the way, basically the entirety of this file is going to end up in std4 instead of mathlib4, although I will wait until it gets merged in mathlib4 first)

Mario Carneiro (Oct 30 2022 at 14:51):

The equation lemmas don't exist if you just try looking for them

Mario Carneiro (Oct 30 2022 at 14:52):

they are generated lazily

Mario Carneiro (Oct 30 2022 at 14:52):

(this is also a lean 4 behavior change)

Kevin Buzzard (Oct 30 2022 at 14:52):

so in practice this means that I should write the equation lemmas myself. I was hoping to not have to generate my own names for them but I'll give it a go.

Kevin Buzzard (Oct 30 2022 at 14:53):

Should I #align them with the lean 3 equation lemmas or will this not be necessary because it will only be the simplifier which is using them?

Mario Carneiro (Oct 30 2022 at 14:53):

TBH I think this gives some flexibility to do the equation lemmas a bit better

Mario Carneiro (Oct 30 2022 at 14:54):

like the lemmas for or can have both sides, or true y = true and or x true = true

Mario Carneiro (Oct 30 2022 at 14:54):

which is like your classic example of definitional equality being stupid

Kevin Buzzard (Oct 30 2022 at 14:55):

Aah I see, now is my change to somehow create all the correct simp lemmas as opposed to just the ones which the equation compiler generated.

Kevin Buzzard (Oct 30 2022 at 14:55):

Is xor a a = false a good simp lemma by the way?

Mario Carneiro (Oct 30 2022 at 14:55):

yeah, presumably all the equation lemmas are reasonable theorems about these functions in their own right, just give them good names

Mario Carneiro (Oct 30 2022 at 14:55):

yeah that's a simp lemma

Kevin Buzzard (Oct 30 2022 at 14:56):

It would only fire when the two inputs are syntactically equal, right?

Mario Carneiro (Oct 30 2022 at 14:56):

no, I think they need to be the same up to reducible defeq

Mario Carneiro (Oct 30 2022 at 14:57):

which is the same unfolding relation used by rw and most other tactics when you don't specifically ask for unfolding

Kevin Buzzard (Oct 30 2022 at 14:57):

OK thanks a lot! I'll see if I can placate the linter.

Kevin Buzzard (Oct 30 2022 at 15:02):

Oh many (but not all) of these are already in core. I still don't know how to check if a lemma is tagged @[simp] (especially if it was not tagged @[simp] when it was created).

Kevin Buzzard (Oct 30 2022 at 15:08):

BTW I went to a one day AI workshop on Friday and bumped into Ed Ayres; I moaned to him that I couldn't jump to definition using widgets in Lean 4 (in the sense that the arrow wasn't there like it was in Lean 3) and he told me to ctrl/command click :D . I just discovered that this trick even works with linter output even though it's "plain text" as opposed to "tactic state" :smiley: :big_smile:


Last updated: Dec 20 2023 at 11:08 UTC