rat.denumerable

Stream: new members

[Matt Diamond]

Just curious: is there a reason why rat.denumerable is proved via an equivalence to a subtype instead of just doing of_encodable_of_infinite ℚ directly?

[Matt Diamond]

As far as I can tell, the only thing the subtype provides is an easy proof of encodability, but we already have encodable ℚ so it seems unnecessary.

[Kyle Miller]

Here's where it was introduced: https://github.com/leanprover-community/mathlib/commit/3ad35223f321e644ef3e16ae9ec5b9383b2baabe

The encodable instance uses very nearly the same subtype, but with a sigma type factored out.

Maybe you want to investigate a creating a denumerable ℚ instance that uses the encodable instance more directly?

[Matt Diamond]

I'm just wondering why we don't simply write instance : denumerable ℚ := of_encodable_of_infinite ℚ

[Matt Diamond]

are you saying that we want the denumerability encoding to be a bit different than the usual encoding?

[Kyle Miller]

No, I'm not meaning to imply anything, other than suggesting you could try simplifying that instance and see whether it breaks anything.

[Kyle Miller]

The git commit link also suggests that @Chris Hughes might have an answer.

[Chris Hughes]

Matt Diamond said:

I'm just wondering why we don't simply write instance : denumerable ℚ := of_encodable_of_infinite ℚ

I think it's because there was no encodable instance for ℚ. I had to prove encodable ℚ inside the proof of denumerable ℚ.

[Chris Hughes]

Not sure but there might even be two different encodable instances for ℚ at the moment if there's a denumerable to encodable instance.

[Matt Diamond]

it looks like the encodable instance for Q was added back in October 2017

[Kyle Miller]

It looks like there was an encodable instance at least four years ago, and the denumerable instance was 2-3 years ago

[Matt Diamond]

perhaps it was just overlooked

[Chris Hughes]

I think I probably overlooked it.

[Matt Diamond]

all good