The Coq mailing list

[Gregory Malecha <gmalecha AT cs.harvard.edu>]

I assume that you are abbreviating some things here. Given that the problem is in the details, it might be helpful to give a minimal example that I/other people can run.

Occasionally, it can be helpful to give an explicit cast to tell Coq exactly what type you expect something to have so that it doesn't go too crazy with unfolding.

On Wed, Sep 3, 2014 at 8:33 AM, Martin Bodin <martin.bodin AT inria.fr> wrote:

Hi,

Thanks a lot to both of you!  I have indeed forgotten both these effects.

After tweaking a little my proof—using the tactic “abstract” to understand where the “Qed” needs time—, I have extracted a “minimalistic” example of the following form:
Definition test : A -> B -> C.
Proof.
  exact (fun a => proj1 T). (* Immediate response from Coq *)
Qed. (* Takes a lot of time (I didn't try to let it go on) *)
Where “T” is of type “B <-> C” using “a” as a free variable (and “A”, “B” and “C” are several lines long).

I've tested the “Print Universes.” command before the definition, after the “Proof” keyword, and before the “Qed” keyword and they all give the same amount of constraints. Although these commands outputs several thousands of lines, their outputs are identical: I concluded (in relief!) that this slow final check wasn't due to the universe checking.

I'm thus thinking that Gregory Malecha's explanation may be the cause of this… but I don't understand where I use a particular reduction in this example :-\ Does the “exact” tactic a lot of computation work?

What's also interesting is that the following definition is immediately accepted by Coq:
Definition test' : A -> (B <-> C).
Proof.
  exact (fun a => T).
Qed.

Someone suggested to me that I may be using some opaque terms that “Qed” wants to unfold more than reasonably, but that the “exact” tactic accepts as-is. Do you think that it's possible?

I have to admit being a little lost in this particular example… and I don't think that it would really help to have my full development (I am afraid that the term “T” depends on a lot of file ☹) :-\
Any idea would be highly welcomed! ☺
Martin.

If you are relying on certain types of reductions, e.g. doing [cbv] or [compute] that do a lot of work this can also be an issue. Coq's kernel essentially uses something like [lazy] to do reductions which can be significantly slower.

On Tue, Sep 2, 2014 at 11:57 AM, Robbert Krebbers <mailinglists AT robbertkrebbers.nl> wrote:

On 09/02/2014 05:32 PM, Martin Bodin wrote:

I naively thought that “Qed” only consists of a guard checking followed
by a type checking, but I guess that I've missed one step spending in my
example far more time than both.

It is also checking whether the universes are consistent, which may take a non-neglectable amount of time. You can figure out whether universe checking is the problem my turning off universe polymorphism entirely (*). For this you can patch Coq using [1].

In the Coq development of my C11 semantics [2], the majority of the definitions is parametrized by a type class that describes implementation defined behaviors. This parameterization was causing universe checking to become incredibly slow, Qeds were taking minutes for proof scripts that check in less than a second. I temporarily solved the problem by putting many data structures in the sort [Set] instead of the universe polymorphic sort [Type].

In case your problem is indeed caused by universe checking, you may also try Coq trunk, which contains a new implementation of universe polymorphism. I haven't tried it yet, so I do not know whether it solves the problem in my development.

Robbert

(*) Disclaimer: this makes Coq inconsistent!

[1] https://raw.githubusercontent.com/vladimirias/Foundations/master/Coq_patches/patch.type-in-type
[2] https://github.com/robbertkrebbers/ch2o/tree/new_memory

--

gregory malecha

http://www.people.fas.harvard.edu/~gmalecha/

--

gregory malecha

http://www.people.fas.harvard.edu/~gmalecha/