The Coq mailing list

[Jason -Zhong Sheng- Hu <fdhzs2010 AT hotmail.com>]

Hi Matthieu,

thx. indeed, proving inductive principle separately works much better and the inductive principle itself only takes 8 seconds to close. I guess in the original case, it indeed tries to unfold the definition of the proposition itself, which in turn could be very expensive while quite unnecessary.

Sincerely Yours,

Jason Hu

---

From: coq-club-request AT inria.fr <coq-club-request AT inria.fr> on behalf of Matthieu Sozeau <matthieu.sozeau AT inria.fr>
Sent: February 11, 2019 9:49 AM
To: Coq Club
Subject: Re: [Coq-Club] Understanding why Qed is slow

 

> Le 11 févr. 2019 à 15:26, Jason -Zhong Sheng- Hu <fdhzs2010 AT hotmail.com> a écrit :
>
> Hi,
>
> I was proving a quite intuitive lemma the termination of which is quite obvious to me on paper. However, it took Coq almost 4 hours to close Qed.
>
> <infomsg>Finished transaction in 13391.78 secs (13357.157u,6.398s) (successful)
> </infomsg>
>
> It's not a direct structural induction in the sense that the structure does not decrease layer by layer, but just sometimes it decreases by two layers. Hence I define the lemma directly using Fixpoint and rely on termination checking for correctness. I suppose that's why Qed took so long to come back. However, I don't understand exactly why because the termination is almost immediate to me (and I suppose Qed passed termination checking for the same reason). Is there any way for me to optimize the Qed time?

Hi Jason,

  It could be that the guard checker is looking for recursive calls to check in parts of the proof that are not
really using the recursive function but still depend on it, potentially doing costly unfoldings of definitions. One way to avoid that is to clear the assumption as soon as you do not need it anymore. Another way is to prove your elimination principle separately or to switch to well-founded induction, to avoid guard checking entirely in your lemma.

Best,
— Matthieu