eqの性質の証明

  • 1
    Like
  • 0
    Comment

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

各種定義

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

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

eq x yx = 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=yyzにします.

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

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は証明できる」ということが明確になりました.