---
title: Coq: 引数にパターンが使えるようになったので試してみた
tags: Coq Coq-8.6
author: mathink
slide: false
---Coq の 8.6 が出た ので CHANGES を覗いてみたら
- Ability to put any pattern in binders, prefixed by quote, e.g.
"fun '(a,b) => ...", "λ '(a,(b,c)), ...", "Definition foo '(x,y) := ...".
It expands into a "let 'pattern := ..."
という記述があった。
let 'pattern := ... は確か既に使えていた気がするんだけど、それが函数定義の引数部にも使えるようになったということらしい。
この機能を少し触ってみたので、軽くまとめることにする。
- 型とか項の形には注意
- 複雑なレコードを使うときに便利かも
ちょっといじってみると、どうやら fun '(a,b) => ... は fun ab => let '(a,b) := ab in ... のシンタックスシュガーのようだ。
たとえば
Definition uncurry (X Y Z: Type)(f: X -> Y -> Z): X * Y -> Z :=
fun '(x,y) => f x y.
Definition uncurry' (X Y Z: Type)(f: X -> Y -> Z): X * Y -> Z :=
fun xy => let '(x,y) := xy in f x y.としてから Print uncurry'.すると、
(* uncurry' = *)
(* fun (X Y Z : Type) (f : X -> Y -> Z) '(x, y) => f x y *)
(* : forall X Y Z : Type, (X -> Y -> Z) -> X * Y -> Z *)
(* Arguments X, Y, Z are implicit *)
(* Argument scopes are [type_scope type_scope type_scope function_scope *)
(* _] *)という結果が得られる。 Print uncurry. した結果も
(* uncurry = *)
(* fun (X Y Z : Type) (f : X -> Y -> Z) '(x, y) => f x y *)
(* : forall X Y Z : Type, (X -> Y -> Z) -> X * Y -> Z *)
(* Arguments X, Y, Z are implicit *)
(* Argument scopes are [type_scope type_scope type_scope function_scope *)
(* _] *)となっているので、実際同一の項であることが確かめられる。当然、
Goal @uncurry = @uncurry'.
reflexivity.
Qed.である。
さて、この例では(見た目の)異なる定義が同じ項を与えていたのだが、もちろん、やり方によっては異なる項を生成することもある。
次のような函数を考えよう。意味は考えず、形だけを見ればよい。
Definition fuga '(x,y)(n: nat): nat :=
n * (x + y).これと「同等な」函数は、次のように定義することもできる。
Definition fuga' (p: nat * nat)(n: nat): nat :=
let (x,y) := p in n * (x + y).このとき、 forall p n, fuga p n = fuga' p n が成り立っている。
Goal forall p n, fuga p n = fuga' p n.
intros [x y] n; reflexivity.
Qed.ただし、 fuga と fuga' は異なる項である。
Goal fuga = fuga'.
Fail reflexivity.
Abort.何故かと言えば、上述の通り fun '(a,b) => ... は fun ab => let '(a,b) := ab in ... のシンタックスシュガーなので、 fuga という項は
fuga := fun xy => let '(x,y) := xy in fun n => n * (x + y)という形になっているからである。
この事実は、函数 fuga'' を次のように定義すると、
Definition fuga'' (p: nat * nat) :=
let '(x,y) := p in fun n => n * (x + y).以下の等式が成り立つことから示すことができる。
Goal fuga = fuga''.
reflexivity.
Qed.もちろん fuga p n = fuga' p n = fuga'' p n なのだが、これは函数が項として等しいという意味ではない。
「同等な」とは、函数が外延的に等しいという意味である。
パターン中では型指定が出来ない。つまり型推論を手助けできない。
どういうことかというと、たとえば次のような形で函数を定義するのは無理ということである。
Definition hoge '((x:nat),(y:bool)) := x.試みると、次のようなエラーメッセージが返ってくる。
(* Toplevel input, characters 18-25: *)
(* > Definition hoge '((x:nat),(y:bool)) := x. *)
(* > ^^^^^^^ *)
(* Error: Casts are not supported here. *)つまり、素直に
Definition hoge '(x,y) := x.と書くしかないのだが、実際はこの定義も通らない。
x と y の型が推論できないからである。
(x,y) は pair x y のシンタックスシュガーであり pair: forall (X Y: Type), X -> Y -> prod X Y だから、なんとかして X と Y の情報を復元したいのだが、そうするには定義部でどうにか情報を与えるしかない。
hoge の返り値の型を書いても推論できるのは x の型だけなので、まだ足りない。
ということで、たとえば
Definition hoge '(x,y) := let _ := y:bool in x: nat.といった形にすれば定義は通るようになるが、こんなことをするくらいなら
Definition hoge (p: nat * bool) := let '(x,y) := p in x.とした方がよいだろう。
パターンを使う時は、定義部を見ただけでマッチした要素の型がわかるようにしておかねばならないということである。
あるいは、パターンの中に必要な情報を込められるようにしておこう(Notation とか使うのもよいね(たとえば (x : X , y : Y) という記法を定義してしまう <- 無理でした (パターンとして依存関係をどうこうしようとするのが無理っぽい))。
Record Foo :=
{
bar: nat;
baz: nat
}.とやってレコードを定義すると Build_Foo x y のシンタックスシュガーとして {| bar := x ; baz := y |} という記法が使えるようになるのだが、これ以外にも
{| bar := x |} := {| bar := x ; baz := _ |}や
{| baz := y |} := {| bar := _ ; baz := y |}といった具合に、フィールドの定義を一部省略した記法も使えるようになる。
これがどういう意味を持つのかというと、たとえば Foo 型の引数を取るんだけど bar フィールドにしか用が無い場合、
Definition bar_map (f: nat -> nat)'{| bar := x |} := f x.といった感じに、パターン部分においても、以降で必要のないフィールドを記述するのを省略できる(_ がいい仕事する、ということ)。
このくらいの規模のレコードであれば素直にアクセサ bar を使えばいいのだけど、同じ要素が複数の場所に出現したりする場合とかには便利だろうと思う(し、使っておきたい)。
Record Hoge :=
{
hoge_type: Type;
hoge_elem: hoge_type
}.というようにフィールド感に依存関係のあるレコードを定義すると、このレコード用の記法はパターンとして使えなくなる。
Definition hoge_elem' '({| hoge_type := nat; hoge_elem := n |}) := n.という定義をしようとしても、
(* Toplevel input, characters 24-62: *)
(* > Definition hoge_elem' '({| hoge_type := nat; hoge_elem := n |}) := n. *)
(* > ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ *)
(* Error: The constructor Build_Hoge (in type Hoge) expects 1 argument. *)と怒られる。
Definition hoge_elem' '({| hoge_elem := n |}) := n: nat.とやってもだめなので、諦めた方がよい。
依存関係のあるものについては、大人しく match しよう。
自前の Notation でも 'pattern 記法が使えるようになったらいいのになぁ(今後に期待)。