The Coq mailing list

[Andreas Abel <andreas.abel AT ifi.lmu.de>]

Hello Robert,

your definition looks fine, but it is known that the guardedness check 
is quite incomplete.  Sorry, I cannot help here, but out of curiousity I 
ported your definition to Agda and there it is accepted.

module GraphSpanningTree (I : Set) where

open import Coinduction
open import Data.List using (List; []; _∷_; map)

-- Graph as adjacency list
Graph = I → List I

data SpanningTree : Set where
  span : ∞ (List SpanningTree) → SpanningTree

module Mutual (g : Graph) where

  mutual

    graphToSpan : (root : I) → SpanningTree
    graphToSpan root = span (♯ (mapAdj (g root)))

    mapAdj : List I → List SpanningTree
    mapAdj []       = []
    mapAdj (i ∷ is) = graphToSpan i ∷ mapAdj is

Cheers,
Andreas

On 16.09.12 9:19 PM, Robert Dockins wrote:
> 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))".

--
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel AT ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/