coq - 如何在 Coq 的模块中使用引理？

Question

我在一个名为的文件中定义了一个模块类型A.v

Module Type WeakPair.
...

End WeakPair.

Module WeakPairProps (Import WP : WeakPair).

 Lemma Weak_A ....

End WeakPairProps.

然后我想定义另一个B.v可以使用的文件，Lemma例如WeakPairProps：Weak_A. 因为WeakPairProps不是模块类型所以我不知道如何编写一个可以在WeakPairProps.

Answer 1

首先，您需要定义一个实现模块类型的模块WeakPair：

Module WeakPairImpl <: WeakPair.
(* stuff goes here *)
End WeakPairImpl.

现在您可以实例化仿函数WeakPairProps：

Module WeakPairPropsInst := WeakPairProps(WeakPairImpl).

您现在可以参考引理：

WeakPairPropsInst.lemma

如果您不想使用限定名称，可以导入WeakPairPropsInst。