Zulip Chat Archive
Stream: new members
Topic: Square root of -1 as a Real
Dan Abramov (Mar 12 2025 at 12:34):
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 whatReal.sqrt (-1)
actually is, and it doesn’t even matter, because I am a mathematician, so I only runReal.sqrt
on non-negative real numbers. If I want to take the square root of a negative number, I useComplex.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 functionf
on the real numbers, byf(x) = sqrt(x)
forx ≥ 0
, andf(x) = 37
ifx<0
. Does defining such a function lead to a contradiction in mathematics? Of course it does not! That’s whatReal.sqrt
looks like (although they might have chosen0
orsqrt(-x)
for the output whenx
was negative – who knows, and who cares). The trick is that it is in the theorems aboutReal.sqrt
where the hypotheses of nonnegativity appear. For example, it is probably not true thatReal.sqrt (a * b) = Real.sqrt (a) * Real.sqrt (b)
in general, becausea
orb
might be negative. However it is true thatReal.sqrt (a * b) = Real.sqrt (a) * Real.sqrt (b)
ifa ≥ 0
andb ≥ 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 (Mar 12 2025 at 12:37):
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 (Mar 12 2025 at 12:39):
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 (Mar 12 2025 at 12:39):
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 (Mar 12 2025 at 12:46):
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 (Mar 12 2025 at 12:47):
Kevin should quote his own blog here!
Aaron Liu (Mar 12 2025 at 12:49):
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 (Mar 12 2025 at 12:58):
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 (Mar 12 2025 at 13:12):
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 (Mar 12 2025 at 13:13):
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 . In this case is true without any assumption, and the idiomatic way of stating this in mathlib is in full generality.
Riccardo Brasca (Mar 12 2025 at 13:14):
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 (Mar 12 2025 at 13:15):
Note that if you really want you can prove in this way statement that are mathematically false, like .
Riccardo Brasca (Mar 12 2025 at 13:16):
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 (Mar 12 2025 at 13:22):
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 (Mar 12 2025 at 13:24):
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 (Mar 12 2025 at 13:36):
You can google "checking formalized mathematics" or something similar to understand this is not a trivial job. Here an interesting article.
Damiano Testa (Mar 12 2025 at 13:47):
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 (Mar 12 2025 at 14:43):
@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 (Mar 13 2025 at 19:52):
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 (Mar 14 2025 at 08:58):
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 (Mar 14 2025 at 09:11):
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 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 (Mar 14 2025 at 09:51):
Mario Carneiro said:
But now suppose you want to rewrite the
x + y
toy + x
. If you userw [add_comm]
you will get amotive 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, andrw
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 (Mar 14 2025 at 11:40):
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.
Last updated: May 02 2025 at 03:31 UTC