The "flexible" linter

The "flexible" linter makes sure that a "rigid" tactic (such as rw) does not act on the output of a "flexible" tactic (such as simp).

For example, this ensures that, if you want to use simp [...] in the middle of a proof, then you should replace simp [...] by one of

• a suffices \"expr after simp\" by simpa line;
• the output of simp? [...], so that the final code contains simp only [...];
• something else that does not involve simp!

Otherwise, the linter will complain.

Simplifying and appealing to a geometric intuition, you can imagine a (tactic) proof like a directed graph, where

• each node is a local hypothesis or a goal in some metavariable and
• two hypotheses/goals are connected by an arrow if there is a tactic that modifies the source of the arrow into the target (this does not apply well to all tactics, but it does apply to a large number of them). With this in mind, a tactic like rw [lemma] takes a very specific input and return a very predictable output. Such a tactic is "rigid". Any tactic is rigid, unless it is in flexible or stoppers. Conversely, 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,... Let's go back to the graph picture above.
• ✅️ [rigid --> flexible] A sequence rw [lemma]; simp is unlikely to break, since rw [lemma] produces the same output unless some really major change happens!
• ❌️ [flexible --> rigid] A sequence simp; rw [lemma] is instead more likely to break, since the goal after simp is subject to change by even a small, likely, modification of the simp set.
• ✅️ [flexible --> flexible] A sequence simp; linarith is also quite stable, since if linarith was able to close the goal with a "weaker" simp, it will likely still be able to close the goal with a simp that takes one further step.
• ✅️ [flexible --> stopper] Finally, a sequence simp; ring_nf is stable and, moreover, the output of ring_nf is a "normal form", which means that it is likely to produce an unchanged result, even if the initial input is different from the proof in its initial form. A stopper can be followed by a rigid tactic, "stopping" the spread of the flexible reach.

What the linter does is keeping track of nodes that are connected by flexible tactics and makes sure that only flexible or stoppers follow them. Such nodes are Stained. Whenever it reaches a stopper edge, the target node is no longer Stained and it is available again to rigid tactics.

Currently, the only tactics that "start" the bookkeeping are most forms of non-only simps. These are encoded by the flexible? predicate. Future modifications of the linter may increase the scope of the flexible? predicate and forbid a wider range of combinations.

TODO

The example

example (h : 0 = 0) : True := by
  simp at h
  assumption

should trigger the linter, since assumption uses h that has been "stained" by simp at h. However, assumption contains no syntax information for the location h, so the linter in its current form does not catch this.

Implementation notes

A large part of the code is devoted to tracking FVars and MVars between tactics.

For the FVars, this follows the following heuristic:

• if the unique name of the FVar is preserved, then we use that;
• otherwise, if the userName of the FVar is preserved, then we use that;
• if neither is preserved, we drop the ball and stop tracking the FVarId.

For the MVars, we use the information of Lean.Elab.TacticInfo.goalsBefore and Lean.Elab.TacticInfo.goalsAfter. By looking at the mvars that are either only "before" or only "after", we focus on the "active" goals. We then propagate all the FVarIds that were present in the "before" goals to the "after" goals, while leaving untouched the ones in the "inert" goals.

opaque Mathlib.Linter.linter.flexible : Lean.Option Bool

The flexible linter makes sure that "rigid" tactics do not follow "flexible" tactics.

Heuristics for determining goals that a tactic modifies and what they become

The two definitions goalsTargetedBy, goalsCreatedBy extract a list of MVarIds attempting to determine on which goals the tactic t is acting and what are the resulting modified goals. This is mostly based on the heuristic that the tactic will "change" an MVarId.

Tactics often change the name of the current MVarId, as well as the names of the FVarIds appearing in their local contexts. The function reallyPersist makes an attempt at "tracking" pairs (fvar, mvar) across a simultaneous change represented by an "old" list of MVarIds and the corresponding MetavarContext and a new one.

This arises in the context of the information encoded in the InfoTrees when processing a tactic proof.