The Coq mailing list

[Maxime Dénès <mail AT maximedenes.fr>]

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