The Coq mailing list

[Christian Doczkal <christian.doczkal AT ens-lyon.fr>]

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

On 02/12/2018 21:25, Fred Smith wrote:
> 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.
>  *)
> 
>

Attachment: signature.asc
Description: OpenPGP digital signature