I ran into a situation where a proof seems to work fine (no more subgoals) but then Qed seems to run forever. I am fairly new to Coq, so I have no idea how to deal with this. Are there certain situations where this happens, or is this not a common occurrence? Is this some kind of limitation I'm not aware of? Is there some known approach to work around it?

There are certain situations where this happens (here's a recent one: https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/How.20to.20Debug.20slow.20QED.3F) but from my experience it is not common. Can you give some more context or even show an excerpt of your file / the whole file?

What helped me in the end is the OCaml debugger. With an endless Qed it is easy to break in the right spot (just hit Ctrl+C after a minute) and one can go back and forth in time in ocamldebug. The Coq printers produce readable result for the kernel terms involved which where easy to recognize for me although I don't know much about the Coq kernel. If you are on Mac you need a few tweaks to get the printers loaded. Other methods didn't really help me to debug my Qed issue.

In my case the root cause was a hnf in a hypothesis.

Last updated: Oct 04 2023 at 20:01 UTC