The Coq mailing list

[Martin Bodin <martin.bodin AT inria.fr>]

Hi,

I'm facing a problem with a proof's final “Qed” which I've never seen 
terminated, and I would appreciate some details about how “Qed” exactly 
works.
I'm in the middle of a proof using some libraries, so I can't give a 
minimalistic example for the moment, but here are some traits of my 
current proof:
    → The proof script terminates relatively rapidly (~10s), and I 
think that I only used tactics returning well-typed terms (such as 
“eapply”, “econstructor”, “destruct” or “inversion”).
    → No existential variables are left at the end of the proof script.
    → The “Guarded” command terminates almost immediately without error.
    → I've let the “Qed” working for hours without any response. Given 
the CPU-usage of Coq, it is still actually working.
    → I'm using some type classes… but from what I've understood of 
them, tactics like “apply” should instantiate them, right?
    → I may have nested some matches, each of them with a 
non-negligible number of cases.

What surprises me is that the proof script created a proof term, which I 
think is already checked step by step by the tactics, spends far more 
time to be checked than the gathered amount of time to check every part 
of it.
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.

Do you have any idea of what might cause this problem?
Thank you by advance,
Martin.