The Coq mailing list

[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