The Coq mailing list

[Emilio Jesús Gallego Arias <e AT x80.org>]

Hi Fred,

Fred Smith 
<fsmith1024 AT gmail.com>
 writes:

> I am looking for engineering advice to help me understand the tradeoffs
> between different ways of encoding the same information in Coq.
>
> As my exercise, I am trying to encode paths in a graph.  For simplicity
> these are just lists of edges where each edge ends where the next edge
> begins.
>
> Below is a Coq file that uses 3 different encodings.  Two inductive ones,
> and the third as a predicate.  What are the pros and cons of these choices?

You may also be interested in the math-comp's definition of path:

Fixpoint path T (e : rel T) x (p : seq T) :=
  if p is y :: p' then e x y && path y p' else true.

Actually there are some talks by George Gonthier where [IRRC] he
discussed the different tradeoffs among the different ways of encoding
paths [I'm afraid you'll have to google for the exact video link]

Cheers,
E.