Digraphs

Stream: graph theory

[Rida Hamadani]

Now that we have digraphs in mathlib, what are the next steps to have things such as walks, paths, cycles, (in, out)-degrees, adjacency matrices, etc for digraphs? Do we plan to just redo these definitions from SimpleGraphs, or should we relate them in some way to their adjacent definitions in SimpleGraph?

[Bhavik Mehta]

My first guess would be to redo the definitions, and have lemmas relating them to the SimpleGraph versions where appropriate. For example, once we have the map sending a digraph to a simple graph which forgets orientations, construct the function from a walk in a digraph to a walk in the corresponding simple graph.

[Vincent Beffara]

It feels like a lot of duplication coming up ... Is the plan to refactor SimpleGraph now to say that a SimpleGraph is a Digraph where Adj is symmetric and has no self-loop? And then we could move to Digraph everything that is not dependent on these particular properties of Adj, typically the definition of Path.

[Rida Hamadani]

Does this "orientation-forgetting" map from Digraphs to SimpleGraphs look okay?

import Mathlib

def toSimpleGraph {V : Type*} (G : Digraph V) : SimpleGraph V where
  Adj v w := v ≠ w ∧ (G.Adj v w ∨ G.Adj w v)
  symm := by
    intro v w ⟨h₁, h₂⟩
    apply And.intro h₁.symm
    cases h₂
    · exact Or.inr ‹_›
    · exact Or.inl ‹_›
  loopless := fun _ h ↦ h.1 rfl

[Shreyas Srinivas]

My impression is that a copy paste and modify job will suffice

[Shreyas Srinivas]

At least for some of the basic files

[Bhavik Mehta]

Vincent Beffara said:

It feels like a lot of duplication coming up ... Is the plan to refactor SimpleGraph now to say that a SimpleGraph is a Digraph where Adj is symmetric and has no self-loop? And then we could move to Digraph everything that is not dependent on these particular properties of Adj, typically the definition of Path.

Yup, could do! That's definitely a sensible thing to try

[Rida Hamadani]

Thanks, I'll try porting some of the things from SimpleGraphs to Digraphs while taking these points into consideration.

[Rida Hamadani]

Another point:
Since we are having an orientation-forgetting map, how can we formalize the opposite: an "orientation" of a SimpleGraph, which results in a Digraphs. I'm asking because I've seen this used often in literature, for instance, tournaments are often defined as an "orientation of a complete simple graph".

[Rida Hamadani]

Is there a way to do this without having to "choose" the orientations

[Bhavik Mehta]

You can turn every edge into a pair of directed edges in opposite directions (and maybe this turns out to give a galois connection with the forgetful map). But otherwise you do need to specify the orientations in some way, for the notion to be well-defined up to isomorphisms on the vertex set

[Vincent Beffara]

Beware that there are two ways to forget orientation, you can have an unoriented edge if either orientation is present, or alternatively if both are present. I don’t know which one is more natural for applications. You did the first, but the second is more dual to Bhavik’s double orientation

[Bhavik Mehta]

We should have both!

[Shreyas Srinivas]

there are other notions of adding orientation. For example a bfs tree with edges oriented towards the starting node, Sinkless orientations etc

[Shreyas Srinivas]

it might be nice to a generic way of orienting each undirected edge

[Rida Hamadani]

Maybe we can have an Orientation.lean file in the SimpleGraph (or Digraph?) folder that contains such orientations, and maybe it can contain the Digraph.toSimpleGraph function with some basic lemmas too.

[Rida Hamadani]

According to https://en.wikipedia.org/wiki/Orientation_(graph_theory), an oriented graph is a Digraph such that none of its pairs of vertices is linked by two mutually symmetric edges. There are many different types of orientations and it would be nice to formalize some of this! It would come in handy once we want to formalize tournaments.

[Rida Hamadani]

What do you think about defining it like this:

import Mathlib

variable {V : Type}

def Digraph.IsOriented (G : Digraph V) : Prop :=
  ∀ v w : V, ¬G.Adj v v ∧ ¬(G.Adj v w ∧ G.Adj w v)

Should oriented graphs contain self-loops or not?
I've found papers that assume they don't, and I think that is better for our purposes.

[Vincent Beffara]

Equivalently, its "strong" map into a SimpleGraph is bot

[Rida Hamadani]

What is a "strong map"?

[Mauricio Collares]

Vincent Beffara said:

Beware that there are two ways to forget orientation, you can have an unoriented edge if either orientation is present, or alternatively if both are present. I don’t know which one is more natural for applications. You did the first, but the second is more dual to Bhavik’s double orientation

I think Vincent is referring to the "unoriented edge if both oriented edges are present" map

[Rida Hamadani]

If we define oriented graphs in that way then we will be allowing them to have self-loops

[Daniel Weber]

Rida Hamadani said:

Does this "orientation-forgetting" map from Digraphs to SimpleGraphs look okay?

import Mathlib

def toSimpleGraph {V : Type*} (G : Digraph V) : SimpleGraph V where
  Adj v w := v ≠ w ∧ (G.Adj v w ∨ G.Adj w v)
  symm := by
    intro v w ⟨h₁, h₂⟩
    apply And.intro h₁.symm
    cases h₂
    · exact Or.inr ‹_›
    · exact Or.inl ‹_›
  loopless := fun _ h ↦ h.1 rfl

Perhaps it's better to use docs#SimpleGraph.fromRel ?

def toSimpleGraph {V : Type*} (G : Digraph V) : SimpleGraph V := .fromRel G.Adj

[Rida Hamadani]

That's a great idea, thank you!

[Rida Hamadani]

#16954 starts with some of the things discussed here, but doesn't port anything from SimpleGraphs to Digraphs yet

[Rida Hamadani]

It would be nice to have an IsLoopless predicate.

[Vincent Beffara]

We have the classes docs#IsIrrefl for loopless, docs#IsAsymm for oriented, and so on ... would it make sense to use these instead of explicit quantifiers?

[Rida Hamadani]

Nice idea, but what do you think about using docs#AntiSymmetric and docs#Irreflexive instead? So we won't have to deal with adding h.asymm every time we want to use the hypothesis h : G.IsOriented. Also Irreflexive is used already when defining the loopless property on SimpleGraphs.

[Rida Hamadani]

Oh, Antisymmetric is different from Asymmetric, and apparently we don't have Asymmetric in mathlib

[Rida Hamadani]

I've added Asymmetric and rewrote the PR to use it instead, alongside Irreflexive.

[Mitchell Horner]

I don't know if this is the place to ask, but is there an advantage to implementing digraphs, simple graphs, etc. as separate structures instead of say:

abbrev Graph (V : Type*) := Rel V V

namespace Graph

variable {V : Type*}

class UndirectedGraph (G : Graph V) where
  undirected : Symmetric G

class LooplessGraph (G : Graph V) where
  loopless : Irreflexive G

class SimpleGraph (G : Graph V) extends UndirectedGraph G, LooplessGraph G

-- and so on

class SemicompleteGraph (G : Graph V) extends LooplessGraph G where
  semicomplete : ∀ v₁ v₂, G v₁ v₂ ∨ G v₂ v₁

class QuasiTransitiveGraph (G : Graph V) extends LooplessGraph G where
  quasi_transitive : ∀ v₁ v₂ v₃, G v₁ v₂ ∧ G v₂ v₃ → G v₁ v₃ ∨ G v₃ v₁

instance (G : Graph V) [h : SemicompleteGraph G] : QuasiTransitiveGraph G where
  quasi_transitive v₁ _ v₃ _ := h.semicomplete v₁ v₃

class OrientedGraph (G : Graph V) where
  oriented : ∀ v₁ v₂, Xor' (G v₁ v₂) (G v₂ v₁)

-- DAG, tree, etc.

In this case digraphs, simple graphs, etc. are built up using classes and definitions/theorems pick the resolution they need so no duplication. It also future proofs implementation of new subclasses of graphs.

I'm relatively new to Lean, but this reminds me of how say Ring is defined as a class extending SemiRing, AddCommGroup, AddGroupWithOne. Is there some lurking reason as to why this isn't done?

[Kyle Miller]

@Mitchell Horner There's a bit of discussion about this today at #Is there code for X? > Weak components of a digraph @ 💬, including a reference to a relevant PR. One other reason is that it's good to have actual types per class of object — for example the lattice structures on Digraph and SimpleGraph are interesting and useful.

[Kyle Miller]

For Ring, etc., the key difference is that these typeclasses implementing synecdoche. We talk about the underlying type for a ring as if it's the ring itself. It's nice because a single type can "be" multiple things in the algebraic hierarchy.

The first complication are types like Subgroup, but then there's a trick you can use. Given H : Subgroup G, you can use H as if it were a type, because Lean has its CoeSort system. Then we can say H "is" a group by synecdoche through the coercion — that is to say, H as a type has a Group instance.

However, this all falls apart when you start working with homomorphisms. You want types of homomorphisms, and there are some complications to, for example, a ring homomorphism "being" an additive homomorphism. This is all the DFunlike business patching it over.

Graphs are similar to homomorphisms. There are complications, and as that PR in the link shows, it's possible to do similar things, but it's not as nice of a situation as Ring et al.

[Mitchell Horner]

Kyle Miller said:

Mitchell Horner There's a bit of discussion about this today at #Is there code for X? > Weak components of a digraph @ 💬, including a reference to a relevant PR. One other reason is that it's good to have actual types per class of object — for example the lattice structures on Digraph and SimpleGraph are interesting and useful.

Thanks for this explanation. That discussion and #4127 is exactly what I was looking for.