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

Question

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

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

我可以将定理、其证明和引理放入模块中，受模块类型限制，并且仅使定理可用吗？

类似于:

Module Type T_MY_T.
End T_MY_T.

Module T_My_theorem : T_MY_T.
  Lemma L1: ...
  Proof. Admitted.
  Lemma L2: ...
  Proof. Admitted.
  Theorem My_Great_Theorem: ...
  Proof. apply L1; apply L2. Qed.
End T_My_theorem.

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

Answer 1

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