Zulip Chat Archive

Stream: general

Topic: simp_nf linter trolling me


Kevin Buzzard (Aug 18 2020 at 11:19):

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 (Aug 18 2020 at 11:22):

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

Kevin Buzzard (Aug 18 2020 at 11:22):

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

Kevin Buzzard (Aug 18 2020 at 11:25):

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 (Aug 18 2020 at 11:26):

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

Kevin Buzzard (Aug 18 2020 at 11:26):

I don't understand what you're suggesting

Johan Commelin (Aug 18 2020 at 11:26):

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

Johan Commelin (Aug 18 2020 at 11:26):

Which is a pain

Johan Commelin (Aug 18 2020 at 11:27):

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

Johan Commelin (Aug 18 2020 at 11:27):

But I wouldn't be surprised if that breaks everything

Kevin Buzzard (Aug 18 2020 at 11:27):

OTOH is that the "correct" thing to do?

Kevin Buzzard (Aug 18 2020 at 11:32):

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

Kevin Buzzard (Aug 18 2020 at 11:32):

so indeed it breaks everything :-)

Johan Commelin (Aug 18 2020 at 11:36):

No, that's to early

Johan Commelin (Aug 18 2020 at 11:36):

You should do it after setting up the api

Johan Commelin (Aug 18 2020 at 11:36):

At the end of that file

Johan Commelin (Aug 18 2020 at 11:37):

And then it shouldn't give a SEGV


Last updated: Dec 20 2023 at 11:08 UTC