うーむ、話はそんなに単純じゃないみたい。
「Coq小ネタ：関数の外延的等値性とか」において、f, g:A→B に対して、f ≡ g ⇔ ∀x.(f(x) = g(x)) として、関数の外延的等値性「≡」を定義したのですが、これではすぐにボロが出ますね。
f ≡ g を定義するために f(x) = g(x) を使ってますが、f, g:A→(B→C) になると、イコール記号「=」は関数集合 B→C の組み込みイコールの意味になります。関数集合の組み込みイコール「=」が具合が悪いから外延的イコール「≡」を導入したはずなのに、これじゃ元も子もない。
f ≡ g ⇔ ∀x.(f(x) ≡ g(x)) とすべきですね。同じ記号「≡」を使っているので分かりにくいですが、もっと一般に集合X上に同値関係「〜」があるとします。X上の「〜」は適切な同値関係だとすれば、f, g:A→X に対して f ≡ g ⇔ ∀x.(f(x) 〜 g(x)) と定義するのが適切でしょう。X = (B→C) のときは、適切な同値関係が、B→C 上の外延的等値性なわけです。
B→C 上の外延的等値性の定義には、さらにC上の適切な同値関係が必要です。となると、特定の集合にだけ適切な同値関係を考えていてもダメで、すべての集合に同値関係を添えておく必要があります。集合とその上の同値関係の組をセットイド（setoid）と呼ぶので、セットイドの世界を作って、そこで議論することになりますね。
tmiyaさんがコメントで「同値関係を自分で定義するには setoid を使う必要があります」とおっしゃってましたが、Coqの標準ライブラリには確かにSetoidというのがあります。これを使えばいいのかも知れません。
と、そんな面倒な話があるのですが、それとは別に、イイカゲンですが外延的等値性「≡」を定義した後で2つ困ったことに出会いました。
- セクション（Section）のなかでノーテーション定義した記号「≡」がセクションを出たら使えない。
- 組み込みのタクティクreflexivity、symmetry、transitivityを使って「≡」に関する推論が行えない。
一番目のノーテーションの問題は今も分かりません。Global NotationとかNotation Globalとかやってみたのですが構文エラー。ext_eqという名前はセクションの外でも使えるのに、それと一緒に定義した記号「≡」が使えないのは不便なんですけど。ノーテーションの有効範囲ってそんなもんなの？
二番目の問題はtmiyaさんのスライド（7枚目）に解決法が書いてありました。Add Parametric Relation というコマンドで、ユーザー定義の同値関係を登録すると、reflexivity、symmetry、transitivityがその同値関係を認識してくれるようになります。これは便利。詳しくはCoqリファレンスマニュアルの"Chapter 26 User defined equalities and relations"。
Require Import Utf8_core. Section 関数の外延的等値性. (* ... 省略 ... *) End 関数の外延的等値性. (* しょうがないので、 * セクションの外でノーテーションを再定義 *) Notation "f ≡ g" := (ext_eq f g) (at level 75, no associativity). Require Import Setoid. Add Parametric Relation (A B: Set) : (A->B) (@ext_eq A B) reflexivity proved by (ext_eq_refl A B) symmetry proved by (ext_eq_sym A B) transitivity proved by (ext_eq_trans A B) as ext_eq_rel. (* タクティクを使ってみる *) Goal ∀(f:nat->nat), f ≡ f. Proof. intro f. reflexivity. Qed. Goal ∀(f g:nat->nat), f ≡ g → g ≡ f. Proof. intros f g. symmetry. assumption. Qed. Goal ∀(f g h:nat->nat), f ≡ g → g ≡ h → f ≡ h. Proof. intros f g h. intro. transitivity g. assumption. assumption. Qed.
