The Coq mailing list

[Elnatan Reisner <elnatan AT cs.umd.edu>]

I saw some old discussions about this in the archives, but I couldn't 
figure out an answer.

If I want to define a module type with parameters and definitions, 
where the definitions depend on the parameters, is there a way to do 
this without having to copy and paste the definitions in modules which 
instantiate the module type? And beyond that, can I prove things about 
a module type (without instantiating the parameters), and then refer to 
those lemmas within a module where I *have* instantiated the 
parameters?

I hope my sample code below illustrates what I mean. (I use an 
Inductive definition below, rather than a regular Definition, because 
in my actual development, I have Inductive definitions, and I wanted to 
make sure any response doesn't depend on having only Definitions.)

Thanks for any assistance.

As an aside, I read a suggestion that Records are better to use than 
Modules anyway. If they provide a solution, great; I'm not committed to 
Modules.
-Elnatan


Require Import List.
Module Type MY_SIG.
  Parameter aList : list nat.
  Inductive sublist : list nat -> Prop :=
     | sl : forall L n, In n L -> In n aList -> sublist L.
End MY_SIG.

Declare Module X : MY_SIG.
Import X.

(* Prove things about any MY_SIG here *)

Module MyMod : MY_SIG.
  Definition aList := 1::2::4::nil.
  (* Prove things about MY_SIGs with this particular value for the 
parameter, *)
  (* but I should be able to refer to things I proved above *)
End MyMod.
(* This gives an error, but I want the definition of sublist from 
MY_SIG to be used. *)
(* I don't want to have to redefine it here. *)