Comment by IshKebab | Hacker News Reader

Comment by IshKebab | Hacker News Reader

Parent Full thread

I would expect it to require a proof that 1 - 2 is non-negative. That's kind of the raison d'etre of Lean isn't it?

The reason they don't do that is because Lean treats proofs as manually generated explicit objects, unlike other languages like Dafny (IIRC) where they are implicit. Requiring explicit proofs for every subtraction was presumably seen as too onerous.

Which is fine... BUT they then should have said "so we're going to define a more convenient operator which is LIKE subtraction but isn't actually standard subtraction, and therefore we won't use the standard subtraction notation for it".

If they had used something like 1 -_ 2 then that would be much less surprising because you'd think "oh right, it's the special saturating subtraction".

Similarly for Uint8.ofNat it should have been Uint8.ofNatWrapping or similar.

This shouldn't be news.

>I would expect it to require a proof that 1 - 2 is non-negative. That's kind of the raison d'etre of Lean isn't it?

The reason is to be able to write mathematical proofs, including proofs about your code, but not to attach proofs to every single function. This definition of subtraction does not prevent you from reasoning about it and requiring `a ≥ b` in the proofs/code for which this is really important.

>Requiring explicit proofs for every subtraction was presumably seen as too onerous.

Lean can deduce proofs implicitly as well. It’s just not a very reliable mechanism. That is, imagine your code breaking after an update, because Lean suddenly can’t deduce `a ≥ b` automatically for you anymore.

>Which is fine... BUT they then should have said "so we're going to define a more convenient operator which is LIKE subtraction but isn't actually standard subtraction, and therefore we won't use the standard subtraction notation for it".

What is a standard subtraction over natural numbers at all? As you know, under a standard addition natural numbers form a monoid but not a group.

> Lean can deduce proofs implicitly as well.

Sure, but you still have to explicitly ask it to.

> What is a standard subtraction over natural numbers at all?

If you need something that is always defined then you have to use a non-standard subtraction (i.e. saturating subtraction). In other words the `-` operator should not work for Nat. It should require you to use `-_`.

i agree about this point, i think this is one of the ways extensible syntax can save (or damn, like in this case) you

Reply on news.ycombinator.com