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。