Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Qed. does not terminate

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Qed. does not terminate


Chronological Thread 
  • From: Benoît Viguier <beviguier AT gmail.com>
  • To: "coq-club AT inria.fr" <coq-club AT inria.fr>, vst-user AT lists.cs.princeton.edu
  • Subject: [Coq-Club] Qed. does not terminate
  • Date: Fri, 29 Jun 2018 11:49:08 +0200
  • Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=beviguier AT gmail.com; spf=Pass smtp.mailfrom=beviguier AT gmail.com; spf=None smtp.helo=postmaster AT mail-ed1-f49.google.com
  • Ironport-phdr: 9a23:ggyi+BfwO4FoGvfQQEHvG1VKlGMj4u6mDksu8pMizoh2WeGdxcS7Yx7h7PlgxGXEQZ/co6odzbaO7ea4ASQp2tWoiDg6aptCVhsI2409vjcLJ4q7M3D9N+PgdCcgHc5PBxdP9nC/NlVJSo6lPwWB6nK94iQPFRrhKAF7Ovr6GpLIj8Swyuu+54Dfbx9HiTahYL5+Ngm6oRnMvcQKnIVuLbo8xAHUqXVSYeRWwm1oJVOXnxni48q74YBu/SdNtf8/7sBMSar1cbg2QrxeFzQmLns65Nb3uhnZTAuA/WUTX2MLmRdVGQfF7RX6XpDssivms+d2xSeXMdHqQb0yRD+v6bpgRh31hycdLzM37mHZhNFzgqxVrh2uqABwzpXOb42JLvdzZL/RcN0YSGdHQ81fVzZBAoS5b4YXEucOI+BYr47zv1sStRSxCgisBOzyyj9JmHD2x7Ax3uM6Hg7YwgwgHt0OsGnVrNrrLqcfSu+1zKzSwjXCa/Nawyvy6I/Nch04p/yHQLx+cc3UyUY1FgPFiE2dqZLkPzOay+QNsnaU7/B6WeKpj24qrRx6rDu3xso0lIXFmoYYxkrH+Ch52oo5O8G0RU1hbdOrFJZcrzyWOoR2T884Xm1kpSc3xqcbtZO1ciUG0oorywPCZ/GBboOG+AjsVPyLLjd9nH9leKywhxK18UW4z+3zTMi00FJToiVbj9bAq2kB1xLc58WDUPd98UCh2TGA1wDX9O5IO1w7la3eK5I5w74wkIQcsVjbEyPohEn7iLWae0Yk9+Sy9ejrfrbrqoWTOoJwkg3+N74hms27AeQ2KAgOWG2b9Pyn27L94035QbpKjuA3kqbHqpDXPssbpqujDA9U1oYv8QqwDzCj0NgAh3kIMEpFeA6bj4juI1zBPPf4De6mj1uwlDdr2uvJM6b6ApTNK3jDiK3ucax8605a0gozzMpQ64haCrEbc7rPXRq7v9vBSxQ9LgacwuD9Cdw72JlUETaEBbbcO6fPu3eJ4PguKq+CftlR8CjmN704/PP0pXs4gkMGO6Kym4MNaXazE+hhJQOUbWe/rM0GFDIgsww5yvDdtlyNTD9efT7mVa8i5z4mCY+8JYjGT4GpxreG2XHoTdVtemlaBwXUQj/TfIKeVqJUMXPAEopaijUBEIOZZcok3BCquhX9zuM+fOXR8ywc85nk0YosvrGBpVQJ7TVxSv+l/SSVVWgtxzEHQjY32OZ0pkkvkg7eg5g9uORREJlo390MUgo+MsSBnelzCtS3Vw6YO9nVGRCpRdKpBTx3RdU0kYcD

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



Archive powered by MHonArc 2.6.18.

Top of Page