The Coq mailing list

[Pierre Casteran <pierre.casteran AT labri.fr>]

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 





----- Fred Smith 
<fsmith1024 AT gmail.com>
 a écrit :
> 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.
> >  *)
> >
> >
> >