依存型/\型クラス/\記法 -> (テスト失敗 <-> 型エラー)

coq_dep_typeclass_notation.md

title	tags	author	slide
依存型/\型クラス/\記法 -> (テスト失敗 <-> 型エラー)	Coq	mathink	false

アドベントカレンダー

7日目の記事は fetburner さんの 単一化の証明 でした。

まとめ

• 依存型と型クラスと Notation を使って、計算結果が合わないときに型エラーを引き起こす仕組みを作った。
• 証明と違い、具体的な計算のチェック。
• 真理値表の確認とか数値計算に便利、かも。
• Proof. now idtac. Qed. って一々書きたくないし Unnamed_thm とかいらん、という人向け。
• スクリプト全体は ここ。
• タイトルは考えるのが面倒でした。

必要な道具を作る。

とりあえず必要なもの

• True_or_Eq :: 決定可能な命題の結果に応じて型が変わる依存型
• I_or_0eq0 :: その結果に応じて変わる型の値を返す函数
• onlyTrue :: その一方の型だけを受け付ける函数

Set Implicit Arguments.
Unset Strict Implicit.

Definition True_or_Eq (P: Prop)(dec: {P}+{~P}): Prop := if dec then True else 0 = 0.
Definition I_or_0eq0 (P: Prop)(dec: {P}+{~P}): True_or_Eq dec :=
  if dec as dec' return True_or_Eq dec' then I else eq_refl 0.
Definition onlyTrue (H: True): True := H.

これらを使うと、(決定可能な)命題の成立する時のみ、 I_or_0eq0 に onlyTrue を適用できることになります。 当然、現時点では適用するとそもそも型エラーになるのですが、 これは Notation と組み合わせることで効果を発揮します。

以降では決定可能な等価性を使い、以上の道具の使い方を見ていきます。

eq が決定可能な型のための検査機構

型クラス dec_Type は、型とその上の等価性の決定手続きとを纏めたものです。 型 A から dec_Type のインスタンスを作っておくと、 dec_Type の存在を意識せずとも、型クラスの仕組みによって必要なインスタンスを推論してくれます。

また、 Coercion を使うことで X: dec_Type について x: X という記述が出来るようにしてあります。

Class dec_Type :=
  {
    carrier: Type;
    decider: forall (x y: carrier), {x = y} + {~x = y}
  }.
Coercion carrier: dec_Type >-> Sortclass.

そして、上で定義した型クラスを使い、函数 check_eq を定義します。

Definition check_eq {X: dec_Type}(x y: X) := I_or_0eq0 (decider x y).

dec_Type はそのフィールドに等価性の決定手続き decider を持っていました。ゆえに decider x y は決定可能です。 先に定義した I_or_0eq0 を適用すれば、これは　x と y が等しければ True の、等しくなければ 0 = 0 の証明を返す項となります。

ここで Notation の機能を使って以下のような記法を定義します。 Notation はあくまで記法を定義するのであって、項を作るわけではありませんから、型検査なども行ないません。

Notation ok x y := (onlyTrue (check_eq x y)).

しかし、この記法を実際に使うタイミングになると、 := の右側に書かれた通りの項が作られることになります。 その段階で check_eq x y の型が True か否かによって onlyTrue が適用できるか否かが決まり、もしも x と y の値が異なれば型エラーが起き、計算そのものか、あるいは計算結果の間違いを検出できることになります。

Check や Compute など、項を触るコマンドに食わせれば型検査が行なわれるので、その時に値が等しいかどうかのチェックができることにもなるわけです。

以降では、この仕組みを実際に使ってみます。 なんだかややこしい説明になりましたが、使ってみればどういうことかはすぐにわかると思います。

ブール函数で試す

bool 型から dec_Type のインスタンスを作っておきます。

Require Import Bool.

Instance dec_bool: dec_Type :=
  {
    decider := bool_dec
  }.

ついでに、記述を簡単にするために true と false をそれぞれ 1,0 で表現できるようにもしておきます。 グローバルにしてしまうと面倒なので、 bool_scope の中に留めておきましょう。

Notation "1" := true: bool_scope.
Notation "0" := false: bool_scope.

Open Scope bool_scope.

NAND から始めて全部作るやつ

以降では基本的なブール函数とその真理値表(に対応した検査)を記述しています。 Bool に定義されているものも容赦なく上書きです。

NAND から始めて

• AND
• NOT
• OR
• XOR
• MUX

を作っていくやつです。

定義の下に真理値表を記述しているので、これらの Check で型エラーが起きないということは函数が正しく定義されていることになります。

NAND

Definition nand (x y: bool): bool :=
  match x, y with
  | 1,1 => 0
  | _,_ => 1
  end.
Notation "x 'NAND' y" := (nand x y) (at level 50, left associativity): bool_scope.

Check ok (0 NAND 0) 1.
Check ok (1 NAND 0) 1.
Check ok (0 NAND 1) 1.
Check ok (1 NAND 1) 0.

AND

Definition and (x y: bool) := let b := (x NAND y) in b NAND b.
Notation "x 'AND' y" := (and x y) (at level 40, left associativity): bool_scope.
Notation "x * y" := (x AND y) (at level 40, left associativity): bool_scope.

Check ok (0 AND 0) 0.
Check ok (1 AND 0) 0.
Check ok (0 AND 1) 0.
Check ok (1 AND 1) 1.

NOT

Definition not (x: bool): bool := x NAND x.
Notation "'NOT' x" := (not x) (at level 35, right associativity): bool_scope.
Notation "! x" := (not x) (at level 35, right associativity): bool_scope.

Check ok (NOT 0) 1.
Check ok (NOT 1) 0.

OR

Definition or (x y: bool) := !(!x * !y).
Notation "x 'OR' y" := (or x y) (at level 50, left associativity): bool_scope.
Notation "x + y" := (x OR y) (at level 50, left associativity): bool_scope.

Check ok (0 OR 0) 0.
Check ok (1 OR 0) 1.
Check ok (0 OR 1) 1.
Check ok (1 OR 1) 1.

XOR

Definition xor (x y: bool): bool := (x + y) * (x NAND y).
Notation "x 'XOR' y" := (xor x y) (at level 55, left associativity): bool_scope.

Check ok (0 XOR 0) 0.
Check ok (1 XOR 0) 1.
Check ok (0 XOR 1) 1.
Check ok (1 XOR 1) 0.

MUX

Definition mux (x y sel: bool): bool := (!sel * x) + (sel * y).

Check ok (mux 0 0 0) 0.
Check ok (mux 0 0 1) 0.
Check ok (mux 0 1 0) 0.
Check ok (mux 0 1 1) 1.
Check ok (mux 1 0 0) 1.
Check ok (mux 1 0 1) 0.
Check ok (mux 1 1 0) 1.
Check ok (mux 1 1 1) 1.

失敗する例

成功する例だけ見ててもつまらんので、失敗する例も見てみましょう。

たとえば、マルチプレクサ(MUX)の定義を次のように少し間違えてしまったとしましょう。 y と AND を取るのは sel のはずですが、ここでは !sel になってしまっていますね。

Definition mux' (x y sel: bool): bool := (!sel * x) + (!sel * y).

すると、以下のように表の三行めの検査が失敗します。

Check ok (mux' 0 0 0) 0.
Check ok (mux' 0 0 1) 0.
Fail Check ok (mux' 0 1 0) 0.
(* The command has indeed failed with message: *)
(* => Error: The term "check_eq (mux' 0 1 0) 0" has type *)
(*     "True_or_Eq (decider (mux' 0 1 0) 0)" while it is expected to have type *)
(*     "True". *)

計算結果が異なると onlyTrue に与えられる項の型が 0 = 0 になり型エラーが起きるからです。 Compute で目視の値チェックをするよりはミスを検出しやすいですね。

計算結果がどうなったのか、は実際に Compute して確かめて下さい。 エラーメッセージで出てくれりゃいいのになぁ。

nat で試す

ブール値だけでは物足りないので、数値計算もしてみます。 まずは nat から dec_Type のインスタンスを作ります。

Require Import Arith.
Open Scope nat_scope.

Instance dec_nat: dec_Type :=
  {
    decider := eq_nat_dec
  }.

検査対象としてなんかよくわからない函数を定義してみます。上がったり下がったり。

Fixpoint evenb (n: nat) :=
  match n with
  | O => true
  | S n' => negb (evenb n')
  end.

Definition updown (n: nat): nat :=
  match n with
  | O => S O
  | S n' => if evenb n' then n' else S n
  end.

updown は引数が偶数の時に +1 、奇数の時に -1 をする函数です。 今回は仕様が単純なので証明もあっさりしていますが、とりあえず計算結果の正しさを幾つかの例で検査してみます。

三つめに間違った計算結果を書いたので、そこでちゃんと型エラーが起き、それ以外は正しく検査されているのがわかると思います。

Check ok (updown 0) 1.
Check ok (updown 1) 0.
Fail Check ok (updown 2) 1.
(* The command has indeed failed with message: *)
(* => Error: The term "check_eq (updown 2) 1" has type *)
(*     "True_or_Eq (decider (updown 2) 1)" while it is expected to have type *)
(*     "True". *)
Check ok (updown 2) 3.
Check ok (updown 3) 2.
Check ok (updown 4) 5.

updown は単純な函数ですが、もっと込み入った計算をする函数を相手取るときはこういう検査が簡単に出来ると便利ですよね。きっと。

どう使おう？

複雑な計算をする函数についての性質を証明したいとき、証明に入る前に幾つかのテストケースを通ることで、函数がちゃんと定義できていそうか確認する。 そんな使い方が便利かもしれません。

あと、こういう記事書く時、 Compute の結果を C-c C-; で挿入する方式だと函数の定義を変えたりしたときにコメントの修正が必要だし妙に見辛いしで不便だったので、この仕組みを使うとそういう心配がいらず楽でした。