The Coq mailing list

[Jason -Zhong Sheng- Hu <fdhzs2010 AT hotmail.com>]

Hi Fred,

I would try to avoid mentioning equality here. You need that because you try to model an edge as a pair. Instead, I would model an edge to be a binary relation and a path to be its transitivity closure:

Require Import Relations.

Section Graph.  

  Variable V : Type.          (* type for vertices *)

  Variable edge : relation V. (* a predicate if an edge exists between two verices. *)

  Definition path : relation V := clos_trans V edge.

End Graph.

It's close to your second choice but your second choice will probably lead to some additional tedious proof steps, because pair in Coq doesn't have definitional eta expansion.

If you need to inspect a path as data, I suppose you want to redefine transitivity closure to be Set/Type. One advantage of defining data, is it gives a structure for induction.

Sincerely Yours,

Jason Hu

---

From: coq-club-request AT inria.fr <coq-club-request AT inria.fr> on behalf of Fred Smith <fsmith1024 AT gmail.com>
Sent: December 2, 2018 3:25 PM
To: coq-club AT inria.fr
Subject: [Coq-Club] A question of encoding...

 

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.

 *)