1/0=0

Stream: new members

[Marko Grdinić]

So it seems that 1/0 does not raise a type error in Lean. That is a surprise.

https://www.hillelwayne.com/post/divide-by-zero/

I've Googled a bit and according to this, it seems that allowing division by zero is a convention in theorem provers and Lean is not an exception. Still, shouldn't there be safe division somewhere in the library. What is it called?

[Kevin Buzzard]

What is unsafe about this? ;-)

[Kevin Buzzard]

It's completely safe because every single theorem where division by 0 isn't allowed contains the hypothesis that the denominator isn't 0 in its statement.

[Mario Carneiro]

this is what I would call a safe division, one where you don't have to worry about it blowing up on you

[Kevin Buzzard]

You should think of Lean's / as a different function to the mathematician's definition of division. It's a new function, which mathematicians should use different notation for (e.g. / with a little asterisk next to it), which is defined by x/^*y = usual x/y if y isn't 0, and 0 otherwise.

[Mario Carneiro]

That said, I know what you mean and there is a function that does division in a ring, where the second argument is a unit, and in a division ring you can construct a unit from a nonzero element

[Kevin Buzzard]

Sure you can make mathematician's /, by just defining a function from the reals times the non-zero reals to the reals, or defining a function from the reals times the reals to the type "option real" consisting of the reals plus an extra element "NaN". Indeed, when I started doing Lean i was so horrified by this convention that I made these functions.

[Kevin Buzzard]

And then I very quickly realised that they were much harder to use in practice than Lean's convention. Because with "mathematician's division" you just can't do things like a/(b/c) at all easily, because b/c is in "reals + NaN" and now you have to insert the proof that c isn't zero and then get the real out of b/c whilst in the middle of writing a mathematical statement

[Kevin Buzzard]

With Lean's convention you just do a/(b/c), don't worry about the answer, and then pick up the pieces later (the moment you start using it Lean will start asking you to prove that c isn't 0 and that b/c isn't zero, and you can do that once, at a time which is convenient for you, and just add them as hypotheses)

[Kevin Buzzard]

In summary, if you're a mathematician who wants to prove a theorem which involves a definition, it's your job to make sure that the denominator isn't zero in your theorem. If you can't do that, then it's your problem, not Lean's. If you can do it, that's great, we'll keep track of that hypothesis, but experience has shown that \^* is a much easier function to manipulate in Lean so in the proof we'd rather use that more convenient function, but we know it agrees with division whenever division makes sense, so we can glue together at the end.

[Kevin Buzzard]

(by \^* I mean Lean's non-mathematical division)

[Marko Grdinić]

@Kevin Buzzard

It's completely safe because every single theorem where division by 0 isn't allowed contains the hypothesis that the denominator isn't 0 in its statement.

Yeah, but I have to write a short program here. I mean sure, I see that there is no chance of it being wrong, but I might write a larger program in the future where this will be an issue.

I guess I'll have to define my own safe division then. Every time I will use it Lean should be able to prove automatically that the division is valid anyway.

Nans

I hate those. When I was working on the Spiral language because Nan <> Nan it turns out that you cannot memoize them and that makes the compiler diverge. I solved that issue in v0.1 by making every compile time Nan a type error. It still causes the compiler to diverge in v0.09.

[Mario Carneiro]

Yeah, but I have to write a short program here. I mean sure, I see that there is no chance of it being wrong, but I might write a larger program in the future where this will be an issue.

What, concretely, do you envision as causing a problem?

[Kevin Buzzard]

I guess I'll have to define my own safe division then. Every time I will use it Lean should be able to prove automatically that the division is valid anyway.

This is exactly how I used to feel, and if you want to try this way of doing it then you will probably learn the way I learnt that it's much more inconvenient. The big question you have is simply: what will the domain and the codomain of your function be?

[Kevin Buzzard]

There is no good answer to this domain/codomain question, as far as I can see.

[Mario Carneiro]

I guess I'll have to define my own safe division then. Every time I will use it Lean should be able to prove automatically that the division is valid anyway.

It won't be automatic, and you will start to hate life if you try to use it for too long

[Marko Grdinić]

@Mario Carneiro

import data.rat
import data.vector

def E {n} (l : vector rat (n+1)) : rat := list.foldl (+) 0 l.val / (n+1)

Here is what I am doing now. This just calculates the mean of a vector. If I mess up and write n rather than n+1, it would have been erroneous on empty vectors.

[Kevin Buzzard]

I used to be very upset about this convention. I am over it now because I simply remember that when I see / in Lean it is not mathemtician's division, it is simply another function with a bad name.

[Mario Carneiro]

This is only the weakest kind of safety that you achieve. The real safety comes from proving theorems about your definition, and you will notice immediately if you have an off by one error

[Kevin Buzzard]

This function E above will be hard to work with because you have built in your own off-by-one error-possibility in its definition. I would definitely recommend you change n+1 to n

[Kevin Buzzard]

I have been burnt by this several times. You always think it's a good idea, and then when you're writing code you're just "crap crap crap, I have this n and I know it's non-zero but I now need to feed n-1 into this function and now I have to deal with natural number subtraction which is a pain because 2-3 isn't -1 it's 0"

[Mario Carneiro]

and n-1+1 isn't definitionally equal to n, so l isn't even in the same type, so you need a cast, so now addition of vectors is borked...

[Kevin Buzzard]

With type theory you have to think about things in a slightly different way. If you define E with n's instead of n+1's then you, as someone new to this area, is thinking "oh goodness this will be horrible if n=0". But it's just like division. You're defining a function and you know you'll only be running it on positive integers, but that's fine, define it for all naturals, let it return junk for n=0, but the theorems will come out much nicer if you define it like that, and like division it doesn't matter that it's defined on a larger domain than you need.

[Kevin Buzzard]

This point of view pervades mathematics in Lean. We even defined a sheaf on an open subset U of X to just be a sheaf on X; this is a more complex example but the upshot is that we had a vast amount of extra data which was just meaningless but which was being ignored.

[Mario Carneiro]

Actually that post by hillel wayne is a good one to read for understanding this kind of approach

[Kevin Buzzard]

The aim is to get crisp clear theorems with no random +1's in. This turns out, from experience, to be a more efficient way to proceed than having functions which take n as input and return something of size n+1

[Marko Grdinić]

I found the replies here interesting.

def div (a : rat) (b : rat) {_ : 0 < b} := a / b
def E {n} (l : vector rat (n+1)) : rat := div (list.foldl (+) 0 l.val) (n+1)

Since it seems that lean cannot automatically synthesize that 0 < n+1 here in order to pass it to div, I'll go with what you suggest. I've been hoping that it would, but no way would I produce the proofs by hand for every single division. That settles it for me.

[Mario Carneiro]

There are tricks you can do to make this work in some cases (in particular, you would want that third argument in square brackets), but that needs additional setup as well, to make a typeclass for nonzeroness and some instances

[Marc Huisinga]

this is perhaps a bit more general, but my experience from doing a bit of program verification with lean is that there are essentially two ways of doing this:

you can either carry around an invariant everywhere you go or use seperate hypotheses.
for the list example, you can either use vectors that are parameterized by some n, or pass in a proof that the list you're using has the right length. the div example looks similar.

on paper, algorithms are usually proven correct using the invariant approach, but when working with a theorem prover, maintaining the invariant is a lot more effort than on paper, and the approach with separate hypotheses is usually more comfortable in my experience.

that being said, i do believe that the invariant approach can be useful, in particular when the invariant is needed for many different parts of the function you're trying to prove things for or when the invariant is very easy to maintain. if it is only needed rarely, passing in a separate hypothesis seems to be more comfortable.

[Marc Huisinga]

for another example, you can use finsets and maintain the nodup invariant by using finset functions (and then when using map and the like prove that f is an injection to maintain the invariant), or you can use multisets and just prove nodup when you actually need it in a proof. i've found both useful in different cases.

[Miguel Raz Guzmán Macedo]

Hey gang.
When I'm proving a theorem,like

  include h₁ h₂
  theorem foo : x = z :=
  begin
    rw [h₁, h₂]
  end
  omit h₁ h₂

I really like taht in VSCode I get the tactic goal to show me example what is next in the proof.

However, When I try to prove other theorems, the goal state only shows the current error.
Am I just messing up the examples?
Am I supposed to be able to view the current goal state like the Natural Number Game in the panel?
How Can I get that in VScode?

Thanks!

[Kenny Lau]

you need to put a comma

[Scott Morrison]

like so:

begin
    rw [h₁, h₂], -- now put your cursor after the trailing comma!
 end

[Kevin Buzzard]

Yes the boxes on the top right and bottom right of the natural number game are just the outputs of the two "Lean messages" options in VS Code that you can get by clicking on the weird symbols which look like piles of books