Coq小ネタ：関数の外延的等値性とか - 檜山正幸のキマイラ飼育記 (はてなBlog)A, Bが集合で、f, g:A→B のとき、Coqの組み込みのイコールによる f = g はあんまり具合がよくないようです。普通「関数が等しい」とは、「Aのすべての点において関数値が等しい」ことです。Coqのイコールはそうなってないのです。 そこで、ユーザー定義のイコール「≡」を次のように定義します。 f ≡ g ⇔ ∀x∈A.(f(x) = g(x)) この「≡」は外延的等値性（Extensional Equality）と呼ばれる関係です。もちろん、同値関係である必要があるので、次が要請されます。 f ≡ f f ≡ g ならば g ≡ f f ≡ g かつ g ≡ h ならば f ≡ h 3番目の法則・推移律を、x∈A の「∈A」を省略して（書くのが面倒だったので）自然演繹風の証明図を書いてみると次のようでしょう（一例です）。 (1)∀x.(f(x) = g(x)) (2)∀x.(g(
