在 Coq 模块系统中，导入 <Module> 和包含 <Module> 的区别是什么？

Question

Include M1指在另一个模块（例如M）中包含M1的确切语义是什么？与在模块M内执行 Import M1 有何不同？更准确地说，以下命令的语义是什么：

Module Type M := M1 <+ M2 <+ M3.

- Abhishek Kr Singh

Answer 1

总结俗语命令的语义：

• Include M1 命令（可用于定义 模块 或 模块类型）要求 Coq 复制 M1 的所有字段。因此，它就像在环境模块（相应地，模块类型）中“复制并粘贴”M1 的内容。
• Import M1 命令（也可用于定义 模块 或 模块类型，但需要 M1 是一个 模块）允许使用其短标识符引用 M1 的字段（即，无需使用限定标识符 M1.field_name）

接下来，语法 Module Type M := M1 <+ M2 <+ M3 是以下方式的快捷方式：

Module Type M.
  Include M1.
  Include M2.
  Include M3.
End M.

请参阅Coq参考手册中关于Include和Import命令的相应部分，您可能还想查看Export命令（Import的变体）。如果您在Include和Import之间犹豫不决，那么您应该首先尝试使用Import，因为它会产生较轻的影响（它不会克隆指定模块的内容，而只是定义更短的名称）。

最后，以下是两个综合示例，演示了Coq中模块、模块类型和函数子的使用以及Include和Import命令：

(********************************************)
(* Example involving a parameterized module *)
(********************************************)
(* A signature *)
Module Type MT.
  Parameter t : Type.
End MT.

(* A bigger signature *)
Module Type MT1.
  Include MT.
  Parameter u : t.
  Parameter f : t -> t.
End MT1.

(* A parameterized module *)
Module F1 (M1 : MT1).
  Import M1. (* => we can now write f rather than M1.f *)
  Definition fu := f u.
End F1.

(* A module implementing MT1 *)
Module M1 <: MT1. (* => check the signature but don't make the module opaque *)
  Definition t := nat.
  Definition u := O.
  Definition f := S.
End M1.

(* Instantiation *)
Module FM1 := F1 M1.
Compute FM1.fu.

我记得 Compute 是 Eval vm_compute in 的快捷方式

(********************************************)
(* Extra example: a parameterized signature *)
(*                                          *)
(* It can be noted that this feature of Coq *)
(* module types has no equivalent in OCaml… *)
(********************************************)
Module Type MT2 (M : MT).
  Parameter u : M.t.
  Import M. (* => we can now write t rather than M.t *)
  Parameter f : t -> t.
End MT2.

(* Another parameterized module *)
Module F2 (M : MT) (M2 : MT2 M).
  Import M2.
  Definition fu := f u.
End F2.

(* Modules implementing MT and MT2 *)
Module M <: MT.
  Definition t := bool.
End M.

Module M2 <: MT2 M.
  Definition u := false.
  Definition f := negb.
End M2.

(* Instantiation *)
Module FM2 := F2 M M2.
Compute FM2.fu.

- ErikMD