simp_nf linter trolling me

Stream: general

[Kevin Buzzard]

The simp normal form linter is complaining about my code.

The issue is on the with-zero-stuff branch of mathlib, which is compiling. The complaint is about this lemma: coe_mul and the linter output is

/- The `simp_nf` 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
: -/
#print with_one.coe_mul /- Left-hand side simplifies from
  ↑(a * b)
to
  ↑a * ↑b
using
  [with_zero.coe_mul]
Try to change the left-hand side to the simplified term!
 -/

I don't know if I'm confused or the linter is confused or both. This is the file where with_one and with_zero are defined, and they're both defined to be option, but I would not expect simp to be able to see through this definition. Furthermore, with_zero.coe_mul is defined on line 136, after with_one.coe_mul. To my surprise, it is true that if I try simp in the proof of with_zero.coe_mul then it simplifies ↑(a * b) : with_zero α to ↑a * ↑b : with_one α (and then fails to close the goal with refl). I don't know what to do here. simp trace says it's doing exactly what the linter is warning me about -- just changing a with_zero to a with_one. I don't want the simplifier to do this, I don't think. It's breaking some kind of abstraction barrier as far as I can see. What can I do here?

[Johan Commelin]

@Kevin Buzzard Did you see my remark on the PR page?

[Kevin Buzzard]

Aah! I knew I'd asked about this somewhere last night when I was tired :-)

[Kevin Buzzard]

So another linter complaint is

with_zero.coe_le_coe /- simp can prove this:
  by simp only [with_bot.coe_le_coe]

This is a bit more excusable because at least you can imagine a situation where zero = bot. But zero = one is kind of inexcusable. So you suggest to mark them locally irreducible -- but this is basically just to trick the linter, right?

[Johan Commelin]

no, I because then the problem will show up in other files

[Kevin Buzzard]

I don't understand what you're suggesting

[Johan Commelin]

And you will get \u up arrows that are sometimes doing a with_one coe, and sometimes a with_zero coe

[Johan Commelin]

Which is a pain

[Johan Commelin]

So the only solution I know, is to make them globally irreducible.

[Johan Commelin]

But I wouldn't be surprised if that breaks everything

[Kevin Buzzard]

OTOH is that the "correct" thing to do?

[Kevin Buzzard]

aargh adding line attribute [irreducible] with_one on line 32 of algebra.group.with_one gives me a SEGV :-/

[Kevin Buzzard]

so indeed it breaks everything :-)

[Johan Commelin]

No, that's to early

[Johan Commelin]

You should do it after setting up the api

[Johan Commelin]

At the end of that file

[Johan Commelin]

And then it shouldn't give a SEGV