> I feel like a proof assistant is amongst the worst places to have something like this
It's one of the best places! You know how in programming, your code looks like this?
func my_function(inputs) -> output { do something }
In theorem proving, it's almost the same:
theorem my_theorem(assumptions) -> conclusion { prove something }
But there's a single crucial difference: in programming, the "do something" is really important, whereas in Lean, the "prove something" isn't important at all: as long as the typechecker is happy with it, everyone can forget about it once it's written.
So as long as your assumptions and conclusion don't involve any division by zero, it doesn't matter what goes on inside the proof.
Regarding division by zero, you sort of have three options:
* Output an error / checked null when there's division by zero.
* Require a proof that the denominator is nonzero before you're even allowed to use division.
* Allow division by zero, making it return some nonsense. Then, add an assumption that the denominator is nonzero to all your theorems about division.
The first two options (especially the second one) make the definition of functions that involve division horrifically messy. (Idk, it might be easier if Lean had exceptions, but that also sounds messy.) I think that's why Lean goes with the third option.
https://xenaproject.wordpress.com/2020/07/05/division-by-zer...