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.

def Mathlib.Linter.flexible? : Lean.Syntax → Bool

flexible? stx is true if stx is syntax for a tactic that takes a "wide" variety of inputs and modifies them in possibly unpredictable ways.

The prototypical flexible tactic is simp. The prototypical non-flexible tactic rw. simp only is also non-flexible.

Heuristics for determining goals goals that a tactic modifies 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.

def Lean.Elab.TacticInfo.goalsTargetedBy (t : TacticInfo) : List MVarId

goalsTargetedBy t are the MVarIds before the TacticInfo t that "disappear" after it. They should correspond to the goals in which the tactic t performs some action.

def Lean.Elab.TacticInfo.goalsCreatedBy (t : TacticInfo) : List MVarId

goalsCreatedBy t are the MVarIds after the TacticInfo t that were not present before. They should correspond to the goals created or changed by the tactic t.

partial def Mathlib.Linter.Flexible.extractCtxAndGoals (take? : Lean.Syntax → Bool) : Lean.Elab.InfoTree → Array (Lean.Syntax × Lean.MetavarContext × Lean.MetavarContext × List Lean.MVarId × List Lean.MVarId)

extractCtxAndGoals take? tree takes as input a function take? : Syntax → Bool and an InfoTree and returns the array of pairs (stx, mvars), where stx is a syntax node such that take? stx is true and mvars indicates the goal state:

• the context before stx
• the context after stx
• a list of metavariables closed by stx
• a list of metavariables created by stx

A typical usage is to find the goals following a simp application.

inductive Mathlib.Linter.Flexible.Stained : Type

Stained is the type of the stained locations: it can be

• a Name (typically of associated to the FVarId of a local declaration);
• the goal (⊢);
• the "wildcard" -- all the declaration in context (*).

• name : Lean.Name → Stained
• goal : Stained
• wildcard : Stained

instance Mathlib.Linter.Flexible.instReprStained : Repr Stained

instance Mathlib.Linter.Flexible.instInhabitedStained : Inhabited Stained

instance Mathlib.Linter.Flexible.instDecidableEqStained : DecidableEq Stained

instance Mathlib.Linter.Flexible.instHashableStained : Hashable Stained

instance Mathlib.Linter.Flexible.instToStringStained : ToString Stained

Converting a Stained to a String:

• a Name is represented by the corresponding string;
• goal is represented by ⊢;
• wildcard is represented by *.

partial def Mathlib.Linter.Flexible.toStained : Lean.Syntax → Std.HashSet Stained

toStained stx scans the input Syntax stx extracting identifiers and atoms, making an effort to convert them to Stained. The function is used to extract "location" information about stx: either explicit locations as in rw [] at locations or implicit ones as rw [h].

Whether or not what this function extracts really is a location will be determined by the linter using data embedded in the InfoTrees.

partial def Mathlib.Linter.Flexible.getStained (stx : Lean.Syntax) (all? : Lean.Syntax → Bool := fun (x : Lean.Syntax) => false) : Std.HashSet Stained

getStained stx expects stx to be an argument of a node of SyntaxNodeKind Lean.Parser.Tactic.location. Typically, we apply getStained to the output of getLocs.

See getStained! for a similar function.

def Mathlib.Linter.Flexible.getStained! (stx : Lean.Syntax) (all? : Lean.Syntax → Bool := fun (x : Lean.Syntax) => false) : Std.HashSet Stained

getStained! stx expects stx to be an argument of a node of SyntaxNodeKind Lean.Parser.Tactic.location. Typically, we apply getStained! to the output of getLocs.

It returns the HashSet of Stained determined by the locations in stx.

The only difference with getStained stx, is that getStained! never returns {}: if getStained stx = {}, then getStained' stx = {.goal}.

This means that tactics that do not have an explicit "at" in their syntax will be treated as acting on the main goal.

def Mathlib.Linter.Flexible.Stained.toFMVarId (mv : Lean.MVarId) (lctx : Lean.LocalContext) : Stained → Array (Lean.FVarId × Lean.MVarId)

Stained.toFMVarId mv lctx st takes a metavariable mv, a local context lctx and a Stained st and returns the array of pairs (FVarId, mv)s that lctx assigns to st (the second component is always mv):

• if st "is" a Name, returns the singleton of the FVarId with the name carried by st;
• if st is .goal, returns the singleton #[default];
• if st is .wildcard, returns the array of all the FVarIds in lctx with also default (to keep track of the goal).

def Mathlib.Linter.Flexible.stoppers : Std.HashSet Lean.Name

SyntaxNodeKinds that are mostly "formatting": mostly they are ignored because we do not want the linter to spend time on them. The nodes that they contain will be visited by the linter anyway. The nodes that follow them, though, will not be visited by the linter.

def Mathlib.Linter.Flexible.flexible : Std.HashSet Lean.Name

SyntaxNodeKinds that are allowed to follow a flexible tactic: simp, simp_all, simpa, dsimp, constructor, congr, done, rfl, omega, abel, ring, linarith, nlinarith, norm_cast, aesop, tauto, fun_prop, split, split_ifs.

def Mathlib.Linter.Flexible.usesGoal? : Lean.SyntaxNodeKind → Bool

By default, if a SyntaxNodeKind is not special-cased here, then the linter assumes that the tactic will use the goal as well: this heuristic works well with exact, refine, apply. For tactics such as cases this is not true: for these tactics, usesGoal? yields `false.

def Mathlib.Linter.Flexible.getFVarIdCandidates (fv : Lean.FVarId) (name : Lean.Name) (lctx : Lean.LocalContext) : Array Lean.FVarId

getFVarIdCandidates fv name lctx takes an input an FVarId, a Name and a LocalContext. It returns an array of guesses for a "best fit" FVarId in the given LocalContext. The first entry of the array is the input FVarId fv, if it is present. The next entry of the array is the FVarId with the given Name, if present.

Usually, the first entry of the returned array is "the best approximation" to (fv, name).

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.

def Mathlib.Linter.Flexible.persistFVars (fv : Lean.FVarId) (before after : Lean.LocalContext) : Lean.FVarId

persistFVars is one step in persisting: track a single FVarId between two LocalContexts. If an FVarId with the same unique name exists in the new context, use it. Otherwise, if an FVarId with the same userName exists in the new context, use it. If both of these fail, return default (i.e. "fail").

def Mathlib.Linter.Flexible.reallyPersist (fmvars : Array (Lean.FVarId × Lean.MVarId)) (mvs0 mvs1 : List Lean.MVarId) (ctx0 ctx1 : Lean.MetavarContext) : Array (Lean.FVarId × Lean.MVarId)

reallyPersist converts an array of pairs (fvar, mvar) to another array of the same type.

def Mathlib.Linter.Flexible.flexibleLinter : Lean.Linter

The main implementation of the flexible linter.