The Coq mailing list

[Fred Smith <fsmith1024 AT gmail.com>]

Hi Emilio,

Thanks for the pointer.  George actually starts off his paper "Packaging Mathematical Structures" with exactly the path example I raised.  I still don't fully understand his use of coercions and voodoo Coq meta-theoretic programming, but it is certainly worth studying.

-Fred

On Mon, Dec 3, 2018 at 5:52 AM Emilio Jesús Gallego Arias <e AT x80.org> wrote:

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.