Decidable assumptions in Computability

Stream: mathlib4

[Yury G. Kudryashov]

My new Decidable linter matched on some theorems/defs in Computability (note: it has false positive matches; I know about it and I don't want to fix it now; I'll fix it before making the PR non-draft).
Does Mathlib convention "don't assume Decidable unless you need it to state the theorem" apply to Computability? I guess, some people (@Mario Carneiro ?) may want choice-free proofs in that part of the library.

[Mario Carneiro]

can you name some specific violators?

[Mario Carneiro]

probably they should be nolinted but I'd like to review them first

[Yury G. Kudryashov]

E.g.,

• docs#Computability.Encoding.card_le_aleph0 assumes Encodable instead of Countable
• docs#ComputablePred.computable_iff_re_compl_re assumes DecidablePred

[Yury G. Kudryashov]

You can open https://github.com/leanprover-community/mathlib4/actions/runs/8010176407/job/21880540054?pr=10235 and search for "Mathlib/Computability"

[Yury G. Kudryashov]

Note that the linter matches on all structures that assume Decidable/Fintype/Inhabited for now.

[Mario Carneiro]

I think the first one should be exempted because it's about an encodable hypothesis

[Yury G. Kudryashov]

I think that the first can be proved with [Countable] assumption without choice.

[Mario Carneiro]

sure, but then it will be more work to use

[Mario Carneiro]

I think the consequent is literally the definition of Countable

[Yury G. Kudryashov]

Why? We have [Encodable α] : Countable α instance.

[Mario Carneiro]

This is not about Encodable it's about Encoding

[Yury G. Kudryashov]

It has [Encodable e.Γ] assumption.

[Yury G. Kudryashov]

That can be replaced by [Countable e.Γ]

[Mario Carneiro]

I see, that seems reasonable

[Mario Carneiro]

assuming it doesn't add imports

[Yury G. Kudryashov]

Do you plan to add an @[allowedAxioms] attribute, so that we can track theorems you want to stay choice-free?

[Mario Carneiro]

Some time after we fix the issues that broke everything in lean 4

[Mario Carneiro]

because right now it's pointless, everything depends on all the axioms for stupid reasons

[Yury G. Kudryashov]

"everything" means "everything" or "choice-free proofs"?

[Mario Carneiro]

all the theorems that used to be choice-free are no longer so in lean 4

[Mario Carneiro]

docs#ComputablePred.computable_iff_re_compl_re should definitely be nolinted, there is even a nolint in the source commented out

[Yury G. Kudryashov]

OK, I'll look for those nolints

[Yury G. Kudryashov]

Let me prepare a PR and ask for your review.

[Yury G. Kudryashov]

#10869, assigned to you

[Yury G. Kudryashov]

Pushed +1 theorem

[Eric Wieser]

Mario Carneiro said:

because right now it's pointless, everything depends on all the axioms for stupid reasons

I think the existence of the attribute will be a much stronger argument for the feature existing in the first place