Coqのモジュールの基本機能

あけましておめでとうございます。今年もよろしくお願いします。


Coqのモジュール関連の機能について和訳したので基本的な機能を紹介します。
リファレンスの文中で「対話的」モジュールとされているのは Vernacular を使って定義するからで、実体は Structure です*1


Coqのモジュールは(S)MLのモジュールに近い機能で、型とその実装をひとまとめにして名前を付けることができます。
実はリファレンスを読んだだけではどんな機能か分からなかったので分かったことをこの記事にまとめます(多分構文はOCamlに近いけどワタシ用のメモなので随所でSMLと比較しています)。

基本

SMLで言うstructuresignatureはそれぞれCoqでは Module(モジュール) と Module Type(モジュール型) という名前で扱われます。
ただしCoqではこれらはお互いにネストできます。


モジュールのフィールドにアクセスするには、MLと同じくモジュールとフィールド名をドット(.)で区切った表記を使います。
例えばモジュールOptionのフィールドmapにアクセスしたければOption.mapです。

定義

モジュールはModule identからEnd identの間に、モジュール型の方は Module Type identEnd identの間に定義を書きます。

モジュールの定義
(* モジュール M の定義 *)
Module M.
  Definition T := nat.         (* 型 T を持つ *)
  Definition x : T := 0.       (* 型 T を持つ x を持つ *)
  Definition y : bool.         (* 型だけ指定すると証明モードになる *)
  Proof. exact true. Defined.
End M.

普通ですね。Module M : SIG. で制約を指定して定義を始めることも出来ます。

モジュール型の定義
Module Type SigM.
  Parameter T : Set.
  Parameter x : T.
  Declare Module M : SigM2.
End SigM.

こちらもほぼ見たままで、モジュールに要求する制約に名前を付ける定義です。

Declare というのは「~というモジュール型を満たすモジュールを含むべき」という制約の宣言を表します。
SMLなら単に structure M : SigM2 と書くところですが、Coq では冒頭述べた通りモジュール型の定義中にモジュールの定義が出来てしまうので明示的に書き分ける必要があります。

制約

MLのモジュールは特定のシグネチャを満たしていることを強制出来ますが、Coqでも同じことが出来ます。
(SMLと表記が微妙に違って混乱する…)

不透明(opaque)制約

Module CM : SigM := M. (* SigM を満たす実装 M を与える *)
Fail Print CM.y.       (* SigM には y が含まれていないので CM.y も見え無い *)

: SigMは不透明制約と呼ばれます。モジュールCMがモジュール型SigMを満たすことを確認し、かつSigMに含まれるフィールド以外を隠蔽します。
つまりSigMに記述されているフィールドにのみCMのフィールドとしてアクセス出来ます。


以下のようにその場で実装を与えることも出来ます。

Module CM : SigM.
  Definition T := nat.
  Definition x := 0.
  Definition y : bool.
  Proof. exact true. Defined.
End CM.

CM.xCMモジュールの外からxにアクセス出来ますが、SigM.Tの実装は隠蔽されているため、CM.xの値は見えません。

Print CM.x.  (* *** [ CM.x : CM.T ] *)

透明(transparent)制約

モジュールが特定の制約を満たすことだけを確認し、実装を隠蔽しないことも出来ます。これを透明制約と言います。

Module TCM <: SigM := M. (* SigM を満たす実装 M を与える *)
Print TCM.x.
(* TCM.x = 0 : nat *)

透明制約はモジュールの実装に影響しないため、モジュール外部でもTCM.xnatだということが分かります。

合成/拡張

Coqのモジュール(型)はモジュール同士を合成したり、一部を詳細化したり、拡張したり出来ます。

Include

モジュール(型)定義内でInclude <module-ident>を実行すると、指定したモジュールの内容がその場に導入されます。

Module Nat1Core.
  Inductive natopt := SOME : nat -> natopt | NONE.
  Definition t := natopt.
End Nat1Core.

Module Nat1Map.
  Include Nat1Core.
  Definition map f (x : t) : t := (* Nat1Core.t が修飾無しで使える *)
    match x with | SOME x => SOME (f x) | NONE => NONE end.
End Nat1Map.

Print Nat1Map.
(**
Module Nat1Map := Struct
     Inductive natopt : Set :=  SOME : nat -> natopt | NONE : natopt.
     Definition natopt_rect : ..
     Definition natopt_ind : ..
     Definition natopt_rec : ..
     Definition natopt_sind : ..
     Definition t : Set.
     Definition map : (nat -> nat) -> t -> t.
   End
 *)

SMLのopenincludeに似ていますが、同名の定義が表れたときの扱いはCoqの方が厳しく、後に出現した方は(同様の定義であっても)エラーになります。

Module OnlyNat. Definition n := nat. End OnlyNat.
Module Nat2.
  Include OnlyNat. (* n := nat が導入される *)
  Definition n := nat. (* n already exists. *)
End Nat2.

Import

モジュール(型)定義内でImport <module-ident>を実行すると、指定したモジュールのフィールド名が導入されます。
上のIncludeに似ていますが、インポートしたフィールドはモジュール定義の一部になるわけでは無いことに注意して下さい。

Module Nat1Core. .. End Nat1Core.

Module Nat1Map.
  Import Nat1Core.
  Definition map f (x : t) : t := (* Include のときと同じく Nat1Core.t が修飾無しで使える *)
    match x with | SOME x => SOME (f x) | NONE => NONE end.
End Nat1Map.

Print Nat1Map.
(**
Module Nat1Map := Struct
  (* t の定義は含まれ無い *)
  Definition map : (nat -> nat) -> Nat1Core.t -> Nat1Core.t.
End
 *)

Nat1Mapの定義にDefinition tが含まれていないことに注意して下さい。
定義時に(モジュール内部で)修飾無しにアクセス出来るようになっただけであり、現在のモジュールの一部になるわけでは無いということです。


定義の一部になっていないため、以下のように定義し直せば(?)実装の一部にすることが出来ます。

Module Nat1Map.
  Import Nat1Core.
  Definition t := t.       (* インポートされた t を使って Nat1Map.t を定義 *)
  ..
End Nat1Map.
Print Nat1Map.
(**
Module Nat1Map := Struct
  Definition t : Set.      (* 定義に追加されている *)
  Definition map : (nat -> nat) -> t -> t.
End
 *)

Export

Export <module-ident>は、Importに加えて、現在のモジュールがImportされた際にmodule-identのフィールドも同時に導入される機能です。

Module Nat2Map.
  Export Nat1Core.
  Check t.                        (* Import と同様にフィールドを導入する *)
  Definition map f (x : t) : t := ..
End Nat2Map.
Print Nat2Map.
(**
Module Nat2Map := Struct 
  Definition map : (nat -> nat) -> t -> t. (* Nat1Core.t は定義の一部にはならないが… *)
End
 *)

Import Nat2Map.
Check t.        (* インポートすると t が見える *)

定義に表れない名前が導入されるなんて実際に使われたらものすごく混乱する機能な気がします…。

with句

(公式には特に構文に名称は付いてないもよう)

型指定

Module Typeに含まれる一部の定義をその場で与えて詳細化することが出来ます。SMLのwhereに相当します。

Module N : SigM with Definition T := nat := M.
Eval compute in (N.x : nat).
(* = N.x : nat *)
Fail Eval compute in (CM.x : nat). (* CM: 不透明制約のセクションで定義したやつ *)
(**
The term "CM.x" has type "CM.T" while it is expected to have type "nat".
 *)
モジュール指定

withにはモジュールを指定することも出来、サブモジュールが特定の実装になっていることも表現出来ます*2

Module Type Single.
  Parameter t : Set.  Parameter v : t.
End Single.

(* モジュールを要求するモジュール型を作る *)
Module Type Wrap.
  Declare Module In : Single.
End Wrap.
Module SBool.
  Definition t := bool.  Definition v : t := true.
End SBool.

(* boolで実装を与える *)
Module WrapB.
  Module In := SBool.
End WrapB.

Module MBool : Wrap := WrapB.
Fail Check (false : MBool.In.t). (* 実装は見えないため型チェックに失敗する *)

Module MBool' : Wrap with Module In := SBool := WrapB. (* サブモジュールに SBool を指定 *)
Print MBool'.
Check (false : MBool'.In.t).     (* 実装が見えている *)

この例の場合、サブモジュールInSBoolになっていることを強制しています。

*1:さらにStructureはRecordの別名です。https://coq.inria.fr/distrib/V8.8.2/refman/language/gallina-extensions.html#coq:warn.ident-cannot-be-defined

*2:これに相当することはSMLでは出来ません