need help placating simpNF linter

Stream: mathlib4

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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]

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

[Yakov Pechersky]

Or adding it to the nolints

[Kevin Buzzard]

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

[Yakov Pechersky]

Not tagging cond_a_a with simp

[Kevin Buzzard]

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

[Mario Carneiro]

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

[Mario Carneiro]

who did that?

[Kevin Buzzard]

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

[Mario Carneiro]

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

[Mario Carneiro]

ah yeah

[Mario Carneiro]

remove cond there

[Mario Carneiro]

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

[Kevin Buzzard]

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]

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]

@[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]

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]

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]

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

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

Thanks -- I'll give this a go.

[Mario Carneiro]

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]

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

[Mario Carneiro]

(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]

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

[Mario Carneiro]

they are generated lazily

[Mario Carneiro]

(this is also a lean 4 behavior change)

[Kevin Buzzard]

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]

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]

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

[Mario Carneiro]

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

[Mario Carneiro]

which is like your classic example of definitional equality being stupid

[Kevin Buzzard]

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]

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

[Mario Carneiro]

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

[Mario Carneiro]

yeah that's a simp lemma

[Kevin Buzzard]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

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: