CoqでRとCの証明をまとめる方法

はじめに

解析の教科書を読んでいるとKをRまたはCを表すものとしていることがあると思います。そしてRに関する証明とCに関する証明がKという文字を利用してまとめられていると思います。このRとCの証明をまとめるということを形式的証明ではどうすればよいかを本記事で書きたいと思います。
この記事ではCoqを使う形式的証明での説明を行います。Coqや形式的証明に関する基本的な知識は前提にします。

代数的構造との比較

やりたいことはRとCの両方に共通する性質のみを用い様々な議論を行いその結果得られたことをRやCに当てはめ、Rに関する命題とCに関する命題の証明を同時に得ることです。代数で同じようなことをしているのでまずは代数について見ていきます。

代数的構造では

代数では体や群やモノイドなどの代数的構造がでてきてます。そしてそれぞれの代数的構造に対して、定義として与えられた性質のみを用いて様々な議論を行います。議論によって示された代数的構造に関する命題は、その代数的構造の性質を満たす数学的構造に当てはめることができます。
これをCoqで実現するのは簡単です。 Record を使えばできます。例えばモノイドは以下のように定義できます。

      Record Monoid : Type := mkMonoid
{
MT : Type;
Me : MT;
Mc : MT -> MT -> MT;
M_O_r : forall (x : MT), (Mc x Me) = x;
M_O_l : forall (x : MT), (Mc Me x) = x;
M_assoc : forall (x y z : MT), (Mc (Mc x y) z) = (Mc x (Mc y z))
}.
    

そしてモノイドに関する命題を以下のように証明できます。

      Lemma M_assoc_2 : forall (M : Monoid) (x y z w : MT M), Mc M (Mc M (Mc M x y) z) w = Mc M x (Mc M y (Mc M z w)).
Proof.
intros M x y z w.
rewrite (M_assoc M (Mc M x y) z w).
rewrite (M_assoc M x y (Mc M z w)).
reflexivity.
Qed.
    

Rは足し算についてモノイドの性質を満たすので以下のようにモノイドを作ることができます。

      Definition RplusMonoid := mkMonoid R 0%R Rplus Rplus_0_r Rplus_0_l Rplus_assoc.
    

そして上で示したM_assoc_2を当てはめることができます。

      Definition Rplus_assoc_2 : forall (x y z w : R), (x + y + z + w = x + (y + (z + w)))%R := M_assoc_2 RplusMonoid.
    

このようにして代数に関してはやりたいことができます。

RやCでは

同じことをしてRとCをまとめることを考えます。まずRとCを共通化した構造に与える演算や性質を考える必要があります。体の演算や性質や連続の公理が思いつきますがそれだけで十分ではありません。
ノルムに関する命題をまとめて扱う場合はノルムやその性質を加えないといけません。Rの転置行列やCの随伴行列をまとめて扱う場合はRについては恒等写像Cについては共役をとるという演算を加える必要があります。
このように必要なものが増えていきあらかじめ共通化した構造を定義することはできません。

RとCの証明のまとめ方

ではRとCをどうまとめるかを見ていきます。まずは以下のような列挙体を定義します。

      Inductive RC : Set :=
  | RK : RC
  | CK : RC.
    

RCにはRKとCKの2つの要素があります。RKをRにCKをCに対応させます。

      Definition RCT (K : RC) := match K with
  | RK => R
  | CK => C
end.
    

そして議論をしたい演算や議論に必要な性質を定義します。

      Definition RCO : forall (K : RC), RCT K := fun (K : RC) => match K with
  | RK => 0
  | CK => CO
end.

Definition RCplus : forall (K : RC), RCT K -> RCT K -> RCT K := fun (K : RC) => match K with
  | RK => Rplus
  | CK => Cplus
end.

Definition RCplus_assoc : forall (K : RC) (a b c : RCT K), RCplus K (RCplus K a b) c = RCplus K a (RCplus K b c) := fun (K : RC) => match K with
  | RK => Rplus_assoc
  | CK => Cplus_assoc
end.
    

例えばRCplus KはKにRKを入れればRplusにKにCKを入れればCplusになります。
このように演算や性質を定義した後はRやCをまとめて扱うことができます。ここでは2変数の三角不等式から3変数の三角不等式を導くのをまとめてやってみます。まずノルムに関する議論なのでRのノルムとCのノルムをまとめます。

      Definition RCnorm : forall (K : RC), RCT K -> R := fun (K : RC) => match K with
  | RK => Rnorm
  | CK => Cnorm
end.
    

また元々持っていることにしている2変数の三角不等式もまとめます。

      Lemma Rnorm_triang : forall (r1 r2 : R), (Rnorm (r1 + r2) <= Rnorm r1 + Rnorm r2)%R.
Proof.
...

Lemma Cnorm_triang : forall (c1 c2 : C), (Cnorm (Cplus c1 c2) <= Cnorm c1 + Cnorm c2)%R.
Proof.
...

Definition RCnorm_triang : forall (K : RC) (c1 c2 : RCT K), (RCnorm K (RCplus K c1 c2) <= RCnorm K c1 + RCnorm K c2)%R := fun (K : RC) => match K with
  | RK => Rnorm_triang
  | CK => Cnorm_triang
end.
    

このRCnorm_triangを使って3変数の三角不等式を示してみます。

      Lemma RCnorm_triang_3 : forall (K : RC) (c1 c2 c3 : RCT K), (RCnorm K (RCplus K (RCplus K c1 c2) c3) <= RCnorm K c1 + RCnorm K c2 + RCnorm K c3)%R.
Proof.
intros K c1 c2 c3.
apply (Rle_trans (RCnorm K (RCplus K (RCplus K c1 c2) c3)) (RCnorm K (RCplus K c1 c2) + RCnorm K c3) (RCnorm K c1 + RCnorm K c2 + RCnorm K c3))%R.
apply (RCnorm_triang K (RCplus K c1 c2) c3).
apply (Rplus_le_compat_r (RCnorm K c3) (RCnorm K (RCplus K c1 c2)) (RCnorm K c1 + RCnorm K c2) (RCnorm_triang K c1 c2)).
Qed.
    

このように2変数の三角不等式を2度使う議論をRとCについてまとめてできます。そしてKにRKやCKを入れてそれぞれRとCに関する命題にできます。

      Definition Rnorm_triang_3 : forall (r1 r2 r3 : R), (Rnorm (r1 + r2 + r3) <= Rnorm r1 + Rnorm r2 + Rnorm r3)%R := RCnorm_triang_3 RK.

Definition Cnorm_triang_3 : forall (c1 c2 c3 : C), (Cnorm (Cplus (Cplus c1 c2) c3) <= Cnorm c1 + Cnorm c2 + Cnorm c3)%R := RCnorm_triang_3 CK.
    

応用

以前解析入門の1章をCoqで形式的証明を行うという 記事 を作成しました。当時は今回紹介した方法に気付かなかったのでRとCについて同じことをして証明していました。しかしRとCについてまとめた命題がないのは不便だったのでリファクタリングしました。( PR )
最近は特異値分解や疑似逆行列など線形代数の議論をするときに使っています。( ソースコード )

まとめ

RとCの証明をまとめるのは、最初にRとCに共通する性質を列挙してそれを満たす構造の議論をするという方針では、使う性質が限られてしまい列挙していない性質を使う議論ができないという問題がありました。そこでRとCに対応させた2つの要素を持つ列挙体を考えそれに対して様々な演算子や性質を後から必要に応じて定義するという方法を考えました。この方法で筆者はRの証明とCの証明で二度手間になることを避けることができています。

最後に

私は今回紹介した方法に気付かなくて同じ証明をRとCで二度やってしまっていました。あるときふと今回の方法に気付き時間をかけてリファクタリングをして使えるようにしました。今後同じことをして時間を無駄にする人がでないようにと思い今回の記事を書きました。
また今回の方法を知る前は代数的構造での抽象化とRとCの証明をまとめることは違うものと考えていました。前者は代数的構造に具体的な数学的構造を代入しているのに対し、後者は2つのものを表現したものの見た目が変わらないので1つに省略していると思っていました。しかし今回の方法を知って、後者も適切に演算子や性質を定義したKにRやCを代入しているのだと気付きました。それも共有したいと思いました。