The Coq mailing list

[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