The unused tactic linter

The unused linter makes sure that every tactic call actually changes something.

The inner workings of the linter are as follows.

The linter inspects the goals before and after each tactic execution. If they are not identical, the linter is happy. If they are identical, then the linter checks if the tactic is whitelisted. Possible reason for whitelisting are

• tactics that emit messages, such as have?, extract_goal, or says;
• tactics that are in place to assert something, such as guard;
• tactics that allow to work on a specific goal, such as on_goal;
• "flow control" tactics, such as success_if_fail and related.

The only tactic that has a bespoke criterion is swap_var: the reason is that the only change that swap_var has is to relabel the usernames of local declarations. Thus, to check that swap_var was used, so we inspect the names of all the local declarations before and after and see if there is some change.

Notable exclusions

• conv is completely ignored by the linter.

• The linter does not enter a "sequence tactic": upon finding tac <;> [tac1, tac2, ...] the linter assumes that the tactic is doing something and does not recurse into each tac1, tac2, .... This is just for lack of an implementation: it may not be hard to do this.

• The tactic does not check the discharger for linear_combination, but checks linear_combination itself. The main reason is that skip is a common discharger tactic and the linter would then always fail whenever the user explicitly chose to pass skip as a discharger tactic.

TODO

• The linter seems to be silenced by set_option ... in: maybe it should enter ins?

Implementation notes

Yet another linter copied from the unreachableTactic linter!

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

The unused tactic linter makes sure that every tactic call actually changes something.