Coq: viewing proof term during proof script writing

Question

So, I've got a proof that looks like this:

induction t; intros; inversion H ; crush.

It solves all my goals, but when I do Qed, I get the following error:

Cannot guess decreasing argument of fix.

So somewhere in the generated proof term, there's non-well-founded recursion. The problem is, I have no idea where.

Is there a way to debug this kind of error, or to see the (possibly non halting) proof term that the tactics script generates?

Answer 1

You can use Show Proof. to view the proof term so far.

Another command that can help with seeing where the recursion went wrong is Guarded., which runs the termination checker on the proof term so far. You'll need to break apart the tactic script into independent sentences to use it, though. Here's an example:

Fixpoint f (n:nat) :  nat.
Proof.
  apply plus.
  exact (f n).
  Guarded.
(* fails with:
   Error:
   Recursive definition of f is ill-formed.
   ...
 *)
Defined.

Answer 2

You can use the Show Proof. command inside proof mode to print the proof term produced so far.