hyperreal.lean in math lib

Stream: new members

[Dan Stanescu]

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]

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

[Kevin Buzzard]

Whereas mathematicians think it's not defined.

[Dan Stanescu]

No.

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

Not really!

[Kevin Buzzard]

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]

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]

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]

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]

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]

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]

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]

Right, except when you browse through the file.

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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

[Dan Stanescu]

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

[Kevin Buzzard]

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]

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

[Chris Hughes]

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]

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