The Coq mailing list

[Fabrice Lemercier <nouvid-coq AT yahoo.fr>]

I want to formalize in Coq finite directed graphs with
a relation on paths. But I cannot find an elegant
definition.

My graphs are defined by:

  * The number of nodes n;

  * A list of arrows l: already here I have to use 
sig in order to make sure that source and target are
existing nodes (i.e., integers strictly less that the
number of nodes n);

  * A list of pairs of path: here I must use  sig  to
make sure that path are composed of existing arrows
(i.e., in the list of arrows l), and to make sure that
the two paths have the same source and target nodes!

It seems tricky. Is there more elegant way to define
such notion?

I had a look inside the library GRAPH-BASICS but it
does not seem simpler, on the contrary.

Thanks for any suggestion.



        

        
                
___________________________________________________________________________ 
Nouveau : téléphonez moins cher avec Yahoo! Messenger ! Découvez les tarifs 
exceptionnels pour appeler la France et l'international.
Téléchargez sur http://fr.messenger.yahoo.com