Skip to Content.
Sympa Menu

coq-club - [Coq-Club] fixpoint nested inside cofixpoint

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] fixpoint nested inside cofixpoint


Chronological Thread 
  • From: Robert Dockins <robdockins AT fastmail.fm>
  • To: Coq Club <coq-club AT inria.fr>
  • Subject: [Coq-Club] fixpoint nested inside cofixpoint
  • Date: Sun, 16 Sep 2012 12:19:32 -0700

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))".




Archive powered by MHonArc 2.6.18.

Top of Page