在Coq Module系统中导入<Module>与Include <Module>

Question

Include M1M说另一个模块内部的确切语义是什么？与Import M1在模块M内部进行操作有何不同？更准确地说，以下命令的语义是什么：

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

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参考手册的相关部分是Sect。2.5.1（包含），派。2.5.8（导入），您可能还想看看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.