The Coq mailing list

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

2017-04-27 17:40 GMT+02:00 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.

Hiding the definitions makes computation with these functions
impossible. So this is not what you are looking for.

If it is really important to hide these functions to the user you can
do the following:

1) Define a module type T with definitions hidden

Module Type T.
Variable f: ...
End T.

2) Start the module definition with

Module Foo<:T.
Definition t :=....
End T.

At this moment Foo.f is visible. Now you can hide it if you start a
new functor taking a T as argument instead of using Foo explicitely.

Modul Bar (F:T).
(* F.f is hidden. *)
...
End Bar.

Now if you want to have an instance of Bar you can do

Module B := Bar(Foo).

The problem with this approach is that each time you want to hide f
you need to start a functor. You generally end up with functors
everywhere. You should balance the pros and cons of simply showing the
auxiliary functions to the user.

Class types are generally considered an alternative to modules but I
don't know if there is a hiding mechanism.

Hope this helps,
Pierre






This is generally not true that function definition (even auxiliary
ones) are of no use for the user. Coq has dependent types, which means
that typing needs to compute with these functions (to check
convertibility).



You may hide Lemmas because there is no reason the typer will need to
reduce in there body (except lemmas used in well founded proofs used
in recursive functions). But you can't hide function definitions most
of the time because




> 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
>> >
>>
>