5 ms·

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 g

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.

SquishyPanda23 6y ago
> 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.
- jhanschoo 6y ago
  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.
e79 6y ago
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.
kmill 6y ago
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.
empath75 6y ago
> 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.
- leanuser57 6y ago
  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.
  - empath75 6y ago
    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.

SquishyPanda23 6y ago

> 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.

jhanschoo 6y ago
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.

e79 6y ago

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.

kmill 6y ago

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.

empath75 6y ago

> 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.

leanuser57 6y ago
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.
- empath75 6y ago
  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.