The Coq mailing list

["Namio Namelander" <verifying AT ndtvmail.com>]

Thanks!

--- sedrikov AT gmail.com wrote:

From: Cedric Auger <sedrikov AT gmail.com>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Declaring a well colored digraph in COQ
Date: Wed, 12 Nov 2014 19:17:29 +0100

2014-11-12 18:09 GMT+01:00 Namio Namelander <verifying AT ndtvmail.com>:

I would like to declare a structure in coq which represents a digraph which is well colored. I declared a Register which is accepted by coq if I don't
have a condition. However I tried many ways of writing the condition
wellColored in coq without exit. Each time I get a new error message.

The condition wellColored is the following:

for every pair of vertices $v1$, $v2$ and every edge $e$, if the source of $e$ is $v1$,
the target of $e$ is $v2$ and the color of $v1$ is $a$ then there is a color $b$ such that $b$ is different from $a$ and the color of $v2$ is $b$.

​This property can be shortened as follows:

Every edge has its source and target of different color.​

 

My attempt is written below. What are the mistakes in the condition wellColored and what is the correct definition?

Record dirgraph:={  
V:Set;  
E:Set;  
s:E->V; (\* source function \*)  
t:E->V; (\* target function \*)  
l:V->nat;  
wellColored: forall (v1:V) (v2:V) (e:E) (a:nat),   
In V v1 /\ In V v2 /\ In E e /\ s e v1 /\ t e v2 /\ l v1 a-> (exists b, b<>a /\ l v2 b)  
}.


Obs: For the moment I'm not interested in using packages with formalization of graphs. My main interest is to understand how to define structures and prove things about them. So I would like to define the graph precisely as it is above except with the correct condition.

​My restatement provides:

wellColored: forall (e:E), I (s e) = I​ (t e) -> False

--

.../Sedrikov\...