[Coq-Club] A question of encoding...

[Fred Smith]

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.
*)

[Jason -Zhong Sheng- Hu]

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-***@inria.fr <coq-club-***@inria.fr> on behalf of Fred Smith <***@gmail.com>
Sent: December 2, 2018 3:25 PM
To: coq-***@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.
*)

[Fred Smith]

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

Post by Jason -Zhong Sheng- Hu
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
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*
------------------------------
*Sent:* December 2, 2018 3:25 PM
*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.
*)

[Jason -Zhong Sheng- Hu]

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 <***@gmail.com>
Sent: December 2, 2018 5:29 PM
To: ***@hotmail.com
Cc: coq-***@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 <***@hotmail.com<mailto:***@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-***@inria.fr<mailto:coq-club-***@inria.fr> <coq-club-***@inria.fr<mailto:coq-club-***@inria.fr>> on behalf of Fred Smith <***@gmail.com<mailto:***@gmail.com>>
Sent: December 2, 2018 3:25 PM
To: coq-***@inria.fr<mailto:coq-***@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.
*)

[Fred Smith]

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

Post by Jason -Zhong Sheng- Hu
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*
------------------------------
*Sent:* December 2, 2018 5:29 PM
*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 <
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
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*
------------------------------
*Sent:* December 2, 2018 3:25 PM
*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.
*)

[Pierre Casteran]

Hi Fred,

In a former development on transition systems I used a predicate relating the ends and intermediate steps of a path.
path : vertex -> list vertex -> vertex -> Prop

It is Ok wrt path concatenation and relation with transitive closures.

Hope this helps.

Pierre

Post by Fred Smith
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

Post by Jason -Zhong Sheng- Hu
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*
------------------------------
*Sent:* December 2, 2018 5:29 PM
*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 <
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
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*
------------------------------
*Sent:* December 2, 2018 3:25 PM
*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.
*)

[Emilio Jesús Gallego Arias]

Hi Fred,

Post by Fred Smith
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.

[Fred Smith]

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

Post by Jason -Zhong Sheng- Hu
Hi Fred,

Post by Fred Smith
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?
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.

[Christian Doczkal]

Hi,

having recently formalized quite a bit of graph theory [1], I think the
trade-offs depend a lot on what the notion of graphs is, what operations
you need on these graphs and, an what type of statements you want to prove.

Are you talking about undirected graphs or do edge directions matter?
Are you allowing multiple (identically labeled) edges between two nodes?
Are you considering finite or possibly infinite graphs?
Do you regularly need to construct new graphs (subgraphs, disjoint
unions, adding verices or edges, quotients, etc.)?
Do you need to transfer paths between related graphs?

In [1], we consider paths in finite simple graphs (i.e., undirected
graphs without self-loops). We started with paths as a predicate (on
vertices). However, we used the ternary predicate "path e x s" (to be
read as "x::s" is a path in the relation e.; provided by MathComp). This
takes care of the fact that paths are never empty and thus always have a
beginning and an end.

However, this quickly turned out to be rather cumbersome for two
reasons. First, the definition is asymmetric, which gets in the way of
without loss of generality reasoning. Second, one has to manually prove
things like that composing an xy-path with a yz-path yields an xz-path.

Thus, we ended up packaging the path predicate into a vertex-indexed
collection of path types:

Record sgraph := SGraph {
svertex :> finType ;
sedge: rel svertex;
sg_sym: symmetric sedge;
sg_irrefl: irreflexive sedge}.

Variable (G : sgraph).

Definition spath (x y : G) p := path sedge x p && (last x p == y).

Record Path (x y : G) := { pval : list G; _ : spath x y pval }.

This allows us to define dependently typed concatenation, reversal,
etc., and then prove a load of lemmas getting closer and closer to the
reasoning steps one would do on paper. See [2] for detail.

I realize that this advice is very specific to the case of (simple)
graphs. But then, I'm not sure the general question can be answered in a
satisfactory manner.

Best,
Christian


[1] https://hal.archives-ouvertes.fr/hal-01703922
[2]
https://perso.ens-lyon.fr/damien.pous/covece/k4tw2/coq/TwoPoint.sgraph.html#Path

Post by Fred Smith
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.
 *)

[Xuanrui Qi]

Hello Fred,

I will go slightly off-topic here and suggest two alternative (more
advanced) encodings of graphs: it might be overkill for what you are
doing, but they are good purely functional encodings of graphs (which
may or may not be cyclic).

The first encoding is a purely applicative encoding invented by Norman
Ramsey and Jõao Dias based on Huet's zipper. It is first described in
their ML Workshop 2005 paper (
https://www.cs.tufts.edu/~nr/pubs/zipcfg.pdf). Norman and Jõao
invented this representation to implement CFGs, but I think it could be
adapted to normal graphs as well.

The other is an algebraic, higher-order representation, presented in
the Haskell 2017 functional pearl "Algebraic Graphs with Class" by
Andrey Mokhov (
https://eprint.ncl.ac.uk/file_store/production/239461/EF82F5FE-66E3-4F64-A1AC-A366D1961738.pdf
). The code presented makes heavy use of type classes, but I believe it
could be modified to not use type classes (and, failing that, Coq does
have type classes anyway).

Since both representations are pure and total, I think they could be
adapted into Coq easily. It would probably be totally overkill for your
task at hand, but they seem like good, clever, purely functional
representations of graphs in general.

-Ray

Post by Fred Smith
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.
*)

[Fred Smith]

Hi Ray,

Thanks for pointing out this work. It was a thought provoking read. My
own experience with imperative control-flow graphs matches their experience
pretty well.

-Fred

Post by Xuanrui Qi
Hello Fred,
I will go slightly off-topic here and suggest two alternative (more
advanced) encodings of graphs: it might be overkill for what you are
doing, but they are good purely functional encodings of graphs (which
may or may not be cyclic).
The first encoding is a purely applicative encoding invented by Norman
Ramsey and Jõao Dias based on Huet's zipper. It is first described in
their ML Workshop 2005 paper (
https://www.cs.tufts.edu/~nr/pubs/zipcfg.pdf). Norman and Jõao
invented this representation to implement CFGs, but I think it could be
adapted to normal graphs as well.
The other is an algebraic, higher-order representation, presented in
the Haskell 2017 functional pearl "Algebraic Graphs with Class" by
Andrey Mokhov (
https://eprint.ncl.ac.uk/file_store/production/239461/EF82F5FE-66E3-4F64-A1AC-A366D1961738.pdf
). The code presented makes heavy use of type classes, but I believe it
could be modified to not use type classes (and, failing that, Coq does
have type classes anyway).
Since both representations are pure and total, I think they could be
adapted into Coq easily. It would probably be totally overkill for your
task at hand, but they seem like good, clever, purely functional
representations of graphs in general.
-Ray

Post by Fred Smith
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.
*)

[Fred Smith]

The second paper by Mokhov was also very interesting. Thanks for the
pointers.

-Fred

Post by Fred Smith
Hi Ray,
Thanks for pointing out this work. It was a thought provoking read. My
own experience with imperative control-flow graphs matches their experience
pretty well.
-Fred

Post by Xuanrui Qi
Hello Fred,
I will go slightly off-topic here and suggest two alternative (more
advanced) encodings of graphs: it might be overkill for what you are
doing, but they are good purely functional encodings of graphs (which
may or may not be cyclic).
The first encoding is a purely applicative encoding invented by Norman
Ramsey and Jõao Dias based on Huet's zipper. It is first described in
their ML Workshop 2005 paper (
https://www.cs.tufts.edu/~nr/pubs/zipcfg.pdf). Norman and Jõao
invented this representation to implement CFGs, but I think it could be
adapted to normal graphs as well.
The other is an algebraic, higher-order representation, presented in
the Haskell 2017 functional pearl "Algebraic Graphs with Class" by
Andrey Mokhov (
https://eprint.ncl.ac.uk/file_store/production/239461/EF82F5FE-66E3-4F64-A1AC-A366D1961738.pdf
). The code presented makes heavy use of type classes, but I believe it
could be modified to not use type classes (and, failing that, Coq does
have type classes anyway).
Since both representations are pure and total, I think they could be
adapted into Coq easily. It would probably be totally overkill for your
task at hand, but they seem like good, clever, purely functional
representations of graphs in general.
-Ray

Post by Fred Smith
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.
*)