Comment by jhanschoo | Hacker News Reader

Comment by jhanschoo | Hacker News Reader

Parent Full thread

I don't understand what you mean. You still have the different obvious ways of formulating, e.g. division in type theory:

1. The article's way: "R^2->R", but garbage value for 0 in the second argument.

2. What you propose: "R^2->Maybe R"

3. The mathematician's dependent-type-theoretic way "R * (x:R, proof that x!=0) -> R",

4. the conventional way "R * (R\{0}) -> R".

They have their advantages and disadvantages. The first is useful in proof verification since it simplifies most proofs, from which perspective this garbage value of 0 is actually well-behaved, and doesn't need to be handled as a special case. But you allow seemingly nonsense theorems when you forget to condition (x>0).

What you propose is similar, except that you are forced to reason about whether the output value is valid.

3 and 4 are tedious, since you always need to prove that the inputs are nonzero. 4 is more tedious since you have merely shifted the problem of handling the zero case into proving properties about the canonical embedding "R->R\{0}" (which must still have a garbage value for 0). On the upside, these functions surject into R.

By the way, 3 and 4 are pretty much the same in Lean, assuming you define "R\{0}" using complementation rather that somehow defining the nonzero reals from scratch.

> But you allow seemingly nonsense theorems when you forget to condition (x>0).

Such as what? I’ve only spent a few hours with lean, but I’m fairly sure that any attempt to prove something silly would fail because it would catch the weird behavior of 0.

For example. If you tried to use a/a = 1 as the article mentions, you’d be unable to prove it without adding the condition that a != 0, and you’d be unable to use it further on without that condition in place.

Here is a "nonsense" theorem that is provable in Lean:

“There exists a real number r such that 1/r = 0.”

If you try to translate this theorem into maths, you will run into trouble at some point. At which point exactly depends on how you want to make things precise... which is exactly what mathematicians avoid when talking about division in fields.

That’s a perfectly sensible function, it’s just not ordinary division on the reals where x = 0, and you can’t use it that way.

I agree that they all have their advantages and disadvantages. My point was agreeing with the author that a proof assistant returning 0 for n/0 isn’t nonsensical. It’s debatable whether it is the best approach, but it is sound. The reasoning is clear if you consider R to be an inductive type, which many proof assistants including Lean do. Returning anything but an element of an inductive type would be wrong.

> 3 and 4 are tedious, since you always need to prove that the inputs are nonzero.

Or assume it. This is what you have to do in real life anyway. If you can't assume the inputs are nonzero you have to prove it. Otherwise the proof doesn't work.

As the article mentions, it doesn't necessarily work this way in a verified proof. Every time you form an expression involving division, you have to supply the proof. It is this repeated supplying of a proof (not necessarily having to reprove it) that is omitted in regular informal proofs that is tedious. In certain situations you can write automation to help you with that. But more frequently, you already have automation for other aspects of your proof, and this need to prove this is tripping up your other automation.

Reply on news.ycombinator.com