Non-terminal simps in `Mathlib.Computability.PartrecCode`

Stream: mathlib4

[Kim Morrison]

The proofs in Mathlib.Computability.PartrecCode contain some non-terminal simps.

I just had to make some modifications in these proofs to adapt to a potential change in Lean. Fortunately I managed to work it out fairly quickly, but nevertheless the non-terminal simps made it marginally harder.

Could I please request an upgrade here?

[Kim Morrison]

Pinging @Mario Carneiro as the original author of this code, but hopefully this doesn't need to be solely his problem.

[Mario Carneiro]

is there a linter which flags the offenses?

[Michael Rothgang]

The python style linter for non-terminal simps is apparently too simple-minded - would @Damiano Testa's "flexible tactics linter" help here? (I could imagine it does, but they are the author, so let's hear from them.)

[Damiano Testa]

The linter "works" in the sense that it does flag "rigid tactics" following "flexible tactics". One of the reasons why I stopped pushing for it, though, is that I did not really find a good way to silence the linter: most of the times, neither simp only [...], nor suffices ... feels like an improvement.

[Mario Carneiro]

#13791

[Mario Carneiro]

@Damiano Testa said:

The linter "works" in the sense that it does flag "rigid tactics" following "flexible tactics". One of the reasons why I stopped pushing for it, though, is that I did not really find a good way to silence the linter: most of the times, neither simp only [...], nor suffices ... feels like an improvement.

One easy thing that would help here would be to add the linter, but disable it by default. Then it would be possible to enable it locally for cleanups like this

[Damiano Testa]

Ok, I can certainly do that, though I'll have to bump it: I may not have much lean time for a week or two, since it is end of term and I'll be busy with exams.

[Damiano Testa]

I think that the relevant PR is #11821.

[Damiano Testa]

I updated #11821 and marked it as awaiting-review.

The PR is over 700 lines long, but half of it is tests, the linter is documented and verbose.

The extensive tests show what the linter flags and what it does not flag -- they are really intended to be close to a specification of the linter and of which tactics are considered flexible (by default, a new tactic is rigid, not flexible).

Pro: As I mentioned above, I think that in terms of flagging rigid tactics that follow flexible ones, it does a good job.

Cons: I also think that the code could probably be improved upon and I suspect that it does not perform very well.

Conclusion: If the intention is to leave it silent (as it is now in the PR) and only activate it locally, it is probably in a pretty good state!

[Damiano Testa]

For the specific case in question, Mathlib.Computability.PartrecCode, the output of lake build with the linter turned on is too long for Zulip, but this is how it starts:

⚠ [678/678] Replayed Mathlib.Computability.PartrecCode
warning: ././././Mathlib/Computability/PartrecCode.lean:70:4: 'simp at this' stains 'this'...
note: this linter can be disabled with `set_option linter.flexible false`
info: ././././Mathlib/Computability/PartrecCode.lean:70:18: ... and 'exact this' uses 'this'!
warning: ././././Mathlib/Computability/PartrecCode.lean:341:2: 'simp' stains '⊢'...
note: this linter can be disabled with `set_option linter.flexible false`
info: ././././Mathlib/Computability/PartrecCode.lean:342:2: ... and 'iterate 4 cases' n with n; · simp [ofNatCode_eq, ofNatCode]; rfl' uses '⊢'!
warning: ././././Mathlib/Computability/PartrecCode.lean:341:2: 'simp' stains '⊢'...
note: this linter can be disabled with `set_option linter.flexible false`
info: ././././Mathlib/Computability/PartrecCode.lean:343:17: ... and 'rw [List.length_map, List.length_range]' uses '⊢'!
warning: ././././Mathlib/Computability/PartrecCode.lean:341:2: 'simp' stains '⊢'...
note: this linter can be disabled with `set_option linter.flexible false`
info: ././././Mathlib/Computability/PartrecCode.lean:344:2: ... and 'let m := n.div2.div2' uses '⊢'!
warning: ././././Mathlib/Computability/PartrecCode.lean:341:2: 'simp' stains '⊢'...
note: this linter can be disabled with `set_option linter.flexible false`
info: ././././Mathlib/Computability/PartrecCode.lean:345:2: ... and 'show
  G₁ ((a, (List.range (n + 4)).map fun n => F a (ofNat Code n)), n, m) = some (F a (ofNat Code (n + 4)))' uses '⊢'!
warning: ././././Mathlib/Computability/PartrecCode.lean:341:2: 'simp' stains '⊢'...
note: this linter can be disabled with `set_option linter.flexible false`
info: ././././Mathlib/Computability/PartrecCode.lean:355:2: ... and 'rw [show ofNat Code (n + 4) = ofNatCode (n + 4) from rfl]' uses '⊢'!
warning: ././././Mathlib/Computability/PartrecCode.lean:454:2: 'simp' stains '⊢'...
note: this linter can be disabled with `set_option linter.flexible false`

... 358 lines of output

Build completed successfully.

The linter warns at the first flexible tactic that is followed by a rigid one and then informs all the following rigid tactics, until the next flexible tactic appears. Essentially, it follows the proof tree and reports all rigid nodes that have a flexible ancestor.

[Yaël Dillies]

Damiano Testa said:

I updated #11821 and marked it as awaiting-review.

What about the linter output that I asked in https://github.com/leanprover-community/mathlib4/pull/11821#issuecomment-2152119886 ?

[Damiano Testa]

Yaël, #13812 sets the default of the linter to true and imports it in .Tactic.Linter.

[Yaël Dillies]

The output looks very reasonable

[Damiano Testa]

I'm glad you like it! :smile: