walking a graph

walks.v

Require Import List.
Import ListNotations.

CoInductive Graph (X : Type) : Type :=
  | node : X -> list (Graph X) -> Graph X.

Arguments node {_}.

Fixpoint walks {X} (n : nat) (g : Graph X)
  {struct n} : list (list X) :=
  match g with
  | node x gs =>
    match n with
    | 0 => [[x]]
    | S m => map (cons x) (concat (map (walks m) gs))
    end
  end.

  (* 1 <-> 2 <-> 3
           ^   ^
           |  /
           v /
           4<
  *)

CoFixpoint example : Graph nat :=
    node 1 [two]
  with
    two := node 2 [example; three; four]
  with
    three := node 3 [two; four]
  with
    four := node 4 [two; three].

Compute walks 4 example.