The Coq mailing list

[Julia Belyakova <julbinb AT gmail.com>]

Jason, Gaëtan,

Thank you for replies!

Local definitions are still available through qualified names. And I would like to hide them completely.

My motivation is as follows: I want to provide a module with some datatypes, functions, and theorems about them. To implement those functions and prove theorems, I use many auxiliary functions and lemmas, which are of no utility for the user of the module.
So I want to keep an interface of the module clean and concise. For example, when the module is printed, I don't want it to show all the aux stuff.

Opaque typing is ok for hiding aux lemmas, because I still can use (apply) main theorems to prove something outside of the module. But what hits me is that it's not possible to use functions. The module becomes totally useless.

In the worst case I will simply put all the aux stuff into a submodule, so that an interface of the main module does not look dirty.

--

Kind regards, Julia

чт, 27 апр. 2017 г. в 11:12, Gaetan Gilbert <gaetan.gilbert AT ens-lyon.fr>:

What do you mean by hiding? Is "Local Definition"/"Local Lemma" enough?
(https://coq.inria.fr/distrib/current/refman/Reference-Manual003.html#hevea_command10)

Gaëtan Gilbert

On 27/04/2017 03:03, Julia Belyakova wrote:
> Thank you for reply!
>
> Are there other ways to hide some parts of a module except for opaque
> typing? I am primarily interested in hiding auxiliary lemmas.
>
> It seems to me strange though that one cannot actually _use_ functions
> from the opaque-typed module.
>
> --
> Kind regards,
> Julia
>
>
> ср, 26 апр. 2017 г., 17:10 ikdc <ikdc AT mit.edu <mailto:ikdc AT mit.edu>>:
>
>     On 04/26/2017 04:57 PM, Julia Belyakova wrote:
>     > Dear Coq users,
>     >
>     > I guess it's a stupid question, but...
>     >
>     > I want to define a module with certain parts being hidden. For
>     this I
>     > define a module type and then use opaque typing for the module.
>     And the
>     > problem is that now I cannot compute functions of the module, their
>     > definitions are not accessible.
>     >
>     > Please, find a simple example below.
>     >
>     > Module Type Addition.
>     >   Parameter t : Type.
>     >   Parameter add : t -> t -> t.
>     > End Addition.
>     >
>     > Module MAddition : Addition with Definition t := nat.
>     >   Definition t := nat.
>     >   Definition add x y := x + y.     (* I want this to be available *)
>     >   Definition priv_id (x : t) := x. (* This must be hidden *)
>     > End MAddition.
>     >
>     > (* priv_id is not available as desired *)
>     > (* Compute (MAddition.priv_id 4). *)
>     > (* add is available, but the call does not reduce to 7 *)
>     > Compute (MAddition.add 3 4).
>     >
>
>
>     If I understand correctly, I don't think you can do this. The fact
>     that
>     the module type is opaque means that any program which uses a module
>     with that type must behave the same way; in particular it may not
>     unfold
>     the definitions hidden by the module type.  You could of course do
>     this:
>
>
>     Module MAddition : Addition
>          with Definition t := nat
>          with Definition add := fun x y => x + y.
>        Definition t := nat.
>        Definition add x y := x + y.
>        Definition priv_id (x : t) := x.
>     End MAddition.
>
>
>     But if you want to be able to compute through [add], then perhaps the
>     module type "Addition" isn't actually the interface you want to be
>     using
>     in the first place.
>
>     I don't know very much about the module system, so someone please
>     correct me if this is wrong.
>
>     --
>     Istvan Chung
>