Dyadic rationals

Stream: combinatorial-games

[Violeta Hernández]

Just found something really exciting: https://github.com/leanprover/lean4/pull/9993

[Aaron Liu]

yeah I saw this too

[Aaron Liu]

does this implementation of dyadic rationals look reasonable

[Violeta Hernández]

It's not the most useful representation of dyadic rationals for game theory purposes but presumably we can implement functions Dyadic.num and Dyadic.den on top of this and call it a day

[Violeta Hernández]

Really I just want to have this in Mathlib

[Violeta Hernández]

So, it turns out Lean now has Dyadic rationals! docs#Dyadic

[Violeta Hernández]

I've attempted to update our repo with this new material over at https://github.com/vihdzp/combinatorial-games/tree/vi.update_24

[Violeta Hernández]

But I'm finding it a bit difficult, mostly because we no longer have an equivalent of CGT#Dyadic.mkRat

[Violeta Hernández]

I believe the correct thing to do here is to redefine CGT#Dyadic.upper and CGT#Dyadic.lower as upper x = x + half ^ x.den and lower x = x - half ^ x.den. Still, there's a bunch of theorems I have to reprove using these new definitions.

[Violeta Hernández]

I think I'll first make an interim update where I change our Dyadic type to Dyadic' (as well as the other changes required for the version bump), and then a followup will replace Dyadic' by Dyadic by introducing all the API and whatnot

[Violeta Hernández]

CGT#244 for the bump PR