The Coq mailing list

[Kevin Hamlen <hamlen AT utdallas.edu>]

Hi Adam,

Yes, pulling the Inductive definitions out and parameterizing them with 
type variables is possible.  But it can lead to unpleasantly large 
parameter lists and huge proof contexts.  For example, if FOO_TYPE 
contains 20 parameters, each of which appear individually in 
constructors of bar, then we're stuck writing 19 extra arguments to each 
bar-constructor.  It gets worse when FOO_TYPE contains Axioms that leak 
into inductive types as  dependently typed parameters.  We could, of 
course, create specialized versions of all the constructors (e.g., 
barfoo := Bar Foo.foo), but then we get back into the original problem: 
distinct but equivalent instantiations of FooTheory1 Foo create separate 
versions of barfoo that don't always unify easily.

What we really want, I think, is a single, centralized definition of 
Foo.foo that all the FooTheory's share, so that there are never any 
duplicate names floating around.  That seems to jive with Michael's 
solution: Functors that want to share a definition of Foo.foo should 
incorporate that definition as part of the Module Type of their module 
parameters, so that it becomes part of their interfaces.

--Kevin




On 8/21/2018 12:58 PM, Adam Chlipala wrote:
> On 08/17/2018 04:36 PM, Kevin Hamlen wrote:
> > What do Coq programmers consider the "right way" to organize large 
> > projects containing functors?  In particular, how do authors of large 
> > projects define collections of modules that all build upon some 
> > shared functor without getting duplicate name-conflicts?
>
> It really seems like a distraction to work so hard to put an inductive 
> definition directly inside a functor body.  I would do it like this:
>
> Module Type FOO_TYPE.
>   Parameter foo: Type.
> End FOO_TYPE.
>
> Inductive bar T := Bar (f : T).
>
> Module FooDefs (Foo: FOO_TYPE).
>   Definition bar := bar Foo.foo.
>   (* ... hundreds more definitions ... *)
> End FooDefs.
>
> Module FooTheory1 (Foo: FOO_TYPE).
>   Module Import F := FooDefs Foo.
>   Ltac silly1 := match goal with |- Bar _ _ = Bar _ _ => reflexivity end.
>   (* ... more theorems, proofs, and ltacs ... *)
> End FooTheory1.
>
> Module Foo:FOO_TYPE.
>   Definition foo:=nat.
> End Foo.
> Module Import FD := FooDefs Foo.
> Module Import FT1 := FooTheory1 Foo.
> Theorem silly: forall (x:bar), x=x.
> Proof.
>   destruct x.
>   silly1.
> Qed.