The Coq mailing list

[Pierre Courtieu <pierre.courtieu AT gmail.com>]

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.

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.



(* Minimal module type to write visible definitions in main module
type. This will be taken as parameter by all module types AND modules,
that is the main point. *)
Module TEST_SIG_SIG.
  Variable A: Type.
End TEST_SIG_SIG.

(* Visible definitions are stored in a functor, this is the shared
part (included in both main module type and main module. *)
Module Type TEST_F(TSS:TEST_SIG_SIG).
  Include TSS.
  Definition f : TSS.A -> TSS.A := fun n => n.
End TEST_F.

(* The main module type  *)
Module Type TEST_SIG(TSS:TEST_SIG_SIG).
  Include TEST_F(TSS).
  Parameter g : nat -> TSS.A.
  Axiom t : True.
End TEST_SIG.

(* Instantiating the parameter module*)
Module TEST_nat.
  Definition A := nat.
End TEST_nat.

(* Instantiating the main module type *)
Module TEST : TEST_SIG(TEST_nat).
  Include TEST_F(TEST_nat).

  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.

Hope this helps.

Pierre


2017-10-12 16:50 GMT+02:00 Anders Lundstedt 
<anders AT anderslundstedt.se>:
> Hi,
>
>
> I am doing some theorem proving in Coq. My development is split over
> multiple files. 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. So, something like this:
>
> (* exposing the definition of f *)
> Definition f : nat -> nat := fun n => n.
>
> (* g should be opaque, its definition is not shown here *)
> Parameter g : nat -> nat.
>
> (* opaque theorems *)
> Axiom t : True.
>
> (* implementations *)
>
> (* helper lemma, should not be exposed at all *)
> Lemma helper_lemma : True.
> Proof. exact I. Qed.
>
> Theorem t : True.
> Proof. apply helper_lemma. Qed.
>
> (* helper function, should not be exposed at all *)
> Definition g_helper : nat -> nat := S.
>
> Definition g : nat -> nat := g_helper.
>
>
> Questions:
>
> (1) What is the best way to accomplish this in Coq?
>
> (2) Is this a good idea? If not, what should I do instead?
>
>
> Regarding (1): I can achieve this using modules, but I have not found
> a way to avoid having to define all transparent definitions
> twice—first in the module type and then in the module. (If I also have
> notations I want to expose it seems even worse: I have to define them
> in the module type and in the module and then outside the module.)
> Here is how I have achieved the above example using modules:
>
> Module Type TEST_SIG.
>
>   Definition f : nat -> nat := fun n => n.
>
>   Parameter g : nat -> nat.
>
>   Axiom t : True.
>
> End TEST_SIG.
>
> Module TEST : TEST_SIG.
>
>   Definition f : nat -> nat := fun n => n.
>
>   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.
>
>
>
>
> Anders