The Coq mailing list

[Robert Dockins <robdockins AT fastmail.fm>]

I'm playing around with representations for graphs, and I've run into 
difficulty stating a definition I want.  I'd like to prove some results 
relating graphs represented via successor lists to a representation via an 
infinite "spanning tree," but Coq will not accept a cofixpoint definition 
that seems productive to me. The following is a simplified form.  Coq 8.3pl1 
and 8.4 give the same error (reproduced below).

I think this definition ought to be accepted, but it runs afoul of the 
guardness checker.  Apparently you cannot have fixpoints nested inside 
cofixpoints?  Is there any nice way to get around this?


Thanks,
Rob Dockins

========================

Require Import List.
  
Record graph (I:Type) := { succ_list : I -> list I }.

CoInductive spanning_tree :=
  | span : list (spanning_tree) -> spanning_tree.

CoFixpoint graph_to_span I (G:graph I) (root:I) : spanning_tree :=
   span ((fix f (l:list I) : list spanning_tree :=
              match l with
              | nil => nil
              | i::is => graph_to_span I G i :: f is
              end) 
         (succ_list I G root)).

=======================

Coq responds:

Error:
Recursive definition of graph_to_span is ill-formed.
In environment
graph_to_span : forall I : Type, graph I -> I -> spanning_tree
I : Type
G : graph I
root : I
Sub-expression "(fix f (l : list I) : list spanning_tree :=
                   match l with
                   | nil => nil
                   | i :: is => graph_to_span I G i :: f is
                   end) (succ_list I G root)" not in guarded form (should be
a constructor, an abstraction, a match, a cofix or a recursive
call).
Recursive definition is:
"fun (I : Type) (G : graph I) (root : I) =>
 span
   ((fix f (l : list I) : list spanning_tree :=
       match l with
       | nil => nil
       | i :: is => graph_to_span I G i :: f is
       end) (succ_list I G root))".