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.

[Iván Renison]

Hi, is somebody working in the HasAdj class? I wanted to define walks and paths in Digraph, but I don't think redoing everything from SimpleGraph is a good idea. The HasAdj class looks like a good idea for me, and if nobody is working in it I would be happy to try to do it (if you agree that it is a good idea)

[Snir Broshi]

Well I was under the impression that we're all waiting for #33466, and then consider next steps (add a vertex set to SimpleGraph and maybe a HasAdj refactor).
Meanwhile people seem to be working on docs#Graph instead, and @Shreyas Srinivas is busy on CSLib and not the Digraph PR.
So basically I think you should go for it, or perhaps take over #33466 first.
Also see this message - #graph theory > Set in definition of Graph @ 💬

[Shreyas Srinivas]

I don’t actually have much to do on that PR

[Shreyas Srinivas]

There are some suggestions for proof golfs that don’t work as suggested

[Snir Broshi]

It is awaiting-author and merge-conflict

[Shreyas Srinivas]

The merge conflict is recent. The awaiting author thing is from the reviews mentioned above

[Shreyas Srinivas]

Just cleanly merged master

[Shreyas Srinivas]

I don't see the merge conflict

[Shreyas Srinivas]

And tbh I don't understand this review comment entirely. if someone wants to wrap it up, feel free : https://github.com/leanprover-community/mathlib4/pull/33466#discussion_r2777430599

[Shreyas Srinivas]

I indeed don't have much time to spend on this PR's review cycle, so I welcome PRs to my PR or something similar

[Snir Broshi]

Shreyas Srinivas said:

I don't see the merge conflict

I believe the conflicts were from #30484, and since you just pushed 2 commits the first of which is from a week ago, perhaps you already fixed those conflicts a week ago but forgot to push

[Shreyas Srinivas]

Fair. But now there is some build failure. Probably introduced by me

[Shreyas Srinivas]

Fixed the build

[Shreyas Srinivas]

I'll leave the review comments and golfing to whoever wants to takeover the PR or make a PR to the PR

[Shreyas Srinivas]

#33466 is green again per CI

[Shreyas Srinivas]

I made it run CI by merging master again, hence the yellow emoji

[Iván Renison]

Snir Broshi said:

Well I was under the impression that we're all waiting for #33466, and then consider next steps (add a vertex set to SimpleGraph and maybe a HasAdj refactor).
Meanwhile people seem to be working on docs#Graph instead, and Shreyas Srinivas is busy on CSLib and not the Digraph PR.
So basically I think you should go for it, or perhaps take over #33466 first.
Also see this message - #graph theory > Set in definition of Graph @ 💬

Okay

[Iván Renison]

I think that probably the best will be to directly implemente HasAdj also with the vertex set, instead of how it is done in #4127. We could initially make it be the complete set for SimpleGraph, and change it latter when SimpleGraph is refactored. What do you think?

[Shreyas Srinivas]

I don't recommend HasAdj level changes until you can refactor SimpleGraph to use vertex sets. I once underestimated the length of this task. You are just adding one more brick on that wall. Nvm : this should not be an issue.

[Snir Broshi]

Iván Renison said:

I wanted to define walks and paths in Digraph, but I don't think redoing everything from SimpleGraph is a good idea.

Oh I forgot to mention – if you're defining walks, consider Shreyas's Walk := {support : List V // support ≠ [] ∧ support.IsChain G.Adj} from #graph theory > New Walk definition without index parameters, it's pretty cool

[Shreyas Srinivas]

Snir Broshi said:

Iván Renison said:

I wanted to define walks and paths in Digraph, but I don't think redoing everything from SimpleGraph is a good idea.

Oh I forgot to mention – if you're defining walks, consider Shreyas's Walk := {support : List V // support ≠ [] ∧ support.IsChain G.Adj} from #graph theory > New Walk definition without index parameters, it's pretty cool

Write it as a structure though. It gives nicer looking goals.

[Snir Broshi]

Shreyas Srinivas said:

I'll leave the review comments and golfing to whoever wants to takeover the PR or make a PR to the PR

Can you add please-adopt to the PR if that's the case? Or are you planning to come back to it after cslib#275?

[Shreyas Srinivas]

I fixed a small mistake in the circuit definition. Now it is correct and so is the definition of cycles.

[Shreyas Srinivas]

Snir Broshi said:

Shreyas Srinivas said:

I'll leave the review comments and golfing to whoever wants to takeover the PR or make a PR to the PR

Can you add please-adopt to the PR if that's the case? Or are you planning to come back to it after cslib#275?

Done. I added the adopt label

[Shreyas Srinivas]

I don't time for the golfing stuff right now. If someone can do it I am happy

[Shreyas Srinivas]

Btw, the commits in this PR contains useful samples of code for the difficulties of writing manual instances without incremental elaboration.