The Coq mailing list

[Andrew McCreight <andrew.mccreight AT yale.edu>]

Hi,

I've written a functorized implementation of finite sets implemented using 
lists.  The modules have worked pretty well there.  I didn't have the 
problem that you did with export.  For me, it works just fine, although I 
exported at the top level of the file instead of within a module.  Maybe 
that's the difference.

I also encountered the second problem, where the names are not quite what 
you'd like.  This is a problem when the arguments are actual nat and you 
try to use Omega, because Omega says that it cannot operate on that type, 
so you have to do some unfolding.  A brute force way around this would be 
to write an unfolding tactic, but I haven't bothered.

-Andrew


On Tue, 22 Aug 2006, 
roconnor AT theorem.ca
 wrote:

> I've written a small development of inequalities about Q for the new Q 
> library in 8.1beta.  Rather than again repeating the same theorems about Z, 
> I've written a module that gives theorems for inequalities over any ordered 
> ring.  The idea was that the same module can be used to give theorems for Z, 
> Q, and R in a uniform way.  However, I have encountered two problems.
>
> In my functor development I have theorems with names like plus_lt_0_compat. 
> My idea was to collect theorems from this functor and other functors into the 
> a module called Q.  Thus the user would access the lemma by the name 
> Q.plus_lt_compat, and similarly Z.plus_lt_compat for Z. However my attempts 
> to do this
>
> Module Q.
> Module QOrderedRing := OrderedRing.OrderedRing QSig.
> Export QOrderedRing.
> End Q.
>
> do not seem to work. :(
>
> Another more serious problem is that the statement of the theorems in the 
> module refer to the names of the module type parameters, rather than the 
> names of the parameters given in the module signature.  So, after applying 
> Q.QOrderedRing.plus_lt_0_compat, one get the goals:
>
> ______________________________________(1/2)
> QSig.lt QSig.zero x
>
>
> ______________________________________(2/2)
> QSig.lt QSig.zero y
>
> instead of the nice
>
> ______________________________________(1/2)
> 0 < x
>
>
> ______________________________________(2/2)
> 0 < y
>
> Both these problems could be solved by writing out for each theorem an new 
> definition with the nice signature, such as
>
> Definition Qplus_lt_0_compat : forall n m:Q, 0 < n -> 0 < m -> 0 < n + m := 
> Q.QOrderedRing.plus_lt_0_compat.
>
> But this seems to largely defeat the purpose of using modules.  If someone 
> adds a new theorem to the module, then every type that uses the module will 
> have to add a new definition.
>
> Has anyone had any practical success using modules to modularise theories?
>
> --
> Russell O'Connor                                      <http://r6.ca/>
> ``All talk about `theft,''' the general counsel of the American Graphophone
> Company wrote, ``is the merest claptrap, for there exists no property in
> ideas musical, literary or artistic, except as defined by statute.''
>
> --------------------------------------------------------
> Bug reports: http://coq.inria.fr/bin/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>         http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club