coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Qed. does not terminate

From: Fabian Kunze <kunze AT ps.uni-saarland.de>
To: coq-club AT inria.fr
Cc: vst-user AT lists.cs.princeton.edu
Subject: Re: [Coq-Club] Qed. does not terminate
Date: Fri, 29 Jun 2018 14:09:53 +0200
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=kunze AT ps.uni-saarland.de; spf=Pass smtp.mailfrom=kunze AT ps.uni-saarland.de; spf=None smtp.helo=postmaster AT theia.rz.uni-saarland.de
Ironport-phdr: 9a23:1XGgchZn0WcAo6JwjxRd1JX/LSx+4OfEezUN459isYplN5qZoMW9bnLW6fgltlLVR4KTs6sC17KI9fi4EUU7or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6arXK99yMdFQviPgRpOOv1BpTSj8Oq3Oyu5pHfeQpFiCa8bL9oMBm6sRjau9ULj4dlNqs/0AbCrGFSe+RRy2NoJFaTkAj568yt4pNt8Dletuw4+cJYXqr0Y6o3TbpDDDQ7KG81/9HktQPCTQSU+HQRVHgdnwdSDAjE6BH6WYrxsjf/u+Fg1iSWIdH6QLYpUjmk8qxlSgLniD0fOjE2/mHYiMx+gqxYrhy8uRJw35XZb5uJOPdkZK7RYc8WSGhHU81MVyJBGIS8b44XAuQBJ+lXtIj9qEEIrRCjAAesGeXvyz5WiXTr2qA60PkhEQfH3QM+BN8OqG/UoM/oNKcUUOC51bLIwi/ZYPNM3Tfy8o7IfQ07rf6RQ719aMzcwlQhGQPCi1Wfs43lPzWN2+QTsmib4PdgVeOxhG49sQ1xpDyvyt8jionOgYIVxVTE+jtjzIovOdK4T0t7bNi5G5VTryGXL5Z6T80tTm1yvCs3y6cKtJyhcCUE1Zgr3wDTZ+CDfoSS4R/uVPydLSlliH9qYr6yiBK//E69wePmTMa0ykxFri9dn9nMqH8N0xvT59CbSvt94Eih2CyA2xrJ6uBFO0w0iKzbK584zr4rjJUcq17DHivsl0XwkaCabFgr9faw5+TmZLXpuIOcOpdphgzwPakigMiyDOUiPgUMRWSW9/mw2KXm/ULjQbVKivM2krPesJDfPckbpbO5AwlU04k98Bu/Fyym3M4FnXkBLVJJYQmHgJLzNFHUJPD3F/G/jEm2nDh22f/KJqfhDYnVLnjfjLfheq5w5FJbyAoq1NxQ+5ZUCqwaL//oQU/wtNnYDgcjPACuwubnDs991oIEVm6VDK+ZKvCajVjd7eU2ZuKIeYU9uTDnKvFj6eS9o2U+nAozdKOo1J1fS22+DPkud0aEZ2jhqs8aV3oMv08lReXwjFSEXXhfaiDhDOoH+jgnBdf+Xs/4TYe3jenZhXbpLthtfmlDT2u0PzLtfoSAVe0LbXjKcNd61CECVP26QoY70RiouEn2xug+d7aGymgjrZvmkeNNyajLjxhorW5sFIKA1WDIVGh9hGcBQTNw0K0t+RUgmGfG6rBxhrljLfIW5/5NVV1kZ4Lcwu1zTcrgHB/Hf5KSQV+8RtygDXc9Q4Bpzg==

Hi Benoît,

Does the Guarded command terminate if put right before the QED? Otherwise you could try to bisect the problem with that.

You could also try to add False as an axiom/Parameter, and use this to close of parts of your proof to bisect the Problem.

Best,

Fabian

Benoît Viguier <beviguier AT gmail.com> schrieb am Fr., 29. Juni 2018, 11:49:

Dear all,

I'm faced with quite an anoying problem. I get my proofs in the state "No more subgoals" totally fine.
But then when I start Qed my proofs just does not terminate (I did try to let it run for 15 hours).

I did split my proofs into sub lemmas (I have about 14 of them).
So now my proofs looks like that (using VST):
forward
forward
forward
entailer!
apply lemma_1; assumption
forward
rewrite ...
2: apply lemma_2 ; eauto
forward
...
I know that Opaque won't help as those are not visible by the Type-checker.

What can I do to solve this problem?
-- 
Kind regards,

Benoît Viguier
Software Engineer - PhD Student | Cryptography & Formal Methods
Radboud University | Mercator 1, room 03.17, Toernooiveld 212
6525 EC Nijmegen, the Netherlands | www.viguier.nl

[Coq-Club] Qed. does not terminate, Benoît Viguier, 06/29/2018
- Re: [Coq-Club] Qed. does not terminate, Fabian Kunze, 06/29/2018