The Coq mailing list

[Abhishek Anand <abhishek.anand.iitg AT gmail.com>]

Hi,

I'm getting the following error at the end of a long proof:

"Recursive definition of approx_trans is ill-formed"

The error message then goes on for several lines listing the variables and their types

in the environment. After that, it says:

Invalid recursive call in a branch of

"let (_, H) :=

     let (a, a0) :=

         (let (_, H) :=

              let (a, a0) :=

                  let (a, a0) :=

                      match

                        match

                          match

                            (if (fix F (l : list NVar) :

                                   (fun la : list NVar =>

                                    forall lb : list NVar,

                                    disjoint la lb[+]!disjoint la lb) l :=

                                   match

                                     l as l0

...............

(thousands of lines)

The proof begins with:

  cofix.

  intros ? ? ? Hab Hbc.

  constructor.

So, I think that all co-recursive calls are made inside the constructor for the co-inductive return type.

I'm invoking the recursive call much later in the proof. I'm not sure how to check that the recursive call is 

directly under the constructor. The output of Show Proof runs into several thousands of lines.

Is there a way to debug such errors?

I googled for "Invalid recursive call in a branch of" and the only thing I found is:

http://www.lix.polytechnique.fr/coq/bugs/show_bug.cgi?id=2246

I understand that my question is very vague. But I could not come up with an example that is simple enough to post here. If these error messages could somehow indicate a debugging strategy, I'd be grateful to know that.

Is there a better way to do proofs by coinduction?  Are sized types(http://coq.inria.fr/files/coq5_submission_5.pdf) available in some version of Coq?

Thanks,

-- Abhishek

http://www.cs.cornell.edu/~aa755/