Simple graph theory proofs using Coq

Question

Is there a well established Coq graph library for proving simple theorems ? I would like to learn how to prove simple stuff like: "G1, G2 are isomorphic if and only if their complements are isomorphic". Are there related/similar examples or tutorials available?

Accepted Answer

Here's a demonstration. Allow rewriting with equivalence relations. ``` Require Import Coq.Setoids.Setoid. ``` A graph is a set of vertices along with an adjacency relation. ``` Definition graph : Type := {V : Type & V -> V -> bool}. ``` A graph from vertices and adjacency. ``` Definition create : forall V, (V -> V -> bool) -> graph := @existT _ _. ``` Vertices from a graph. ``` Definition vertices : graph -> Type := @projT1 _ _. ``` Adjacency from a graph. ``` Definition adjacent : forall g1, vertices g1 -> vertices g1 -> bool := @projT2 _ _. ``` The complement of a graph has the same vertices, but a negated adjacency relation. ``` Definition complement : graph -> graph := fun g1 => create (vertices g1) (fun v1 v2 => negb (adjacent g1 v1 v2)). ``` Standard stuff. ``` Definition injective : forall {t1 t2}, (t1 -> t2) -> Prop := fun t1 t2 f1 => forall x1 x2, f1 x1 = f1 x2 -> x1 = x2. Definition surjective : forall {t1 t2}, (t1 -> t2) -> Prop := fun t1 t2 f1 => forall x1, exists x2, f1 x2 = x1. Definition bijective : forall {t1 t2}, (t1 -> t2) -> Prop := fun t1 t2 f1 => injective f1 /\ surjective f1. ``` Two graphs are isomorphic if there's a bijection between their vertices that preserves adjacency. ``` Definition isomorphic : graph -> graph -> Prop := fun g1 g2 => exists f1, bijective f1 /\ (forall x1 x2, adjacent g1 x1 x2 = adjacent g2 (f1 x1) (f1 x2)). Infix "~" := isomorphic (at level 70). ``` A helpful fact whose proof I leave to you. ``` Conjecture C1 : forall b1 b2, negb b1 = negb b2 <-> b1 = b2. ``` Your fact. ``` Goal forall g1 g2, g1 ~ g2 <-> complement g1 ~ complement g2. Proof. ``` Access the components of the graphs. ``` destruct g1. destruct g2. ``` Substitute defined by definition. ``` unfold isomorphic, complement, adjacent, vertices, create, projT2, projT1. ``` First-order logic simplifications. ``` firstorder. ``` Instanciation. ``` exists x1. firstorder. rewrite C1. firstorder. exists x1. firstorder. ``` Instanciation. ``` specialize (H0 x2 x3). rewrite C1 in H0. firstorder. Qed. ``` Actually, this is a formalization of graphs whose adjacency relation is decidable `V -> V -> bool`. In intuitionistic logic, not all graphs with a general adjacency relation `V -> V -> Prop` have the property you want to prove. Instead of sticking to finite or otherwise decidable graphs, you can also move to classical logic or use double negation translation.

Simple graph theory proofs using Coq

Solution

Problem