Formalizing Abstract Algebra in Rocq Uncovers a Bug in Dummit and Foote
Finding a bug in Dummit and Foote's Abstract Algebra
During his second week at the Recurse Center, Ben Kallus attempted to formalize Dummit and Foote's Abstract Algebra textbook in the Rocq proof assistant. He discovered that the first proof exercise—proving a function is injective if and only if it has a left inverse—is false due to a corner case involving the empty set. The bug is already listed in the book's errata, but Kallus's experience highlights the value of formal verification in catching subtle mathematical errors.
I probably wouldn't have thought of this corner case if I was doing this exercise on paper.
- generationP
This one is not just in Dummit and Foote; it's just too easy to miss. I'd guess it appears in half the places that state this result. Fixed it in my own lecture notes a few months ago.
- Paracompact
It warms my heart every time I see an interactive proof assistant being used to improve rather than simply slow down mathematical thinking.
After years of using the things, I believe not enough focus is given to high-velocity uses of proof assistants for prototyping. They can altogether replace scratch paper for fumbling around with new concepts.
- troethe
While the proposed fix of requiring "either that A be inhabited or that B be uninhabited" works, it seems tacked on just to solve this particular edge-case.
I think a more elegant solution would be to soften the definition of a left inverse from a function `g: B -> A` to a function `g: f(A) -> A` where `f(A)` is the subset of elements in `B`, that actually get mapped to by `f` or in the words of the book's function definition, the set of "right" elements in `f`.
This solves the edge-case too, as `f(A) = f({}) = {}` and there exists (exactly one) function `g: {} -> {}`, which also trivially is a left inverse of `f`.
The real problem here was, that the statement `g: B -> A` needlessly required `g` to map back elements in B to A, that couldn't even be produced by `f` and should therefore be irrelevant for a left inverse.
- jonlong
What I would add here is that the property of left-cancellation is exactly equivalent to injectivity, i.e., f : A -> B is injective iff, for any g, h : C -> A, f o g = f o h implies g = h. If A = {} then f is injective and left-cancellative, both vacuously.
The subtlety is now that left-cancellativity is not equivalent to having a left inverse, for exactly the reason pointed out.
The value of this observation is that left-cancellativity is a useful generalization of injectivity that works in any category, where left-cancellative morphisms are called monomorphisms. If you already know about monomorphisms, it's easier to notice that there's something "off" about D&F's exercise!
- hyperhello
I don’t think it’s fair to call {}-> injective just because no two inputs map to the same output. That’s vacuous.