The Coq mailing list

[Andrei Popescu <andrei.h.popescu AT gmail.com>]

Hello,

I am working (with Dmitriy Traytel, in CC) on a problem motivated by
simplifying the formal developments in Isabelle/HOL, and would like to
know to which extent this is also relevant for Coq. I would appreciate
any insight on this from people who develop or use Coq mathematical
libraries.

Let's say one has libraries L_1, ..., L_n containing theories of
algebraic structures (such as groups, monoids, relation algebras
etc.). Then say one has a concrete type T and operations on this type,
in such a way that, for any i between 1 and n, the restriction of some
of these operations on a subset A_i of T forms an algebraic structure
satisfying the assumptions of library L_i. And say one wants to prove
a result that needs to instantiate results from all of these libraries
to T. (For example, T could be the type of relations on S for some
type S, and we may want to instantiate: results from relation algebras
to the entire type T, results from groups to the restriction of T to
bijective functional relations, etc.)

My question is: What is a good approach to achieve the above, and how
are things currently done in Coq? Three approaches come to mind:

(1) Put the burden on the user who instantiates the library: Develop
the libraries without explicit carrier sets. Then the user would
seemingly have to introduce custom types different from T
(corresponding to the subsets A_i) in order to instantiate the
different libraries, and then some transfer would be necessary in
order to apply them to T.

(2) Put the burden on the library developer: Develop the libraries L_i
not considering the entire type as carrier, but maintaining explicit
carrier sets (subsets of the entire type) and assuming that they are
closed under the operations (e.g., by giving a more specific type for
these operations). Then instantiation can go smoothly, but with the
price of dealing with additional bureaucracy when developing the
library.

(3) A hybrid between (1) and (2): Develop the libraries without
explicit carrier sets, and then, for the main (to be exported) results
only, infer carrier-set-based versions -- so that one still achieves
instantiation flexibility.

I would very much like to hear your thoughts. Also, I apologise for
the potentially naive suggestions included in the above analysis -- I
am not a Coq expert.

Best wishes,
Andrei