Random decidability assumption

Stream: mathlib4

[Patrick Massot]

I’d be grateful if someone can help me explain in MIL why docs#DirectSum.toModule needs decidable equality on the indexing type but docs#DirectSum.linearEquivFunOnFintype doesn’t.

[Patrick Massot]

And also why we have this Fintype version but seemingly no Finite version.

[Eric Wieser]

Why would we want both a finite version and a fintype version?

[Eric Wieser]

(I claim that at least that shouldn't be a general principle; we'd end up needing two different multiplications on Matrix, one for Finite and one for Fintype)

[Patrick Massot]

Because Finite is much nicer?

[Patrick Massot]

I mean I wouldn’t mind getting rid of the Fintype version.

[Eric Wieser]

I think the decidable equality might be accidental, since the docstring for docs#DFinsupp.sumAddHom says no decidable assumption is needed, and indeed docs3#dfinsupp.sum_add_hom does not have that assumption

[Eric Wieser]

That is, this looks like a misfiring variable inclusion

[Patrick Massot]

I won’t insist on the Fintype vs Finite thing. Right now I am only trying to get a consistent story to explain in my new MIL chapter.

[Patrick Massot]

I’ll try to open a Mathlib PR fixing this accidental assumption (unless you would prefer to do it).

[Eric Wieser]

In retrospect, I think it's talking about a different decidability assumption

[Eric Wieser]

Yes, the reason that assumption is needed is that DFinsupp stores a multiset of its support, and so to sum over the support you need to first deduplicate

[Eric Wieser]

So I think the fix here is perhaps just an explanation in the docstrings

[Eric Wieser]

Meanwhile, DirectSum.linearEquivFunOnFintype does not need to sum over the support, as it knows that it can just use the underlying function directly; so no decidable equality is needed

[Patrick Massot]

Ok, I guess I will stick to my “Note that the direct sum notation is scoped to the DirectSum namespace, and that the universal property of direct sums requires decidable equality on the indexing type (this is somehow an implementation accident).”

[Eric Wieser]

I might be biased, but I think decidable equality on the index type is a totally reasonable thing to require in general, and in fact its absence in some functions is more the implementation detail. Using the multivariate polynomial analogy, I think assuming an algorithm to tell the variable names apart is valid except possibly in the case of bad handwriting on a blackboard.

[Eric Wieser]

I guess the other way you could spin it is that to mathematicians, Decidable is always an implementation detail

[Kevin Buzzard]

Yes, decidability is not taught in mathematics departments and is universally found confusing by my students (as is noncomputability). The less of it we have, the better, in my opinion!

[Yury G. Kudryashov]

About decidability: I have a linter in #10235 that detects unneeded Decidable*/Fintype/Encodable assumptions. It needs some work to avoid false positives (most come from structures) and some nolints, but I have no time to finish it.

[Edward van de Meent]

what exactly is the accepted practice with regards to these kinds of assumptions?

[Edward van de Meent]

i'm not very acquainted with writing linters, but i get the impression that the linter wants you to replace all Decidable parameters with uses of classical? but surely that's not right?

[Edward van de Meent]

i thought the whole point of using Decidable instances is so you don't have to assume classical?

[Yury G. Kudryashov]

The linter enforces the following rule: if you don't need Decidable to formulate a theorem, then don't use it.

[Yury G. Kudryashov]

For definitions, if you don't need Decidable to generate data, then don't use it.

[Yury G. Kudryashov]

So, it allows Decidable used to generate data but bans non-classical proofs (several exceptions will be added before we merge it).

[Edward van de Meent]

why is the decision being made to ban non-classical proofs?

[Yury G. Kudryashov]

Because we decided to focus on classical math to make it easier for mathematicians.

[Yury G. Kudryashov]

Non-classical proofs are tolerated (especially if @Mario Carneiro will PR his @[allowed_axioms] attribute and mark lemmas that are supposed to stay non-classical), but most of the library uses Decidable only if it's required for data.

[Edward van de Meent]

in what contexts will non-classical proofs be allowed?

[Yury G. Kudryashov]

E.g., Mario formalized something about Turing machines, and one of the points in his paper was that the proof didn't depend on Clasical.choice. If a theorem already relies on Classical.choice (e.g., anything in topology/analysis), then it makes no sense to make the proof "a bit less" classical.

[Yury G. Kudryashov]

There are no formal rules for exceptions, but the idea is that in Coq you need to justify why you use classical reasoning, while in Mathlib you need to justify why you avoid it.

[Edward van de Meent]

so there's no real reason why, just "because"?

[Edward van de Meent]

to be clear, i do think it makes sense that if dependencies of a theorem already use classical, it's ok to continue to do so... it just strikes me as odd that that is used to justify forcing any proof to do so

[Eric Wieser]

Yury G. Kudryashov said:

For definitions, if you don't need Decidable to generate data, then don't use it.

In Patrick's original example, we do need this instance to (computably) generate the data.

Kevin Buzzard said:

The less of it we have, the better, in my opinion!

I don't think we should be making things noncomputable just to avoid confusing students, because this can often just create more work for tactic writing, cripple #eval for quick tests (which confuses other students), and prevents kernel reduction (which breaks decide). There are ways to reduce confusion without removing it!

[Eric Wieser]

Do you think we can somehow get a "docstring for mathematicians" at docs#DecidableEq ? I can see this being contentious from the FRO's perspective since not all users are mathematicians. Was there any progress towards docstring extension by downstream packages?

[Patrick Massot]

Eric Wieser said:

I don't think we should be making things noncomputable just to avoid confusing students, because this can often just create more work for tactic writing, cripple #eval for quick tests (which confuses other students), and prevents kernel reduction (which breaks decide). There are ways to reduce confusion without removing it!

This is not only confusing students, this is confusing professional mathematicians. Crippling #eval confuses students only if you tell students about #eval, which I never did, and I would be surprised if Kevin did. Do you know any proof in Mathlib that actually benefits from those DecidableEq? I am not saying we must get rid of them, but I am far from convinced by your arguments.

[Yury G. Kudryashov]

One setting where computability matters is functions about Nat, especially those used in norm_num and other tactic.

[Yury G. Kudryashov]

This may include docs#Nat.factorization, hence bits of Finsupp.

[Patrick Massot]

I am talking about direct sums of modules here, not computability in general.

[Eric Wieser]

I have numerous threads on Zulip (admittedly not in mathlib), where I use direct sums to build computable polynomials in about 20 lines. This depends on decidability, and I think enables rfl for some trivial statements

[Eric Wieser]

Patrick Massot said:

Do you know any proof in Mathlib that actually benefits from those DecidableEq?

Speculating for now, I would expect this to be convenient for working with the graded structure of Exterior algebra, since otherwise you end up with a classical decidable instance for Nat when selecting a single element from DirectSum.of

[Patrick Massot]

By the way docs#DirectSum.of and docs#DirectSum.lof are also embarassing to explain in succession given the way they disagree on implicitness of arguments.

[Patrick Massot]

Maybe the explicit indexing type in the second one is a typo.

[Eric Wieser]

I suspect it's there due to elaboration issues; if you want the linear map version, then probably you're not applying it to i and so need to pass the type I instead

[Eric Wieser]

Oh, I guess the same is true for the AddMonoidHom, so this is inconsistent however you look at it

[Eric Wieser]

In the past I suggested making of a plain unbundled function. Would that be worse in your opinion?

[Patrick Massot]

It is definitely inconsistent. And you don’t need to apply it to infer I, it is already given by M (or β).

[Kim Morrison]

Edward van de Meent said:

so there's no real reason why, just "because"?

@Edward van de Meent, there's definitely a real reason, which is that nearly all mathematicians (one can of course quibble of what that means) don't care at all (or know!) about decidability, and the decision to have Mathlib be as classical as possible was intentional, and I think highly successful, in making Mathlib appealing and useful to these users.

It is easy to find many people who've looked at other theorem provers libraries and essentially immediately dismissed them as being "about" constructivism or intuitionism or ..., rather than about "mathematics". Preferring classical reasoning in Mathlib is a direct response to this.

[Kim Morrison]

We're well aware this makes some people sad, and at the margins are willing to accommodate, but not on the core principle that Mathlib is intended to be primarily classical.