Why does the flexible linter trigger here?

Stream: mathlib4

[Etienne Marion]

I discovered that there was a flexible linter, and it triggers on this example:

import Mathlib

set_option linter.flexible true

example (n : ℕ) : ((n + 2 - 1) / (2 * (n + 2)) : ℝ) = ((fun n ↦ 2⁻¹ * (n / (n + 1) : ℝ)) ∘ (fun n ↦ n + 1)) n := by
  simp
  field_simp
  ring

  ring

But I would have thought that field_simp was a flexible tactic :

a tactic like simp acts on a wide variety of inputs and returns an output that is possibly unpredictable: if later modifications adds a simp-lemma or some internals of simp changes, the output of simp may change as well. Such a tactic is flexible. Other examples are split, abel, norm_cast, ...

Am I missing something?

[Bolton Bailey]

I guess previous discussion on this here, I think there was debate on this.

[Etienne Marion]

Thanks for the pointer. I am still not sure why the linter triggers though. The debate in the thread seems to be more about whether we should allow field_simp to be followed by rigid tactics. Then again I noticed that field_simp was recently rewritten to not rely on simp anymore, which probably makes this debate kind of obsolete? But I don't see the difference between field_simp and ring_nf which would make one the latter flexible but not the former.

[Chris Henson]

Note this naming in the linter that might cause some confusion:

• docs#Mathlib.Linter.flexible? returns true for only simp and simp_all without only
• docs#Mathlib.Linter.Flexible.flexible defines what is allowed to follow a flexible tactic, including omega, linarith, etc.

Currently only simp or simp_all can "start" a check of the flexible linter. For your example it sees simp followed by field_simp, which is not included in Mathlib.Linter.Flexible.flexible, so triggers a failure.

[Chris Henson]

(perhaps these should have more distinct names like flexible? and follow_flexible?)

[Etienne Marion]

My question I think is then why isn't field_simp in docs#Mathlib.Linter.Flexible.flexible? Looking more closely at this it looks like the reason is that field_simp is not a finishing tactic nor outputting a normal form.

[Damiano Testa]

I think that for a few of the questions in this thread, the answer is simply that the linter has not been used much.

[Damiano Testa]

When the linter was first written, there were already thousands of exceptions in mathlib. Hence, there was not incentive to really flag all flexible tactics, because already flagging simp was more than enough!

[Damiano Testa]

So, the linter was added to mathlib, but off by default. This meant that it did not get feedback on bugs and improvements.

[Damiano Testa]

Specifically with field_simp, I think that the tactic itself used to be one that everyone hoped was better, so again there was little incentive to change its "flexible" status.

[Damiano Testa]

Now, with the recent improvements, it probably makes sense to make it flexible.

[Damiano Testa]

I am not sure if it is normalising enough to consider it stopping, since I have not actually looked at the implementation.

[Michael Rothgang]

See #29027

[Michael Rothgang]

I propose marking field_simp as flexible and normalising

[Michael Rothgang]

(And can write more in a week, if you like.)