Square root typeclass

Stream: mathlib4

[Violeta Hernández]

There's a TODO comment above the docs#Real.sqrt notation, suggesting turning it into a typeclass. Has there been any progress on this?

[Yakov Pechersky]

src#Real.sqrt

[Kevin Buzzard]

What does this comment even mean? Edit: oh, the issue seems to be that the notation should be HasSqrt.sqrt so it works for NNReal etc.

[Violeta Hernández]

I imagine it means one of two things

• Make a typeclass for the notation
• Make a typeclass for types with a "well-behaved" square root operation

[Violeta Hernández]

I'm not sure what the second one would entail (and I don't really find it feasible), but the first one seems very uncontroversial

[Niels Voss]

Do we want to turn Nat.sqrt into a typeclass instance? I personally don't think that's a good idea, but I want to hear what other people's perspectives are

[Violeta Hernández]

I don't really see why not. It might look a bit weird to write stuff like √5 = 2 but I'd argue this is no worse than what Nat substraction and division already allow.

[Niels Voss]

I guess that's fair. I'm just used to having sqrt automatically coerce Nat to Real

[Violeta Hernández]

Hmmm yeah, that's actually a really good point against this idea

[Violeta Hernández]

I recently defined a square root on a new type (CGT#335) and came back to this. Surely it wouldn't be controversial to add this code somewhere?

/--
The notation typeclass for square roots.
This enables the notation `√a : α` where `a : α`.
-/
class Sqrt (α : Type u) where
  /-- `√a` computes the square root of `a`.
  The meaning of this notation is type-dependent. -/
  sqrt : α → α

@[inherit_doc] prefix:max "√" => Sqrt.sqrt

macro_rules | `(√ $x) => `(unop% Sqrt.sqrt $x)

[Violeta Hernández]

(The question of course is, does this go in core, or in some basic file in Mathlib?)

[Weiyi Wang]

It feels more Mathlib to me

[Violeta Hernández]

What would be a good file for it?

[Violeta Hernández]

I don't want to put it in the same file as docs#Real.sqrt because that would dramatically raise the imports to use this notation

[Yury G. Kudryashov]

I think that I wrote this comment some time ago, but some of use cases I thought about (e.g., Nat.sqrt) were later dismissed, because it isn't clear whether the floor one or the ceiling one should be given by the notation.

[Yury G. Kudryashov]

Also, note that a notation class makes all expressions heavier. If we aren't going to have any generic theory, then I'm not sure that we should have a notation class.

[Yury G. Kudryashov]

Another option is to have an overloaded notation.

[Violeta Hernández]

Truthfully I just wanted to get the elaborator for free. If there's an actual cost to introducing this notation typeclass then we probably shouldn't.

[Yury G. Kudryashov]

It turns every Real.sqrt into @Sqrt.sqrt Real instRealSqrt, same for other use cases.

[Jireh Loreaux]

If it were a notation typeclass we could use it for docs#CFC.sqrt

[Violeta Hernández]

We could also use it for docs#Ideal.radical, though I'm not sure we would want to.

[Violeta Hernández]

And of course there's my motivating example CGT#Nimber.sqrt (not yet merged)

[Yury G. Kudryashov]

Will an overloaded notation work for all these cases?

[Violeta Hernández]

I think it makes sense that we'd like to talk about CFC.sqrt and Real.sqrt simultaneously. For the other examples I don't believe there's any possible confusion.

[Yury G. Kudryashov]

Ah yes, is there an instance of whatever is needed for CFC.sqrt for Real?

[Yury G. Kudryashov]

If yes, then adding a notation typeclass will lead to a non-defeq diamond for Real, and we don't want that.

[Jireh Loreaux]

Yury, the answer is currently no, but it will be yes when we eventually get real C*-algebras. I'll note though that we already have a non-defeq diamond somewhere for real powers.

[Yury G. Kudryashov]

Where?

[Yury G. Kudryashov]

Do you mean docs#CFC.instPowReal ?

[Yury G. Kudryashov]

(assuming that Real satisfies assumptions on A)

[Jireh Loreaux]

Ah, maybe we don't have a diamond yet. I thought Mathlib had a Pow Complex Real instance, but apparently not. But yes, the point is that when we have real C*-algebras, Real will be one.

[Yury G. Kudryashov]

Is there a reasonable typeclass that can use forgetful inheritance here?