在Coq中声明色彩鲜艳的有向图 [英] Declaring a well colored digraph in coq

问题描述

我想在coq中声明一个结构，该结构表示有色的有向图。我声明了一个注册簿，如果我没有条件的话，将被coq接受。但是，我尝试了多种在不退出的情况下用coq编写条件 wellColored 的方法。每次收到新的错误消息：

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

我的尝试写在下面。条件 wellColored 有什么错误，正确的定义是什么？

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.

推荐答案

定义的问题是，您对 wellColored 不需要用Coq的形式主义表达，或者根本就不能表达：

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. 我假设在V v1 中，您的意思是 v1 应该是 V 的成员。 Coq（以及大多数类型理论）在这方面与通常的集合论有很大不同，因为断言一个对象具有某种类型的命题（Coq中的类型）没有任何意义。 （包括类型为 Set 的东西，例如您定义中的 V ）是 not 集合在集合论中。相反，该理论中的每个对象都具有一劳永逸的类型，并且该类型不能更改。当您编写 forall（v1：V），... 时，已经假定 v1 是 V 。

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.

如果您想说某些类型为 T 的对象具有并非所有该类型对象都具有的特殊属性（例如，某些数字 n 是质数），您可以在 predicate 上表示出来该类型（例如，类型为 T-> Prop 的某种东西），而 not 作为子集 T 的集合，就像在集合论中一样。

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.

您定义了 s ， t 和 l 作为一个参数的函数，但使用了它们是两个参数的函数，例如 se v1 。我想您想说类似 v1 = se 之类的东西，即 v1 是边缘 e 。但是，不必说： se 是 V 类型的表达式，与其他表达式一样，可以使用直接，无需声明其他变量（请参见下文）。同样，您不必说存在 b 与 a 不同的颜色：您可以

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

这篇关于在Coq中声明色彩鲜艳的有向图的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！