coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Understanding why Qed is slow

From: Jason -Zhong Sheng- Hu <fdhzs2010 AT hotmail.com>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: [Coq-Club] Understanding why Qed is slow
Date: Mon, 11 Feb 2019 14:26:48 +0000
Accept-language: en-CA, en-US
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=fdhzs2010 AT hotmail.com; spf=Pass smtp.mailfrom=fdhzs2010 AT hotmail.com; spf=Pass smtp.helo=postmaster AT NAM01-BN3-obe.outbound.protection.outlook.com
Ironport-phdr: 9a23:hG49UBVnYWTtQ4V4f20IN/HndjDV8LGtZVwlr6E/grcLSJyIuqrYbBeFt8tkgFKBZ4jH8fUM07OQ7/iwHzRYqb+681k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i764jEdAAjwOhRoLerpBIHSk9631+ev8JHPfglEnjWwba9xIRmssQndqtQdjJd/JKo21hbHuGZDdf5MxWNvK1KTnhL86dm18ZV+7SleuO8v+tBZX6nicKs2UbJXDDI9M2Ao/8LrrgXMTRGO5nQHTGoblAdDDhXf4xH7WpfxtTb6tvZ41SKHM8D6Uaw4VDK/5KptVRTmijoINyQh/W/XlMJ+kb5brhyiqRNjzIHZe5uaOOZicq7HYd8WWXdNU8BMXCJBGIO8aI4PAvIFM+lCtIn9oF0OpganCQavBOPvzTlIhnDr1qMn0+QuDwfG3AM5E9kTsnrUscj+OaAcUe+ozKnJzC7DY+1K1Tvg9ITFaRAhofaQXbJ1a8XRyE0vGxnZgVWXrIzoJjWY3fkOvWiD9+dtWv6jh3Qjpg1vuDSj2t0gh4vLi44NxFDL6yZ0zJowKNC9U0F0fcKrHZhVui6BK4d7Q8EvTmRmtSkh0LILuZu2fCYLxZkkxRPSbeGMfZKS7RL5TumRJC91hHJ7d7K7gBa/6VCux/H7WMWozVpGtzdInMHCu3wU0Bzc8daIRuF6/ke8xTaAzAfT6vxCIU8pj6bbM4QhwrkslpUNrUvDAi72mELwjKOMcUUk5/So6+DgYrXhpZ+QLZN7igb7Mqg2m8y/B/o3MhQWUmWU5eiwzrnu8VPjTLlWlPE7kKvUvIjfJcsBp665BwFV0pwk6xa6Fzqm3skXnXkGLVJeZh6Lk5XlN03VLfD4Cve/n1Gsny1qx/DCJLHuHpLNLn3bnLf7Ybl981JcyBY0zd1H+51UDagBLOvvVU/1qdzXFQQ0Mxe0wubiENVyzJkSWWOJAq+DMaPdq0WE5uw1I7rEWIhA8j36Mr0u4+PkpX4/g14UO6ezl9NDY3ehW/9iPk+xYHz2g95HH31c7SQkS+m/qlSZVjgbIkSyWKQzrgo7BYSpSM/jW8j5jrCBzjzhRsQOTmBBFlWFEHOufIKBDaRfIBmOK9Nsx2RXHYOqTJUsgEn35V3KjoF/J++RwRU28Jfq1dx7/erWzEpg9TtoCs2c1yeGSGQmxzpUFQ9z57h2pAlG8nnGybJx2qcKFdtP4vpIVkExMpuOl7UnWeC3YRrIe5KycHjjQtiiBm1uHPQY5odXJmxbQJClhB2F2De2CbgIkbDNHIYz7q/Xw3n2IYB61mrC064iyVIhR5kWOA==

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?

Sincerely Yours,

Jason Hu

[Coq-Club] Understanding why Qed is slow, Jason -Zhong Sheng- Hu, 02/11/2019
- Re: [Coq-Club] Understanding why Qed is slow, Matthieu Sozeau, 02/11/2019
  - Re: [Coq-Club] Understanding why Qed is slow, Jason -Zhong Sheng- Hu, 02/12/2019