letで束縛とはこれいかに - コンピュータってすごいらしい

概要

Coqの些末な話。
proj2_sigの定義が読めなかったのでletについて調べた。

(* proj2_sig = 
fun (A : Type) (P : A -> Prop) (e : sig P) =>
let (a, b) as e0 return (P (proj1_sig e0)) := e in b
     : forall (A : Type) (P : A -> Prop) (e : sig P), P (proj1_sig e) *)
Print proj2_sig.

let〜as〜returnはどういう意味か？

基本:matchへの読み替え方

let(ident1,...,identn) := 〜 in 〜は1つのコンストラクタをもつ型の項を
パターンマッチするためのシンタックスシュガーである。
リファレンスマニュアル2.2.3節

If term inhabits an inductive type with one constructor C, we have an equivalence between
let (ident1,...,identn) [dep_ret_type] := term in term’
and
match term [dep_ret_type] with C ident1 ... identn => term’ end

いくつか実験

コンストラクタの引数が0または1の場合

まず気になったのが、コンストラクタが0引数または1引数でも使えるかどうか。

(* one constructor that takes no argument *)
Inductive T0 : Type := c0.
(* one constructor that takes one argument *)
Inductive T1 : Type := c1 : nat -> T1.
(* one constructor that takes two arguments *)
Inductive T2 : Type := c2 : nat -> nat -> T2.

Definition test0 := let () := c0 in 0.
Definition test1 := let (n) := c1 100 in n.
Definition test2 := let (n, m) := c2 100 200 in n + m.

Eval compute in test0.
Eval compute in test1.
Eval compute in test2.

これはいずれもOK.しかし0引数は役に立たない。
1引数の場合、紛らわしい。括弧の有る無しで束縛される変数の型が変わる。

(* nat *)
Check (let (n) := c1 100 in n).
(* T1 *)
Check (let n := c1 100 in n).

プライム

マニュアルの続きには'(プライム)の使い方が書いてある。
プライムを付けるとコンストラクタを明示的に書くことになるかわりに、
パターン中にパターンが書ける。
以下はマニュアルの例。

Definition deep_tuple (A : Set) (x : (A * A) * (A * A)) : A * A * A * A :=
  let '((a,b), (c, d)) := x in (a,b,c,d).

ちなみに(x, y)は意外と複雑なNotationによる。Locateするのも大変。

(*
Notation            Scope     
"( x , y , .. , z )" := pair .. (pair x y) .. z
                      : core_scope
                      (default interpretation)
*)
Locate "( _ , _ , .. , _ )".

T0からT2だとこんな感じ。

Definition test02 := let 'c0 := c0 in 0.
Definition test12 := let 'c1 n := c1 100 in n.
Definition test22 := let 'c2 n m := c2 100 200 in n + m.

括弧をつけてもよい

パターンに括弧は割と付け放題。
c2 (n) (m)とするとnとmが束縛されると分かりやすいかもしれない。

Definition test03 := let '(c0) := c0 in 0.
Definition test13 := let '(c1 n) := c1 100 in n.
Definition test14 := let '(c1) n := c1 100 in n.
Definition test15 := let 'c1 (n) := c1 100 in n.
Definition test23 := let '(c2 n m) := c2 100 200 in n + m.
Definition test24 := let 'c2 (n) (m) := c2 100 200 in m.

ただマニュアルにsigの例があるが、Notationを入れて変数以外をアルファベットでない記号にするのが
よりスマートだと思う。

Infix "&" := c2 (at level 50).
Definition test25 := let 'n & m := c2 100 200 in n + m.

パターンを網羅していません

コンストラクタの引数が、2種類以上のコンストラクタを持つ型の場合
シンタックスシュガーらしいエラーが出る。
たとえばc1の引数に100 = S (S ... (S O)...)を使うと…

(* error. "Non exhaustive pattern-matching" *)
(*
Definition test16 := let 'c1 100 := c1 100 in 0.
*)
(*
Definition test17 := match c1 100 with c1 100 => 0 end.
*)

コンストラクタを間違えた

コンストラクタを間違えると「コンストラクタが間違っている」という旨のエラーが出る。
これもmatchと同じ挙動。

(* Error: Found a constructor of inductive type unit while a constructor of T0
 is expected. *)
(*
Definition test18 := let 'tt := c0 in 0.
*)
(*
Definition test19 := match c0 with tt => 0 end.
*)

let..in..return..in?

letはmatch .. as .. returnの代わりに使えるが
match .. in .. returnの代わりには使えないらしい。

Inductive Tnat : nat -> Type := cnat : Tnat 0.
Definition testnat := match cnat in Tnat t return t = 0 with
   cnat => refl_equal 0 end.
(* error *)
(*
Definition testnat := let () in Tnat t return t = 0 := cnat in refl_equal 0.
*)

BNFではasにしなさいと書いてある。
リファレンスマニュアル1.2節Figure 1.2

dep_ret_type ::= [as name] return_type
return_type ::= return term

射影関数が面倒

proj2_sigが以下のように簡単に書くことができないのは、
pの型がaに依存するから。

(* Error: Cannot infer type of pattern-matching on "s". *)
(*
Definition proj2_sig2 (A : Set) (P : A -> Prop) (s : sig P) :=
  let (a, p) := s in p.
*)

そこでas〜returnが必要。returnの中でもletは使える。

Definition proj2_sig3 (A : Set) (P : A -> Prop) (s : sig P) :=
  let (_, p) as s return P (let (a, _) := s in a) := s in p.

Recordにすれば

Recordにすればこのような射影関数は勝手に作ってくれるので便利。
sigがそうなっていないのは定義が古く、互換性のためか。

Set Implicit Arguments.
Record sig' (A : Set) (P : A -> Prop) : Set := {
  proj1_sig' : A;
  proj2_sig' : P proj1_sig'
}.

Print proj1_sig'.
Print proj2_sig'.