The Coq mailing list

[Fred Smith <fsmith1024 AT gmail.com>]

Hi,

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?

Thanks,

Fred

----- path.v below -----

(* Experiments in encoding paths in Coq.

A path is simply a list of edges where the destination of the

preceding edge is the source of the next edge.

*)

Require Import List.

Definition vertex := nat.

Definition edge := (vertex * vertex)%type.

(* Simple encoding as lists with a predicate *)

Fixpoint path (l : list edge) :=

  match l with

  | nil => False

  | hd :: tl => (match tl with

                 | nil => True

                 | hd2 :: tl2 => (snd hd) = (fst hd2)

                 end) /\ (path tl)

  end.

(* Define as a subset. *)

Definition Path := { l : list edge | path l }.

(* Encode as an inductive definition that makes the path correct by

construction.  Note, need to include the vertex endpoints in the type

to enforce the invariants. *)

Inductive pathI : vertex -> vertex -> Set :=

| path_tl : forall e:edge, pathI (fst e) (snd e)

| path_hd : forall e:edge, forall v1 v2:vertex, forall p:pathI v1 v2, (snd e) = v1 -> pathI (fst e) v2.

(* We could write a symmetrical encoding as well. *)

Inductive pathS : vertex -> vertex -> Set :=

| pathS_edge : forall e:edge, pathS (fst e) (snd e)

| pathS_compose : forall v1 v2 v3 : vertex, forall p1 : pathS v1 v2, forall p2 : pathS v2 v3, pathS v1 v3.

                                    

(* Which of these encoding is preferred?

  1. Predicate encoding allows reuse of list facts and definitions, but requires lemmas connecting them together.

  2. Inductive encoding requires reimplmenting all list elements.

  3. Symmetric encoding makes simple equality not work, requires a special equality operator.

 *)