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
と組み合わせることで効果を発揮します。
以降では決定可能な等価性を使い、以上の道具の使い方を見ていきます。
型クラス 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.
以降では基本的なブール函数とその真理値表(に対応した検査)を記述しています。
Bool
に定義されているものも容赦なく上書きです。
NAND から始めて
- AND
- NOT
- OR
- XOR
- MUX
を作っていくやつです。
定義の下に真理値表を記述しているので、これらの Check
で型エラーが起きないということは函数が正しく定義されていることになります。
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.
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.
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.
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.
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.
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
から 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-;
で挿入する方式だと函数の定義を変えたりしたときにコメントの修正が必要だし妙に見辛いしで不便だったので、この仕組みを使うとそういう心配がいらず楽でした。