Re:Junk Theorems in Lean
by 414owen on Saturday December 27, 2025 @06:49AM
(#46401140)
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...
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...