2

2 つの異なるファイルに 2 つの異なるモジュール署名があります。フィールド名は同じですが、動作が異なります。

そして内部のファンクターは別のファンクターを定義します。

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.vMI.v

そして、たとえば、両方を使用する必要がある1つの定義。

 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 Rsigpi_inttrsIntTPImint_inttrsIntTMI

これが私が定義した方法です：

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です? ご協力ありがとうございました。

4

1 に答える 1

3

実際には、 の定義では、とが同じ型であるredPairという保証はないため、このエラー メッセージが表示されます。P.sigM.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 でモジュールとファンクターを使用することには注意することをお勧めします。ほとんどの場合、実際には従属レコードのみが必要です。モジュールとファンクターは誰にとっても複雑です。抽象化、共有制約などに注意する必要があります。

現状では、依存レコードに対して提供するもの、つまり抽象化やサブタイプ化のために実際に必要でない限り、それらを使用しないようにする必要があるようです。

実際のところ、私は今あなたの定義に少し不安を感じています. たとえば、MIを の中で定義するのは理にかなっていPIますか? これ以上の文脈がなければ、それは恣意的に思えます。モジュールを使用するときは注意が必要であり、何をしているのかをよく理解していることを確認してください。そうしないと、逆効果になる可能性があります。:)

しかし、あなたがただ実験しているのであれば、それらを試してみてください. 可能性の範囲とそれぞれの長所と短所を知っておくとよいでしょう。

于 2013-04-04T04:06:13.967 に答える