x = y型と型アノテーションで4択クイズ

Coq

概要

2回ハマったのでメモ。
eqの定義とパターンマッチ(の型アノテーション)の難しさのせいで、
eqがtransitiveであることの証明は意外に難しい。

クイズ

イコールの推移律(任意のx,y,zについて、x = y ⇒ (y = z ⇒ x = z))を
Coqで証明しようとしています。
以下のeq_transitive1からeq_transitive4のうち、正しいtermはいくつあるでしょう？

Variables (A : Type) (x y z : A).

Definition eq_transitive1 : x = y -> y = z -> x = z :=
  fun xey yez => match xey in (_ = t) return t = z with
                            | refl_equal => yez
                          end.

Definition eq_transitive2 : x = y -> y = z -> x = z :=
  fun xey yez => match xey in (t = _) return t = z with
                            | refl_equal => yez
                          end.

Definition eq_transitive3 : x = y -> y = z -> x = z :=
  fun xey yez => match yez in (_ = t) return x = t with
                            | refl_equal => xey
                          end.

Definition eq_transitive4 : x = y -> y = z -> x = z :=
  fun xey yez => match yez in (t = _) return x = t with
                            | refl_equal => xey
                          end.

説明

このクイズには二種類の説明がいる。
第一に、eqの型はこんな感じ

Check eq.
(*
eq : forall A : Type, A -> A -> Prop
*)

なので、一見するとA型の第二引数とA型の第三引数は対称に見える。
が、実は第二引数はパラメータで、第三引数はindexである。

Print eq.
(*
Inductive eq (A : Type) (x : A) : A -> Prop :=  refl_equal : x = x
*)

1つめの(x : A)がコロンの左側にあって、2つめのAがコロンの右側にあるのがその証拠。
パターンマッチのmatch ... in (constructor var [var...])では
変数にindexを束縛できるが
パラメータを束縛することはできない。
したがってeq_transitive2と4はこんなエラーで弾かれる。

Error: The parameters of inductive types do not bind in
the 'return' clauses; they must be replaced by '_' in the 'in' clauses.

つまり「in (_ = t)」とは書けるが「in (t = _)」とは書けない。

第二に、eq_transitive1の(match xey in (_ = t) return t = z with ...)の型は
returnの中でtがyに束縛されてy = zになる。
また、| refl_equal => の中では、
return t = zはreturn x = zになり、x = z型を返さなくてはならない。
したがってeq_transitive1は2か所で型エラー。(先に後者でエラーになる)

結局、正解はeq_transitive3のみ。

束縛遅延

必ずyezのパターンマッチをしなければいけないなんて理不尽だ！
という場合、returnの中を関数型にすることで、
xeyからパターンマッチすることもできる。

Definition eq_transitive5 : x = y -> y = z -> x = z :=
  fun xey => match xey in (_ = t) return (t = z -> x = z) with
                            | refl_equal => fun xez => xez
                    end.

Definition eq_transitive6 : x = y -> y = z -> x = z :=
  fun xey yez => (match yez in (_ = t) return (x = y -> x = t) with
                            | refl_equal => fun xey => xey
                           end) xey.

eq_transitive5は、(match xey in (_ = t) return (t = z -> x = z) with ...)は
全体としてy = z -> x = z型になり、
refl_equal =>の中ではreturn (x = z -> x = z)になるため
fun xez => xez(恒等関数)で型が合う。
returnの中を関数型にするのは
Certified Programming with Dependent Types
http://adam.chlipala.net/cpdt/
で"delay the binding" "delay arguments"などと呼ばれていたテクニック。
match...in...returnは厄介なので詳しい説明が欲しいところ。