alt Hacker NewsI don't understand why they would make such footgun functions either, especially because (IIUC, and I probably don't) in a way the whole point of Lean's dependent type system is to be able to express arbitrary constraints on the inputs of these functions so that they can be total -- e.g., to be able to define a subtraction function on the nonnegative integers that takes one integer and one {integer that is less than or equal to the first integer}. And to even call this function, you (or perhaps Lean itself) would need to first prove that its second argument is less than or equal to its first.
Replies
There’s a good blog post on this by Kevin Buzzard. I suggest to give it a read: https://xenaproject.wordpress.com/2020/07/05/division-by-zer...
I found the last section especially helpful.
This is a topic of contention in formalized math with no universal right answer. Some libraries go heavy on the dependent types, and some like mathlib try to avoid them. I do math in both Rocq and Lean and I find I like the latter style a lot more for my work for a couple reasons:
- Fewer side conditions: Setting a / 0 = 0 means that some laws hold even when a denominator is 0, and so you don't need to prove the denominator is nonzero. This is super nice when the denominator is horrible. I heard once that if you set the junk value for a non-converging Riemann integral to the average of the lim sup and lim inf you can obliterate a huge number of integrability side conditions (though I didn't track down this paper to find out for sure).
- Some of the wacky junk arithmetic values, especially as it relates to extended reals, do show up in measure theory. Point being: "junk arithmetic" is a different mathematical theory than normal math, but it's no less legitimate, and is closely related.
- Definition with Hilbert's epsilon operator. If I want to define a function that takes eg. a measurable set S as an argument, I could do the dependent types way
def MyDef (S) (H : measurable S) := /-- real definition -/
but then I need to write all of my theorems in terms of (MyDef S H) and this can cause annoying unification problems (moreso in Rocq than in Lean, assuming H is a Prop). Alternatively, I could use junk math
def MyDef' (S) := if (choose (H : measurable S)) then /-- real definition -/ else /-- junk -/
I can prove (MyDef' S = MyDef S H) when I have access to (H : measurable S). And the property H here can be be really complex, convergence properties, existence properties, etc. It's nice to avoid trucking them around everywhere.
You can express those constraints; it just turns out to be less ergonomic in practice if you do. (You can even do so in terms of the junk-valued total functions! Just define `actual_subtraction` to call straight through to `junky_subtraction`, but `actual_subtraction` has these constraints on its domain.)
The mathlib way to do things is to push those requirements out to the one who wishes to use the theorem. If you find that you're depending on a junk value in a way that's incompatible with what you wanted to prove, then you've simply discovered that you forgot to restrict your own domain to exclude the junk. (And if your desired usage lines up with the junk, then great, you get to omit an annoying busywork hypothesis.) A sqrt function that gives 0 on the negatives isn't breaking any of sqrt's properties on the positives!
The mathlib way means that instead of every function having to express these constraints and pass proofs down the line, only some functions have to.