countable types

Stream: general

[Violeta Hernández]

@Yury G. Kudryashov I'm interested in where you're taking the new countable typeclass and the finite typeclass. I know that there was very recently a huge refactor with set.finite, but I wonder if it would be a good idea to redefine set.finite s as finite ↥s and set.countable s as countable ↥s. Would most likely save us from a lot of API duplication.

[Violeta Hernández]

And regarding this same topic: your new files on countable types seem to cause trouble when imported at the same time as the file on countable sets. There's name clashes like countable_iff_exists_surjective and set.countable_iff_exists_surjective.

[Violeta Hernández]

(deleted)

[Violeta Hernández]

Just opened #14515 to adress this

[Yaël Dillies]

Prepare to be mindblown: We don't say (s : set α).nonempty for s : finset α. Instead, we say s.nonempty.

[Yury G. Kudryashov]

I have more not-yet-PRd stuff about countable and finite. I'm going to open some PRs later today.

[Violeta Hernández]

Oh, then I hope my attempts at fleshing out the API don't clash with yours

[Yury G. Kudryashov]

I'll have a look at your pr once I check in to the hotel (in about 4 hours)

[Yury G. Kudryashov]

The pr you mentioned above is not about countable. What's the correct number?

[Mauricio Collares]

#15415

[Matt Diamond]

could be worth adding a proof of countable α ↔ # α ≤ ℵ₀ somewhere... though it's also pretty trivial to prove it from countable_iff_nonempty_embedding

[Yury G. Kudryashov]

Please don't add more facts about countable yet. I have some unpushed stuff that I hope to PR tomorrow or the day after tomorrow.

[Violeta Hernández]

Are you planning on refactoring set.countable soon?

[Yury G. Kudryashov]

Yes.

[Yury G. Kudryashov]

See branch#YK-countable-set

[Yury G. Kudryashov]

What should be the instance priorities for:

• encodable X -> countable X;
• subtype.countable;
• quotient.countable?

[Yury G. Kudryashov]

We also have instances with default (1000) priority for prod.countable etc.

[Violeta Hernández]

Why does this matter? Isn't countable a Prop?

[Yaël Dillies]

Is there any reason to move away from the general rule? namely:

• 100
• 1000
• 1000

[Yury G. Kudryashov]

@Violeta Hernández It affects typeclass search speed.

[Yury G. Kudryashov]

@Yaël Dillies I think that we should use something smaller than 1000 for subtype and quotient instances so that instances for specific subtypes and quotients get higher priority.

[Yaël Dillies]

Will there be that many instances of countable?

[Yury G. Kudryashov]

I don't know.

[Yaël Dillies]

I doubt this is all that important.

[Yury G. Kudryashov]

In case of finite (IMHO, we should have the same priorities), we'll definitely have instances for some specific sets.

[Yury G. Kudryashov]

E.g., the index set of some basis.

[Yury G. Kudryashov]

(in a finite dimensional space)

[Yaël Dillies]

Also, aren't specific subtypes and quotients often being declared as type synonyms? If so, subtype.countable and quotient.countable won't even apply to them.

[Yury G. Kudryashov]

Some of them are declared as sets.

[Violeta Hernández]

I don't think we even have that many concrete subtypes or quotients

[Violeta Hernández]

Much less countable ones

[Violeta Hernández]

I can think of pnatand fin

[Yury G. Kudryashov]

pnat and fin aren't subtypes from the typeclass search point of view.

[Violeta Hernández]

So that's zero examples

[Yury G. Kudryashov]

For finite, we have instances for set operations (in particular, an instance for each set of the form {a, b, c, d}) and instances for some sets like "the index set of an unspecified finite basis in a finite dimensional space".

[Yury G. Kudryashov]

(probably, the latter is a noncomputable ... : fintype ... now)

[Violeta Hernández]

These would all be finite as well, right? How are those priorities set up?

[Kyle Miller]

Violeta Hernández said:

I don't think we even have that many concrete subtypes or quotients

Subtypes do appear. I invite you to search for // in https://leanprover-community.github.io/mathlib_docs/data/fintype/basic.html

[Kyle Miller]

Violeta Hernández said:

These would all be finite as well, right? How are those priorities set up?

So far we have a priority 900 instance for fintype -> finite since finite instances should be faster to synthesize in general. https://github.com/leanprover-community/mathlib/blob/2220b0cbab795e73674b8191170b0cc68c6b54a8/src/data/finite/basic.lean#L50

[Kyle Miller]

Yury G. Kudryashov said:

I think that we should use something smaller than 1000 for subtype and quotient instances so that instances for specific subtypes and quotients get higher priority.

Won't specific subtypes and quotients have instances that are defined after subtype.countable and quotient.countable? (As in, they'll be in modules that import the instances from the module where these are defined?) Can we rely on typeclass inference trying later instances of the same priority first?

[Kyle Miller]

Yury G. Kudryashov said:

(probably, the latter is a noncomputable ... : fintype ... now)

(Just wanted to mention that what I'd like to see is that all these noncomputable instances become finite instances. I haven't seriously dug in to see how feasible this is -- have you had a chance to?)

[Violeta Hernández]

Kyle Miller said:

Subtypes do appear. I invite you to search for // in https://leanprover-community.github.io/mathlib_docs/data/fintype/basic.html

I meant concrete as in specific named types that were defined in terms of a subtype. But judging from Yury's later comments, I think I might have misunderstood what sorts of types we were considering here.

[Yaël Dillies]

Yes, we're specifically interested in unnamed subtypes here?

[Yury G. Kudryashov]

@Kyle Miller Sometimes these noncomputable ... fintype instances are used for fintype.sum.

[Yury G. Kudryashov]

We're interested in definitions def lalala : set X := _

[Yury G. Kudryashov]

With instances on (lalala : Type*)

[Yaël Dillies]

Yes, we already override Prop versions by noncomputable Type versions when there's no hope of getting a computable one. This mostly happens for nonempty and inhabited.

[Yaël Dillies]

So, no, we should not get rid of the noncomputable fintype instances.

[Violeta Hernández]

Yury G. Kudryashov said:

Kyle Miller Sometimes these noncomputable ... fintype instances are used for fintype.sum.

Then maybe we should have a finite.sum to match?

[Kyle Miller]

I'd like to see a way to get fintype instances from finite instances in a classical context. I believe this should be possible in Lean 4 due to its improved handling of typeclass search loops, but I'm not completely sure.

[Violeta Hernández]

This already exists: docs#fintype.of_finite

[Kyle Miller]

I'm aware of that function -- I mean automatically when you do classical or open_locale classical.

[Yaël Dillies]

I'm not sure what you find harmful about having noncomputable instances when no computable one can exist.

[Kyle Miller]

If you're in a noncomputable theory, then that's fine I think, but having any noncomputable fintype instances means you can't rely on it for computability. I think of it as being like that computable class I proposed before but specialized for finite.

[Kyle Miller]

inhabited and nonempty share a similar relation (by the way, is there a reason we use an inhabited linter rather than a nonempty linter?)

[Yury G. Kudryashov]

Violeta Hernández said:

Yury G. Kudryashov said:

Kyle Miller Sometimes these noncomputable ... fintype instances are used for fintype.sum.

Then maybe we should have a finite.sum to match?

We have docs#finsum

[Junyan Xu]

Kyle Miller said:

inhabited and nonempty share a similar relation (by the way, is there a reason we use an inhabited linter rather than a nonempty linter?)

Notice that some types are inhabited by 37, for example: docs#polynomial.splitting_field.inhabited

[Kyle Miller]

(I guess let's see what happens with a has_nonempty_instance linter: #15542)

[Matt Diamond]

just curious, what's the significance of 37? just a running joke?

[Kyle Miller]

It's apparently the most random integer from 1 to 100.

[Matt Diamond]

ah ha... alright then

[Kyle Miller]

Huh, there's a website full of 37 factoids: http://magliery.com/37/index.html

[Matt Diamond]

and of course there's https://en.wikipedia.org/wiki/37_(number)