4

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?

jmite
  • 8,171
  • 6
  • 40
  • 81
  • Note that you can write `{struct n}` to tell Coq that the decreasing argument should be `n`, and thereby get a better error message. – Jason Gross Aug 02 '18 at 13:12

3 Answers3

6

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.
Tej Chajed
  • 3,749
  • 14
  • 18
  • Does `Guarded` work when Coq cannot guess the decreasing argument of fix? – Jason Gross Aug 02 '18 at 13:13
  • It turns out when you define a Fixpoint in proof mode, Coq always uses the last argument as the decreasing argument (and if it's not inductive, the command just fails). Then `Guarded` ensures that this argument is decreased. Note that you can always explicitly provide a `{struct n}` annotation at definition time, though. – Tej Chajed Aug 03 '18 at 13:58
4

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

Arthur Azevedo De Amorim
  • 23,012
  • 3
  • 33
  • 39
3

In addition to the other excellent answers, I also want to point out that using induction inside an interactive-mode Fixpoint is usually a mistake, because you're recursing twice. Writing fixpoints in interactive mode is often tricky because most automation tools will happily make a recursive call at every possible opportunity, even when it would be ill-founded.

I would advise to use Definition instead of Fixpoint and use induction in the proof script. This invokes the explicit recursor, which allows for much better control of automation. The disadvantage is decreased flexibility since fixpoints have fewer restrictions than recursors - but as we've seen, that is both a blessing and a curse.

Lily Chung
  • 2,919
  • 1
  • 25
  • 42
  • 1
    If you are very careful, using `induction` inside of a `Fixpoint` is a relatively easy way to prove things about functions which contain nested fixpoints. You have to make sure to specialize the fixpoint before running anything like `auto`, though. – Jason Gross Aug 02 '18 at 13:10
  • 1
    @JasonGross That's reasonable, though I would also consider abstracting the necessary nested induction into its own scheme so that there's no need to be so careful. – Lily Chung Aug 06 '18 at 03:44