# 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` `simp`s. 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 `FVar`s and `MVar`s between tactics.

For the `FVar`s, 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 `MVar`s, we use the information of `Lean.Elab.TacticInfo.goalsBefore` and `Lean.Elab.TacticInfo.goalsAfter`. By looking at the `mvar`s that are either only "before" or only "after", we focus on the "active" goals. We then propagate all the `FVarId`s that were present in the "before" goals to the "after" goals, while leaving untouched the ones in the "inert" goals.

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

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

source
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.

Equations

- One or more equations did not get rendered due to their size.

Instances For

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

The two definitions `goalsTargetedBy`, `goalsCreatedBy` extract a list of `MVarId`s 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`.

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

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

Equations

- t.goalsTargetedBy = List.filter (fun (x : Lean.MVarId) => decide ¬x.name ∈ List.map (fun (x : Lean.MVarId) => x.name) t.goalsAfter) t.goalsBefore

Instances For

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

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

Equations

- t.goalsCreatedBy = List.filter (fun (x : Lean.MVarId) => decide ¬x.name ∈ List.map (fun (x : Lean.MVarId) => x.name) t.goalsBefore) t.goalsAfter

Instances For

source
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.

source
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

Instances For

source
instance Mathlib.Linter.Flexible.instReprStained :
Repr Stained
Equations

- Mathlib.Linter.Flexible.instReprStained = { reprPrec := Mathlib.Linter.Flexible.instReprStained.repr }

source
def Mathlib.Linter.Flexible.instReprStained.repr :
Stained → Nat → Std.Format
Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Mathlib.Linter.Flexible.instInhabitedStained.default :
Stained
Equations

- Mathlib.Linter.Flexible.instInhabitedStained.default = Mathlib.Linter.Flexible.Stained.name default

Instances For

source
instance Mathlib.Linter.Flexible.instInhabitedStained :
Inhabited Stained
Equations

- Mathlib.Linter.Flexible.instInhabitedStained = { default := Mathlib.Linter.Flexible.instInhabitedStained.default }

source
instance Mathlib.Linter.Flexible.instDecidableEqStained :
DecidableEq Stained
Equations

- Mathlib.Linter.Flexible.instDecidableEqStained = Mathlib.Linter.Flexible.instDecidableEqStained.decEq

source
def Mathlib.Linter.Flexible.instDecidableEqStained.decEq (x✝ x✝¹ : Stained) :
Decidable (x✝ = x✝¹)
Equations

- One or more equations did not get rendered due to their size.
- Mathlib.Linter.Flexible.instDecidableEqStained.decEq (Mathlib.Linter.Flexible.Stained.name a) (Mathlib.Linter.Flexible.Stained.name b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
- Mathlib.Linter.Flexible.instDecidableEqStained.decEq (Mathlib.Linter.Flexible.Stained.name a) Mathlib.Linter.Flexible.Stained.goal = isFalse ⋯
- Mathlib.Linter.Flexible.instDecidableEqStained.decEq (Mathlib.Linter.Flexible.Stained.name a) Mathlib.Linter.Flexible.Stained.wildcard = isFalse ⋯
- Mathlib.Linter.Flexible.instDecidableEqStained.decEq Mathlib.Linter.Flexible.Stained.goal (Mathlib.Linter.Flexible.Stained.name a) = isFalse ⋯
- Mathlib.Linter.Flexible.instDecidableEqStained.decEq Mathlib.Linter.Flexible.Stained.goal Mathlib.Linter.Flexible.Stained.goal = isTrue ⋯
- Mathlib.Linter.Flexible.instDecidableEqStained.decEq Mathlib.Linter.Flexible.Stained.wildcard (Mathlib.Linter.Flexible.Stained.name a) = isFalse ⋯
- Mathlib.Linter.Flexible.instDecidableEqStained.decEq Mathlib.Linter.Flexible.Stained.wildcard Mathlib.Linter.Flexible.Stained.wildcard = isTrue ⋯

Instances For

source
instance Mathlib.Linter.Flexible.instHashableStained :
Hashable Stained
Equations

- Mathlib.Linter.Flexible.instHashableStained = { hash := Mathlib.Linter.Flexible.instHashableStained.hash }

source
def Mathlib.Linter.Flexible.instHashableStained.hash :
Stained → UInt64
Equations

- Mathlib.Linter.Flexible.instHashableStained.hash (Mathlib.Linter.Flexible.Stained.name a) = mixHash 0 (hash a)
- Mathlib.Linter.Flexible.instHashableStained.hash Mathlib.Linter.Flexible.Stained.goal = 1
- Mathlib.Linter.Flexible.instHashableStained.hash Mathlib.Linter.Flexible.Stained.wildcard = 2

Instances For

source
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 `*`.

Equations

- One or more equations did not get rendered due to their size.

source
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 `InfoTree`s.

source
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.

source
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.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
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 `FVarId`s in `lctx` with also `default` (to keep track of the `goal`).

Equations

- Mathlib.Linter.Flexible.Stained.toFMVarId mv lctx (Mathlib.Linter.Flexible.Stained.name a) = match lctx.findFromUserName? a with | none => #[] | some decl => #[(decl.fvarId, mv)]
- Mathlib.Linter.Flexible.Stained.toFMVarId mv lctx Mathlib.Linter.Flexible.Stained.goal = #[(default, mv)]
- Mathlib.Linter.Flexible.Stained.toFMVarId mv lctx Mathlib.Linter.Flexible.Stained.wildcard = Array.map (fun (x : Lean.FVarId) => (x, mv)) (lctx.getFVarIds.push default)

Instances For

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

`SyntaxNodeKind`s 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.

Equations

- One or more equations did not get rendered due to their size.

Instances For

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

`SyntaxNodeKind`s that are allowed to follow a flexible tactic: `simp`, `simp_all`, `simpa`, `dsimp`, `grind`, `constructor`, `congr`, `done`, `rfl`, `omega` and `cutsat`, `grobner` `abel` and `abel!`, `group`, `ring` and `ring!`, `module`, `field_simp` and `field`, `norm_num`, `linarith`, `nlinarith` and `nlinarith!`, `norm_cast`, `tauto`, `aesop`, `cfc_tac` (and `cfc_zero_tac` and `cfc_cont_tac`), `continuity` and `measurability`, `finiteness`, `finiteness?`, `split`, `split_ifs`.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
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.

Equations

- Mathlib.Linter.Flexible.usesGoal? `Lean.Parser.Tactic.cases = false
- Mathlib.Linter.Flexible.usesGoal? `Mathlib.Tactic.cases' = false
- Mathlib.Linter.Flexible.usesGoal? `Lean.Parser.Tactic.obtain = false
- Mathlib.Linter.Flexible.usesGoal? `Lean.Parser.Tactic.tacticHave__ = false
- Mathlib.Linter.Flexible.usesGoal? `Lean.Parser.Tactic.rcases = false
- Mathlib.Linter.Flexible.usesGoal? `Lean.Parser.Tactic.specialize = false
- Mathlib.Linter.Flexible.usesGoal? `Lean.Parser.Tactic.subst = false
- Mathlib.Linter.Flexible.usesGoal? `«tacticBy_cases_:_» = false
- Mathlib.Linter.Flexible.usesGoal? `Lean.Parser.Tactic.induction = false
- Mathlib.Linter.Flexible.usesGoal? x✝ = true

Instances For

source
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)`.

Equations

- Mathlib.Linter.Flexible.getFVarIdCandidates fv name lctx = Array.map (fun (x : Lean.LocalDecl) => x.fvarId) #[lctx.find? fv, lctx.findFromUserName? name].reduceOption

Instances For

Tactics often change the name of the current `MVarId`, as well as the names of the `FVarId`s 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 `MVarId`s and the corresponding `MetavarContext` and a new one.

This arises in the context of the information encoded in the `InfoTree`s when processing a tactic proof.

source
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 `LocalContext`s. 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").

Equations

- Mathlib.Linter.Flexible.persistFVars fv before after = (Mathlib.Linter.Flexible.getFVarIdCandidates fv ((before.find? fv).getD default).userName after).getD 0 default

Instances For

source
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.

Equations

- One or more equations did not get rendered due to their size.

Instances For

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

The main implementation of the flexible linter.

Equations

- One or more equations did not get rendered due to their size.

Instances For