The Coq mailing list

["Elie Soubiran" <soubiran AT lix.polytechnique.fr>]

Hello Julien,

In Coq V8.2 beta (http://coq.inria.fr/V8.2beta) you can use the
Include keyword to factorize your developement:

Module Type B.
  Parameter C : Set.
  Parameter rel : C->C->Prop.

 Axiom  rel_trans :
  forall (c1 c2 c3 : C) , rel c1 c2-> rel c2 c3 -> rel c1 c3.
End B.

Module Type B1.
  Include Type B.
(* copy the fields of the module type B in the current module type*)

  Axiom Specific_B1_Axiom :
            forall (c : C) ...
End B1.

Module Type B2.
  Include Type B.

  Axiom Specific_B2_Axiom :
            forall (c : C) ...
End B1.

Elie

2008/9/15 Julien Tesson 
<julien.tesson AT univ-orleans.fr>:
> Hi,
> I have the following modelling problem :
> I have two module types which contain some similar fields and I'd like to
> factorize them in one module.
>
> example :
> for two module B1 and B2
>
> Module Type B1.
>   Parameter C : Set.
>   Parameter rel : C->C->Prop.
>
>  Axiom  rel_trans :
>   forall (c1 c2 c3 : C) , rel c1 c2-> rel c2 c3 -> rel c1 c3.
>
>   Axiom Specific_B1_Axiom :
>             forall (c : C) ...
> End B1.
>
> Module Type B2.
>   Parameter C : Set.
>   Parameter rel : C->C->Prop.
>
>  Axiom  rel_trans :
>   forall (c1 c2 c3 : C) , rel c1 c2-> rel c2 c3 -> rel c1 c3.
>
>   Axiom Specific_B2_Axiom :
>        forall (c : C) ...
> End B2.
>
>  I'd like to do something like
>
> Module Type B.
>   Parameter C : Set.
>   Parameter rel : C->C->Prop.
>
>  Axiom  rel_trans :
>   forall (c1 c2 c3 : C) , rel c1 c2-> rel c2 c3 -> rel c1 c3.
> End B.
>
> and deriving from B the module types B1 and B2 that embed their specific
> axioms.
>
> The coq'art suggest to write
> Module Type B1.
>   Declare Module root : B.
>   Axiom Specific_B1_Axiom :
>      ...
> End B1.
>
> but it's not satisfying to me because it force to use B1.root.C to access C
> instead of B1.C .
>
> Is there a way to derive a module from an other one  more transparently so
> that I can access C through B1.C ?
>
> Best Regards,
> Julien.
>