Dyadic rationals

Stream: lean4

[Violeta Hernández]

Hi! I'm currently attempting to update the combinatorial-games repository to the latest Mathlib. We had our own custom implementation of Dyadic rationals (directly as just a subtype of ℚ), so I'm currently trying to merge our implementations together.

Here's a few questions that I have:

• What's the preferred way to write 1/2 : Dyadic? There's a few candidates, like Dyadic.ofOdd 1 2 sorry or 1 >> 1. Is there a reason for this to not just be a constant Dyadic.half?
• Where should all the Mathlib instances for this type go? I particularly want four of them: CommRing, IsStrictOrderedRing, DenselyOrdered, and Archimedean. IsLocalization would also be nice. (Maybe this question is off-topic, in which case I ask a different one: is anyone already working on this?)
• Would definitions Dyadic.num and Dyadic.den make sense? I make pretty heavy use of them in my own implementation. Or would it be preferred to just pass through ℚ for this?

[Kim Morrison]

1. I'd suggest 1 >> 1 to avoid needing extra API relating half back to everything else. But it wouldn't be terrible.
2. Can the instances just go in combinatorial-games for now? If we identify another situation where people want these instances, we can move them to Mathlib then.
3. num and den sound good.

[Violeta Hernández]

Alright then. I'll do the necessary adaptations over there. I'll link to the file here once I'm done in case you want to borrow anything :slight_smile:

[Robin Arnez]

Oh I just realized, we're missing these lemmas:

@[simp]
theorem Dyadic.toRat_shiftRight_int (x : Dyadic) (n : Int) : (x >>> n).toRat = x.toRat / 2 ^ n := by
  change (x.shiftRight n).toRat = _
  cases x
  · simp [Rat.div_def, Dyadic.shiftRight]
  · simp [Rat.div_def, Dyadic.shiftRight, Dyadic.toRat_ofOdd_eq_mul_two_pow, Int.neg_add,
      Rat.zpow_add, Rat.zpow_neg, Rat.mul_assoc]

@[simp]
theorem Dyadic.toRat_shiftRight_nat (x : Dyadic) (n : Nat) : (x >>> n).toRat = x.toRat / 2 ^ n :=
  toRat_shiftRight_int x n

@[simp]
theorem Dyadic.toRat_shiftLeft_int (x : Dyadic) (n : Int) : (x <<< n).toRat = x.toRat * 2 ^ n := by
  refine Eq.trans (toRat_shiftRight_int x (-n)) ?_
  simp [Rat.div_def, ← Rat.zpow_neg]

@[simp]
theorem Dyadic.toRat_shiftLeft_nat (x : Dyadic) (n : Nat) : (x <<< n).toRat = x.toRat * 2 ^ n :=
  toRat_shiftLeft_int x n

[Violeta Hernández]

Another implementation question: is there a reason why Dyadic.toRat isn't a coercion?

[Robin Arnez]

You're right, I thought about that too; that would probably be best for the benefit of enabling norm_cast

[Violeta Hernández]

The CGT repo makes very heavy use of norm_cast (we have no less than five numeric types casting into games), so this would be very appreciated!

[Violeta Hernández]

Another question. Shouldn't docs#Dyadic.lt_iff_toRat and docs#Dyadic.le_iff_toRat be backwards? Then they could be made into simp lemmas.

[Violeta Hernández]

Oh also, there should probably be an inhabited instance for Dyadic

[Violeta Hernández]

norm_cast is great (none of these lemmas can be solved by simp alone)
image.png

[Kim Morrison]

PRs very welcome (Robin's shift lemmas, making toRat a coercion, reversing lt_iff_toRat, and Inhabited)!

[Robin Arnez]

Violeta Hernández schrieb:

Another question. Shouldn't docs#Dyadic.lt_iff_toRat and docs#Dyadic.le_iff_toRat be backwards? Then they could be made into simp lemmas.

I think on the side of core it makes more sense to use it in the other direction because we have more verification for Rat than for Dyadic. Anyways, you can still attribute [simp ←] Dyadic.le_iff_toRat Dyadic.lt_iff_toRat if it's useful to you

[Violeta Hernández]

we have more verification for Rat than Dyadic

is this something that will remain true, or does it just reflect an unfinished API?

[Robin Arnez]

I would definitely say that Dyadic has unfinished API on core, at least in comparison to Rat. Most of that is made up through mathlib though so extending the API probably doesn't have too high priority right now

[Robin Arnez]

I guess of all of them, <<< and >>> probably need the most API extensions since we don't have type classes about them in mathlib

[Robin Arnez]

Maybe it'd be worth introducing Dyadic.twoPow : Int -> Dyadic and then say a <<< b = a * twoPow b and a >>> b = a * twoPow (-b)?

[Violeta Hernández]

That seems like a very reasonable idea, it'd give a more canonical way to write 1/2 as twoPow (-1)

[Jovan Gerbscheid]

Violeta Hernández said:

Another question. Shouldn't docs#Dyadic.lt_iff_toRat and docs#Dyadic.le_iff_toRat be backwards? Then they could be made into simp lemmas.

I agree that they're backwards, but you can add reverse direction simp lemmas with @[simp ←]

[Kim Morrison]

lean#10994