During my second week at the Recurse Center, I've been trying to formalize Dummit and Foote's abstract algebra textbook (appropriately titled "Abstract Algebra") in Rocq. I had quite a hard time with the first proof exercise in the book because the stated proof goal is not true. This was both frustrating and exciting to figure out :)
A function f from a set A to a set B (written "f: A -> B") is a set of pairs such that
A function is injective if no two distinct inputs map to the same output. For example, f: int -> int by f(x) = x^2 is not injective because f(1) = f(-1).
A function f: A -> B has a left inverse if there exists a function g: B -> A such that forall a in A, g(f(a)) = a. In other words, f's left inverse "undoes" f.
The first proof exercise in the book is to show that a function is injective if and only if it has a left inverse.
This statement is false. Let A = {}, and B = {1}. Let f: A -> B = {}. The function f is indeed a function because it satisfies the 3 criteria listed in the definition above. The function f is injective because it is (vacuously) true that no two distinct inputs map to the same output. However, f does not have a left inverse, because there are no functions from B to A.
I probably wouldn't have thought of this corner case if I was doing this exercise on paper. Because I was using Rocq, I just kept running into walls trying to prove the proposition as stated. All the ways I could think of proving the statement required either that A be inhabited or that B be uninhabited. After way too long, I started to wonder if the proposition just wasn't even true, and here we are :)
While writing this post, I checked the book's errata, and this is already in there. Oh well :)