eqの性質の証明

Coqにおいて「等しい」をあらわす述語eqの，反射律・対称律・推移律を証明します．
これらを2つのアプローチ「matchを使う」と「eq_indを使う」で証明してみます．

各種定義

Coqのeqは次のように定義されています．

Inductive eq (A : Type) (x : A) : A -> Prop :=  eq_refl : x = x

eq x yをx = yとするNotationを使っています．

この定義をすると次のeq_indも証明されます．

eq_ind : forall (A : Type) (x : A) (P : A -> Prop),
    P x -> forall y : A, x = y -> P y

eq_indの証明

まずはeq_indの証明をmatchを使って行います．

fun (A : Type) (x : A) (P : A -> Prop) (H : P x) (y : A) (H1 : x = y) =>
    match H1 in (_ = z) return (P z) with
    | eq_refl => H
    end
        : forall (A : Type) (x : A) (P : A -> Prop), P x -> 
            forall y : A, x = y -> P y

eqの証明をmatchするには，in (_ = z)というのをつければよいようです．
これを使って対称律・推移律の証明を調べてみましょう．

反射律

次のように証明できます．

fun (A : Type) (x : A) => eq_refl x
     : forall (A : Type) (x : A), x = x

対称律

対称律の主張を以下に示します．

forall (A : Type) (x y : A), x = y -> y = x

matchを使った証明

次のように，eq_refl xを使います．

fun (A : Type) (x y : A) (H : x = y) =>
    match H in (_ = z) return (z = x) with
    | eq_refl => eq_refl x
    end
        : forall (A : Type) (x y : A), x = y -> y = x

eq_indを使った証明

eq_indの仮定をひとつずつ準備して，証明します．

fun (A : Type) (x y : A) (H : x = y) =>
    eq_ind x (fun z : A => z = x) (eq_refl x) y H
        : forall (A : Type) (x y : A), x = y -> y = x

推移律

推移律の主張を以下に示します．

forall (A : Type) (x y z : A), x = y -> y = z -> x = z

matchを使った証明

次のように，y=zを分解して，x=yのyをzにします．

fun (A : Type) (x y z : A) (H1 : x = y) (H2 : y = z) =>
    match H2 in (_ = a) return (x = a) with
    | eq_refl => H1
    end
     : forall (A : Type) (x y z : A), x = y -> y = z -> x = z

2019-12-08追記 次の記事で考察されています
http://kyasmt.hatenablog.com/entry/20091214/1260801722

eq_indを使った証明

上のmatchを使った証明をeq_indを使って書き直した感じです．

fun (A : Type) (x y z : A) (H1 : x = y) (H2 : y = z) =>
    eq_ind y (fun a : A => x = a) H1 z H2
        : forall (A : Type) (x y z : A), x = y -> y = z -> x = z

まとめ

等号の3つの性質をCoqで定式化し，証明を行いました．Coqでは等号が帰納的に定義されていて，3つの性質それぞれはCoqによって証明される定理だとわかりました．

次のようなことがわかりました．．

• 学生のときに，「同値関係」を「反射的かつ対称的かつ推移的」と習います．等号にこのような性質があるのは自明ですが，私には引っかかっていました．今回，より原理原則といえる部分を確認できました．
• 「等号を帰納的に定義する」「matchの型付けが少し複雑」「eq_indは証明できる」ということが明確になりました．