默认实现

Question

我有我想要实现数倍的接口：

Module Type I. 
    Parameter a : A. 
    Parameter b : B. 
    Parameter c : C. 
End I. 

（并假设每个a，b和c实际上许多定义）。

的实现将是

Module Imp1 <: I. 
    Definition a : A := bar. 
    Definition b : B := foo a. 
    Definition c : C := baz a b. 
End I. 

现在事实证明，许多实现共享的b定义（这需要a），但有c不同的定义。

如何集中b的定义？最好不要改变I或重复大量的定义？

（我想编写一个模块仿BImp期待a:A为某种参数，然后我可以Import (BImp a)。）

Answer 1

你可以外包你的共享定义为参数的改变零件的全球化定义（这里outsourced）你的模块（这里是a）。我不知道是否有像Haskell的默认实现。

Module Type I. 
    Parameter a : A. 
    Parameter b : B. 
    Parameter c : C. 
End I. 

Definition outsourced (a:A) := foo a. 

Module Imp1 <: I. 
    Definition a : A := bar. 
    Definition b : B := outsourced a. 
    Definition c : C := baz a b. 
End Imp1. 

Module Imp2 <: I. 
    Definition a : A := bar'. 
    Definition b : B := outsourced a. 
    Definition c : C := baz' a b. 
End Imp2. 

Answer 2

您可以在其他模块内安装模块。这迫使您复制模块的签名的一部分，但不是模块包含的证明。

Module Type PreorderSignature. 
Parameter Inline type : Type. 
Parameter Inline less : type -> type -> Prop. 
Parameter Inline reflexivity : forall x1, less x1 x1. 
Parameter Inline transitivity : forall x1 x2 x3, less x1 x2 -> less x2 x3 -> less x1 x3. 
End PreorderSignature. 

Module Preorder (PS : PreorderSignature). 
Import PS. 
(* Preorder facts. *) 
End Preorder. 

Module Type EquivalenceRelationSignature. 
Parameter Inline type : Type. 
Parameter Inline equal : type -> type -> Prop. 
Parameter Inline reflexivity : forall x1, equal x1 x1. 
Parameter Inline symmetry : forall x1 x2, equal x1 x2 -> equal x2 x1. 
Parameter Inline transitivity : forall x1 x2 x3, equal x1 x2 -> equal x2 x3 -> equal x1 x3. 
End EquivalenceRelationSignature. 

Module EquivalenceRelation (ERS : EquivalenceRelationSignature). 
Import ERS. 
Module PreorderSignatureInstance <: PreorderSignature. 
Definition type := type. 
Definition less := equal. 
Definition reflexivity := reflexivity. 
Definition transitivity := transitivity. 
End PreorderSignatureInstance. 
Module PreorderInstance := Preorder PreorderSignatureInstance. 
Import PreorderInstance. 
(* Now your equivalence relations will inherit all the facts about preorders. *) 
(* Other equivalence relation facts. *) 
End EquivalenceRelation. 

Module Type PartialOrderSignature. 
Parameter Inline type : Type. 
Parameter Inline less : type -> type -> Prop. 
Parameter Inline reflexivity : forall x1, less x1 x1. 
Parameter Inline antisymmetry : forall x1 x2, less x1 x2 -> less x2 x1 -> x1 = x2. 
Parameter Inline transitivity : forall x1 x2 x3, less x1 x2 -> less x2 x3 -> less x1 x3. 
End PartialOrderSignature. 

Module PartialOrder (POS : PartialOrderSignature). 
Import POS. 
Module PreorderSignatureInstance <: PreorderSignature. 
Definition type := type. 
Definition less := less. 
Definition reflexivity := reflexivity. 
Definition transitivity := transitivity. 
End PreorderSignatureInstance. 
Module PreorderInstance := Preorder PreorderSignatureInstance. 
Import PreorderInstance. 
(* Now your partial orders will inherit all the facts about preorders. *) 
(* Other partial order facts. *) 
End PartialOrder. 

并平整模块层次一点，你可以使用Import和Parameter Inline命令。