The Coq mailing list

[Ralf Jung <jung AT mpi-sws.org>]

Hi,

> I would like each file to first list all its
> definitions and theorems. Some definitions should be transparent: they
> should be listed in full here. Theorems and some definitions should be
> opaque: only their name and type should be shown. The proof of
> theorems and implementation of opaque definitions should come later.
> Any helper lemmas and functions used here should not be exposed at
> all.

Thanks for this question!  We have wanted the same feature as well
several times.

On 12.10.2017 18:45, Pierre Courtieu wrote:
> Hi,
> First note people generally use "Module Foo <: Bar", which checks the
> type of Foo against Bar but leaves everything in Foo visible.
> 
> However the duplication problem remains and here is how I would do
> (look at the Include directive):
> 
> 
> Module TEST_F.
>   Definition f : nat -> nat := fun n => n.
> End TEST_F.
> 
> Module Type TEST_SIG.
>   Include TEST_F.
>   Parameter g : nat -> nat.
>   Axiom t : True.
> End TEST_SIG.

There is another problem with this:  Include will duplicate typeclass
instances.  We have had problems with exponential blowup of typeclass
search due to this.
Though maybe the fact that Module Types and nod just Module is involved
here makes a difference?

> Module TEST : TEST_SIG.
>   Include TEST_F.
>   Definition g_helper : nat -> nat := S.
> 
>   Definition g : nat -> nat := g_helper.
> 
>   Lemma helper_lemma : True.
>   Proof. exact I. Qed.
> 
>   Theorem t : True.
>   Proof. apply helper_lemma. Qed.
> 
> End TEST.
> 
> BUT your example is oversimplified: TEST_F is a module but in general
> it is a module type, and then Include a module Type inside a module
> does not work. Suppose for instance that your module type is like
> this:
> 
> Module Type TEST_SIG.
>   Variable A:Type.
>   Definition f : A -> A := fun n => n. (* Notice how f depends on a
> *variable* *)
>   Parameter g : nat -> nat.
>   Axiom t : True.
> End TEST_SIG.
> 
> The solution I know for this is a bit heavy.
> 
> 1) Define a minimal module type MINMT which contains every variable
> needed by visible definitions.
> 
> 2) define the common part of both module and module type as a functor
> on a MINMT.
> 
> 3) define module types as a functor on MINMT and including ("Include")
> this common part. Everything takes INMT as a parameter.
> 
> 4) Instantiate the module and also include MINMT in it.
> 
> 
> 
[snip]
>   Parameter g : nat -> TSS.A.
[snip]
>   Definition g : nat -> nat := g_helper.

Also, the type of g is duplicated.  Ideally, it should be possible to
seal g without duplicating its type.

Kind regards,
Ralf