Unused Fact in type linter

Stream: mathlib4

[Bhavik Mehta]

Can we also have a version of the "Unused fintype in type" linter for Fact instances? The general consensus for Fintype vs Finite (use Fintype only if the statement's type requires it, otherwise use Finite) seems generally similar for Fact instances, eg Fact p.Prime or Fact (1 <= p); ie only have it as an (instance) assumption if the statement's type requires it. (Apologies if this is the wrong thread for that, I couldn't find an existing thread about this linter)

[Notification Bot]

A message was moved here from #mathlib4 > Unused fintype in type linter by Thomas Murrills.

[Thomas Murrills]

Hmm, I'm guessing instances of Prop classes should be permitted to use [Fact _], right? :thinking: ( :working_on_it: #32436)

[Thomas Murrills]

(A potential false positive of this form that I have in mind is expChar_prime in Mathlib.Algebra.CharP.Defs.)

[Thomas Murrills]

Also, to be clear: I suppose the linter's suggestion ought to be to simply replace it with an ordinary hypothesis of the form (h : p.Prime), right? Are there any weird but systematic cases where this is not what we want? :eyes:

[Thomas Murrills]

Wow, quite a few violations! :dizzy: If i'm counting correctly, 110 files violated this linter (but this does include linting against instances, which we might not want to do).

[Bhavik Mehta]

We definitely want to allow data-carrying instances to have this assumption. I'm not certain but it seems reasonable to me to allow propositional instances to have it too; and it also seems okay to be more permissive in the first version.

[Thomas Murrills]

Data-carrying instances are already excluded by the linter—however, by exempting propositional instances too, we've reduced the number of files with violations by 22 (to 88). :)