prop decidable linter

Stream: mathlib4

[Floris van Doorn]

I encountered some lemmas that use Classical.PropDecidable in their type instead of properly assuming decidability assumptions, e.g. docs#contDiff_update (which - of course - I added myself).
Therefore I wrote a simple linter on branch#fvd/illegalpropdec to find such theorems. The output on Mathlib is here:
https://gist.github.com/fpvandoorn/05cca028139e98bded9874169a1332d5
There are probably false positives. E.g. assuming that ℝ has decidable equality using Classical.PropDecidable is fine, assuming that a variable type has decidable equality is almost never fine.
Is someone willing to go through the list of the Gist and fix all theorems that need fixing. I might not have time for it myself in the near future.

[Timo Carlin-Burns]

assuming that ℝ has decidable equality using Classical.PropDecidable is fine

Why? Is the distinction that ℝ is a concrete type that we know cannot have a computable DecidableEq instance? Why isn't there then an instance DecidableEq ℝ := Classical.propDecidable?

[Timo Carlin-Burns]

I will start going through the gist!

[Floris van Doorn]

Yes, for fixed types it is fine. The problem is when instantiating variables in lemmas to types that suddenly do have decidable equality.
And the Real was just an example (and it turns out a bad one). In fact this instance does exist: docs#Real.decidableEq.

[Timo Carlin-Burns]

Where should I record false positives for improving the lint?

[Floris van Doorn]

You can do it in a comment here.

[Floris van Doorn]

And thanks for doing this!

[Floris van Doorn]

Or feel free to push nolint attributes to the linter branch. If you think that the linter can be improved to automatically recognize false positives, you can discuss that here (or improve the linter yourself :-) )

[Timo Carlin-Burns]

False positive:

Error: ./././Mathlib/Algebra/DirectLimit.lean:708:1: error: Ring.DirectLimit.of.zero_exact_aux.{v, w} theorem statement contains `Classical.propDecidable`.

The missing decidable instance is [DecidablePred (· ∈ s)] where s is an existential variable in the conclusion.

[Timo Carlin-Burns]

False positives:

Error: ./././Mathlib/Algebra/BigOperators/Finprod.lean:94:1: error: finsum_def'.{u_8, u_7} theorem statement contains `Classical.propDecidable`.
Error: ./././Mathlib/Algebra/BigOperators/Finprod.lean:100:1: error: finprod_def'.{u_8, u_7} theorem statement contains `Classical.propDecidable`.

The Classical.propDecidable is occurring as the body of a definition, which is allowed, and then occurs in the statement of an irreducible_def definitional lemma, which seems unavoidable.

[Timo Carlin-Burns]

The missing decidable instance is [DecidablePred (· ∈ s)] where s is an existential variable in the conclusion.

Ohh actually I think this is a true positive. The correct fix is to change \ex s, ... to \ex s, \forall [DecidablePred (. \in s)], ...

[Timo Carlin-Burns]

Autogenerated by @[simps]:

-- Mathlib.Algebra.Homology.DifferentialObject
Error: ./././Mathlib/Algebra/Homology/DifferentialObject.lean:88:3: error: HomologicalComplex.dgoToHomologicalComplex_obj_d.{u_2, u_1, u_3} theorem statement contains `Classical.propDecidable`.
Error: ./././Mathlib/Algebra/Homology/DifferentialObject.lean:88:3: error: HomologicalComplex.dgoToHomologicalComplex_map_f.{u_2, u_1, u_3} theorem statement contains `Classical.propDecidable`.

Not necessarily a false positive, but it seems like way too big a pain to manually write the generated lemmas so I'm gonna hope we can improve @[simps] instead.

[Damiano Testa]

Is this related to Yury's #10235 as well?

[Floris van Doorn]

Yes, but that is the opposite linter. Each of these two linters checks one implication of
"A decidable hypothesis should be part of a theorem if and only if that hypothesis is used in the type of the theorem"

[Timo Carlin-Burns]

Why does docs#UniqueFactorizationMonoid.factors take a DecidableEq instance when its definition uses Classical.choice anyway?

[Timo Carlin-Burns]

Here is an example of the kind of false positive you were predicting: docs#isInternal_prime_power_torsion_of_is_torsion_by_ideal uses factors and Multiset.toFinset on Multiset (Ideal R), so uses classical for DecidableEq (Ideal R). Ideal R contains Set R, so can only have computable decidable equality if Empty R. I wonder if there should be an instance of [Nonempty R] : DecidableEq (Set R) or at least DecidableEq (Ideal R) for the canonical noncomputable instance. It would silence this linter, but I don't know if it has a lot of precedent in the library or if there's downsides to making such instances.

[Yury G. Kudryashov]

Timo Carlin-Burns said:

Why does docs#UniqueFactorizationMonoid.factors take a DecidableEq instance when its definition uses Classical.choice anyway?

There are quite a few matches my linter finds in that file because of these design decisions. IMHO, we should refactor this file but I had no time to do this.

[Floris van Doorn]

Timo, thanks for your work on this. I'd have to think how we avoid some of these false positives in the linter. But hopefully you also found some true positives, and if you could make a PR with those, that would be really great!

[Timo Carlin-Burns]

PR fixing a few true positives: #11157

[Timo Carlin-Burns]

Yury G. Kudryashov said:

Timo Carlin-Burns said:

Why does docs#UniqueFactorizationMonoid.factors take a DecidableEq instance when its definition uses Classical.choice anyway?

There are quite a few matches my linter finds in that file because of these design decisions. IMHO, we should refactor this file but I had no time to do this.

#11158