The Coq mailing list

[Fred Smith <fsmith1024 AT gmail.com>]

If I am not mistaken, that is exactly my definition pathS?  It has the disadvantage as data that the path doesn't have a normal form; so strict equality (=) doesn't correspond directly to the desired semantic equality.  

One can always normalize before comparing, but it is exactly this kind of subtle tradeoff that puzzles me.  Is it better to make the relation construction simple, but give up equality; or make the relation have a normal form by definition (pathI) and then write all kinds of convenience utilities to make this convenient.  Both choices seem equally bad.  I am concerned that in a few weeks I'll discover that one or the other is better for some very specific reason and end up having both versions with translations between them.  

-Fred

On Sun, Dec 2, 2018 at 5:34 PM Jason -Zhong Sheng- Hu <fdhzs2010 AT hotmail.com> wrote:

Hi Fred,

yes, transitivity closure in Coq's standard library is defined to be a proposition. But as I said, it doesn't prevent you from re-defining the counter-part definition in Type, which gives you the full right to treat it as data and consequently extract a sequence of vertices along the path.

Sincerely Yours,

Jason Hu

---

From: Fred Smith <fsmith1024 AT gmail.com>
Sent: December 2, 2018 5:29 PM
To: fdhzs2010 AT hotmail.com
Cc: coq-club AT inria.fr
Subject: Re: [Coq-Club] A question of encoding...

 

Hi Jason,

Thanks for the suggestion.  Unfortunately, I need the actual paths as data and not just the relation between endpoints of paths.  If I understand your proposal correctly it would give me a relation (path v1 v2) which holds whenever there exists a path between v1 and v2 without providing the actual path.

-Fred

On Sun, Dec 2, 2018 at 3:50 PM Jason -Zhong Sheng- Hu <fdhzs2010 AT hotmail.com> wrote:

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.

 *)