Zulip Chat Archive

Stream: new members

Topic: hyperreal.lean in math lib


view this post on Zulip 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?

view this post on Zulip Kevin Buzzard (Mar 08 2020 at 16:40):

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

view this post on Zulip Kevin Buzzard (Mar 08 2020 at 16:40):

Whereas mathematicians think it's not defined.

view this post on Zulip Dan Stanescu (Mar 08 2020 at 16:40):

No.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Dan Stanescu (Mar 08 2020 at 16:41):

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

view this post on Zulip 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.

view this post on Zulip Dan Stanescu (Mar 08 2020 at 16:42):

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

view this post on Zulip Kevin Buzzard (Mar 08 2020 at 16:43):

Not really!

view this post on Zulip 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"

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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=0a/^*b=0 if b=0b=0 and a/b=a/ba/^*b=a/b otherwise. Then..."

view this post on Zulip 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"

view this post on Zulip 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

view this post on Zulip 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 :-)

view this post on Zulip Dan Stanescu (Mar 08 2020 at 16:50):

Right, except when you browse through the file.

view this post on Zulip 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)

view this post on Zulip 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!!

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Abhimanyu Pallavi Sudhir (Mar 08 2020 at 18:13):

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

view this post on Zulip 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

view this post on Zulip 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