The Coq mailing list

[Georges Gonthier <gonthier AT microsoft.com>]

  Hi all,
 Let me fill in a few more technical points:
  - the ssreflect library uses four different "locking" idioms:
       + The weakest (nosimpl) only affects the heruristics of the simpl 
reduction strategy, and will be subsumed by some of the modifiers of the new 
Arguments command.
      + The strongest, described by Assia, uses module signature ascription. 
It is supported by an "Unlockable" interface supporting a generic unlock 
rewrite rule. In Assia's example one would register f  and fEdef with 
Unlockable, and avoid exporting the whole fDef module, using, e.g., Notation 
f := fDef.f instead
(one should also use Local Notation f_ := (...) to "define" f_, as this 
avoids the creation of a spurious constant).
      + There's a somewhat weaker "Definition f := locked_with my_key f_" 
mechanism that avoids the use of Modules, which are rather verbose and are 
incompatible with the use of Section parametrization. This relies on you 
defining a Qed-opaque my_key : bool specific to each definition you need to 
lock, and generically supports the Unlockable interface.
   + Finally, the locked/master_key, which you experimented with, is a 
degraded version of the former, where the same key is used for all 
definitions. It is intended for controlling the behaviour of rewrite/simpl on 
the fly, rather than defining opaque constants. However, it was used for the 
latter purpose in the past, until performance issues showed that this was a 
bad idea.
- With the strongest method Coq believes that the abstracted constant "f" is 
a new axiom (earlier versions of Coq would report it as such!), so it is 
computationally inert.
- With the weaker method (unlocked_with), the constant f is "almost inert", 
in that expanding f and unlocked_with (which happens atomically) exposes
   match my_key with tt => f_ end which is inert.
- The reason "almost inert" might not be good enough is that in principle 
that single constant expansion (delta-)step creates a backtracking point for 
term comparison; since the latter does no direct caching, this may multiply 
failed comparison time by 2^n, where n is the number of locked definitions in 
your goal with all transparent constants expanded.
- Usually things are not that bad because lazy reduction provides some 
indirect caching, through sharing of delta-beta reductions (but it does 
happen, and it may have been the case for you).
- Unfortunately, sharing of delta-beta reductions can introduce problems on 
its own, which are potentially more severe than the above. Constant 
expansions that happen during failed comparisons are shared throughout, 
including in comparisons that succeed. These then become much slower, because 
they need to traverse the entire expanded tree (which may be exponential in 
the actual graph representation) instead of simply equating constants (in 
O(1)). The effect can be quite noticeable (I've experienced x100,000 
slowdowns...).
- The above problem can be compounded if the f_ term in locked_with my_key f_ 
is not a constant but something that has reductions and can be affected by 
the above issue. This can easily happen via the insertion of section 
parameters, so some care is required (roughly, f_ should only have explicit 
parameters of the type of f as arguments). At the worst, setting f a b c := 
locked (f_ a b c) does not prevent Coq from computing f_ a b c.
- A similar issue can happen if you have multiple opaque constants 
(implementing, say, different operators of a theory) that share the same key, 
e.g. if you use f := locked f_ and g := locked g_, because comparing f and g 
unequal will require to compare f_ and g_ unequal, possibly triggering the 
issues above. Worse, because the kernel comparison code (but not the 
unification code!) compares arguments right-to-left, comparing f a b to g c d 
will try to compare b to d, then a to c, before comparing f_ to g_, thus 
performing arbitrarily large and completely unnecessary work.
- These issues have been known for at least seven to eight years, but a 
satisfactory solution has remained elusive. In particular, it seems that 
naïve blanket caching strategies, such as hash-consing all Coq terms, only 
mitigates the problem while introducing so much constant overhead as to make 
Coq significantly slower overall.

      I hope this will help clarify the issue a bit, and perhaps help you 
understand better what's going on in your examples. If you do come across 
interesting findings, please share them -- I know several people that have a 
keen interest in making things go better.

Best,
   Georges


-----Original Message-----
From: 
coq-club-request AT inria.fr
 
[mailto:coq-club-request AT inria.fr]
 On Behalf Of Assia Mahboubi
Sent: 29 June 2013 13:38
To: 
coq-club AT inria.fr
Subject: Re: [Coq-Club] Difference between [Opaque] and [Qed]?

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