coq - 如何使用模块来隐藏 coq 中的引理？

Question

我有一个定理 T，它的证明，以及用于证明它的无数个引理。

我想隐藏引理，只提供定理——主要是因为我不想为引理想出好的全局名称。

我可以将定理、它的证明和引理放在一个模块中，受模块类型的限制，并且只使定理可用吗？

就像是：

模块类型 T_MY_T。
结束 T_MY_T。

模块 T_My_theorem：T_MY_T。
  引理 L1：...
  证明。承认。
  引理 L2：...
  证明。承认。
  定理 My_Great_Theorem: ...
  证明。申请L1；应用 L2。Qed。
结束 T_My_theorem。

如果是这样，有人可以发帖或指出一个简单的例子吗？

Answer 1

Module Type A应该包含您希望导出的定理的公理。Module B : A包含这些公理作为需要证明的定理。它还可以包含证明定理所需的任何引理和其他机制。要从模块外部访问定理，您可以apply B.Theorem1等。