Wow, okay. I would imagine this makes mathematicians quite angry? I guess you're responsible for all the operations you use in your proof being well-behaved.
It sounds like subtraction over Nats needs to be split into `sub?`, and `sub!`, the former returning an option, and the latter crashing, on underflow, as is the Lean convention?
To use the default `sub`, you should need to provide a witness that the minuend is >= the subtrahend...
The version with silent underflow is still useful, it should just be called `saturatingSub`, or something, so that mathematicians using it know what they're getting themselves into...
Wow, okay. I would imagine this makes mathematicians quite angry? I guess you're responsible for all the operations you use in your proof being well-behaved.
It sounds like subtraction over Nats needs to be split into `sub?`, and `sub!`, the former returning an option, and the latter crashing, on underflow, as is the Lean convention?
To use the default `sub`, you should need to provide a witness that the minuend is >= the subtrahend...
The version with silent underflow is still useful, it should just be called `saturatingSub`, or something, so that mathematicians using it know what they're getting themselves into...
TIL that "junk theorems" are a thing in mathematics. Not being a mathematician myself, I found this [1] article a useful primer.
[1] https://www.cantorsparadise.com/what-are-junk-theorems-29868...
I don't understand. What does this mean?
The following are equivalent: