coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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))".
>
- [Coq-Club] fixpoint nested inside cofixpoint, Robert Dockins, 09/16/2012
- Re: [Coq-Club] fixpoint nested inside cofixpoint, Andreas Abel, 09/18/2012
- Re: [Coq-Club] fixpoint nested inside cofixpoint, Chung-Kil Hur, 09/18/2012
- [Coq-Club] Re: fixpoint nested inside cofixpoint, Dimitur Krustev, 09/18/2012
Archive powered by MHonArc 2.6.18.