The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

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