Square root of -1 as a Real

Stream: new members

[Dan Abramov]

So I was reading a section on Reals from Kevin's course notes and this stood out to me:

So what happens if you feed in -1 or some other negative number? Lean doesn’t give you an error! It just spits out some arbitrary answer – for all I know, Real.sqrt (-1) = 37. I have no idea what Real.sqrt (-1) actually is, and it doesn’t even matter, because I am a mathematician, so I only run Real.sqrt on non-negative real numbers. If I want to take the square root of a negative number, I use Complex.sqrt. Perhaps you are worried that such a cavalier attitude towards square roots of negative numbers leads to contradictions in the system – but it does not. The simplest way to explain why is the following. Let me define a function f on the real numbers, by f(x) = sqrt(x) for x ≥ 0, and f(x) = 37 if x<0. Does defining such a function lead to a contradiction in mathematics? Of course it does not! That’s what Real.sqrt looks like (although they might have chosen 0 or sqrt(-x) for the output when x was negative – who knows, and who cares). The trick is that it is in the theorems about Real.sqrt where the hypotheses of nonnegativity appear. For example, it is probably not true that Real.sqrt (a * b) = Real.sqrt (a) * Real.sqrt (b) in general, because a or b might be negative. However it is true that Real.sqrt (a * b) = Real.sqrt (a) * Real.sqrt (b) if a ≥ 0 and b ≥ 0, and this is the theorem in the library. So you do have to check that you’re not taking the square roots of negative numbers – just not where you might expect.

This freaked me out a bit so I'm trying to reconstruct my mental model after this devastating blow. I want to understand this from the first principles. Why is it that the hypothesis is not "needed" at Real.sqrt stage? And if it only shows up later when I use the theorems, what (in Mathlib? in Lean?) ensures that no one "forgot" to enforce this constraint in all the relevant theorems about square roots? Does the need for nonnegativity emerge from the structure of how roots are defined but is also somehow naturally delayed until some fact about it is retrieved? I guess this is similar to how I can define 0 / 0 but then wouldn't be able to "work" with it?

I feel like this almost makes sense but I'm struggling to convince myself that something underneath is holding all of this to be sound.

[Weiyi Wang]

https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Real/Sqrt.html#Real.sqrt
Maybe I missed something, but the doc says it returns 0 for negative numbers?

[Dan Abramov]

So I think it's really two different questions:

• "How": What mechanism ensures that at some point nonnegativity would have to be checked? Presumably, if it's ensured by the system, it's also encoded somewhere in the structure of the "square root" itself, even if we don't have to "fill it in" during a call. So where is it?

• "Why": Is there a need and/or a benefit to this kind of delayed justification? Could we define Real.sqrt as accepting the nonnegativity and "carrying" it? I guess this would force the return value to be a different structure from normal \R which would be inconvenient? Is there some reason why it just can't be "filled in" early?

[Dan Abramov]

https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Real/Sqrt.html#Real.sqrt
Maybe I missed something, but the doc says it returns 0 for negative numbers?

Right, my question is more philosophical — I'm asking why it's designed this way.

[Aaron Liu]

Dan Abramov said:

• "How": What mechanism ensures that at some point nonnegativity would have to be checked? Presumably, if it's ensured by the system, it's also encoded somewhere in the structure of the "square root" itself, even if we don't have to "fill it in" during a call. So where is it?

Real.sqrt is defined something like fun x => if h : 0 ≤ x then (NNReal.sqrt ⟨x, h⟩).toReal else 0. When you prove stuff about Real.sqrt, you have to do a case split on this if-then-else block, and sometimes you need the assumption that 0 ≤ x to discard the else branch.

[Riccardo Brasca]

Kevin should quote his own blog here!

[Aaron Liu]

Dan Abramov said:

• "Why": Is there a need and/or a benefit to this kind of delayed justification? Could we define Real.sqrt as accepting the nonnegativity and "carrying" it? I guess this would force the return value to be a different structure from normal \R which would be inconvenient? Is there some reason why it just can't be "filled in" early?

That's docs#NNReal.sqrt, which also exists, and you can use it. But you can't plug in real numbers, you have to use NNReal.

[Dan Abramov]

OK so reading Kevin's post about defining square root is helpful and helps me refine my question. If I were setting up my own sqrt from scratch, and if I did not follow Kevin's original approach (i.e. if I did similar to Mathlib and allowed any \R inputs), would anything in Lean force me to make sure my theorems about sqrt took the nonnegativity hypothesis? Or would I be able to define it unsoundly and still have the proofs type check? (I don't mean it as "Lean core has some opinions about square roots" but more like, if math needs this constraint to be sound, surely this soundness has to creep up on me somewhere, as long as I'm not just defining new axioms?)

Not sure if this makes sense. I'm mostly trying to understand whether anything "forces" the existing Mathlib theorems about square root to have the nonnegativity constraint, or whether it relies on the maintainers being careful. (There's also a question whether a structure like NNReal is essential to developing theorems about a square root — and that's what provides this enforcement — or whether it would be possible to develop the same user-facing theorems without a structure like this internally.)

[Arend Mellendijk]

Any theorem mentioning Real.sqrt might indeed not mean what you expect it to mean, and you do have to be a little careful when reading such a theorem. Two points though - (1) the theorems are still true, and (2) you can still use Real.sqrt to prove theorems that don't mention Real.sqrt at all. At no point does using this definition introduce soundness issues.

Indeed the nonnegativity constraint is not generally enforced in mathlib: consider Real.sqrt_inv

[Riccardo Brasca]

Let's imagine that your definition is

fun x => if h : 0 ≤ x then (NNReal.sqrt ⟨x, h⟩).toReal else (NNReal.sqrt ⟨-x, ...⟩).toReal

so in practice $\sqrt{-4}= \sqrt{|4|}=2$. In this case $\sqrt{xy}= \sqrt{x}\sqrt{y}$ is true without any assumption, and the idiomatic way of stating this in mathlib is in full generality.

[Riccardo Brasca]

The idea is that if you want to mathematically use the theorem you do it in the case both x and y are positive, and it says what you want. The fact that it doesn't ask for those assumptions may be surprising, but it doesn't say something false.

[Riccardo Brasca]

Note that if you really want you can prove in this way statement that are mathematically false, like $\exists x \neq 4, \; \sqrt{x} = 2$.

[Riccardo Brasca]

but this is a more philosophical question: checking that a Lean statement means what you have in mind cannot be done by a computer, that does not know what you have in mind. (In practice asserting the existence of something is probably the only way of doing this.)

[Riccardo Brasca]

It's not about soundness, it's about translating what a human being has in mind to Lean. This is checked by other human beings, and in general it is a nontrivial task (are you sure Lean real numbers are what you think they are? You can check the definition of course, but at some point you just trust that nobody cheated in defining, say, the addition of natural numbers)

[Riccardo Brasca]

You can have a look at post where we explain why we claimed to have formalized a theorem in some paper (the actual statement doesn't matter, the point is "we have a proof of something, is this something the theorem we wanted?")

[Riccardo Brasca]

You can google "checking formalized mathematics" or something similar to understand this is not a trivial job. Here an interesting article.

[Damiano Testa]

In direct analogy with division by zero, a theorem that must assume 0 ≤ x is the equality x.sqrt ^ 2 = x.

With Riccardo's "extension", the analogous theorem would be x.sqrt ^ 2 = x.abs which works for all x.

With mathlib's convention, the analogous theorem would be x.sqrt ^ 2 = max x 0 which works for all x.

Notice that over the "interesting" domain, the two conventions give you the same result. You are simply able to prove other theorems, depending on which definition you use.

[Johan Commelin]

@Dan Abramov One reason, in my opinion, to not include the condition hx : 0 <= x or hx : x \ne 0 in things like sqrt x or 1 / x, is because now we can have nice notation. Our usual notation does not have a slot where we can add the extra argument that proves the side condition.

And notation is worth a lot...

[Mario Carneiro]

There is a more technical / pragmatic reason to not want to have sqrt be a function with the type sqrt (x : ℝ) (hx : x ≥ 0) : ℝ, which is that this makes sqrt have a dependent type (the type of hx depends on x), and that can cause very annoying rewrite blockage. For example, suppose you have a goal that has sqrt (x + y) (...) in it, where ... is a proof that x + y ≥ 0. The usage of the dependent type here means that you are forced to prove that x + y ≥ 0 upfront, which is what we signed up for, so everything is looking as expected so far.

But now suppose you want to rewrite the x + y to y + x. If you use rw [add_comm] you will get a motive is not type correct error, and this is an extraordinarily frustrating experience because all of the workarounds are very verbose. What is happening is that rw tries to rewrite the goal to sqrt (y + x) (...), where the ... is the same as before, and in particular it still has type x + y ≥ 0, which is a problem since it's now supposed to be a proof of y + x ≥ 0. This is of course also true but the proof of y + x ≥ 0 is different from the proof of x + y ≥ 0, and rw tried to rewrite only one piece of it. To do this rewrite properly you have to replace both terms at the same time, and rw isn't equipped to do that because rewriting the proof is much more than a find and replace job.

By making the function simply typed, even if it's just a wrapper around the dependently typed function like this, this issue disappears and you can perform rewrites under the sqrt freely.

[Riccardo Brasca]

A mathematician would probably say that the "right" solution is to consider a function ℝ≥0 → ℝ≥0, that has not this problem (of curse it has the problem that now we cannot apply it to π).

[Oliver Nash]

If I was informally discussing the square root with someone I would defer being precise about the details until they mattered.

E.g., I might say "well $\sqrt{tr(A^tA)}$ is an integer and so ..." and only later when I wanted to justify some claim would I confront issues like the trace being non-negative.

This is exactly the sort of freedom the junk-value pattern gives us here.

[Eric Wieser]

Mario Carneiro said:

But now suppose you want to rewrite the x + y to y + x. If you use rw [add_comm] you will get a motive is not type correct error, and this is an extraordinarily frustrating experience because all of the workarounds are very verbose. [...] To do this rewrite properly you have to replace both terms at the same time, and rw isn't equipped to do that because rewriting the proof is much more than a find and replace job.

This example feels weak to me; simp_rw can handle such a rewrite IIRC, and I think there's a thread about a version of rw that can handle such dependent goals (by inserting casts into the proofs)

[Mario Carneiro]

That's why I called it a pragmatic issue, not a theoretical one. Sure you can have tactics that work around this issue, and there are proof assistants that do this systematically and partial functions are all the rage there. Lean is not such a system, and you will frequently run into rough edges when working with dependent types.