在Recurse Center的第二周，我在Rocq中形式化Dummit和Foote的《抽象代数》时，发现第一个证明练习的目标是假的。该命题声称一个函数是单射当且仅当它有左逆。但存在一个反例：设A为空集，B = {1}。空函数f: A -> B是空真单射，然而不存在函数g: B -> A，因为B非空而A为空。这个边界情况在纸上很容易忽略，但Rocq迫使我面对它。经过挣扎，我查阅了书的勘误表，发现它已被列出。这虽然令人沮丧，但独立发现它也很令人兴奋。