The Coq mailing list

[Matthieu Sozeau <matthieu.sozeau AT inria.fr>]

> 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