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.

The "flexible" linter #

TODO #

Implementation notes #

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