导入<模块>与包含< Module>在Coq模块系统中

问题描述

在另一个模块中说 Include M1 的确切语义是什么？与在模块M中进行 M1 导入有什么不同？更确切地说，以下命令的语义是什么：

What is the exact semantics of Include M1 inside another module, say M ? How is it different from doing Import M1 inside the module M ? More precisely what is the semantics of the following command:

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

推荐答案

总结两个白话命令的语义：

To summarize the semantics of both vernacular commands:

• 命令 Include M1 （可在的定义中使用） module 或 module type ）要求Coq复制 M1 的所有字段。因此，它就像对环境模块内部的 M1 内容（复制模块类型）进行复制粘贴一样。


• 导入M1 命令（也可以用于定义 module 或 module type 的命令） >，但另外要求 M1 是 module ）允许一个人引用 M1 及其短标识符（即，无需使用合格的标识符 M1.field_name ）



• The command Include M1 (which can be used in the definition of a module or a module type) asks Coq to make a copy of all the fields of M1. Thus, it acts just like a "copy-and-paste" of the contents of M1 inside the ambient module (resp. module type).
• The command Import M1 (which can also be used in the definition of a module or a module type, but additionally requires that M1 is a module) allows one to refer to the fields of M1 with their short identifier (i.e., without needing to use qualified identifiers M1.field_name)

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

Next, the syntax Module Type M := M1 <+ M2 <+ M3 is a shortcut for:

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

Coq参考手册的相关部分为，，您可能还想看看命令（ Import 的变体）。

The relevant sections of Coq's reference manual are Sect. 2.5.1 (Include), Sect. 2.5.8 (Import) and you may also want to take a look at the Export command (a variant of Import).

如果在某些时候您犹豫了 Include 和 Import 之间，您可能应该尝试使用 Import 首先，因为它的效果更浅（它不会克隆指定模块的内容，而只是定义较短的名称）。

If at some point you hesitate between Include and Import, you should probably try to use Import in the first place, because it will have a lighter effect (it won't clone the contents of the specified module but just define shorter names).

最后，下面是两个综合示例，这些示例说明了Coq中模块，模块类型和函子的用法，以及命令 Include 和 Import ：

Finally, below are two comprehensive examples that illustrate the use of modules, module types, and functors in Coq as well as the commands Include and 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.

我记得是评估vm_compute在

(********************************************)
(* 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.

这篇关于导入<模块>与包含< Module>在Coq模块系统中的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持！