The Coq mailing list

[Assia Mahboubi <Assia.Mahboubi AT inria.fr>]

Dear Jason,

a more complete description of the mechanisms used in the Mathematical
Components library to control the impact of convertibility in type checking 
can
be found in the comments of the ssreflect.v file of the distribution.

You can either have a look at the online coqdoc documentation here :

http://ssr.msr-inria.inria.fr/~jenkins/current/ssreflect.html

[look for Term tagging (user-level)]

or go directly to line 271 of the ssreflect.v file included in the 
distribution
of the MathComp library here :

https://gforge.inria.fr/frs/?group_id=401
[both feit-thompson or ssreflect distributions will contain this file]

In particular, this comment mentions a third control mechanism, based on the 
use
of Module Types.

The pattern to follow is : suppose you want to opacify a function f : nat -> 
bool.

(* Implementation of the (computational version of the) f function *)
Definition f_ : nat -> bool := ...

(* Definition of an ad hoc interface for a locked version of f providing the
opaque version plus a (rewrite) lemma to substitute f with its computational
version when needed in proofs *)

Module Type fSig.
Parameter  f : nat -> bool. Axiom fEdef : f = f_.
End fSig.

(* Implementation of the suitable instance of the fSig interface. *)
Module fDef : fSig.
Definition f : nat -> bool := f_. Definition fEdef := refl_equal f_.
End fDef.

(* Exporting the previous module *)
Export fDef.

Hope this helps,

assia

Le 28/06/2013 18:55, Jason Gross a écrit :
> Thanks.
> 
> I have tried using the following lock definition based on version 11 of the 
> pdf
> at http://hal.inria.fr/inria-00258384:
> 
> Section lock.
>   (* Taken from ssreflect *)
>   Lemma master_key : unit. Proof. exact tt. Qed.
>   Definition locked {A} := match master_key with tt => fun x : A => x end.
>   Lemma lock : forall A x, x = locked x :> A.
>     intros; expand; destruct master_key.
>     reflexivity.
>   Qed.
> End lock.
> 
> And then I am comparing the following two versions:
> locked-version:
> Definition fooT : Prop := ....
> Lemma foo' : fooT.
>   ...
> Defined.
> Global Opaque foo'.
> Definition foo := locked foo'.
> Global Opaque foo.
> 
> qed-version:
> Definition fooT : Prop := ....
> Lemma foo' : fooT.
>   ...
> Defined.
> Global Opaque foo'.
> Lemma foo : fooT.
>   exact foo'.
> Qed.
> 
> 
> In the qed-version, it takes under 4 seconds for a particular [apply lem] to
> fail to unify types.  In the locked-version, it takes around 6000 seconds.  
> I
> have both versions at 
> http://people.csail.mit.edu/jgross/slow-opaque/catdb-qed/
> and http://people.csail.mit.edu/jgross/slow-opaque/catdb-lock/; the file is
> LaxCommaCategory.v (the lock is in Functor.v, in the ComposeFunctors
> definition), and the application is LaxSliceCategory_LeftIdentity on the 
> third
> branch of LaxSliceCategory (which is actually taken
> by LaxSliceCategory_RightIdentity).  These are compiled with the trunk 
> version
> of HoTT/coq.
> 
> -Jason
> 
> On Wed, Jun 26, 2013 at 5:19 PM, Maxime Dénès 
> <mail AT maximedenes.fr
> <mailto:mail AT maximedenes.fr>>
>  wrote:
> 
>     Hello Jason,
> 
>     Coq indeed has a variety of notions related to opacity of constants, 
> with
>     often subtle differences.
> 
>     The "Opaque" command plays two roles to my knowledge: it prevents
>     delta-unfolding in unification, and delays that unfolding in the kernel
>     comparison of terms. It should be noted that "Opaque" does not prevent 
> Coq's
>     kernel from accessing the body of a constant.
> 
>     On the other hand, Qed really makes a constant really opaque, in the 
> sense
>     that its body will not be accessed by the kernel once declared.
> 
>     To sum up, if c1 and c2 are constants declared using Opaque, they will 
> be
>     unifiable only if c1 = c2 as names, but convertible as soon as they have
>     convertible bodys. If c1 and c2 are declared using Qed, they will be
>     unifiable or convertible only if c1 = c2 as names.
> 
>     As for the larger amount of time spent checking the version of your file
>     which uses "Opaque", it is probably due to costly terms comparisons, 
> which
>     are prevented by the use of Qed.
> 
>     As a final note, SSReflect provides some machinery to "lock" a 
> constant, and
>     hence avoid these costly comparisons, while retaining the ability to
>     generically unlock the constant manually.
> 
>     Hope it helps.
> 
>     Maxime.
> 
>     On 26/06/2013 22:58, Jason Gross wrote:
> 
>         Hi,
>         Can someone explain to me the differences between [Lemma foo : fooT.
>         ... Qed.] and [Lemma foo : fooT. ... Defined. Global Opaque foo.]?
>          The ones I know are:
>         The former is affected by "-dont-load-proofs", the latter is not.
>         The latter can later be made [Transparent], the former cannot.
> 
>         Neither of these explains to me why using Qed in one place allows 
> one
>         of my files to compile in about 4 minutes (about 3 minutes, 45 
> seconds
>         with -dont-load-proofs), but using Defined + Global Opaque in that
>         place causes the other file to take about 90 minutes to compile.  My
>         current hypothesis is that it has something to do with universe
>         polymorphism, as this is using HoTT/coq.
> 
>         -Jason
> 
> 
>