The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

Thanks for all the info!  The locked_with_key variant will not help me, I think, because I am comparing two different applications of the same locked lemma, where the arguments differ (in particular, the blow-up is caused by a failure of [apply left_identity_lemma] where [apply right_identity_lemma] would succeed, and the constants I am locking live inside the definition of composition.  (When I tried locking, I made sure that all arguments not part of the type of the lemma appeared after the [end] in the [match opaque_tt with tt => lemma end].)  I suspect the module-based locking will work (because why wouldn't it?), but it is very verbose.

Interestingly, these issues occur only with HoTT/coq.  There is a full log at https://gist.github.com/JasonGross/5894311 using just [Opaque], rather than locking.  In all of HoTT/coq, coq trunk, and coq 8.4, the change adds an extra minute to AdjointPointwise; I believe that this is a result of Coq having trouble seeing that two things are unifiable (I don't know how else to interpret the fact that [simpl; admit] is significantly slower than [admit]).  But there are an extra 232 minutes added in a different file, and only in HoTT/coq, by the [apply <the wrong identity lemma>] code!  Matthieu tells me that he is fixing this as I write this email, by making unification use the Opaque state.

-Jason

On Mon, Jul 1, 2013 at 8:13 AM, Georges Gonthier <gonthier AT microsoft.com> wrote:

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