coq - Coqのモジュール内でLemmaを使用するにはどうすればよいですか？

Question

モジュールタイプを1つのファイルで定義しましたA.v

Module Type WeakPair.
...

End WeakPair.

Module WeakPairProps (Import WP : WeakPair).

 Lemma Weak_A ....

End WeakPairProps.

次に、B.vを使用できる別のファイルを定義します。例：。はモジュールタイプではないので、補題を再利用できるモジュールの書き方がわかりません。LemmaWeakPairPropsWeak_AWeakPairPropsWeakPairProps

Answer 1

まず、モジュール タイプを実装するモジュールを定義する必要がありますWeakPair。

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

これで functorをインスタンス化できますWeakPairProps:

Module WeakPairPropsInst := WeakPairProps(WeakPairImpl).

補題を参照できるようになりました。

WeakPairPropsInst.lemma

修飾名を使用したくない場合は、WeakPairPropsInstをインポートできます。