Stream: new members

Topic: hyperreal.lean in math lib

Dan Stanescu (Mar 08 2020 at 16:39):

Hi all,
Just browsed through this file and bumped into this at line 199:

theorem st_infinite {x : ℝ*} (hi : infinite x) : st x = 0 :=
begin
unfold st, split_ifs,
{ exact false.elim ((infinite_iff_not_exists_st.mp hi) h) },
{ refl }
end


It looks like this is defining the standard part of an infinite hyperreal to be zero. It also is at odds with the stuff just above, like for example infinite_iff_not_exists_st. To the best of my recollection, the standard part of an infinite hyperreal is not defined; it is the infinitesimals that have standard part zero, as per line 121 in the same file: def infinitesimal (x : ℝ*) := is_st x 0. Since I'm pretty new with Lean, is there anything I'm missing here - is this needed to fix some technical issue? Or is this something else, like a typo?

Kevin Buzzard (Mar 08 2020 at 16:40):

Did you know that Lean thinks that 1/0=0?

Kevin Buzzard (Mar 08 2020 at 16:40):

Whereas mathematicians think it's not defined.

No.

Kevin Buzzard (Mar 08 2020 at 16:40):

This is some weird computer science thing -- if something isn't defined, they want to define it to be 0.

Kevin Buzzard (Mar 08 2020 at 16:41):

This is all over the library -- the sup of a set of reals which isn't bounded above, or is empty, is zero.

Dan Stanescu (Mar 08 2020 at 16:41):

OK, that's along the lines of what I expected.

Kevin Buzzard (Mar 08 2020 at 16:42):

You might think this is insanity (I certainly did at first) -- but what's happening is that the definitions are "liberal" and then the hypotheses are in all the theorems, e.g. the theorem that a/b*b=a has the hypothesis that b isn't zero.

Dan Stanescu (Mar 08 2020 at 16:42):

So we just need to be careful with how we use these.

Not really!

Kevin Buzzard (Mar 08 2020 at 16:44):

In some sense, this idea is better than the mathematician's idea of "just go ahead and write stuff and let the reader implicitly do the work in checking that it's well-defined"

Kevin Buzzard (Mar 08 2020 at 16:45):

The point is no theorems apply to a/b if b is actually zero, so if you accidentally divide by zero then you're not going to be able to prove anything about your result anyway. In some sense this stops you having to worry about these issues. But if you want to think about it as being careful -- I contend that you have to be no more careful than if you're doing normal mathematics.

Kevin Buzzard (Mar 08 2020 at 16:46):

Another way of thinking about it is that when you see / in Lean it's not "mathematician's /", it's something which should be called $/^*$ or something, which agrees with $/$ whenever $/$ is defined, and returns goodness knows what when $/$ isn't defined.

Kevin Buzzard (Mar 08 2020 at 16:47):

The place you have to be careful is in the statements of your theorems. In your proofs you don't have to be careful at all, because you could imagine that the first line of your proof is "let's define a function $/^*$ by $a/^*b=0$ if $b=0$ and $a/^*b=a/b$ otherwise. Then..."

Kevin Buzzard (Mar 08 2020 at 16:49):

So similarly this function st should be interpreted as "the function which sends a hyperreal with a standard part to its standard part, and which sends a hyperreal with no standard part to 0"

Dan Stanescu (Mar 08 2020 at 16:49):

I guess another way one can think about it is that from the CS perspective, 0 is just false. Or the empty set. So yes, it makes sense but I'm still glad I asked. Thank you @Kevin Buzzard

Kevin Buzzard (Mar 08 2020 at 16:49):

and because a mathematician would never dream of applying this function to a hyperreal which doesn't have a standard part, we should never notice :-)

Dan Stanescu (Mar 08 2020 at 16:50):

Right, except when you browse through the file.

Kevin Buzzard (Mar 08 2020 at 16:50):

The computer scientists are particularly proud of lemmas like (a+b)/c=a/c+b/c, which they proudly tell us are also true when c=0 (although they wouldn't be true if we defined a/0 to be 37, which was something I pushed for for a while, to no avail)

Kevin Buzzard (Mar 08 2020 at 16:50):

There has been some talk recently of adding a/0=0 as an axiom to the definition of a field!!

Kevin Buzzard (Mar 08 2020 at 16:51):

The advantage of this is that the corresponding structures would then biject with what mathematicians regard as fields.

Dan Stanescu (Mar 08 2020 at 16:56):

I guess this must have been contemplated: couldn't hyperreal.lean be used to deal more easily with function continuity?

Kevin Buzzard (Mar 08 2020 at 16:58):

I think this was part of @Abhimanyu Pallavi Sudhir 's original plan -- in fact I think he wanted to do differentiability using them -- but I think there are some technical issues involving meta-level reasoning somehow? I've forgotten the details.

Abhimanyu Pallavi Sudhir (Mar 08 2020 at 18:13):

You need the transfer theorem. Although it can probably be accomplished using tactics.

Chris Hughes (Mar 08 2020 at 18:51):

Kevin Buzzard said:

There has been some talk recently of adding a/0=0 as an axiom to the definition of a field!!

This has happened

Reid Barton (Mar 08 2020 at 19:51):

My personal opinion is that this extension by zero stuff is indeed more convenient in a formal theorem prover but mainly because of a lack of automation

Last updated: May 10 2021 at 18:22 UTC