1 Introduction

Relation algebra (as first introduced in [19] and further studied, e.g., in [10, 16]) provides an elegant way to reason about many discrete structures. For instance, there is a direct relationship between relations and graphs via adjacency relations. Hence, computational problems on graphs can be expressed and solved by using the relation-algebraic method as shown in [16], for example. The relation-algebraic approach is known for many methodical advantages in contrast to the conventional set-theoretic one. For example, it allows consice problem specifications and hence very formal calculations. Due to this, relation-algebraic reasoning turned out to be well-suited for mechanisation.

Thus, in [2] the authors develop a relational program for computing vertex colorings in undirected (and loop-free) graphs. The correctness proof is given by combining the assertion-based verification method with relation-algebraic calculations. In this context the usability of an automated theorem prover and the proof assistants Coq and Isabelle/HOL is shown and compared. However, the approximation ratio of the underlying Greedy algorithm is not studied at all since there were no obvious tools to tackle proofs involving cardinalities.

In the last years there has been a lot of work concerning the cardinalities of relations, mostly based on a definition of a cardinality operation for heterogeneous relation algebras presented by Kawahara in [9]. For example, in [3] and [1], the authors present first results about the cardinalities of special relations as points and vectors building the basis for reasoning about approximation ratios algebraically. Furthermore, in [5], a library for Coq providing an implementation of this cardinality operation in heterogeneous relation algebras is developed.

In the present paper the mentioned results about cardinalities of relations are used to prove the approximation ratio of the program presented in [2]. Furthermore, we study the application of the proof assistants Coq and Isabelle/HOL in this context. Therefore, we first use the library developed in [5] for mechanising the correctness proof in Coq. Our implementation in Isabelle/HOL builds on a library for untyped relations (see [17]). Thus, we modify Y. Kawahara’s definition of a cardinality operation and present a new theoretical framework for dealing with cardinalities in homogeneous relation algebras. For this framework we develop a library that is eventually applicable for the mechanisation of the programs’ correctness proof. As in [2], we compare the advantages and disadvantages of the usability of both tools in this context.

Our Coq proof script and Isabelle/HOL theories are available here [18].

2 Preliminaries

First, we recall the basic principles of relation algebra based on the heterogeneous approach of [6, 15, 16]. Set-theoretic relations form the standard model of relation algebras. We assume the basic operations on set-theoretic relations, viz. union, intersection, complementation, transposition and composition, in the remainder denoted by , and RS for relations R, S of appropriate type. Furthermore, we consider the predicates \(R \subseteq S\) (inclusion) and \(R = S\) (equality)and the empty, universal and identity relation denoted by and .

Those operations and constants form a (heterogeneous) relation algebra in the sense of [15, 16], with typed relations as elements. We write if R is a relation with source X and target Y and denote the type of R by . In the case of typed relations we frequently overload the symbols , and , if their type can be inferred from the context. If necessary we use indices as e.g., for of type . The axioms of a relation algebra are

  1. (1)

    the axioms of a Boolean lattice for all same typed relations under the Boolean operations and , \(\subseteq \) and and ,

  2. (2)

    the associativity of composition and that identity relations are neutral w.r.t. composition,

  3. (3)

    the Schröder rule, i.e., that for all relations Q, R and S with appropriate types it holds

  4. (4)

    the Tarski rule, i.e., that for all relations R and all universal relations with appropriate types it holds .

In the relation-algebraic proofs of this paper we only indicate applications of (3), (4) and consequences of the above axioms that are not obvious. Furthermore, we assume that complementation and transposition bind stronger than composition and composition binds stronger than union and intersection.

In the following we define some specific classes of relations, for more details we refer again to [15, 16]. If R is homogeneous, i.e., of type , R is called irreflexive iff and symmetric iff . A homogeneous relation R is reflexive iff , antisymmetric iff , and transitive iff . A reflexive, antisymmetric and transitive relation R is a order relation and if additionally holds, i.e., R is linear, then R is called a linear order relation. A relation R is univalent iff and total iff . A mapping is a univalent and total relation.

A vector is a relation v with . For a set-theoretic relation the equality means that v is of the form \(v = Z \times Y\) with a subset Z of X. Then we say that v models the subset Z of X. Since for this purpose the target of a vector is irrelevant, we use the specific singleton set as target. Moreover, a point p is a vector that is injective and surjective, i.e., and .

We also assume the following version of the Point Axiom of [7] holding for set-theoretic relations, where \(\mathcal {P}(v):=\{p \mid p \subseteq v \wedge p \text { is point}\}\) for all vectors v.

Axiom 2.1

For all objects X we have .

Additionally we have the following lemma which states that this property can be generalised for arbitrary vectors (see [7]).

Lemma 2.1

If is a vector, then .    \(\square \)

In [9], Kawahara investigates the cardinality of set-theoretic relations. The main result is a characterisation of the cardinalities of relations. Considering the properties of this characterisation as axiomatic specification of the cardinality operation \(| \cdot |\) leads to the following definition:

Definition 2.1

For all relations R we denote its cardinality by |R|. The following axioms specify the meaning of the cardinality operation, where Q, R and S are arbitrary relations with appropriate types:

  1. (C1)

    If R is finite, then and iff .

  2. (C2)

    .

  3. (C3)

    If R and S are finite, then .

  4. (C4)

    If Q is univalent, then and .

  5. (C5)

In (C1) and (C3) the occuring relations are assumed to be finite so that the cardinality |R| can be regarded as a natural number, in (C2) and (C4) the notation \(|R| = |S|\) (respectively \(|R| \le |S|\)) is equivalent to the fact that there exists a bijection between R and S (respectively an injection from R to S) and (C5) says that the identity relation on the set contains precisely one pair. In the present paper we assumes in case of an expression |R| the sets of R’s type to be finite and thus .

Based on the above axioms in [9] a lot of laws for the cardinality operation are derived in a purely algebraic manner, for instance, the monotonicity of the cardinality operation, i.e., that \(R \subseteq S\) implies \(|R| \le |S|\). Futhermore, they imply \(|\bigcup _{R \in \mathcal {R}} R| = \sum _{R \in \mathcal {R}} |R|\), for all finite sets \(\mathcal {R}\) of pairwise disjoint relations. Other consequences of the axioms we use in the remainder are the following:

Lemma 2.2

  1. 1.

    If R and S are univalent, then .

  2. 2.

    If R is univalent and S is a mapping, then .

  3. 3.

    If R is univalent, then .

The cardinality of points and vectors of type can be studied by using the above results. The next lemma states that a point contains exactly one pair.

Lemma 2.3

If is a point, then \(|p| = 1\).

Proof

Using cardinality axioms (C2) and (C5) and Lemma 2.2 ( is univalent and is a mapping), we have the following calculation:

   \(\square \)

This lemma allows to show that the cardinality of a vector with target is equal to the cardinality of the set of all points it contains.

Lemma 2.4

For all we have \(|v| = |\mathcal {P}(v)|\).

Note that in the above lemma with \(|\mathcal {P}(v)|\) we denote the usual cardinality of the set \(\mathcal {P}(v)\). For more details, in particular omitted proofs, and results concerning the cardinality operation as well as applications we refer to [1, 3, 9].

3 Approximating Minimal Vertex Colorings

In [2] the authors present a relational program for computing vertex colorings in undirected (and loop-free) graphs. The verification tasks arising by applying the assertion-based verification method are supported by the automated theorem prover Prover9 and the proof assistants Coq and Isabelle/HOL. By this example the advantages and disadvantages of these tools are studied and compared.

The presented program is based on the well-known Greedy algorithm that assigns sequentially a proper color to each vertex, i.e., a color that is not already assigned to one of its neighbours. This procedure does not consider the fact that one is usually interested in computing a minimal and not an arbitrary coloring of a graph. Thus, one usually assumes the colors to be ordered so that the algorithm chooses a minimal color for each vertex. By this approach a minimal vertex coloring is approximated with a ratio of \(\varDelta +1\), where \(\varDelta \) is the maximum degree of the given graph.

In [2] the approximation ratio is not treated at all. Thus, in the remainder of this section we prove the ratio of the following program with the modified choice of the color q using the results about the cardinality operation presented in Sect. 2:

The input relations of this program are an adjacency relation , modelling a given graph G with a set of vertices X, and a linear order relation on a set of colors F. The output relation of the program is representing the vertex coloring, i.e., a mapping so that in addition holds. The latter condition is called the coloring property. Furthermore, all occuring universal relations in the program have target . As in [2] we assume the deterministic operation selecting a point to a given nonempty vector v such that . For more details we refer to [2] since the only difference to our program is the choice of the point q. In [2], q is choosen as , i.e., q is not used for one of p’s neighbours. If we choose q as instead we also ensure that q is minimal since is the vector of all minimal colors w.r.t. the order relation M, see, e.g., [16] for further information.

To formally verify the correctness of the above program we apply the assertion-based verification method. Thus, we first specify the programs’ pre- and postcondition. The precondition is the conjunction of the following formulae specifying E as an adjacency relation, i.e., an irreflexive and symmetric relation, and M as a linear, reflexiv and antisymmetric relation (transitivity is not needed here).

In the remainder we furthermore use the abbreviation for all vectors v and for the maximum degree of a given graph modelled by E. If we do not specify a universal or empty relation’s type in this section we assume its target to be .

The postcondition is a conjuction of three formulae stating that C is a vertex coloring, i.e., an univalent and total relation fulfilling the coloring property, and a formula saying that the number of used colors is at most \(\varDelta + 1\):

The invariant is a conjunction of four formulae, where the first two ensure that C is univalent and fulfills the coloring property and the latter two are essential for proving the desired approximation ratio:

As usual the following proof obligations have to be proved for partial correctness:

  1. (PO1)
  2. (PO2)
  3. (PO3)

    (where p and q are defined as in the given program).

Since and are conjunctions of various formulae the three obligations can be splitted into single statements for each formula. In the remainder we only consider the statements involving cardinalities. For the omitted proofs we refer to Sects. 4 and 5 and the appendix. Here, we start with proving the first proof obligation (PO1), i.e., the establishment of the last formula of the invariant.

Lemma 3.1

For all relation E and M it holds .

Proof

The last formula of the invariant is shown by using cardinality axiom (C1) two times:    \(\square \)

Next, we prove (PO2), i.e., that the invariant and the negation of the loop-condition imply the postcondition. Again we concentrate on the last formula involving cardinalities.

Lemma 3.2

Let E, C, M be relations such that E is symmetric and irreflexive, M is reflexive, antisymmetric and linear and and holds. Then holds.

Proof

Using in the first and in the second step we have the following inequality:    \(\square \)

For proving (PO3), i.e., the maintenance of the last formula of the invariant, we need the following auxiliary result.

Lemma 3.3

Let R be a reflexive, anstisymmetric and linear relation. Then holds.

Proof

Using the antisymmetry of R we have:

By the linearity and reflexivity of R we show:

   \(\square \)

Using the latter Lemma we show the maintenance of the invariants’ last formula:

Lemma 3.4

Let E, C and M be relations so that and hold and p, q points with , . Then holds.

Proof

Since p and q are points it holds and thus . For the same reasons we have which implies Hence we have to show .

Using (C3) and Lemma 2.3 we have the following equality:

If it holds . In this case the claim follows immediately with the assumption , in particular the last formula of it, and the fact that .

Hence, we consider the case that . Then and it follows. Thus, it is sufficient to show that holds.So we show that , and therefor, .

Because of and the third formula of we have

and thus

(1)

Next, we prove

(2)

by the following calculation:

Using (1), (2) and Lemma 2.2.1 (C is univalent because of ) as well as the monotonicity of the cardinality operation we obtain the desired inequality:

   \(\square \)

4 Cardinalities in Coq

In [2] the proofs of the according obligations (PO1)–(PO3) presented in Sect. 3 are mechanised amongst others with the proof assistant Coq using the library RelationAlgebra which provides a model for heterogeneous relation algebra and many other related algebraic structures. The library is available via [13], and presented in [14]. For more general information about Coq we refer to [4, 20].

In [5] the authors extend the mentioned library so that a reasoning about cardinalities is possible. RelationAlgebra is enriched by the module containing the most important definitions of special classes of relations, e.g., those introduced in Sect. 2. For the tools concerning cardinalities a standalone library was developed. To preserve the modularity of RelationAlgebra this library provides a separate module for each algebraic structure we defined in Sect. 2. The hierarchy of the modules is illustrated in Fig. 1.

Fig. 1.
figure 1

Hierarchy of the Coq library

Full size image

To simplify rewriting, the definitions are realized by using classes, for instance, being univalent is defined as follows:

figure a

Here, the variables and specify the type of the relation and provides the notions and operations of a relation algebra. The symbols , and denote transposition, composition and inclusion. The type of the identity relation denoted by is inferred automatically. In the Point Axiom is assumed and several resulting facts are proved, especially those presented in Sect. 2. The definition of the cardinality operation is given in and follows the one presented in Sect. 2. A detailed description of each module and the notations can be found in [5].

In the proofs of all lemmata of Sect. 2 (and many more) are mechanised, for instance, Lemma 2.3 as follows:

figure b

Here, specifies the relation as a point and denotes the cardinality operation. The Coq proof follows exactly the one of Sect. 2 where , and correspond to (C2), Lemma 2.2 and (C5).

With the extended library all proofs of Sect. 3 can be done within Coq. In the following we show the formulations of the Lemmata 3.1, 3.4 and 3.2 where is the definition of the invariant as given in Sect. 3 (the adjacency and order relation are introduced at the beginning of our Coq module once and for all) and the vector of the minimal elements of a vector w.r.t. a linear order relation :

figure c

Mainly, the proofs have to be done step by step. At some points we benefit at the one hand from the smart implementation of the specific relations that makes rewriting less difficult and on the other hand from the decision tactics provided by RelationAlgebra. A detailed description of those tactics can be found in [14].

5 Cardinalities in Isabelle/HOL

In this section we show how the proof assistant Isabelle/HOL can be used to prove the correctness of the program of Sect. 3. In particular, we develop the required theoretical framework for it.

Compared to the one of Coq the type system of Isabelle/HOL is less powerful. In the end the usage of multi-parameter classes is not possible whereby there is no trivial way to define heterogeneous relation algebras. Thus, our Isabelle/HOL theories built on an existing library, Relation_Algebra, for homogeneous relation algebras only, available via the Archive of Formal Proofs, see [17]. More general information about Isabelle/HOL can be found, for example, in [8, 12].

This limitation makes it impossible to transfer the approach realised in Coq to Isabelle/HOL. Namely, if we consider points of type , for instance, it was essential for the proofs of Sect. 3 that they have cardinality 1. This fact is mainly based on the cardinality axiom (C5) and the specific type . When using the Relation_Algebra library we are not only restricted to homogeneous relation algebras, but to untyped relations.

Due to this, we have to modify the definition of the cardinality operation of Sect. 2. The first four axioms (C1)–(C4) can be adapted to untyped relations, but (C5) involves the special singleton set . Thus, we assume the following fifth axiom instead saying that the cardinality of the identity relation equals the number of points (in the relation algebra):

Note that there are equivalent formulations of (C5’), e.g., , but for us, the given one is the most intuitive compared to (C5).

In the remainder we also assume a version of the Point Axiom for untyped relations. The only difference to Axiom 2.1 is that the occuring universal relation is untyped.

Axiom 5.1

(Point Axiom). It holds .

One can easily check that we get the following corresponding consequences as in Sect. 2.

Lemma 5.1

  1. 1.

    For all vectors v we have .

  2. 2.

    We have .

Furthermore, the Lemma 2.2 also holds in the case of untyped relations. The first important result which is significantly different, due to (C5’), is stated in the following lemma and gives us the cardinality of (untyped) points.

Lemma 5.2

If p is a point, then .

Proof

Using cardinality axioms (C2) and (C5’) and Lemma 2.2 ( is univalent and is a mapping) we have    \(\square \)

Obviously, because of the above lemma, points and vectors are no longer suitable for modelling sets if their cardinalities are essential in the context. Thus, in the following and in particular for the formalisation is Isabelle/HOL we use partial identities, i.e., relations R with , instead of vectors to represent sets. In place of points we consider atoms, i.e., nonempty relations a with . We show that the cardinalities of those special relations correspond to the ones of vectors and points. Therefore, we start with a lemma about the cardinality of (untyped) vectors.

Lemma 5.3

If v is a vector, then .

Proof

Because of Lemma 5.1, cardinality axioms (C3) and (C1) (the points in are pairwise disjoint) and Lemma 5.2 we obtain the claim by

   \(\square \)

Note that the above result holds in particular for since is a vector. This gives us because of (C5’).

To prove that every atom has cardinality 1 we need the following technical lemma whose proof we omit due to the lack of space. It states that every atom is the composition of a point and a points’ transposed (and vice versa), and that the universal relation can be written as the union of all atoms it contains. Here, we denote the set of all atoms (containted in ) as .

Lemma 5.4

  1. 1.

    It holds .

  2. 2.

    It holds .

From this we get the desired result about the cardinalities of atoms.

Lemma 5.5

If a is an atom, then \(|a| = 1\).

Proof

For all atoms a it holds and thus \(|a| \ge 1\) with cardinality axiom (C1). We prove \(|a| = 1\), for all atoms a, by contradiction. Thus, we assume that there exists an atom b with \(|b| > 1\). Combining Lemmas 5.3 and 5.4.2 (for ) we have . Due to this and again Lemmas 5.3 and 5.4.2 we have

which is a contradiction.    \(\square \)

From this we get that partial points have cardinality 1 which makes them suitable for modelling single elements of sets.

Lemma 5.6

If p is a partial point, then \(|p|=1\).

Proof

By definition, p is an atom, thus the claim follows immediately with Lemma 5.5.    \(\square \)

We omit the corresponding proofs of the correctness of the program of Sect. 3, but refer to the Isabelle/HOL formalisation we describe in the remainder of this section and available via the web, see [18].

So far, the library Relation_Algebra provides several facts holding in untyped relation algebras as well as theories about functions and vectors with related facts, so that most of the specific relations mentioned in Sect. 2 are already defined. For instance, for vectors this is done in the following way

figure d

In the library the symbols \(+,\,\cdot ,\, -,\, ;\) and \(^\smile \) are used for union, intersection, complement, composition and transposition and \(1,\, 0\) and \(1'\) for the universal, empty and identity relation. For our purpose we import additional theory, e.g., about natural numbers, so that we use \(\sqcup ,\,\sqcap ,\) and \(^, \) for the first three operations and \(top,\, bot\) and \(1'\) for the constants and . As in the case of Coq neither the Tarski rule nor the Point Axiom is provided by the library so far. Follow the approach in Coq we develop a separate theory for each structure we define. The dependencies of the main theories are illustrated in Fig. 2.

Fig. 2.
figure 2

Hierarchy of the Isabelle/HOL library

Full size image

First, we extend the class relation_algebra by the Tarski rule using a class:

figure e

This is done in the theory Relation_Algebra_Tarski where we derive some fundametal properties of points, for instance the following one:

figure f

The theory Relation_Algebra_Points is an extension of the latter providing the Axiom 5.1 and that the number of points is finite:

figure g

Here, is a notation for in Isabelle/HOL. In the theory Relation_Algebra_Sums we proved a several properties of these finite unions, e.g., monotonicity.

Finally, we have a theory called Relation_Algebra_Cardinalities where the cardinality operation is defined in the following way:

figure h

Here, card is the built-in operation for the cardinality of sets. With the given definition we are able to prove the mentioned results about cardinalities, for instance:

figure i

The proofs of these lemmata are found automatically by Sledgehammer. From this we get immediately that the cardinality of a point equals the cardinality of the identity relation. In the same way we formalise all lemmata of this section and many more where most of the proofs are heavily supported by Sledgehammer.

For the verification of the program of Sect. 3 we do not only use the above mentioned theories about relation algebra and cardinalities, but also a library for Hoare Logic in Isabelle/HOL, see [11]. This library provides the opportunity to write, for instance, while-programs as theorems as well as tactics generating the proof obligations for partial correctness automatically. Thus we can encode the program as follows.

figure j

Unfortunately, we have to switch to another symbol for composition here since; is already defined in the theory for Hoare logic. Thus, we use \(\bullet \) in this context. The pre- and postconditions and the invariant slightly differ from the ones presented in Sect. 3 since we have to use partial points and identities for proving the approximation bound.

figure k

One of the big advantages of using the theory for Hoare Logic is that its provides tactis for verification condition generation. In the case of our program or theorem, respectively, we can apply the rule vcg_simp. With this rule the three proof obligations w.r.t. the given pre- and postconditions and the loop-invariant are generated as subgoals automatically. In the following we see the resulting subgoals after applying vcg_simp.

figure l

The three statements are shown stepwise by using the theories mentioned in this section. The proofs that are not found by Sledgehammer automatically are given as structured Isar proofs, see [18], so that the reader can follow the basic ideas.

Besides the results presented in this section our library contains over 150 lemmata about finite unions of relations, points and vectors, atoms, and cardinalities of relations. Furthermore, in Relation_Algebra_Orders we defined order related relations and proved several facts about them.

6 Comparison of the Implementations

In Sects. 4 and 5 we show how the proof assistants Coq and Isabelle/HOL can be used for formal program verfication and reasoning about relation algebras in general. In this section we want to summarise our experiences with both systems and highlight their advantages and disadvantages from our point of view.

For Coq, we used an existing library that already implements tools for proving results regarding cardinalities. One advantage of the library is that it extends a library including a model for heterogeneous relation algebras and related structures. Here, the implementation of typed relations is possible because of Coq’s expressive type system based on the predicative calculus of inductive constructions. Such an expressive type system has many common advantages, for instance, it ensures that all expressions and formulae are well-typed. Thus, the Coq proofs mostly correspond to the handwritten ones we gave in this paper. Coq, and in particular the used library, provides several automated theorem proving tactics and decision procedures, but most of them were not very helpful in our context. Thus, the proofs have mostly to be done step by step using Coqs standard tactics. Unfortunately, a direct link to automated theorem provers is still missing. Furthermore, the formalisation of the proof obligations of the presented program has to be done by hand since there are no tools for an automated generation. For non-experts the Coq code is quite hard to read without using an IDE illustrating proof steps and subgoals.

By contrast, Isabelle/HOL bridges the gap between interactive and automated theorem proving because of its integrated tool Sledgehammer. Due to the limited type system of Isabelle/HOL there is only an existing library for homogeneous relation algebras. For this reason an extension by the cardinality operation, as in the case of Coq, was not possible directly. Thus, we modified the axiomatisation of the operation to make it applicable for homogeneous relations in the first place. We formalised it in Isabelle/HOL and proved the correctness of the relational program heaviliy supported by Sledgehammer. Unlike Coq, Isabelle/HOL provides a library for Hoare Logic including tactics for generating proof obligations automatically. In our context we were able to avoid typed relations by adapting the cardinality operation. In general, reasoning about typed relations can be managed by using, for instance, predicates specifying the source and target of a relation. Such an approach often results in more complicated and longish proofs. In the future, one can benefit from our library containing most of the basic facts that are necessary when dealing with cardinalities. Certainly, invoking Sledgehammer does not always complete proofs successfully. As in Coq, one has to do steps by hand, but Isabelle/HOL supports the proof language Isar. Its intuitive syntax allows to write proofs structured and comprehensible for non-experts.

7 Concluding Remarks

We presented a correctness proof of a relational program for approximating vertex colorings in undirected (and loop-free) graphs. The proof of the approximation ratio we done by using an operation to reason algebraically about cardinalities in heterogeneous relation algebras.

Furthermore, all proofs were mechanised in both proof assistants Coq and Isabelle/HOL and build on existing libraries for relation algebras. In contrast to Coq, there were no tools to tackle cardinalities in Isabelle/HOL so far. To reuse a library for homogeneous relation algebras we presented a new theoretical framework for reasoning about untyped relations. In this context, we not only proved the programs’ correctness in Isabelle/HOL, but also developed a library providing over 150 facts about, for instance, points, atoms and cardinalities.

For the future it would be helpful to have a tool for Hoare Logic in Coq so that the generation of a programs’ proof obligations has not to be done by hand or external programs. A further investigation of the new axiomatisation of the cardinality operation is also conceivable to see how exhaustive this approach is. In general, it would be interesting to study what is provable without the restriction to finite relations.