Non-terminal simps

Stream: mathlib4

[Shuhao Song]

In my pull request https://github.com/leanprover-community/mathlib4/pull/15536, the reviewer commented about "non-terminal simp". I wonder which tactic sequence will be considered as non-terminal simp; some of non-terminal simps would not be checked by script/lint-style.sh. Will simp; omega, simp at hl; simp, simp at hl; simp [hl] be considered as non-terminal simp?

[Notification Bot]

A message was moved here from #mathlib4 > New syntax for weak options by Shuhao Song.

[Eric Wieser]

I think simp at hl; simp [hl] can usually be written simpa using hl?

[Kim Morrison]

simp; omega is allowed, I think, although perhaps if you have reason to suspect fragility it could still be avoided. It is very satisfying when it works, of course. :-)

[Jireh Loreaux]

Also, lint-style.sh won't check for non-terminal simp at all.

[Yury G. Kudryashov]

The issue with simp at hl; simp [hl] is that we may add a lemma in the future that changes the result of simp at hl.

[Yury G. Kudryashov]

Though simp_all does roughly the same and is allowed.

[Jireh Loreaux]

we don't allow simp_all as non-closing, do we?

[Yury G. Kudryashov]

• simp at hl; simp [hl] (this pair closes the goal) has a non-terminal simp and I'm not sure if this version is allowed
• simp_all (closing the goal) is allowed but is roughly equivalent to the previous one.

[Damiano Testa]

For what it's worth, the "flexible" linter would allow this sequence of tactics: it considers a target (hypothesis or goal) "stained" if a tactic like simp acted on it and then only allows stained targets to be targets of simp-like tactics. The prototypical non-simp-like tactic is rw, but, by default, every tactic is non-simp-like, unless explicitly mentioned otherwise.

[Damiano Testa]

Simp-like tactics are called flexible (and include also omega, aesop, tauto), the other tactics are called rigid (by the linter).