The Coq mailing list

["Soegtrop, Michael" <michael.soegtrop AT intel.com>]

Dear Coq Users,

I found that the module system and also the type class system are very 
effective for building up higher structures from basic structures, but I find 
it difficult to avoid repetition in defining the basic structures. E.g. I use 
identical scripts to define the ssreflect equality, countable, choice and 
finite structure for a few basic types, but I couldn't manage to put this 
into a module or other Coq structure which avoids copying the same script a 
few times.

The reason I ask is that I am working on some framework where the "higher 
structures" are given be the framework and the user is mostly providing basic 
structures and their connection, and I want to give some comfort for this.

With modules my problem is that a module evaluates the proof scripts when the 
module is defined, not when it is instantiated. This means that all 
properties of a type which are required for the proofs must be defined in the 
module type parameters. I think for properties as basic as being a finite 
type, it is hardly possible to collect properties in a module type which 
allow to proof this without giving a proof for finiteness itself. So I wonder 
if there is a way to have modules, which evaluate proof scripts when the 
module is instantiated with a specific type. In the end I want to be able to 
instantiate a module with an arbitrary type and see if the proof scripts run 
through. I want this only for some basic types. For the higher order work the 
module and type class system are fine as they are.

Another thing I could imagine to work is a Tactic Notation, which works at 
the level of "Definition" "Canonical Structure" and so on.

Is there a mechanism in Coq which could solve this?

Thanks & best regards,

Michael