coq - 设计仿函数以能够使用不同的模块

Question

我有两个不同的模块签名到两个不同的文件中。它们具有相同的字段名称，但行为不同。

仿函数内部定义另一个仿函数。

PI.v

Module Type TPI.
  Parameter sig : Signature.
  Parameter trsInt: forall f, pi f.
End TPI.

Module P (Export T: TPI).
   Lemma A...
    Module Export Mono <: MonoType.
End P.

和

MI.v

Module Type TMI.
   Parameter sig : Signature.
   Parameter trsInt : forall f, mi f.
End TMI.

Module M (Export TM: TMI).
   Lemma B ...
   Module Export Mono <: MonoType.
End M.

另一个文件中的MonoType，例如Mono.v

这是我的情况。

我在该文件中有另一个名为 B.v 的文件，我需要在文件 PI.v 和 MI.v 中使用定义和引理.

例如，我需要使用一个定义来使用它们。

 Definition redPair R is :=
   match is with
 | Type_PI => pi_int R is
 | Type_MI => mi_int R is
 end.

我在 R 上遇到问题，因为 pi_int R 和 mi_int R 具有不同的 sig(签名)，其中，pi_int 在模块签名 TPI 中使用了 trsInt，而 mint_int 在模块签名 TPI 中使用了 trsInt模块签名TMI。

这是我定义它的方式:

Module PI (Import P : TPI).
Definition pi_int R is := P.trsInt ...

(* inside PI I define another functor for MI *)
  Module MI (Import M : TMI).
   Definition mi_int R is := M.trsInt ...

   Definition redPair R is :=  
     match is with
    | Type_PI => pi_int R is
    | Type_MI => mi_int R is  (* error here saying that it used the sig of 
                    P.sig but in this case mi_int used the sig of M.sig *)
    end.

End MI.
End PI.

我的问题是，有没有一种方法可以让我拥有良好的模块结构，并且可以在定义 redPair 处拥有相同的签名？感谢您的帮助。

Answer 1

实际上，在redPair的定义中，你无法保证P.sig和M.sig具有相同的类型，这就是您收到此错误消息的原因。

解决此类问题的方法是通过“共享约束”强制类型相等。这是与您类似的代码，演示了如何强制 P.sig 和 M.sig 等于 nat:

Module Type TPI.
  Parameter sig : Type.
  Parameter x : sig.
End TPI.

Module Type TMI.
  Parameter sig : Type.
  Parameter x : sig.
End TMI.

Module PI (Import P : TPI with Definition sig := nat).
  Definition pi_int := x.

  Module MI (Import M : TMI with Definition sig := nat).
    Definition mi_int := x.

    Definition f (x : bool) :=
      if x
      then pi_int
      else mi_int.

  End MI.

End PI.

您还可以选择让 P.sig 不受约束，但随后强制 M.sig 保持相同:

Module PI (Import P : TPI).
  Definition pi_int := x.

  Module MI (Import M : TMI with Definition sig := P.sig).
    Definition mi_int := x.

    Definition f (x : bool) :=
      if x
      then pi_int
      else mi_int.

  End MI.

End PI.

---

既然提到了你的问题的解决方案，我建议在 Coq 中使用模块和仿函数时要小心。大多数情况下，您实际上只需要依赖记录。模块和仿函数对每个人来说都很复杂，你必须关心抽象、共享约束等。

现状似乎是，您应该避免使用它们，除非您实际上需要它们来提供相对于依赖记录的功能:抽象和/或子类型。

事实上，我现在对你的定义有点不安。例如，在 PI 内部定义 MI 是否有意义？如果没有更多背景，这似乎是武断的。也许是这样，我只是说你在使用模块时应该小心，并确保你很好地掌握了你在做什么，否则可能会适得其反! :)

但是如果您只是进行试验，请尝试一下它们。了解可能性的范围以及每种可能性的优缺点是件好事。