Coq のモジュールさんの気持ちがわかりませんのこと

coq

あまり元気ではないですが元気です。

さて世間は猫も杓子も証明という感じで大変恐ろしい、ところがボクもご多分にもれず、ということで Coq です。

Module Type A.
  Parameter n : nat.
End A.

Module B : A
  Definition n := 0.
End B.

Theorem B_n_eq_zero : B.n = 0.
Proof.
trivial.
Qed.

上記のコード片に含まれる定理 B_n_eq_zero の証明は、タクティックが示すとおりの trivial に見えますが、実際には Qed で証明を完了することができません。ちなみにゴールはこんな具合です。

1 subgoal
______________________________________(1/1)
B.n = 0

どこが間違っていたのでしょうか。答えはモジュール B の定義で、正しくは以下のようになります。

Module B <: A
  Definition n := 0.
End B.

うーん…？？？あっ、よくよく見ると "B : A" だったのが "B

Module ident : module_type
Starts an interactive module specifying its module type.

Module ident

はい意味わかりませんね…実は Variants を見るともう少し分かりやすい記述があって、

Module ident module_bindings : module_type := module_expression
Defines a functor with parameters given by module_bindings (possibly none), and output module type module_type, with body module_expression.

Module ident module_bindings

ようするに "

Module M.
  Parameter n : nat.
End M.

上記のようなモジュールの定義が許されます。これは、定義の不完全なモジュール、ではなく、簡約することができないメンバを持つモジュール、でしかない…

…らしいぞ！！というのがボクの理解なのですが、

  • この理解は正しいのでしょうか
  • このような定義を伴わないメンバはどのような場面で活用されるのでしょうか

ということを識者の方に伺いたいので、よろしくお願いします、ということです。