The Coq mailing list

[Yucheng Zhang <yczhang89 AT gmail.com>]

I was reading the definition of acyclic graphs in Coq user-contrib library
GraphBasics.  It has the following definition in the file 
'GraphBasics.Acyclic' [1]:

> Inductive Acyclic : V_set -> A_set -> Set :=
>   | AC_empty : Acyclic V_empty A_empty
>   | AC_vertex :
>       forall (v : V_set) (a : A_set) (ac : Acyclic v a) (x : Vertex),
>       ~ v x -> Acyclic (V_union (V_single x) v) a
>   | AC_leaf :
>       forall (v : V_set) (a : A_set) (ac : Acyclic v a) (x y : Vertex),
>       v x ->
>       ~ v y -> Acyclic (V_union (V_single y) v) (A_union (E_set x y) a)
>   | AC_eq :
>       forall (v v' : V_set) (a a' : A_set),
>       v = v' -> a = a' -> Acyclic v a -> Acyclic v' a'.

From the above definition, I get that it does not allow multiple paths to 
exist
between two vertexes.  As an example, if I currently have a graph 'a->b->c', I
won't be allowed to add one more arc 'a->c', but the resulting graph is 
clearly
acyclic for me.

Is the definition incorrect, or am I mistaken somewhere..?


[1]: 
http://coq.inria.fr/pylons/contribs/files/GraphBasics/trunk/GraphBasics.Acyclic.html