Simp priority

Stream: mathlib4

[Antoine Chambert-Loir]

docs#Polynomial.cardPowDegree_zero has a simp attribute.
After the compilation of #5942, the simp_NF linter complained that it could be solved by simp [@map_zero].

• The comment hinted at a page which seems to be relevant for mathlib3.
  The syntax seems to have changed, the attribute priority does not seem to work here, while the syntax @[simp <number>] theorem … works.

• I am not sure I understood the explanations there. IIUC, the linter notes that Lean doesn't need that new lemma, because docs#map_zero applies, and is detected before docs#Polynomial.cardPowDegree_zero.
  This lemma is more specific than docs#map_zero, hence the documentation suggests to put it before, or with a smaller priority. But what happened in my case is that priority 1001 made Lean find it, while 1000 or lower didn't…

[Yury G. Kudryashov]

Does simp prove this lemma?

[Yury G. Kudryashov]

Why #5942 changes anything about this lemma?

[Yury G. Kudryashov]

Why do you want @[simp] on this lemma?

[Antoine Chambert-Loir]

[edited]
It's not that I want. This lemma was there in mathlib3, with simp, and during the port to mathlib4, a note indicated that simp proves it, while the proof given was if_pos rfl. I had to fix something in this file , I don't remember what, and I probably mistakenly added the simp lemma, changed the proof to use simp, and now I have to fix things back.

In this case, the natural thing to do is to remove the @[simp]attribute.

But the initial question remains.

[Yury G. Kudryashov]

In mathlib3, simp gave higher priority to lemmas that appear later in the source. So, simp_nf linter didn't catch the fact that this lemma is in fact map_zero.

[Yury G. Kudryashov]

In fact, Lean doesn't need this lemma and we can drop it completely.

[Antoine Chambert-Loir]

This is the kind of rfl lemma that people like me need until they realize that map_zero rules.

[Yury G. Kudryashov]

We leave rfl lemmas because dsimp can use them. This is not a rfl lemma...

[Antoine Chambert-Loir]

but the proof is rfl…

[Yury G. Kudryashov]

Is it? AFAICS, it was if_pos rfl

[Yury G. Kudryashov]

If it's rfl, then you can use @[simp, nolint simpNF]

[Antoine Chambert-Loir]

This surprises me, because it was if_pow rfl, and when I restored that, Lean didn't compile, and rfl did the job.

[Ruben Van de Velde]

Oh I see, cardPowDegree is defined as fun p => if p = 0 then 0 else (Fintype.card Fq : ℤ) ^ p.natDegree, which used classical equality, but after your change, it's now using your DecidableEq instance

[Ruben Van de Velde]

(Your PR doesn't seem to describe the motivation for the change.)

[Antoine Chambert-Loir]

I updated the header of the PR. Is it enough?