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(x) = h(x))
--------------------------------------------1[∧導入]
∀x.(f(x) = g(x)) ∧ ∀x.(g(x) = h(x))
----------------------------------------2[補題]
∀x.(f(x) = g(x) ∧ g(x) = h(x))
----------------------------------------3[∀除去]
f(x) = g(x) ∧ g(x) = h(x)
----------------------------------------4[等号の推移律]
f(x) = h(x)
----------------------------------------5[∀導入]
∀x.(f(x) = h(x))
----------------------------------------6[→導入 (2)]
∀x.(g(x) = h(x))→∀x.(f(x) = h(x))
----------------------------------------------------------7[→導入 (1)]
∀x.(f(x) = g(x))→(∀x.(g(x) = h(x))→∀x.(f(x) = h(x)))ここで、2番の推論（横線）の「補題」とは次の命題を想定しています。
- (∀x.P(x) ∧ ∀x.Q(x))→∀x.(P(x) ∧ Q(x))
また、3番の「∀除去」は次の命題が背後にあると考えることができます。
- (∀x.P(x))→P(a)
≡の推移律を示すために、最初僕は、上の証明図をそのままCoqに引き写そうと考えていました。結果的には違った形になったのですが、最初にやったことを記してみます。上記2つの補題を準備したのです。
Require Import Utf8_core. Section 補題の準備. Variable A: Set. Variable (P Q: A → Prop). (* 全称命題2つの連言から、連言の全称を導く *) Lemma univConj_to_conjUniv: (∀x:A, P x) ∧ (∀x:A, Q x) → ∀x:A,(P x ∧ Q x). Proof. intros H x. destruct H as [H1 H2]. split. apply H1. apply H2. Qed. (* 全称命題から具体例（インスタンス）を導く *) Lemma univ_inst: ∀a:A, (∀x:A, P(x))→ P(a). Proof. intros a H. apply H. Qed. End 補題の準備.
実際には、準備した補題は不要でした。「∀除去」を逆向きにたどるには、univ_instのような補題を準備しなくても、generalizeというタクティクがあります。
∀x:A.P(x) (a:A)
-------------------↓∀除去 ↑generalizeタクティク
P(a)Coqの証明でgeneralizeを使ってみると：
Goal ∀a:A, (∀x:A, P(x))→ P(a). Proof. intros a H. generalize a. assumption. Qed.
補題univConj_to_conjUnivも使わなかったのは、2[補題]と書いてある推論はCoqではなくなってしまい、代わりに 4[等号の推移律]のところで分岐（ゴールが増える）が起きたのです。紙の上とCoq処理系では、けっこうやることが変わってしまったりします。
4[等号の推移律]のところを下から上に向かってさかのぼるにはtransitivityというタクティクを使います。これを知らなくて、長い時間悩んでしまいました。transitivityの実行で、ゴールは2つに分岐します。2つのゴールは同じタクティクで始末できます。
Require Import Utf8_core. Section 関数の外延的等値性. (* 外延的等値性の定義 *) Definition ext_eq {A B:Set} (f g: A->B) := ∀x:A, f x = g x. (* 外延的等値性に、≡ という記号を割り当てる *) Notation "f ≡ g" := (ext_eq f g) (at level 75, no associativity). (* X, Y, f, g, h を前提する *) Variable (X Y:Set) (f g h : X->Y). (* ≡ の反射律 *) Lemma ext_eq_refl: f ≡ f. Proof. unfold ext_eq. intro. reflexivity. Qed. (* ≡ の対称律 *) Lemma ext_eq_sym: f ≡ g → g ≡ f. Proof. unfold ext_eq. intros H x. symmetry. apply H. Qed. (* ≡ の推移律 *) Lemma ext_eq_trans: f ≡ g → g ≡ h → f ≡ h. Proof. unfold ext_eq. intros H1 H2 x. transitivity (g x). generalize x. assumption. generalize x. assumption. Qed. End 関数の外延的等値性.
