Search code examples
coq

Declaring a well colored digraph in coq

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$.

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

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.

Solution

  • The problem with your definition is that some conditions that you impose on wellColored do not need to be expressed, or simply cannot be expressed, in Coq's formalism:

    1. I assume that by In V v1 you mean that v1 should be a member of V. Coq (as well as most type theories) is very different from usual set theory in this respect, because it doesn't make sense to assert that an object has some type as a proposition -- types in Coq (including things of type Set, like V in your definition) are not like sets in set theory. Instead, each object in the theory has its own type once and for all, and that type cannot change. When you write forall (v1 : V), ..., it is already assumed that v1 is a member of V.

      If you want to say that some object of type T has some special property that not all objects of that type have (e.g., some number n is prime), you would express that with a predicate on that type (i.e., something of type T -> Prop), and not as a "subset" of T, as you would do in set theory.

    2. You defined s, t and l as functions of one argument, but used them as two-argument functions, as in s e v1. I suppose you wanted to say something like v1 = s e, i.e. v1 is the source of edge e. However, there's no need to say that: s e is an expression of type V like any other, and can be used directly, with no need to declare additional variables (see below). Likewise, you don't need to say that there exists some color b that is different from a: you can just refer to the color of that node directly.

    Here's a version of your type that avoids those problems:

    Record dirgraph:={
  V:Set;
  E:Set;
  s:E->V; (* source function *)
  t:E->V; (* target function *)
  color: V->nat;
  wellColored:
    forall e : E, color (s e) <> color (t e)
}.