Dummit and Footeの抽象代数学におけるバグの発見

Ben Kallus Dummit and Footeの抽象代数学におけるバグの発見 Recurse Centerでの2週目に、Dummit and Footeの抽象代数学の教科書（「Abstract Algebra」という適切なタイトルのもの）をRocqで形式化しようとしていました。最初の証明演習で、提示された証明の目標が真ではないことに気づき、非常に苦労しました。これは、解明するのがフラストレーションの溜まるものでもあり、エキサイティングなものでもありました :) 定義 AからBへの関数（「f: A -> B」と表記）は、以下の条件を満たすペアの集合です。 各ペアの最初の要素はAから来ます。 各ペアの2番目の要素はBから来ます。 Aの各要素は、ペアの最初の要素としてちょうど1回現れます。 言い換えれば、プログラマーの皆さんにとって、関数はすべての入力-出力ペアの集合によって定義され、決定論的でなければなりません。 関数が単射であるとは、2つの異なる入力が同じ出力にマッピングされない場合です。例えば、f: int -> int を f(x) = x^2 とする関数は、f(1) = f(-1) であるため単射ではありません。 関数 f: A -> B が左逆元を持つとは、すべての a in A に対して g(f(a)) = a となるような関数 g: B -> A が存在する場合です。言い換えれば、fの左逆元はfを「元に戻す」操作です。 命題1 (1) この本での最初の証明演習は、関数が単射であることと、それが左逆元を持つことが同値であることを示すことです。この命題は偽です。 A = {}（空集合）、B = {1} とします。関数 f: A -> B = {} とします。この関数fは、上記の定義にリストされている3つの基準を満たすため、確かに関数です。関数fは、2つの異なる入力が同じ出力にマッピングされないということが（空虚に）真であるため、単射です。しかし、BからAへの関数が存在しないため、fは左逆元を持ちません。 もし私がこの演習を紙で行っていたら、このコーナーケースを思いつくことはなかったでしょう。Rocqを使用していたため、命題がそのままでは証明できないという壁にぶつかり続けました。私が考えた証明方法はいずれも、Aが空でないか、またはBが空でないことを必要としました。長すぎる時間を費やした後、命題自体が真ではないのではないかと思い始め、そして今に至ります :) この投稿を書いている間に、本の正誤表を確認したところ、これはすでに記載されていました。まあ、仕方ありません :)