The Coq mailing list

[fr�d�ric BESSON <fbesson AT irisa.fr>]

On 6 Mar 2006, at 11:40, Fabrice Lemercier wrote:

> I want to formalize in Coq finite directed graphs with
> a relation on paths. But I cannot find an elegant
> definition.

What about something like that:
* data-structures are not cluttered with sig types.
* well-formedness conditions are stated.


Require Import List.

(* My data-structure for graphs *)
Record Graph: Set :=
  {
    Nb : nat;
    Edges : list (nat* nat);
    sources_ok : forall source target, In (source,target) Edges ->  
source <= Nb;
    target_ok : forall  source target, In (source,target) Edges ->   
target <= Nb
  }.

Definition path := list nat.

(* What it means for a path to belong to a graph *)
Inductive path_ok (G:Graph) : path -> Prop :=
  | empty_path : path_ok  G nil
  | cons_path : forall s t, In (s,t) (Edges G) -> forall p, path_ok   
G (t::p) -> path_ok  G (s::t::p)
.

(* Returns the last element of a path *)
Fixpoint last (A:Set) (l:list A) {struct l}: option A :=
  match l with
    | nil => None
    | e::nil => Some e
    | e::l => last A l
  end.

Record Graph_with_relation : Set :=
  {
(* The graph *)
    G : Graph;
(* The relation *)
    R : list (path * path);
(* well-formedness conditions *)
    R_path_ok1 : forall  p1 p2 , In (p1,p2) R -> path_ok G p1;
    R_path_ok2 : forall p1 p2 , In (p1,p2) R -> path_ok G p2;
    R_same_orig : forall  p1 p2, In (p1,p2) R -> head p1 = head p2;
    R_same_dest : forall  p1 p2 , In (p1,p2) R -> last _ p1 = last _ p2
(* You might also want to rule out the empty path *)
  }.

--
Frédéric Besson