[Coq-Club] Qed. does not terminate

[Benoît Viguier]

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?

[Fabian Kunze]

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

Post by Benoît Viguier
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).
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 <https://maps.google.com/?q=Toernooiveld+212%0D%0A6525+EC+Nijmegen,+the+Netherlands&entry=gmail&source=g> | www.viguier.nl