Dyadic numbers

Stream: new members

[Pieter Collins]

I'm trying to work with the Dyadic numbers, and am having trouble with a few things.

I want to use the absolute value, but Dyadic.abs is not defined. There also does not seem to be an Rat.abs, though there is Int.natAbs. Is this because there is an auto-generated abs somewhere, maybe Mathlib.Algebra.Order.AbsoluteValue.Basic and/or Mathlib.Algebra.Order.Group.Unbundled.Abs? But then I can do |.| of Int, but not |.| of Dyadic ("failed to synthesize instance of type class Lattice Dyadic") or Rat.

There also seems to be quite some inconsistency between different parts of Mathlib. For example, comparing Int, Dyadic and Rat:

• Int has neg_add, but Dyadic and Rat do not.
• Rat has add_right_cancel, but Int and Dyadic are missing this.
• Int and Rat have and instMax but Dyadic does not/
• Int defines .le (via NonNeg), .lt and .ble, but not .blt, whereas Dyadic defines .ble and .blt and Rat just .blt
  Is there any reason for this? Will there be any effort made to standardise the provided operations and lemmas?

It seems like the intention is that the typeclasses organise operators and their properties. This is in principle nice, but there are at lot of typeclasses! This makes it really hard to find what is available. (Int has way more than 100!) Are there any good ways to navigate this?

I've also been having a hard time "unfolding" things, especially with all the casts and notations around. Is there any way of simplifying out all notations, derived operations from typeclasses etc?

Thanks!

[Vlad Tsyrklevich]

By loogling for Rat, "abs", I found docs#Rat.abs_def and clicking on the notation takes you to the origin of that definition.

[Aaron Liu]

there's no LinearOrder instance for Dyadic in mathlib (which is why you can't use docs#abs with it). In fact, there's no mention of Dyadic in mathlib at all.

[Vlad Tsyrklevich]

For add_right_cancel, this seems to be another case where there is a polymorphic method that can handle these: #check @add_right_cancel Int. neg_add appears to be another instance of this behavior. There is a Rat.neg_sub so this does just seem like an oversight. I'm guessing part of the cause is that many users are downstream of mathlib so they just use the mathlib polymorphic methods and some of these oversights may just go unnoticed.

[Vlad Tsyrklevich]

From git history it appears that Dyadic is only 5 months old so it's still relatively new, it may be that there is some missing API

[Vlad Tsyrklevich]

Pieter Collins said:

This is in principle nice, but there are at lot of typeclasses! This makes it really hard to find what is available. (Int has way more than 100!) Are there any good ways to navigate this?

This is not exactly answering your question, but sometimes I can avoid searching myself by using tactics like exact?/apply?/rw? to help direct my search. If I know I want something in a specific shape, like neg_add for Rat for example I could write

import Mathlib
example (a b : Rat) : -(a + b) = -a + -b := by exact?

to help show me if it's already available in some form.

[Vlad Tsyrklevich]

Pieter Collins said:

I've also been having a hard time "unfolding" things, especially with all the casts and notations around. Is there any way of simplifying out all notations, derived operations from typeclasses etc?

Are you looking for something like set_option pp.all true?

[Robin Arnez]

Oh I just noticed an oversight: Init.Data.Dyadic.Instances actually defines some instances which are supposed to make grind work but they are all private and not exposed! Here's a fix: lean4#12199

[Aaron Liu]

oh that wasn't intentional?

[Aaron Liu]

is the other dyadic file with only private stuff in it also not intentional?

[Robin Arnez]

There's another one?

[Robin Arnez]

Fixed that one too

[Violeta Hernández]

We use dyadic numbers in the CGT repo, so it'd be appreciated if someone added its relevant instances to Mathlib.