Dyadic rationals in Mathlib

Stream: mathlib4

[Violeta Hernández]

We have docs#Dyadic in core, and we use this same type in the CGT repo (as of a few minutes ago, thanks to CGT#320). There is currently nothing in Mathlib about dyadic rationals, so we had to build stuff like the CommRing instance from scratch. Would this material he desirable for Mathlib upstreaming?

I believe @Kim Morrison said some months ago we should keep this in our repo. But after another thread recently popped up asking about this I'd like to know if that's still our stance.

[Violeta Hernández]

https://leanprover.zulipchat.com/#narrow/channel/113489-new-members/topic/Dyadic.20numbers/with/570410683

[Kim Morrison]

There's a Lean.Grind.CommRing instance for Dyadic. Just write the conversion function from Lean.Grind.CommRing to (Mathlib.)CommRing, and build the instance using that. Working from scratch is duplicative.

[Eric Wieser]

I would argue that mathlib should provide CommRing instances for every type that core provides, assuming the ring structure is canonical

[Eric Wieser]

But indeed deriving it from the grind structure to avoid repetition makes sense

[Violeta Hernández]

Are there any future plans to merge these two algebraic hierarchies we now have?

[Kim Morrison]

No.

[Kim Morrison]

They intentionally serve different purposes.

[Eric Wieser]

I don't see the Lean.Grind.CommRing instance that Kim describes in the docs; maybe it's not in 4.27.0

[Kim Morrison]

Lean.Grind.* is unapologetically an internal library optimized for the needs of grind.

[Kim Morrison]

Eric Wieser said:

I don't see the instance that Kim describes in the docs

Init.Data.Dyadic.Instances

[Eric Wieser]

https://leanprover-community.github.io/mathlib4_docs/Init/Data/Dyadic/Instances.html is blank, perhaps the docs are stale

[Kim Morrison]

Mathlib should definitely not provide an instance converting from Lean.Grind.X to (Mathlib.)X, just a def. But then it's fine for individual types such as Dyadic to use that def to build an instance.

[Kim Morrison]

Sorry, I don't use the Mathlib docs...

[Eric Wieser]

What do you use instead?

[Violeta Hernández]

What about theorems such as IsLocalization (powers 2) Dyadic? Do those belong in Mathlib?

[Eric Wieser]

Eric Wieser said:

https://leanprover-community.github.io/mathlib4_docs/Init/Data/Dyadic/Instances.html is blank, perhaps the docs are stale

@Henrik Böving, this looks like it might be a doc-gen bug to me; the page exists and the source link leads to a file that contains what Kim says, but the declarations are missing from the HTML

[Aaron Liu]

they're all private

[Aaron Liu]

See lean4#12199

[Aaron Liu]

not a docgen bug

[Kim Morrison]

Eric Wieser said:

What do you use instead?

I just grep in the sources (or more often these days, just ask Claude to find/explain something).

[Kim Morrison]

Violeta Hernández said:

What about theorems such as IsLocalization (powers 2) Dyadic? Do those belong in Mathlib?

Yes.

[Violeta Hernández]

Is there a reason docs#Dyadic.toRat isn't registered as a coercion?

[Kim Morrison]

I wrote Dyadic initially for internal use (when interval arithmetic was higher on our roadmap), and coercions didn't seem helpful.