Skip to Content.
Sympa Menu

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

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] fixpoint nested inside cofixpoint


Chronological Thread 
  • From: Chung-Kil Hur <gil.hur AT gmail.com>
  • To: Robert Dockins <robdockins AT fastmail.fm>
  • Cc: Coq Club <coq-club AT inria.fr>
  • Subject: Re: [Coq-Club] fixpoint nested inside cofixpoint
  • Date: Tue, 18 Sep 2012 10:16:47 +0100

Hi Rob,

If you don't mind the computability of graph_to_span, you can define
it as a coinductive predicate.

------------------------------------------
CoInductive graph_to_span_list I (G: graph I)
: list I -> list spanning_tree -> Prop :=
| g2s_nil : graph_to_span_list I G nil nil
| g2s_cons: forall i is ti ts
(HD: graph_to_span_list I G (succ_list I G i) ti)
(TL: graph_to_span_list I G is ts),
graph_to_span_list I G (i::is) (span ti::ts)
.

Definition graph_to_span I G root t :=
match t with span ts => graph_to_span_list I G (succ_list I G root) ts end.
--------------------------------------------

One advantage of doing this is that you can completely avoid
guardedness checking when you reason about graph_to_span using our new
library "paco".

http://plv.mpi-sws.org/paco/

I hope this helps.
Best,
Gil


On Sun, Sep 16, 2012 at 8:19 PM, Robert Dockins
<robdockins AT fastmail.fm>
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))".
>



Archive powered by MHonArc 2.6.18.

Top of Page