coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Frederic Blanqui <blanqui AT loria.fr>
- To: Adam Koprowski <koper AT astercity.net>
- Cc: coq-club AT pauillac.inria.fr, VAN RAAMSDONK Femke <femke AT cs.vu.nl>
- Subject: Re: [Coq-Club] Some problems with modules.
- Date: Wed, 19 May 2004 18:11:01 +0200 (CEST)
- List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
On Wed, 19 May 2004, Adam Koprowski wrote:
> (1) Below is a structure of my modules simplified and without a content. My
> problem is to make Coq unify between modules H.T and Comp.T (which are
> clearly the same) in module HorpoWF. Basically I won't to get rid of an
> error message that appears when trying to enter definition for HorpoWF.x.
> Note that in case Term is just a definition (not an inductive one)
> everything works fine.
i suspect that it is related to a problem that sebastien hinderer and myself
had in a formalization of rewriting and polynomial interpretations in coq, a
contribution that we should release by the end of june, or in july.
when you define such a functor:
> > Module Terms (S: Signature).
> > Inductive Term: Set :=
> > | blah: Term.
> > End Terms.
with an inductive type definition, two instances of it with the same signature
will be considered as distinct. until it changes in coq, the solution is to
use a module -- type -- TERMS identical to Terms wherever you need to use
terms. then, at the end, you can fill in your functors with Terms.
> (2) Let's say we have a hierarchy of modules one being refinement of
> another.
> For instance modules describing order with more and more assumptions about
> it.
> Below I'll restrict to two modules but in principle there can be much more.
> I can see two methods (at least) of such definition.
>
> > Module Type Relation.
> > Parameter A: Set.
> > Parameter R: A -> A -> Prop.
> > End Relation.
> >
> > Module Type Order.
> > Parameter A: Set.
> > Declare Module R: Relation with Definition A := A.
> > Parameter R_irr: forall (a: A), ~R.R a a.
> > End Order.
>
> or
>
> > Module Type Order'.
> > Declare Module R: Relation.
> > Parameter R_irr: forall (a: R.A), ~R.R a a.
> > End Order'.
>
> Both approaches have disadvantages. It is possible to avoid them?
i also remarked this problem and asked Jacek Chrzaszcz whether it would be
possible to have syntatic sugar to extend modules or module types like the
inheritance mechanism in object-oriented languages.
Module Type Order inherits/extends Relation.
Parameter R_irr: forall (a: A), ~R.R a a.
End Order.
perhaps we could go further in this direction: when we want to implement a
module type containing some definitions, it is not useful to write
them again! in oo languages, only abstract methods need to be defined.
Module Terms implements TERMS.
(* here, we only define/prove the things not already defined/proved
in TERMS *)
End Terms.
- [Coq-Club] Some problems with modules., Adam Koprowski
- Re: [Coq-Club] Some problems with modules., Frederic Blanqui
- Re: [Coq-Club] Some problems with modules., Frederic Blanqui
Archive powered by MhonArc 2.6.16.