n≦n の形式的な証明に学ぶCoC/CIC

18793 ワード
Coq Coq テキストリンク

1. 概要

Coqの背景にある計算体系は、CoCを拡張したCICです。 この拡張部分には「Inductive を使ったデータ型の構成方法」が含まれ、それによって型に付随する言明を正当化する手段を得ます（例:数学的帰納法）。一方、CoCだけであっても同様のことが可能です。そこでCoCとCICの両方で同じ問題を解いて比較します。

とはいえ、紙でやるのも面倒かつ間違える可能性があるのでCoq上でやってみます。この考えは「Coqの正しさをCoqで確かめる」という意味でも「拡張された体系で、拡張前の体系を確かめる」という意味でも、つまり二重の意味で無意味ですが、私の目的が納得であって説明でないのである程度有用と思われます（論理学の言葉を借りるとメタ言語にCoqを使うということです）。

なお、本稿で行うことは、CICについての以下文献の2.1,2.2で記述されていることを理解するためにCoqに落とし込んだものです:

2. n≦nの証明(CoC)

n≦n を証明します。自然数を定義して、数学的帰納法を定義して、順序関係の公理を定義すると証明項を構成できます。ここでいう定義とは Parameter(Axiomでも可)を使うことで、環境に仮定を追加する行為です:

(* numを定義 *)
Parameter num: Set.
Parameter zero: num.
Parameter succ: num -> num.
(* 数学的帰納法の公理図式 *)
Parameter ind: forall P, P zero -> (forall n, P n -> P (succ n))-> forall n, P n.
(* 順序関係の公理 *)
Parameter le: num -> num -> Prop.
Parameter lez: forall n, le zero n.
Parameter leS: forall m n, le m n -> le (succ m) (succ n).

(* n ≦ n の証明 *)
Theorem le_n_n: forall n, le n n.
Proof. apply ind. apply lez. intros n H. apply leS. exact H. Qed.
Print le_n_n.
(* 表示される証明項
     ind (fun n : num => le n n) (lez zero) (fun (n : num) (H : le n n) => leS n n H)
     : forall n : num, le n n *)

3. n≦nの証明(CIC)

CICでは Inductiveな定義により、自動的に環境に各種の情報を詰め込んでくれます。

Inductive num' :=
| zero': num'
| succ': num' -> num'.
Inductive le': num'->num'->Prop :=
| lez': forall n, le' zero' n
| leS': forall m n, le' m n -> le' (succ' m) (succ' n).

Theorem le_n_n': forall n, le' n n.
Proof. induction n. constructor. constructor. assumption. Qed.

Check num'. (* num': Set *)
Check zero'. (* zero': num' *)
Check succ'. (* succ': num' -> num' *)
Check num'_ind. (* num'_ind
     : forall P : num' -> Prop, P zero' -> (forall n : num', P n -> P (succ' n)) -> forall n : num', P n *)
Print le_n_n'. (*  le_n_n' = 
  fun n : num' =>
    num'_ind (fun n0 : num' => le' n0 n0) (lez' zero')
    (fun (n0 : num') (IHn : le' n0 n0) => leS' n0 n0 IHn) n
     : forall n : num', le' n n *)

4. 両者の比較

CoCで手動で環境に登録した「数学的帰納法の正しさ」に対応するtyped object ind は、CICの方法ではInductive にnum'を定義した時に自動的に num'_ind として追加されています。一般にAxiom/Parameterで仮定を環境に追加することは計算体系を矛盾に導く可能性があることから、あまりやりたくないので、自動的にやってくれるというのは大変に便利です。

同じことを別の角度から議論できます。CoCの方法は、numの構成法を示しているとはみなせません。ゼロはnumですし、それにsuccを作用させたものはnumですが、numとはそれで全てだとは一言も言っていません（従ってindの正しさは自明ではありません）。かたやInductiveによる定義では、numとはそのようなもののsmallest setであると構文的・計算規則として言っているわけで、より多くの情報が詰まっておりそれがnum'_indなどのtypingを正当化します（難しい言葉を使うと、num'はzero',succ'に対する始代数を定める、ということらしいです）。実際、num'_indはCICの規則では証明可能です:

Print num'_ind. (* num'_ind = 
fun (P : num' -> Prop) (f : P zero')
  (f0 : forall n : num', P n -> P (succ' n)) =>
fix F (n : num') : P n :=
  match n as n0 return (P n0) with
  | zero' => f
  | succ' n0 => f0 n0 (F n0)
  end
     : forall P : num' -> Prop,
       P zero' ->
       (forall n : num', P n -> P (succ' n)) ->
       forall n : num', P n
 *)

Theorem my_ind: forall P : num' -> Prop, P zero' -> (forall n : num', P n -> P (succ' n)) -> forall n : num', P n.
Proof. intros P f f0. fix F 1;intros. destruct n as [|n0].
- assumption.
- apply f0. apply F. Qed.
Print my_ind. (* my_ind = 
fun (P : num' -> Prop) (f : P zero')
  (f0 : forall n : num', P n -> P (succ' n)) =>
fix F (n : num') : P n :=
  match n as n0 return (P n0) with
  | zero' => f
  | succ' n0 => f0 n0 (F n0)
  end
: 後略 *)

Theorem my_ind': forall P : num' -> Prop, P zero' -> (forall n : num', P n -> P (succ' n)) -> forall n : num', P n.
Proof. induction n. assumption. apply H0. assumption. Qed.
Print my_ind'. (* my_ind' = 
fun (P : num' -> Prop) (H : P zero')
  (H0 : forall n : num', P n -> P (succ' n)) 
  (n : num') =>
num'_ind (fun n0 : num' => P n0) H
  (fun (n0 : num') (IHn : P n0) => H0 n0 IHn) n
: 後略 *)

Coqが作ってくれる証明項と全く同じ証明項を手動で構成するにはfixというtacticが必要でしたが、合わせる必要がなければ inductionを使えばよいだけです。証明項に登場する fix や match はCICにおける項の構成規則で定義されている奴です。

5. まとめ

CICの便利さを実感しました。指摘やコメントは大歓迎です。