Unused Decidable Instances linter

Stream: mathlib4

[Thomas Murrills]

I've ported mathlib3's decidable_classical linter as a syntax linter in #31142, and addressed the remaining 37 violations in a non-dependent PR (#31831). #31747 turns the linter on by default, and is now green. :)

After I did the bulk of porting it, I was made aware that there's an environment linter that's been sitting for a while at #10235! :) @Yury G. Kudryashov has used that to valiantly clean up a bunch of violations already, even though #10235 was never merged, which is why there were so few to catch here. Hopefully a syntax linter that runs interactively (as opposed to only in CI or during #lint, as an env_linter does) is useful enough that the unintentional rewrite was worth it. :)

The backend is also set up to be similarly extensible to allow Fintype, Encodable, etc. linters (e.g. #31794)

I'd love to hear feedback here, especially on

• the message (formatting; is the index of the parameter useful or noise?; etc.)
• behavior (is it enough to lint theorem-kind decls which are user-written, or should we also have an env_linter? I believe it's enough, but I'm interested in edge cases.)
• the name: I'm proposing naming it unusedDecidableInType instead of decidableClassical, so that every linter of this form can be named according to the same pattern (unused<_>InType)
• anything else! :)

Note on planned future improvements: I've opened a couple of dependent PRs that improve the logging location somewhat (to the type signature, but not yet to the binders), and eventually it would be nice to have a try-this suggestion. But try-this suggestions turn out to both require a bunch more API and be quite cursed, so I'm holding off on creating an interactive suggestion for now.

[Yury G. Kudryashov]

The main reason my version didn't get merged back then was bad performance. Could you please compare how fast is your linter compared to mine?

[Thomas Murrills]

Sure! The bench results on #31747, with it turned on everywhere, show no significant changes.

I use a bvar approach to detect dependence instead of telescoping and collecting fvars; this is what helps it be fast, I believe.

Linting wall clock time seems to increase by 2.5%, but it doesn't flag it as significant. If we want to try to get this down further: I wonder if the infotree traversal could be made faster. Though, I'm not sure how much wall clock time fluctuates anyway in these results.

I can't quite find bench results for yours. How did you detect performance issues?

[Yury G. Kudryashov]

AFAIR, it increased the linting time by a "significant" amount, but this increase can be not that significant as a percentage of the total runtime.

[Thomas Murrills]

Hmm, yeah—this one is of course also relative to a different linting process/pool of linters by virtue of being an interactive syntax linter instead of an environment linter, and I'm not sure how that affects the metrics here.

[Yury G. Kudryashov]

But I don't remember the details. I can try to resurrect that PR just to (a) rerun !bench; (b) see if it finds anything on top of #31831

[Thomas Murrills]

(b) is very useful information! I currently don't lint anything besides theorem-kind decls (e.g. not Prop-typed defs, structures, etc.) and only lint declarations with bodies. Would be great to see if that's enough.

Note also that #31747 exempts Mathlib.Data.Fintype.Quotients, Mathlib.Logic.Encodable.Basic, and a definition in Mathlib.Computability.Halting, since these are meant to be constructive—so I would expect you to find violations in these modules when re-running.

[Yury G. Kudryashov]

I'll try to do it tomorrow.

[Thomas Murrills]

By the way, if it helps, I don't mind doing this. :) It looks like all that needs to be done is to copy the file over into current master and add some module incantations.

[Thomas Murrills]

Gave it a shot just to see if it was easy, and it was! :) CI is running at the draft PR #31920.

[Thomas Murrills]

Okay! Results are in. Here's a breakdown, cleaned up and made readable.

env_linter results, commentated

/- The `decidableClassical` linter reports:
USES OF `Decidable` SHOULD BE REPLACED WITH `classical` IN THE PROOF. -/

Syntax linter not imported

The following do not import Mathlib.Tactic.Linter, so the syntax linter is not available. But if we do import it:

:document: Mathlib.Logic.Basic

dec_em argument 2 inst✝ : Decidable p
@Not.decidable_imp_symm argument 3 inst✝ : Decidable a

aliases for Decidable.em and Decidable.not_imp_symm: aliases are not picked up by the syntax linter, and the declarations they are aliases for start with Decidable, which exempts them

dec_em' argument 2 inst✝ : Decidable p

caught by syntax linter as expected

:document: Mathlib.Order.Heyting.Regular

Heyting.isRegular_of_decidable argument 2 inst✝ : Decidable p

caught by syntax linter as expected

Already caught, exempted for constructive reasons

:document: Mathlib.Logic.Encodable.Basic

@Encodable.axiom_of_choice argument 5 inst✝ : (x : α) → (y : β x) → Decidable (R x y)
@Encodable.skolem argument 5 inst✝ : (x : α) → (y : β x) → Decidable (P x y)

:document: Mathlib.Computability.Halting

@ComputablePred.computable_iff_re_compl_re argument 4 inst✝ : DecidablePred p

:document: Mathlib.Data.Fintype.Quotient

@Quotient.list_ind argument 2 inst✝ : DecidableEq ι
@Quotient.ind_fintype_pi argument 3 inst✝ : DecidableEq ι
@Quotient.induction_on_fintype_pi argument 3 inst✝ : DecidableEq ι

False positives from env_linter:

:document: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks

@CategoryTheory.Limits.WidePullbackShape.instDecidableEqHom.decEq argument 4 inst✝ : DecidableEq J✝
@CategoryTheory.Limits.WidePushoutShape.instDecidableEqHom.decEq argument 4 inst✝ : DecidableEq J✝

Both are DecidableEq instances created by deriving, e.g.

/-- The type of arrows for the shape indexing a wide pushout. -/
inductive Hom : WidePushoutShape J → WidePushoutShape J → Type w
  | id : ∀ X, Hom X X
  | init : ∀ j : J, Hom none (some j)
  deriving DecidableEq

-- See https://github.com/leanprover/lean4/issues/10295
attribute [nolint unusedArguments] instDecidableEqHom.decEq

which I suspect makes them false positives.

:document: Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic

@RootPairing.GeckConstruction.h_mem_cartanSubalgebra argument 14 inst✝ : DecidableEq ι

The type does explicitly depend on the instance (via cartanSubalgebra):

@[simp] lemma h_mem_cartanSubalgebra [Fintype ι] [DecidableEq ι] (i : b.support) :
    h i ∈ cartanSubalgebra b :=

New violations in master!

Also picked up by syntax linter after merging master:

:document: Mathlib.RingTheory.TensorProduct.IsBaseChangePi

@IsBaseChange.directSum argument 7 inst✝⁶ : DecidableEq ι
@IsBaseChange.directSumPow argument 7 inst✝⁶ : DecidableEq ι
@IsBaseChange.finsuppPow argument 7 inst✝⁶ : DecidableEq ι

Syntax linter miss: noncomputable def

The current version of the syntax linter doesn't pick up defs.

:document: Mathlib.RingTheory.TensorProduct.IsBaseChangeFree

But this def is data-carrying, and not a Prop.
Is its use of DecidableEq in the body warranted for unfolding/defeq reasons?

noncomputable def basis :
    Module.Basis ι S W where
  repr := (ibc.equiv.symm.trans (b.repr.baseChange R S _ _)).trans
      (finsuppPow ι (linearMap R S)).equiv

@IsBaseChange.basis argument 15 inst✝ : DecidableEq ι

[Thomas Murrills]

The upshot: I feel pretty confident in the syntax linter! :) It's picked up everything I believe it should except that noncomputable def, and I'm not completely sure about that one.

[Aaron Liu]

Thomas Murrills said:

False positives from env_linter:

:document: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks

@CategoryTheory.Limits.WidePullbackShape.instDecidableEqHom.decEq argument 4 inst✝ : DecidableEq J✝
@CategoryTheory.Limits.WidePushoutShape.instDecidableEqHom.decEq argument 4 inst✝ : DecidableEq J✝

Both are DecidableEq instances created by deriving, e.g.

/-- The type of arrows for the shape indexing a wide pushout. -/
inductive Hom : WidePushoutShape J → WidePushoutShape J → Type w
  | id : ∀ X, Hom X X
  | init : ∀ j : J, Hom none (some j)
  deriving DecidableEq

-- See https://github.com/leanprover/lean4/issues/10295
attribute [nolint unusedArguments] instDecidableEqHom.decEq

which I suspect makes them false positives.

Depending on what you mean by false positive, I don't think this is a false positive. These types are subsingleton, so you definitely don't need the decEq arguments.

[Thomas Murrills]

I was partially thinking "and we don't want to lint automatically generated decls" (maybe we do, at least ones generated by deriving?), but also thought that the [nolint unusedArguments] was in some way affirming this type as "correct", and hadn't considered what you said. :)

But, it does go against my intuitions here. It happens to be true that we can rewrite this particular definition without [DecidableEq J]—but in general, we don't want to suggest using classicality in any subsingleton Type us (as the linter would do), right?

[Yury G. Kudryashov]

These autogenerated DecidableEq instances assume DecidableEq but never use it. So, they're wrong. There is a Lean core issue tracking this.

[Yury G. Kudryashov]

Mathlib.RingTheory.TensorProduct.IsBaseChangeFree: I guess, the DecidableEq assumption is used in the proofs only, not in computing the data. I can check it later tonight.

[Yury G. Kudryashov]

I think that we should compare the performance of two linters (disabling Finite/Fintype etc in my version).

[Thomas Murrills]

Ah, I've just realized I left inhabitedNonempty on. :woman_facepalming: Let me fix that and re-bench.

[Thomas Murrills]

Though, if we want to compare like to like, we should really use the bvar machinery in the env linter and the telescoping machinery in the syntax linter, and compare all four... :thinking:

The syntax linter by nature has to do some infotree searching but can run asynchronously on each declaration, and the env_linter is applied to more declarations. It's not clear to me how these might affect the metrics either way!

[Yury G. Kudryashov]

@Kyle Miller I remember that you had an opinion on this topic.

[Thomas Murrills]

(I'll note that there is one part of the telescoping machinery I'm a little suspicious of: checking whether hypotheses of non-Props are used in the body of these defs after erasing proofs. I restrict my attention to theorems for now.)

[Yury G. Kudryashov]

I found some defs that used Decidable assumptions for proofs but not for data.

[Thomas Murrills]

Oh, okay, nice! We should definitely do that in the syntax linter too, then—as long as it's performant. :)

[Yury G. Kudryashov]

I remember that Kyle has ideas about performance but the suggestions were beyond my understanding of Lean metaprogramming at that time.

[Yury G. Kudryashov]

So, let's wait.

[Thomas Murrills]

For sure. :) I'd also like to add it as a subsequent feature to the syntax linter in a future PR, so that it's easier to review.

[Thomas Murrills]

Ah, I assumed Kyle's comment had been incorporated into the PR already.

[Thomas Murrills]

(I'm benching Kyle's version now as well, without checking it works.)

[Thomas Murrills]

(There is one futher optimization that could be done: don't erase proofs, but merely avoid them while traversing the expression to collect fvars.)

[Thomas Murrills]

Aside: I clean up those new violations in #31934.

[Thomas Murrills]

Yury G. Kudryashov said:

Mathlib.RingTheory.TensorProduct.IsBaseChangeFree: I guess, the DecidableEq assumption is used in the proofs only, not in computing the data. I can check it later tonight.

I'm not surprised, but it seems you were right about this. :) The instance becomes completely unnecessary in that file after fixing the violations picked up by the linters in its import Mathlib.RingTheory.TensorProduct.IsBaseChangePi.

[Thomas Murrills]

By the way, @Yury G. Kudryashov, Kim asked as a review question on #31142 why we filter out declarations in the Decidable namespace.

I assumed it's because theorems in the decidable namespace are allowed to be "about" Decidable* classes without "using" them, but ultimately I had cargo culted this later on after having seen yours. :) Is that right, or am I misunderstanding?

[Yury G. Kudryashov]

Yes, we have theorems like docs#Decidable.eq_or_ne that depend on Decidable to avoid classical reasoning.

[Thomas Murrills]

Also, here's a summary of the bench results:

• I benched the environment linter as well as Kyle's suggested optimization to it (after fixing a code typo) at #31920. Kyle's improvements did make it more efficient, but it still showed up as changing linting by +6.7%. Here are the radar results for Kyle's tweaks to the env linter.
  • But: this is an increase relative to environment linting. It doesn't really compare like to like.
• I benched the syntax linter at #31747, results here. It found no significant changes, but is relative to the whole build, which is much bigger.
• So, I put your and Kyle's telescoping implementation into the syntax linter: #32066. I commented out all the features not present in the current syntax linter (erasing proofs, checking def values, etc.) so that we're just comparing the telescoping approach to the bvar approach, and not also doing extra work. That comparison is here (with the bvar method as the reference commit).
  • It seems that the telescoping causes radar to mention "minor changes" of +0.2% to instructions across the whole build.
  • It seems that telescoping also adds a few seconds to the clock.

All in all, these aren't huge changes. We could probably get away with them, and I don't notice a delay while editing interactively. However, the bvar approach seems a hair more performant.

If we compare syntax linting to environment linting, using just the telescoping approach in both, we seem to find that environment linting adds less time to the clock. But, I do believe that the value of an interactive syntax linter one way or another is high enough that we probably ought to go for it. :)

What are your thoughts here? Kim has reviewed and delegated the syntax linter PR to me, so I can pull the trigger if we agree it would be useful to have it in. But I'd like your input first.

[Yury G. Kudryashov]

I would love to have some version of this linter (syntax or environment) in Mathlib. I have no opinion on which approach is better.

[Thomas Murrills]

Ok, great. :) I'll pull the trigger on the syntax linter, then! :tada:

[Thomas Murrills]

Also, not sure I said it explicitly, but apologies for missing your prior work here; it did turn out to be very useful to see the way it was factored to be generic, helped with some specific things like the Decidable name prefix checking, and the work you'd done prior made it feasible to actually turn the linter on.

I know you haven't asked for it, but I think it's only fair to add you as co-author to the current PR to recognize that work, even though the PRs are different. (And technically, the Decidable name prefix check comes directly from your PR, so there is a defensible link! :) )

[Thomas Murrills]

@Yaël Dillies I've exempted Mathlib.Order.Heyting.Regular from the linter; my intuition is that we want this file to be intuitionistic, but I'd like to confirm that with you (since you're the only author on that file), as the linter fires on isRegular_of_decidable. :)

[Yaël Dillies]

Ahah, yes indeed! To be quite fair, this is the only lemma in the whole file that deserves to be nolinted

[Thomas Murrills]

True! I had exempted the whole file with set_option linter.unusedDecidableInType to "future-proof" it (and left a comment, since I'm guessing the whole file really should be intuitionistic, on principle?), but octopus-react to this message and I'll move it to just that declaration :grinning_face_with_smiling_eyes:

[Chris Henson]

This linter just checks the type, not the body of the proof, right? So if for instance I use a term elaborator within the proof that depends on a DecidableEq instance, this is expected to trigger a warning?

[Aaron Liu]

yes

[Aaron Liu]

hmm

[Aaron Liu]

but what if the statement contains a proof?

[Aaron Liu]

does it check those?

[Thomas Murrills]

Not yet; two later improvements in that vein I’d like to incorporate are

• that (not counting dependence from proofs in the statement)
• not counting dependence from proofs in the body of a def

Note that the challenge here is not figuring out how to do this, but staying performant-enough while doing it across all of mathlib. But luckily we haven’t exhausted the possibilities for improving performance yet; there are things to experiment with. :grinning_face_with_smiling_eyes: