Graph Minors

Stream: maths

[Alex Kontorovich]

I've been trying to figure out how to make graph minors work. You have to be able to take a graph, and inductively delete edges, delete vertices, and contract edges. The way a SimpleGraph V is currently defined, the Type V is the vertex set. So if you want to delete a vertex, or worse yet, contract an edge, you get into messy situations like this:

import Mathlib

variable {V : Type*}

-- First, define the equivalence relation for contracting edge e
def SimpleGraph.contractEdgeRel (e : Sym2 V) : V → V → Prop :=
  fun u v => u = v ∨ s(u, v) = e

-- Then define the setoid instance
def SimpleGraph.contractEdgeSetoid (e : Sym2 V) : Setoid V :=
{ r := contractEdgeRel e,
  iseqv := {
    refl x := by left; rfl
    symm h := by
      cases h with
      | inl hh => left; exact hh.symm
      | inr hh => right; rw [← hh, Sym2.eq_swap]
    trans exy eyz := by
      cases exy with
      | inl hxy => rwa [hxy]
      | inr hxy =>
        cases eyz with
        | inl hyz => right; rwa [hyz] at hxy
        | inr hzy =>
          cases Sym2.eq_iff.mp (hxy.trans hzy.symm) with
          | inl h => right; rwa [← h.1] at hzy
          | inr h => left; exact h.1
  } }

-- And now you can define what it means to contract an edge, on the type `V / ⟨e⟩`
def SimpleGraph.contractEdge (G : SimpleGraph V) (e : Sym2 V) :
    SimpleGraph (Quotient (contractEdgeSetoid e)) where
  Adj qu qv :=
    qu ≠ qv ∧
    Quotient.liftOn₂ qu qv
      (fun u v => G.Adj u v)
      (fun u₁ u₂ v₁ v₂ hu hv => by sorry)
  symm := by sorry

So it occurred to me: might it not be better for V to be some "ambient" set of vertices but not necessarily the "official" vertices of G? Then you would add one more field, vert : Set V for the vertex set, and ensure that adjacency requires terms from this set. With that, I could get all the way to the definition of graph minors, please see below. What do people think? Is there a better way to do this? (Or might it be worthwhile to refactor all of SimpleGraph...?)

import Mathlib

open Classical

/--
A `SimpleGraph'` has vertices `verts` which is a subset of some type `V`, and
the condition that if two vertices are adjacent, `Adj u v`, then both are in
the vertex set.
-/
structure SimpleGraph' (V : Type*) where
  verts : Set V
  Adj : V → V → Prop
  Adj_of_verts : ∀ (u v : V), Adj u v → u ∈ verts ∧ v ∈ verts
  symm : Symmetric Adj := by aesop_graph
  loopless : Irreflexive Adj := by aesop_graph

variable {V : Type*}

/--
New graph obtained by deleting some vertices, and any edges through them.
-/
def SimpleGraph'.deleteVerts (G : SimpleGraph' V) (s : Set V) : SimpleGraph' V where
  verts := G.verts \ s
  Adj u v := G.Adj u v ∧ u ∉ s ∧ v ∉ s
  Adj_of_verts u v h :=
    ⟨⟨(G.Adj_of_verts u v h.1).1, h.2.1⟩, ⟨(G.Adj_of_verts u v h.1).2, h.2.2⟩⟩
  symm _ _ h := ⟨G.symm h.1, h.2.2, h.2.1⟩
  loopless v h := G.loopless v h.1

/--
New graph obtained by deleting a given set of edges.
-/
def SimpleGraph'.deleteEdges (G : SimpleGraph' V) (s : Set (Sym2 V)) :
    SimpleGraph' V where
  verts := G.verts
  Adj u v := if s(u, v) ∈ s then False else G.Adj u v
  Adj_of_verts u v h := by
    by_cases h_case : s(u, v) ∈ s
    · simp [h_case] at h
    · simp only [h_case, ↓reduceIte] at h
      exact G.Adj_of_verts u v h
  symm u v h := by
    by_cases h_case : s(u, v) ∈ s
    · simp [h_case] at h
    · simp only [h_case, ↓reduceIte, if_false_left] at h ⊢
      have h_case' : s(v, u) ∉ s := by rwa [Sym2.eq_swap]
      simp only [h_case', not_false_eq_true, true_and]
      exact G.symm h
  loopless v h := by
    by_cases h_case : s(v, v) ∈ s
    · simp [h_case] at h
    · simp only [h_case, ↓reduceIte] at h
      exact G.loopless v h

def SimpleGraph'.edgeSet (G : SimpleGraph' V) : Set (Sym2 V) :=
  {e | ∃ u v, s(u, v) = e ∧ G.Adj u v}

lemma SimpleGraph'.mem_edgeSet (G : SimpleGraph' V) {e : Sym2 V} :
    e ∈ G.edgeSet ↔ ∃ u v, s(u, v) = e ∧ G.Adj u v := by
  simp [SimpleGraph'.edgeSet]

/--
New graph obtained by contracting an edge `e` in the original `edgeSet`. To create this graph,
delete a `choice` of one end of `e` from the vertex set, and reroute any free edges to the other
end of `e`.
-/
def SimpleGraph'.contractEdge (G : SimpleGraph' V) {e : Sym2 V} (he : e ∈ G.edgeSet) :
    SimpleGraph' V where
  verts := G.verts \ {(Quot.out e).1}
  Adj u v :=
    u ≠ v ∧ u ≠ (Quot.out e).1 ∧ v ≠ (Quot.out e).1 ∧ (G.Adj u v ∨
     (u = (Quot.out e).2 ∧ G.Adj (Quot.out e).1 v) ∨
     (v = (Quot.out e).2 ∧ G.Adj u (Quot.out e).1))
  Adj_of_verts u v h := by
    simp only [ne_eq] at h
    obtain ⟨u_ne_v, hadj⟩ := h
    simp only [Set.mem_diff, Set.mem_singleton_iff]
    constructor
    · -- Show u ∈ G.verts \ {(Quot.out e).1}
      refine ⟨?_, hadj.1⟩
      cases hadj.2.2 with
      | inl h => exact (G.Adj_of_verts u v h).1
      | inr h =>
        cases h with
        | inl h =>
          rw [SimpleGraph'.mem_edgeSet] at he
          obtain ⟨u₁, v₁, s_eq_e, adj₁⟩ := he
          have : e = s((Quot.out e).1, (Quot.out e).2) := by exact (Quot.out_eq e).symm
          rw [this, Sym2.eq_iff] at s_eq_e
          have := G.Adj_of_verts u₁ v₁ adj₁
          cases s_eq_e with
          | inl hh => convert this.2
                      exact h.1.trans hh.2.symm
          | inr hh => convert this.1
                      exact h.1.trans hh.1.symm
        | inr h => exact (G.Adj_of_verts u _ h.2).1
    · refine ⟨?_, hadj.2.1⟩
      cases hadj.2.2 with
      | inl h => exact (G.Adj_of_verts u v h).2
      | inr h =>
        cases h with
        | inl h => exact (G.Adj_of_verts _ v h.2).2
        | inr h =>
          rw [SimpleGraph'.mem_edgeSet] at he
          obtain ⟨u₁, v₁, s_eq_e, adj₁⟩ := he
          have : e = s((Quot.out e).1, (Quot.out e).2) := by exact (Quot.out_eq e).symm
          rw [this, Sym2.eq_iff] at s_eq_e
          have := G.Adj_of_verts u₁ v₁ adj₁
          cases s_eq_e with
          | inl hh => convert this.2
                      exact h.1.trans hh.2.symm
          | inr hh => convert this.1
                      exact h.1.trans hh.1.symm
  symm qu qv h := by
    simp only [ne_eq] at h ⊢
    refine ⟨Ne.symm h.1, h.2.2.1, h.2.1, ?_⟩
    cases h.2.2.2 with
    | inl h => left; exact G.symm h
    | inr h => right; cases h with
      | inl h => right; exact ⟨h.1, G.symm h.2⟩
      | inr h => left; exact ⟨h.1, G.symm h.2⟩

/--
Now we can define graph minors: keep the same ambient vertex type, but
inductively delete edges, vertices, or contract an edge.
-/
inductive SimpleGraph'.Minor : SimpleGraph' V → SimpleGraph' V → Prop
| refl (G : SimpleGraph' V) : G.Minor G
| delete_edge {G H : SimpleGraph' V} (e : Sym2 V) :
    H.Minor G → H.Minor (G.deleteEdges {e})
| delete_vertex {G H : SimpleGraph' V} (v : V) :
    H.Minor (G.deleteVerts {v}) → H.Minor G
| contract_edge {G H : SimpleGraph' V} (e : Sym2 V) (he : e ∈ G.edgeSet) :
    H.Minor (G.contractEdge he) → H.Minor G

[Aaron Liu]

We have docs#Graph now

[Alex Kontorovich]

Ah, that's great! Does Graph have a predicate IsSimple or something? (I didn't find such in the docs.) And even with Graph, I don't see Graph.Minor (nor Graph.deleteEdges, Graph.contractEdge, etc...)?

[Alex Kontorovich]

I did find the related Matroid.contract, on which this could be modeled...

[Alex Kontorovich]

Following up: Are there plans to merge Graph and SimpleGraph (I guess I'm imagining that all the theorems proved about SimpeGraphs could be re-written to be about Graphs with the added predicate Graph.IsSimple...?)

[Yaël Dillies]

There are vague plans to at least make them for similar to each other, yes

[Alex Kontorovich]

I see, thanks. And then, assuming SimpleGraph will look more like the proposed SimpleGraph’, what do people think of the proposed definition of SimpleGraph’.Minor?

[Antoine Chambert-Loir]

This is funny because that discussion appeared in a slightly different form a few weeks ago, reaching to the same conclusion. (I was advocating for another definition of graphs, whatever.) And probably for a very similar reason, when Gonthier's team formalized the odd order theorem, their framework had all groups be subgroups of a gigantic group.

[Antoine Chambert-Loir]

This is not the place (neither Zulip, nor mathlib) to redo the foundations of mathematical fields (or, is it?) but it seems that graph theory/matroid theory still haven't endured the categorization process. There is a notion of morphism of graphs, and contracting edges, etc. could appear as a universal construction which would be easy to chain. (Maybe still not easy, just slightly easier.)

[Antoine Chambert-Loir]

In linear algebras, we have subquotients of modules, and we can cope with it. (But, as categories, abelian categories are nice categories, quotient of sub and sub of quotient are the same, I don't know whether it's the same for graphs.)

[Shreyas Srinivas]

From the TCS world: I would argue that a graph H’ is a minor of G if it is a subgraph of another graph H which has a homomorphism into G

[Shreyas Srinivas]

I hope I haven’t made any obvious mistakes

[Shreyas Srinivas]

But the little experience I have with using mappings instead of set theoretic relations in graph theory and lean has taught me that lean’s tactics excel at the latter and they feel more natural than following maps around

[Kevin Buzzard]

@Peter Nelson has long argued that in practice graphs are used in a different way to algebraic structures like groups and rings; whilst it might be true that you can make a category of graphs, in practice graph theorists do not make much use of the concept of a morphism of graphs (indeed this concept was not even defined in my graph theory course), and this is in strong contrast to algebraists who are using morphisms of groups and rings all the time. So we should be dubious of arguments of the form "ring theory works fine with these decisions therefore graph theory should be set up this way".

Gonthier's decision to make all groups equal to subsets was I think motivated by the idea that all groups should be the same kind of object (as opposed to distinguishing groups (types) and subgroups (terms)). However the idea does not scale to rings; given two groups there's a larger group that they're both a subgroup of, but there is no commutative ring containing both $\Z/2\Z$ and $\Z/3\Z$ as subrings (because in applications of comm alg to algebraic geometry we demand that the 1s coincide). So when developing lemmas in ring theory which involve three or four rings (e.g. "let L/K be a finite extension of number fields with rings of integers B/A") we let all of A,B,K,L be types (because again it's important that they're all the same thing; we get exponential growth in the number of lemmas we have to state if we allow for everything to be both a ring and a subring).

[Kyle Miller]

It's not always appropriate, but a reasonable definition of a graph minor is an interval of subgraphs (so, a minor of G is a pair of subgraphs A and B of G where A is a spanning subgraph of B). In some contexts, like for the definition of the Tutte polynomial, both A and B can be spanning subgraphs, since vertex deletion isn't needed.

To realize (A,B) as a graph, you take B and contract all the edges in A.

This is only for representing the data of a minor though. Anything that wants to work with paths in minors for example would want something else almost immediately.

[Kyle Miller]

Antoine Chambert-Loir said:

still haven't endured the categorization process.

Why are submodules represented using carrier sets instead of injective morphisms, despite having endured categorization?

I think the thesis we've been pursuing is that graph theory and matroid theory are best organized as studying subobjects of some unspecified global object, given that there's so little structure involved. We may as well define SimpleGraph to be a subgraph of the complete graph.

I think also that @Peter Nelson and his student have been working on a version of minors that are sort of morphism-ish, and where you choose a particular representative of the quotient on the same vertex type, as Alex Kontorovich has done with SimpleGraph'.contractEdge. My understanding is that it's using a technique that's different from defining an inductive relation for is-minor-of.

[Antoine Chambert-Loir]

Kyle Miller said:

Why are submodules represented using carrier sets instead of injective morphisms, despite having endured categorization?

Because that would probably be too much. In abelian categories, this is what happens and the situation has been made complicated by three things:

• the abstract rigorous reasoning is quite arduous
• for many arguments, the embedding theorem showed that one can pretend that everything is a module
• there is an abstract while rigorous and relatively straightforward way to make these arguments, but it hasn't been put into light. (@Joël Riou has made a version of it into mathlib.)
  But be assured that after some level of complexity, most (if not all) people play a silent game of identifying submodule of a quotient which is a quotient of a submodule without even noticing.

[Antoine Chambert-Loir]

@Kevin Buzzard you're perfectly right, but have you opened papers in BSE (before scheme era) algebraic geometry? There was a gigantic field containing the field of rational functions of any variety you would encounter (all of the same characteristic, of course), and specialization from characteristic zero to characteristic p was a highly technical exercise reserved to acrobats (Néron models were written like this before Bosch, Lütkebohmert and Raynaud gave us their book…)

[Peter Nelson]

There are two parallel discussions here, both interesting. I think the threshold for ‘probably too much’ in graph theory is much lower, because the advantages that come with a categorical perspective are much less compelling. Morphisms between graphs simply aren’t part of the normal idiom of graph theory.

Here is something I see as a requisite for a good notion of graph minor, described a little informally: suppose I have a path P in a graph G, and C is a set of edges of G, none of which are incident with anything in P. There are a lot of different minors of G obtained by contracting and deleting various edges of C, possibly in different orders.

I think that ‘minor’ should be formalized to allow (not force) the perspective that in all of these different minors, P is still ‘the same’ path - that is, I shouldn’t have to worry about graph morphisms that transfer between different versions of P at all. (Fiddling with the road network in London does nothing to change the way the roads look in New York.)

For some applications in graph theory, making this P formally the same for all these minors is too much of a cost. But for a lot of what graph theorists are doing, these paths are all Equal with a capital E, and reasoning about morphisms is suddenly turning something very simple into something very complicated.

Kevin put it very nicely in the other thread with the word ‘mutate’. My view is that combinatorial objects should be formalized flexibly enough that mutating an object does not force one to consider a function between the new and old objects.

I would worry about an inductive definition of minor for this reason.

[Alex Kontorovich]

Very interesting, thanks! So then do you have an alternative suggestion for how to formulate (and then formalize) what a graph minor should be?

[Kyle Miller]

I guess the definition I proposed satisfies Peter's criterion (a minor is a subgraph of G and a subset of edges of that subgraph).

This definition also has the property that deletions and contractions commute, as equalities.

[Kevin Buzzard]

Aah, Peter has reminded me of another aspect of the difference, which was raised in another thread before: you consider maps between groups a lot, and maps between graphs rarely; however you mutate graphs a lot (adding or taking away a few vertices or edges), and you mutate groups essentially never (because this breaks groupiness). So they really do seem to be quite different objects from a formal perspective.

[Alex Kontorovich]

Kyle Miller said:

It's not always appropriate, but a reasonable definition of a graph minor is an interval of subgraphs (so, a minor of G is a pair of subgraphs A and B of G where A is a spanning subgraph of B). In some contexts, like for the definition of the Tutte polynomial, both A and B can be spanning subgraphs, since vertex deletion isn't needed.

To realize (A,B) as a graph, you take B and contract all the edges in A.

This is only for representing the data of a minor though. Anything that wants to work with paths in minors for example would want something else almost immediately.

Sorry, I don't follow; is this what you mean as the structure you envision for minors? Can you say more about realizing (A,B) as a graph by "contracting" the edges in A? The way I had proposed to do this above was, for a given edge, to make a choice of endpoint to exclude, and re-route edges. Another way is to take a quotient where the two edges are identified, but this changes the underlying Type.

[Mario Carneiro]

Kevin Buzzard said:

Aah, Peter has reminded me of another aspect of the difference, which was raised in another thread before: you consider maps between groups a lot, and maps between graphs rarely; however you mutate graphs a lot (adding or taking away a few vertices or edges), and you mutate groups essentially never (because this breaks groupiness). So they really do seem to be quite different objects from a formal perspective.

I think these aren't necessarily as different as you suggest. I would say an edge contraction is structurally similar to an operation like taking the span of an element or the kernel of a homomorphism. There is a question about whether the result is a group or a subgroup, but you can also have graphs vs graph minors on the other side. I expect there are well defined spaces of all contractions and deletions of a base graph, on which contraction acts as a regular function, which can play a similar role as Subgroup does for groups (and something like a composition series would be analogous to a series of contractions or deletions).

[Kevin Buzzard]

My understanding was that the challenge was to make a path in a graph which is nowhere near a collection of contractions/deletions/other mutations be an object which is independent of the order that these mutations are being performed in, and your conflating subgroups and groups in the above post is going to be problematic here

[Mario Carneiro]

I'm not conflating groups and subgroups, I'm drawing an analogy between groups/subgroups and graphs/graph minors

[Mario Carneiro]

in particular, I think we can handle most graph mutation operations by introducing an object that plays the role of Subgroup. Doing everything on Group means you have to change types all the time which can get painful

[Mario Carneiro]

You ultimately want both and easy conversion between them

[Kevin Buzzard]

So how to make a path defeq to the same path once you added and deleted a vertex and an edge connecting the vertex to the graph

[Kevin Buzzard]

And also defeq to the path that you get when you add an extra vertex and edge, and then contract the edge

[Mario Carneiro]

ah, this only handles removing vertices, not adding them. You would need some bigger graph to hold the extra vertices

[Kevin Buzzard]

Then I would argue that we're still a long way of being able to make modern graph theory feasible

[Mario Carneiro]

if you allow the vertices to be a subset of the base type though, I think that's not a major issue

[Mario Carneiro]

because you will need some type to give "coordinates" to the new vertices you want to add anyway

[Kevin Buzzard]

How does this deal with edge contractions?

[Mario Carneiro]

quotients

[Kevin Buzzard]

This will break defeq in the same way that coercing to type from the univ subgroup will

[Mario Carneiro]

I'm not trying to save defeq, I'm trying to have a sensible notion of = which isn't isomorphism or an evil equality

[Kevin Buzzard]

Well if I contract e1 and then e2 that's going to be different to contracting e2 and then e1

[Mario Carneiro]

no, those will be = subgraphs under this approach

[Kevin Buzzard]

But a quotient of a quotient isn't equal to the same thing the other way around?

[Mario Carneiro]

this is basically like doing insert on Set A, it's not definitionally commutative but it does satisfy insert x (insert y S) = insert y (insert x S)

[Mario Carneiro]

sorry, it's not literally a quotient, the space itself is the collection of partial equivalence relations

[Mario Carneiro]

the quotient is the interpretation of that equivalence relation as a graph

[Kevin Buzzard]

Aha, and you start with some huge index type of cardinality greater than any graph showing up in the argument so that you'll always be able to find some more vertices if necessary

[Mario Carneiro]

(it's not just a PER of course, that would only do the vertices. You need edges too so you have some relation that respects the PER)

[Kevin Buzzard]

You are still going to end up with graphs which mathematicians are convinced are defeq but which are just "isomorphic relations" this way because eg you and me added different "random" vertices when we had to adjoin a new vertex which we later on contracted back into our graphs which started off defeq

[Mario Carneiro]

if you change the identity of the vertices, then the resulting graph will not be =, that's true

[Mario Carneiro]

but graphs have nontrivial automorphisms so I don't think it is reasonable to try to make = line up with graph isomorphism

[Kevin Buzzard]

But I think this is a better idea than anything I'd heard before

[Mario Carneiro]

I think you would just have isomorphism as an explicit relation on the type

[Bhavik Mehta]

Mario Carneiro said:

in particular, I think we can handle most graph mutation operations by introducing an object that plays the role of Subgroup. Doing everything on Group means you have to change types all the time which can get painful

Isn't this essentially the setup currently in mathlib, with SimpleGraph and SimpleGraph.Subgraph?

[Mario Carneiro]

Almost. docs#SimpleGraph.Subgraph covers the case of deleting vertices and edges, but not edge contractions. I don't know whether my suggestion has a name in the literature

[Aaron Liu]

Is it called a "graph minor"?

[Kyle Miller]

@Alex Kontorovich I'm saying that the data of a minor is a structure with two things: a subgraph and a subset of edges. It's not a graph on its own, but a "graph minor" that needs to be realized as a graph if it needs to be used as a graph.

Then, there would be two more ingredients. First, a relation SimpleGraph' V -> Minor V -> Prop that says the graph realizes the minor. Second, there can be a function that chooses a particular realization using the axiom of choice. This relation gives freedom to choose how to realize minors, while the functions there if you're just happy with having a realization.

(On my phone, otherwise I might back this up with code.)

[Peter Nelson]

I think that the issue with a master subgraph-like thingy is that you end up needing all the API for graphs to be duplicated, to the extent that the type might as well be Graph, where the vertex and edge sets are structure fields. This was what happened for Matroid. I had a Minor type whose API was expanding enough that it just became a parallel notion of Matroid with no added value. When the Minor type was removed and I started just using Matroid for everything, things became much easier.

The idea that @Hyeokjun Kwon and I are working on for graph minors is something like the following: there is no Minor type. Given G : Graph α β and a function f : α → α',
define G.contractMap f to be the Graph α' β obtained by applying f to every vertex of G,
merging vertices as needed. Then H.IsMinorOf G means that H is a subgraph of G.contractMap f
for some appropriately constrained f. (essentially, f is only allowed to merge vertices that are connected in G).

This definition allows for multiple perspectives. If one wants to view a minor as having vertices
in a quotient type, than α' can be a quotient type. But crucially, we can also just have α' = α.
For instance, if e = xy is an edge of G, then f can be the function with f x = y that is
the identity elsewhere, and then G.contractToRight e x y = (G.contractMap f).delete e is the minor of G formed by merging the vertices x and y into a new vertex labelled y, and leaving every other edge and vertex the same. This means that one can set things up so that the minor and the graph have the same type, and paths of a minor are also paths of the graph, in the strongest sense of the word 'are'.

[Mario Carneiro]

Peter Nelson said:

Then H.IsMinorOf G means that H is a subgraph of G.contractMap f
for some appropriately constrained f. (essentially, f is only allowed to merge vertices that are connected in G).

So does this allow the theorem I mentioned before: contract e1 (contract e2 G) = contract e2 (contract e1 G)?

[Mario Carneiro]

I want an equational theory like that

[Peter Nelson]

It depends how you contract the edges. I think if you have equalities like that unconditionally, then you are unable to reason about paths/subgraphs etc of minors without pain. Things like that will be provable for some notions of contraction if you set up the vertex labels to agree.

[Mario Carneiro]

I don't know what that means. e1 and e2 are what they are, let's say they share a vertex

[Peter Nelson]

What is the vertex set of G / e1?

[Mario Carneiro]

I don't know, that's for you to answer

[Mario Carneiro]

for me that's just some subset of the big set

[Peter Nelson]

If that's the case, then you can prove your equality. This is working with a model where the vertices of every graphs are subsets of some big set.

[Peter Nelson]

But that model is very annoying in other contexts.

[Mario Carneiro]

How would you state that theorem?

[Peter Nelson]

It would involve a certain predicate or subtype of Graph, namely those where the vertices are formally sets.

[Mario Carneiro]

are you saying it's not going to be easy to write down?

[Mario Carneiro]

it's not just combinations of the operators you mentioned above

[Peter Nelson]

It will be a theorem about GraphWhereEveryVertexIsActuallyASet, and it will be easy to write down once that type is defined.

[Peter Nelson]

But the appropriate notion of edge contractions defined for that type of graph is a special case of my framework.

[Peter Nelson]

And that type of graphs is too constraining to be a design that works for everything.

[Mario Carneiro]

I think that just as Subgroup has a lot of usefulness because it has a lot of productive structure on it, so too does this set of graph minors. It's a complete lattice, it has a map and comap, it can be built up from atomic elements (the edges) etc

[Mario Carneiro]

when everything produces a fresh type you lose the ability to talk about that structure

[Mario Carneiro]

Peter Nelson said:

And that type of graphs is too constraining to be a design that works for everything.

I am already primed to expect no possible formalization in graph theory to "work for everything". That sounds like a fool's errand. Rather, we should establish what kind of theorems / argumentation styles we are trying to make easy and what other kind of theorems we want to make possible

[Mario Carneiro]

Do you have a representative example of a theorem which would make use of this library?

[Peter Nelson]

I think there is potential for a single Graph type to be appropriate for all applications, and typeclasses to be used with specialized API for certain settings, such as wanting an equational theory of minors. My issue is with having a Minor type - if it is used, it will grow to the extent that there are now two separate types that just mean 'a graph', with API for each, and lots of mathematically contentless API linking them. I tried this for matroids, and it was a huge waste of time.

I am not sure that the structure of a Minor type is all that useful. It's not a lattice (what would the join or meet of G / e and G \ e be?). The minor order is transitive, and there isn't much more.

The proofs I am thinking of are the ones that contract an edge, and apply induction, such as this one. If you want to apply the inductive hypothesis to G / e, then it's pretty annoying if G and G / e have different types.

[Alex Kontorovich]

I would love to see the setup for this short proof (of Menger's theorem), no need (yet) for the proof...?

[Mario Carneiro]

Remind me what G/e and G\e are?

[Mario Carneiro]

I'm pretty sure the type I described (partial equivalence relations together with an edge relation which respects the equivalence) is a complete lattice. The supremum is the least PER containing all of the given ones, and the least edge relation containing the original ones and respecting the PER

[Antoine Chambert-Loir]

Contraction of edge e, vs removal of edge e.

[Antoine Chambert-Loir]

I'd also guess both descriptions of minors are related in the same way equivalence relations, equivalence classes (subsets) and quotients are related.

[Mario Carneiro]

I'm not sure which way should be up in this lattice, but let's just say it's the set order. In that case the contraction e = {a,b} adds elements to the PER (and the edge relation as a result), while edge removal leaves the PER the same and removes something from the edge relation. So you have the relation G \ e < G < G / e and the meet and join are not too interesting

[Peter Nelson]

And in particular, if G \ e is below G / e (or vice versa), that’s not the minor relation on graphs.

[Peter Nelson]

This is really one of the issues - there are a ton of interrelated posets of graphs : minors, subgraphs, induced subgraphs, pivot minors, vertex minors, Mario’s PER lattice, etc etc. I doubt that giving them all their own types is sustainable.

[Mario Carneiro]

The poset here is I think what you get from graph homomorphisms: as you go up the lattice you can quotient more, and also add edges

[Mario Carneiro]

you can construct a map from G \ e to G which is the identity, and there is a map from G to G / e which is the quotient map

[Peter Nelson]

Right - this is different. The minor order should have the property that a minor of G should have edge set contained in that of G.

[Mario Carneiro]

(note, I wasn't the one who wanted to call this minors, I said I didn't know if it had a name in the literature and someone suggested minor)

[Mario Carneiro]

Peter Nelson said:

Right - this is different. The minor order should have the property that a minor of G should have edge set contained in that of G.

what is an edge set?

[Peter Nelson]

Ok, fair enough. I was assuming you are talking about minors as per the thread title

[Mario Carneiro]

do edges have identities in this setting?

[Peter Nelson]

I don’t know what you mean by this. In a non-simple graph, an edge is a term in an edge type that is related to the terms in the vertex type of the graph by an incidence predicate.

[Mario Carneiro]

okay, I was considering the simple graph case since people were linking to it

[Mario Carneiro]

once more "one definition to rule them all" causes problems

[Peter Nelson]

SimpleGraph is a good type to define. I don’t agree that Subgraph or sub-anything really is helpful

[Mario Carneiro]

For edges with identities, I think you can do something similar but considering subsets of V x E instead of V x V

[Mario Carneiro]

or well maybe it's more complicated than that, not sure how exactly your base type looks like

[Mario Carneiro]

maybe E -> V x V?

[Peter Nelson]

docs#Graph

[Peter Nelson]

But I think that mathematically, what you are talking about is not the minor order on graphs.

[Peter Nelson]

https://en.m.wikipedia.org/wiki/Graph_minor

[Mario Carneiro]

Graph is more complicated, I don't think it has the same nice lattice structure. The trouble is that when edges have identity and you take the union of two graphs, a single edge may end up with more than 2 ends. It would work great for multigraphs but that constraint doesn't have the same nice universal algebra behavior as the simple graph version

[Peter Nelson]

That’s right. But multigraphs with edge identity are the right setting for minors and topological embeddings, so something needs to happen. I’m saying that a Minor type won’t be too helpful, but an IsMinor relation on graphs will be.

[Mario Carneiro]

I think you can have a Minor type using a PER encoding though... I think it would make more sense though to have the type allow non-minors and have an inequality relation on it asserting the minorness relation. Reading the wiki page it's not clear how the infinite version goes; the tricky part is that all the equivalence relations in the smaller graph need to be spanned in the larger graph

[Peter Nelson]

You could encode the minor type in many ways, sure. I like Kyle’s lattice interval approach. But what is the point?

[Mario Carneiro]

to be able to uniformize the types so that you can take sequences and chains and whatnot without a headache to keep track of a bunch of type operators and type isomorphisms

[Mario Carneiro]

Can I write down a concrete minor reduction sequence on 7 vertices without having to talk about 7 completely separate types?

[Peter Nelson]

Yes, they are all Graph.

[Mario Carneiro]

graph is a typeclass, not a type

[Mario Carneiro]

are you swapping out fin 1 thru fin 7 in your representation?

[Peter Nelson]

What?

[Peter Nelson]

They have vertex type Nat, and can be constructed to have nested vertex and edge sets.

[Mario Carneiro]

Graph is a typeclass over V and E. I'm asking whether the 7 graphs in my example will need to have several different types for V and E

[Peter Nelson]

No, all the same type, just different vertex and edge sets.

[Peter Nelson]

And Graph a b is a structure. Does that make it a typeclass?

[Mario Carneiro]

oh, weird

[Mario Carneiro]

it has the look of a typeclass, but it's not

[Mario Carneiro]

doesn't really change the point much

[Mario Carneiro]

If you can keep V and E the same then that's good. But it seems to me like this caters to deletions more than contractions because it's missing the PER bit

[Mario Carneiro]

how are contractions done?

[Mario Carneiro]

I suspect it will force you to make an arbitrary choice of which vertex to keep and then you have some symmetry breaking and I think that's where @Kevin Buzzard's argument comes from that missing defeqs make people sad

[Peter Nelson]

You can contract by mapping the vertex type to another type using a non-injective function. The codomain is allowed to be the same type, so you can identify vertices x and y by mapping them both to x, for example.

[Mario Carneiro]

yeah that sounds really gross

[Mario Carneiro]

in particular you had to pick a non-injective function there

[Mario Carneiro]

I just want G / e to be all the data I need

[Peter Nelson]

It isn’t. It’s how graph theorists do graph theory a lot of the time, and it avoids a whole lot of categorical garbage to describe a simple mutation of a combinatorial object.

[Mario Carneiro]

The notation there isn't supplying any noninjective function though. The only one that has a claim to canonicity is the quotient map

[Mario Carneiro]

and that's type changing

[Peter Nelson]

Canonicity is annoying here.

[Mario Carneiro]

no, you have the wrong representation

[Peter Nelson]

And in practice it’s not what is needed.

[Mario Carneiro]

you can with a small change of representation make the other stuff unaffected and make contractions just as easy as deletions

[Peter Nelson]

It isn’t a small change. Anything that involves defining the minor type is a huge change. If minors are not Graph, then Minor needs a ton of API that eventually will become a parallel version of the graph API, with no extra content.

Can you tell me a proof of something in graph theory where a Minor type will be helpful?

[Mario Carneiro]

I'm talking about a type like Graph, not a type like Minor

[Peter Nelson]

Can you explain the design?

[Shreyas Srinivas]

If you are using maps to represent minors, then in the simplegraph case you also have to undo the self loops in the minor to satisfy loopless. General graphs may allow self loops. How would that work in your definition?

[Mario Carneiro]

structure PERGraph (α β : Type*) where
  vertexRel : α → α → Prop
  vertexRel_symm : vertexRel a b → vertexRel b a
  vertexRel_trans : vertexRel a b → vertexRel b c → vertexRel a c
  IsLink : β → α → α → Prop
  isLink_symm : IsLink e a b → IsLink e b a
  isLink_resp : IsLink e a b → vertexRel b b' → IsLink e a b'
  rel_of_isLink : IsLink e x y → IsLink e v w → vertexRel x v ∨ vertexRel x w
  left_mem_of_isLink : IsLink e x y → vertexRel x x

[Peter Nelson]

I assume that’s a typo in isLink_resp - the conclusion should be vertexRel a b’, right?

[Mario Carneiro]

no

[Mario Carneiro]

it's saying IsLink respects the equivalence relation vertexRel individually on its two variables

[Peter Nelson]

So what is vertexRel describing?

[Mario Carneiro]

a vertex in the traditional sense is an equivalence class of vertexRel

[Mario Carneiro]

IsLink says whether a given edge has the specified two endpoints

[Peter Nelson]

Ok.

[Mario Carneiro]

this is basically exactly the data you need to prove that if you quotient by vertexRel you get a Graph

[Mario Carneiro]

Graph builds in subsets to the definition - it could have required the vertex set to be the whole type but it didn't

[Mario Carneiro]

this builds in both subsets and quotients into the definition

[Peter Nelson]

I think this is just too baroque. Working with it means always caring about different ‘versions’ of a vertex, which will make simple reasoning about paths, sizes of sets, or anything really, very difficult.

[Mario Carneiro]

not really? Most definitions are unchanged

[Peter Nelson]

I don’t think that having a more pleasant calculus of minors is worth that.

[Mario Carneiro]

I think this is something that you need to actually attempt in order to get a better sense for whether that's actually true. Sometimes experimentation is part of formalization

[Peter Nelson]

Maybe. So to talk about something being a vertex of more than one graph, the something needs to have type Set a?

[Mario Carneiro]

no, you would just talk about elements of A

[Mario Carneiro]

there is a fixed background of vertex and edge names which you can use to talk about vertices and edges in multiple graphs

[Mario Carneiro]

it's just that after a contraction, two vertex names might refer to the same vertex in a given graph, or one might refer to no vertex because it got deleted from the graph

[Peter Nelson]

Isn’t this setoid hell?

[Mario Carneiro]

yeah basically

[Mario Carneiro]

at least it's a setoid

[Mario Carneiro]

whether it's hell is TBD

[Philippe Duchon]

No requirement that vertexRel be an equivalence relation (i.e., reflexive)?

[Mario Carneiro]

that's why it's a PER and not an ER

[Peter Nelson]

It should be irreflexive on non-vertices

[Philippe Duchon]

Not sure what ER and PER stand for :)

[Mario Carneiro]

that's what makes it do both subsets and quotients rather than just quotients

[Peter Nelson]

(Partial) equivalence relation

[Peter Nelson]

I am foreseeing a lot of API lemmas that transfer graph predicates across vertexRel. When combined with inductive types like paths, and functions like colouring, this feels explosive.

[Mario Carneiro]

doubling is not explosive

[Peter Nelson]

Doubling for each vertex in the lemma statement

[Mario Carneiro]

?

[Mario Carneiro]

I am tempted to actually change the definition of Graph to this, that would get rid of the redundancy

[Mario Carneiro]

but it's easier to discuss in a non-destructive way as just a new thing with maybe some duplicated API

[Peter Nelson]

I’m suspicious of this. Making things a setoid so that contraction is canonical feels like a bad tradeoff.

[Mario Carneiro]

by the way, the definition of a path is unchanged

[Mario Carneiro]

coloring requires that the coloring function agrees with the equivalence relation

[Peter Nelson]

It’s unchanged, but now there is an equivalence relation on paths.

[Mario Carneiro]

I guess, but I don't see why it would need defining

[Mario Carneiro]

the main place where it might get awkward is if you want to talk about cardinalities of sets

[Mario Carneiro]

in that case I would just suggest taking an actual quotient and looking at the corresponding Graph

[Mario Carneiro]

that could be avoided if we had setoid cardinality (defined using setoid-respecting bijections) but that really does sound like setoid hell

[Peter Nelson]

I see that the cardinality issue will cause problems; taking an actual quotient is a bandaid solution which will have annoying API, and set cardinality is all over the place in graph theory.

I can't think of other concrete problems, apart from the big conceptual one; we can have 'equal' vertices x and y with x \ne y. This is the kind of thing which means that a Graph is not really a 'graph' in the way one would expect; theorem statements have to be read extra-carefully, since they could be saying something other than what they appear to say. I would be embarrassed to have to explain this to someone unaccustomed to formalization; it is much worse than the idea that there can be elements of the vertex type outside the vertex set.

On the other hand: a Graph in the current sense is a graph in Mario's sense, with an additional assumption that the classes of the PER are singletons. This could be a typeclass assumption, which could make interactions between one API and the other go smoothly.

[Alex Kontorovich]

I'm really glad to see this battle play out
image.png

since it's identical to the one that went through my head when I was debating between

Alex Kontorovich said:

def SimpleGraph.contractEdgeRel (e : Sym2 V) : V → V → Prop :=
  fun u v => u = v ∨ s(u, v) = e

def SimpleGraph.contractEdgeSetoid (e : Sym2 V) : Setoid V :=
{ r := contractEdgeRel e, ...}

def SimpleGraph.contractEdge (G : SimpleGraph V) (e : Sym2 V) :
    SimpleGraph (Quotient (contractEdgeSetoid e)) where

and

def SimpleGraph'.contractEdge (G : SimpleGraph' V) {e : Sym2 V} (he : e ∈ G.edgeSet) :
    SimpleGraph' V where
  verts := G.verts \ {(Quot.out e).1}
  Adj u v :=
    u ≠ v ∧ u ≠ (Quot.out e).1 ∧ v ≠ (Quot.out e).1 ∧ (G.Adj u v ∨
     (u = (Quot.out e).2 ∧ G.Adj (Quot.out e).1 v) ∨
     (v = (Quot.out e).2 ∧ G.Adj u (Quot.out e).1))

[Alex Kontorovich]

I still don't know which side will win, but I'm eager to find out!...

[Alex Kontorovich]

Ok I think I finally see what @Mario Carneiro is getting at. I wonder if you can keep this same setup, but also let yourself have a subset of α for the vertex set? And then maybe we don't need to actually take Quotients at all (so as not to change the underlying Types), maybe we can just work at the level of these structures directly?

import Mathlib

structure Graph' (α β : Type*) where
  vertexSet : Set α
  vertexRel : α → α → Prop
  vertexRel_symm : ∀ ⦃a b⦄, a ∈ vertexSet → b ∈ vertexSet → vertexRel a b → vertexRel b a
  vertexRel_trans : ∀ ⦃a b c⦄, a ∈ vertexSet → b ∈ vertexSet → c ∈ vertexSet →
    vertexRel a b → vertexRel b c → vertexRel a c
  IsLink : β → α → α → Prop
  edgeSet : Set β
  isLink_symm : ∀ ⦃e a b⦄, e ∈ edgeSet → a ∈ vertexSet → b ∈ vertexSet → IsLink e a b → IsLink e b a
  isLink_resp : ∀ ⦃e a b b'⦄, e ∈ edgeSet → a ∈ vertexSet → b ∈ vertexSet → b' ∈ vertexSet →
    IsLink e a b → vertexRel b b' → IsLink e a b'
  rel_of_isLink : ∀ ⦃e x y v w⦄, e ∈ edgeSet → x ∈ vertexSet → y ∈ vertexSet →
    v ∈ vertexSet → w ∈ vertexSet → IsLink e x y → IsLink e v w → vertexRel x v ∨ vertexRel x w
   left_mem_of_isLink : IsLink e x y → vertexRel x x

[Mario Carneiro]

You don't need the vertex set, since you can define it as {a | vertexRel a a}

[Mario Carneiro]

they are equivalent

[Alex Kontorovich]

Ah, I was going to say that vertexRel a a holds for all a, without needing to check the vertexSet...

[Mario Carneiro]

that is to say, in my version when you want to subset the vertex set you do so by letting vertexRel be irreflexive sometimes

[Alex Kontorovich]

Yes, I understand... But I think it'll be a little clunkier to check if you're in the vertexSet by testing vertexRel a a, no? It's more natural (to me) to have the set right there from the beginning?

[Mario Carneiro]

(I assume this explains why left_mem_of_isLink exists as well)

[Mario Carneiro]

Oh you can define vertexSet after the fact

[Mario Carneiro]

or alternatively, have it in the structure but mandate it is equivalent to vertexRel a a

[Alex Kontorovich]

Sure, but adding left_mem_of_isLink seems clunkier to me than just giving yourself the vertexSet...?

[Mario Carneiro]

otherwise you get an additional degree of freedom in the definition which is bad for =

[Alex Kontorovich]

I added vertex_rfl to the structure I proposed above. So I don't think I have extra degrees of freedom?

[Mario Carneiro]

in the real definition of docs#Graph there is one of these already for edgeSet, which is equivalent to the set of edges which have at least one point

[Mario Carneiro]

You do; the equivalence relation for points outside the vertex set is underdetermined

[Alex Kontorovich]

ah yes I see

[Mario Carneiro]

why do you want vertexRel_rfl?

[Alex Kontorovich]

so wait, where do you get edgeSet from your structure?

[Mario Carneiro]

that one is also determined from IsLink, exactly as in docs#Graph

[Alex Kontorovich]

ok so you're just dropping edgeSet from the structure, and picking it up later as a definition

[Mario Carneiro]

for those determined and redundant sets, you have the option of either defining them as functions after the structure definition, or adding them as fields but having if and only if hypotheses for them so that they don't become new degrees of freedom

[Mario Carneiro]

I kept them out for simplicity but mathlib style is usually to put them in, sometimes quite a lot of functions end up as fields

[Alex Kontorovich]

got it. So then what's better, having extra fields in the structure with iff's, or smaller structures but then definitions outside of them? (I thought it former was preferred?)

[Mario Carneiro]

extra fields in the structure give you the ability to change the defeqs on that field

[Mario Carneiro]

if that's important in applications then you should consider it, but it's good to default to not doing so until you have an actual motivating use case because the whole kitchen sink can end up in your structure

[Alex Kontorovich]

Shouldn't rel_of_isLink be:

rel_of_isLink e x y z w : IsLink e x y → IsLink e z w → vertexRel x z ∧ vertexRel y w

? So if e represents an edge from x to y and also from z to w, then x had better be in the same vertex class as z and same with y and w, no?

[Alex Kontorovich]

and wouldn't you also want the freedom to collapse multiple edges into one? So then you want to introduce an edgeRel with similar properties?

[Alex Kontorovich]

So now it looks something like this:

structure Graph' (α β : Type*) where
  vertexSet : Set α
  vertexRel : α → α → Prop
  vertex_mem_iff_vertexRel x : x ∈ vertexSet ↔ vertexRel x x
  vertexRel_symm x y : vertexRel x y → vertexRel y x
  vertexRel_trans x y z : vertexRel x y → vertexRel y z → vertexRel x z
  edgeSet : Set β
  edgeRel : β → β → Prop
  edge_mem_iff_edgeRel e : e ∈ edgeSet ↔ edgeRel e e
  edgeRel_symm e₁ e₂ : edgeRel e₁ e₂ → edgeRel e₂ e₁
  edgeRel_trans e₁ e₂ e₃ : edgeRel e₁ e₂ → edgeRel e₂ e₃ → edgeRel e₁ e₃
  IsLink : β → α → α → Prop
  isLink_symm e x y : IsLink e x y → IsLink e y x
  isLink_resp_vertex e x y y' : IsLink e x y → vertexRel y y' → IsLink e x y'
  isLink_resp_edge e₁ e₂ x y : IsLink e₁ x y → edgeRel e₁ e₂ → IsLink e₂ x y
  rel_of_isLink e x y z w : IsLink e x y → IsLink e z w → vertexRel x z ∧ vertexRel y w
  left_mem_of_isLink e x y : IsLink e x y → vertexRel x x
  edge_mem_iff_exists_isLink e : e ∈ edgeSet ↔ ∃ x y, IsLink e x y

[Alex Kontorovich]

Ok, edge deletion is simple enough:

import Mathlib

structure Graph' (α β : Type*) where
  vertexSet : Set α -- possibly omit?
  vertexRel : α → α → Prop
  vertex_mem_iff_vertexRel x : x ∈ vertexSet ↔ vertexRel x x -- possibly omit?
  vertexRel_symm x y : vertexRel x y → vertexRel y x
  vertexRel_trans x y z : vertexRel x y → vertexRel y z → vertexRel x z
  edgeSet : Set β -- possibly omit?
  edgeRel : β → β → Prop
  edge_mem_iff_edgeRel e : e ∈ edgeSet ↔ edgeRel e e -- possibly omit?
  edgeRel_symm e₁ e₂ : edgeRel e₁ e₂ → edgeRel e₂ e₁
  edgeRel_trans e₁ e₂ e₃ : edgeRel e₁ e₂ → edgeRel e₂ e₃ → edgeRel e₁ e₃
  IsLink : β → α → α → Prop
  isLink_symm e x y : IsLink e x y → IsLink e y x
  isLink_resp_vertex e x y y' : IsLink e x y → vertexRel y y' → IsLink e x y'
  isLink_resp_edge e₁ e₂ x y : IsLink e₁ x y → edgeRel e₁ e₂ → IsLink e₂ x y
  rel_of_isLink e x y z w : IsLink e x y → IsLink e z w → vertexRel x z ∧ vertexRel y w
  left_mem_of_isLink e x y : IsLink e x y → vertexRel x x
  edge_mem_iff_exists_isLink e : e ∈ edgeSet ↔ ∃ x y, IsLink e x y -- possibly omit?


variable {α β : Type*}

def Graph'.deleteVertex (G : Graph' α β) (v : α) : Graph' α β where
  vertexSet := {x ∈ G.vertexSet | ¬G.vertexRel x v}
  vertexRel x y := G.vertexRel x y ∧ ¬G.vertexRel x v ∧ ¬G.vertexRel y v
  vertex_mem_iff_vertexRel x := by
    by_cases h : G.vertexRel x v <;> simp [h, G.vertex_mem_iff_vertexRel]
  vertexRel_symm x y := by
    by_cases h_x : G.vertexRel x v <;> by_cases h_y : G.vertexRel y v <;>
    simp only [h_x, not_false_eq_true, h_y, not_true_eq_false, and_false, and_true, imp_self]
    exact G.vertexRel_symm x y -- not picking it up in `simp`?
  vertexRel_trans x y z := by
    by_cases h_x : G.vertexRel x v <;> by_cases h_y : G.vertexRel y v <;>
      by_cases h_z : G.vertexRel z v <;> simp only [h_x, not_false_eq_true, h_y, not_true_eq_false,
        and_false, h_z, and_true, and_self, IsEmpty.forall_iff, implies_true]
    exact G.vertexRel_trans x y z -- not picking it up in `simp`?
  edgeSet := {e ∈ G.edgeSet | ¬∃ x y, G.IsLink e x y ∧ (G.vertexRel x v ∨ G.vertexRel y v)}
  edgeRel e₁ e₂ := G.edgeRel e₁ e₂ ∧
    (¬∃ x y, G.IsLink e₁ x y ∧ (G.vertexRel x v ∨ G.vertexRel y v)) ∧
    (¬∃ x y, G.IsLink e₂ x y ∧ (G.vertexRel x v ∨ G.vertexRel y v))
  edge_mem_iff_edgeRel e := by
    simp only [not_exists, not_and, not_or, Set.mem_setOf_eq, and_self, and_congr_left_iff]
    intro hxy
    by_cases h : ∃ x y, G.IsLink e x y ∧ (G.vertexRel x v ∨ G.vertexRel y v)
    · simp [G.edge_mem_iff_edgeRel]
    · simp [G.edge_mem_iff_edgeRel]
  edgeRel_symm e₁ e₂ := by
    by_cases h₁ : ∃ x y, G.IsLink e₁ x y ∧ (G.vertexRel x v ∨ G.vertexRel y v)
    · by_cases h₂ : ∃ x y, G.IsLink e₂ x y ∧ (G.vertexRel x v ∨ G.vertexRel y v)
      · simp [h₁, h₂]
      · simp [h₁, h₂]
    · by_cases h₂ : ∃ x y, G.IsLink e₂ x y ∧ (G.vertexRel x v ∨ G.vertexRel y v)
      · simp [h₁, h₂]
      · simp only [h₁, not_false_eq_true, h₂, and_self, and_true]
        exact G.edgeRel_symm _ _ -- not picking it up in `simp`?
  edgeRel_trans e₁ e₂ e₃ := by
    by_cases h₁ : ∃ x y, G.IsLink e₁ x y ∧ (G.vertexRel x v ∨ G.vertexRel y v)
    · by_cases h₂ : ∃ x y, G.IsLink e₂ x y ∧ (G.vertexRel x v ∨ G.vertexRel y v)
      · by_cases h₃ : ∃ x y, G.IsLink e₃ x y ∧ (G.vertexRel x v ∨ G.vertexRel y v)
        · simp [h₁, h₂, h₃]
        · simp [h₁, h₂, h₃]
      · by_cases h₃ : ∃ x y, G.IsLink e₃ x y ∧ (G.vertexRel x v ∨ G.vertexRel y v)
        · simp [h₁, h₂, h₃]
        · simp [h₁, h₂, h₃]
    · by_cases h₂ : ∃ x y, G.IsLink e₂ x y ∧ (G.vertexRel x v ∨ G.vertexRel y v)
      · by_cases h₃ : ∃ x y, G.IsLink e₃ x y ∧ (G.vertexRel x v ∨ G.vertexRel y v)
        · simp [h₁, h₂, h₃]
        · simp [h₁, h₂, h₃]
      · by_cases h₃ : ∃ x y, G.IsLink e₃ x y ∧ (G.vertexRel x v ∨ G.vertexRel y v)
        · simp [h₁, h₂, h₃]
        · simp only [h₁, not_false_eq_true, h₂, h₃, and_self, and_true]
          exact G.edgeRel_trans _ _ _
  IsLink e x y := G.IsLink e x y ∧ ¬G.vertexRel x v ∧ ¬G.vertexRel y v
  isLink_symm e x y := by
    by_cases h_x : G.vertexRel x v <;> by_cases h_y : G.vertexRel y v <;>
    simp only [h_x, not_false_eq_true, h_y, not_true_eq_false, and_false, and_true,
      IsEmpty.forall_iff]
    exact G.isLink_symm e x y
  isLink_resp_vertex e x y y' := by
    by_cases h_x : G.vertexRel x v <;> by_cases h_y : G.vertexRel y v <;>
    by_cases h_y' : G.vertexRel y' v <;>
    simp only [h_x, not_false_eq_true, h_y, not_true_eq_false, and_false, h_y',
              and_true, IsEmpty.forall_iff, implies_true, and_self]
    exact G.isLink_resp_vertex e x y y'
  isLink_resp_edge e₁ e₂ x y := by
    by_cases h_e₁ : ∃ a b, G.IsLink e₁ a b ∧ (G.vertexRel a v ∨ G.vertexRel b v) <;>
    by_cases h_e₂ : ∃ a b, G.IsLink e₂ a b ∧ (G.vertexRel a v ∨ G.vertexRel b v) <;>
    by_cases h_x : G.vertexRel x v <;> by_cases h_y : G.vertexRel y v <;>
    simp only [h_e₁, not_false_eq_true, h_e₂, h_x, not_true_eq_false, and_false,
              h_y, and_true, IsEmpty.forall_iff, implies_true, and_self]
    exact G.isLink_resp_edge e₁ e₂ x y
  rel_of_isLink e x y z w := by
    by_cases h_x : G.vertexRel x v <;> by_cases h_y : G.vertexRel y v <;>
    by_cases h_z : G.vertexRel z v <;> by_cases h_w : G.vertexRel w v <;>
    simp only [h_x, not_false_eq_true, h_y, not_true_eq_false, and_false,
              h_z, h_w, and_true, IsEmpty.forall_iff, implies_true, and_self]
    intro h1 h2
    exact G.rel_of_isLink e x y z w h1 h2
  left_mem_of_isLink e x y := by
    by_cases h_x : G.vertexRel x v <;> by_cases h_y : G.vertexRel y v <;>
    simp only [h_x, not_false_eq_true, h_y, not_true_eq_false, and_false, and_true,
      IsEmpty.forall_iff, and_self]
    intro h1
    exact G.left_mem_of_isLink e x y h1
  edge_mem_iff_exists_isLink e := by
    simp only [Set.mem_setOf_eq]
    constructor
    · intro ⟨h1, h2⟩
      obtain ⟨x, y, hxy⟩ := (G.edge_mem_iff_exists_isLink e).mp h1
      use x, y
      constructor
      · exact hxy
      · push_neg at h2
        exact h2 x y hxy
    · intro ⟨x, y, hxy, h_not_v⟩
      constructor
      · exact (G.edge_mem_iff_exists_isLink e).mpr ⟨x, y, hxy⟩
      · intro ⟨a, b, hab, hv⟩
        cases' hv with ha hb
        · have : G.vertexRel x a := (G.rel_of_isLink e x y a b hxy hab).1
          have : G.vertexRel x v := G.vertexRel_trans x a v this ha
          exact h_not_v.1 this
        · have : G.vertexRel y b := (G.rel_of_isLink e x y a b hxy hab).2
          have : G.vertexRel y v := G.vertexRel_trans y b v this hb
          exact h_not_v.2 this

[Alex Kontorovich]

edge deletion is even easier

def Graph'.deleteEdge (G : Graph' α β) (e : β) : Graph' α β where
  vertexSet := G.vertexSet
  vertexRel := G.vertexRel
  vertex_mem_iff_vertexRel := G.vertex_mem_iff_vertexRel
  vertexRel_symm := G.vertexRel_symm
  vertexRel_trans := G.vertexRel_trans
  edgeSet := {e' ∈ G.edgeSet | ¬G.edgeRel e' e}
  edgeRel e₁ e₂ := G.edgeRel e₁ e₂ ∧ ¬G.edgeRel e₁ e ∧ ¬G.edgeRel e₂ e
  edge_mem_iff_edgeRel e₁ := by
    by_cases h : G.edgeRel e₁ e
    · simp [h, G.edge_mem_iff_edgeRel]
    · simp [h, G.edge_mem_iff_edgeRel]
  edgeRel_symm e₁ e₂ := fun ⟨h1, h2, h3⟩ ↦ ⟨G.edgeRel_symm e₁ e₂ h1, h3, h2⟩
  edgeRel_trans e₁ e₂ e₃ := fun ⟨h1, h2, h3⟩ ⟨h4, h5, h6⟩ ↦
    ⟨G.edgeRel_trans e₁ e₂ e₃ h1 h4, h2, h6⟩
  IsLink := fun e' x y => G.IsLink e' x y ∧ ¬G.edgeRel e' e
  isLink_symm e' x y := fun ⟨h1, h2⟩ ↦ ⟨G.isLink_symm e' x y h1, h2⟩
  isLink_resp_vertex e' x y y' := fun ⟨h1, h2⟩ h3 ↦ ⟨G.isLink_resp_vertex e' x y y' h1 h3, h2⟩
  isLink_resp_edge e₁ e₂ x y := fun ⟨h1, h2⟩ ⟨h3, h4, h5⟩ ↦ ⟨G.isLink_resp_edge e₁ e₂ x y h1 h3, h5⟩
  rel_of_isLink e' x y z w := fun ⟨h1, _⟩ ⟨h2, _⟩ ↦ G.rel_of_isLink e' x y z w h1 h2
  left_mem_of_isLink e' x y := fun ⟨h1, _⟩ ↦ G.left_mem_of_isLink e' x y h1
  edge_mem_iff_exists_isLink e' := by
    by_cases h : G.edgeRel e' e
    · simp [h, G.edge_mem_iff_exists_isLink]
    · simp [h, G.edge_mem_iff_exists_isLink]

Now for the "real" test, edge contraction...

[Alex Kontorovich]

that's enough for tonight, off to bed, but I think (?) this will end up being doable? And in the long run, the better way to handle things??

def Graph'.contractEdge (G : Graph' α β) (e : β) : Graph' α β where
  vertexSet := G.vertexSet
  vertexRel x y := G.vertexRel x y ∨
    (∃ u v, G.IsLink e u v ∧
      ((G.vertexRel x u ∧ G.vertexRel y v) ∨ (G.vertexRel x v ∧ G.vertexRel y u)))
  vertex_mem_iff_vertexRel x := by
    simp only [G.vertex_mem_iff_vertexRel]
    constructor
    · intro h
      left
      exact h
    · intro h
      cases' h with h1 h2
      · exact h1
      · obtain ⟨u, v, hlink, hrel⟩ := h2
        cases' hrel with h_case h_case
        · exact G.vertexRel_trans x u x h_case.1 (G.vertexRel_symm x u h_case.1)
        · exact G.vertexRel_trans x v x h_case.1 (G.vertexRel_symm x v h_case.1)
  vertexRel_symm x y h := by
    cases' h with h1 h2
    · left
      exact G.vertexRel_symm x y h1
    · right
      obtain ⟨u, v, hlink, hrel⟩ := h2
      use u, v, hlink
      cases' hrel with h_case h_case
      · right
        exact ⟨h_case.2, h_case.1⟩
      · left
        exact ⟨h_case.2, h_case.1⟩
  vertexRel_trans x y z hxy hyz := by
    cases' hxy with hxy1 hxy2 <;> cases' hyz with hyz1 hyz2
    · left
      exact G.vertexRel_trans x y z hxy1 hyz1
    · right
      obtain ⟨u, v, hlink, hrel⟩ := hyz2
      use u, v, hlink
      cases' hrel with h_case h_case
      · left
        exact ⟨G.vertexRel_trans x y u hxy1 h_case.1, h_case.2⟩
      · right
        exact ⟨G.vertexRel_trans x y v hxy1 h_case.1, h_case.2⟩
    · right
      obtain ⟨u, v, hlink, hrel⟩ := hxy2
      use u, v, hlink
      cases' hrel with h_case h_case
      · left
        exact ⟨h_case.1, G.vertexRel_trans z y v (G.vertexRel_symm _ _ hyz1) h_case.2⟩
      · right
        exact ⟨h_case.1, G.vertexRel_trans z y u (G.vertexRel_symm _ _ hyz1) h_case.2⟩
    · obtain ⟨u₁, v₁, hlink₁, hrel₁⟩ := hxy2
      obtain ⟨u₂, v₂, hlink₂, hrel₂⟩ := hyz2
      have huv_eq : G.vertexRel u₁ u₂ ∧ G.vertexRel v₁ v₂ :=
        G.rel_of_isLink e u₁ v₁ u₂ v₂ hlink₁ hlink₂
      cases' hrel₁ with h₁ h₁ <;> cases' hrel₂ with h₂ h₂
      · right
        use u₁, v₁, hlink₁
        left
        exact ⟨h₁.1, G.vertexRel_trans z v₂ v₁ h₂.2 (G.vertexRel_symm v₁ v₂ huv_eq.2)⟩
      · left
        exact G.vertexRel_trans x u₁ z h₁.1 (G.vertexRel_trans u₁ u₂ z huv_eq.1
          (G.vertexRel_symm z u₂ h₂.2))
      · left
        exact G.vertexRel_trans x v₁ z h₁.1 (G.vertexRel_trans v₁ v₂ z huv_eq.2
          (G.vertexRel_symm z v₂ h₂.2))
      · left
        exact G.vertexRel_trans x v₁ z h₁.1 (G.vertexRel_trans v₁ v₂ z huv_eq.2
            (G.vertexRel_trans v₂ y z (G.vertexRel_symm y v₂ h₂.1) (G.vertexRel_trans y u₁ z h₁.2
                (G.vertexRel_trans u₁ u₂ z huv_eq.1 (G.vertexRel_symm z u₂ h₂.2)))))
  edgeSet := {e' ∈ G.edgeSet | ¬G.edgeRel e' e}
  edgeRel e₁ e₂ := G.edgeRel e₁ e₂ ∧ ¬G.edgeRel e₁ e ∧ ¬G.edgeRel e₂ e
  edge_mem_iff_edgeRel e₁ := by
    by_cases h : G.edgeRel e₁ e
    · simp [h, G.edge_mem_iff_edgeRel]
    · simp [h, G.edge_mem_iff_edgeRel]
  edgeRel_symm e₁ e₂ := fun ⟨h1, h2, h3⟩ ↦ ⟨G.edgeRel_symm e₁ e₂ h1, h3, h2⟩
  edgeRel_trans e₁ e₂ e₃ := fun ⟨h1, h2, h3⟩ ⟨h4, h5, h6⟩ ↦
    ⟨G.edgeRel_trans e₁ e₂ e₃ h1 h4, h2, h6⟩
  -- IsLink e' x y := G.IsLink e' x y ∧ ¬G.edgeRel e' e
  IsLink e' x y := (∃ x' y', G.IsLink e' x' y' ∧
    (G.vertexRel x x' ∨ (∃ u v, G.IsLink e u v ∧
      ((G.vertexRel x u ∧ G.vertexRel x' v) ∨ (G.vertexRel x v ∧ G.vertexRel x' u)))) ∧
    (G.vertexRel y y' ∨ (∃ u v, G.IsLink e u v ∧
      ((G.vertexRel y u ∧ G.vertexRel y' v) ∨ (G.vertexRel y v ∧ G.vertexRel y' u))))) ∧
    ¬G.edgeRel e' e
  isLink_symm e' x y := fun ⟨⟨x', y', hlink, hx, hy⟩, hedge⟩ ↦
    ⟨⟨y', x', G.isLink_symm e' x' y' hlink, hy, hx⟩, hedge⟩
  isLink_resp_vertex e' x y y' := fun ⟨⟨x', y'', hlink, hx, hy''⟩, hedge⟩ hyy' ↦
    ⟨⟨x', y'', hlink, hx, by
      cases' hyy' with hyy'_orig hyy'_contract
      · cases' hy'' with hy''_orig hy''_contract
        · left
          exact G.vertexRel_trans y' y y'' (G.vertexRel_symm y y' hyy'_orig) hy''_orig
        · right
          obtain ⟨u, v, hlink_e, hrel⟩ := hy''_contract
          use u, v, hlink_e
          cases' hrel with h_case h_case
          · left
            exact ⟨G.vertexRel_trans y' y u (G.vertexRel_symm y y' hyy'_orig) h_case.1, h_case.2⟩
          · right
            exact ⟨G.vertexRel_trans y' y v (G.vertexRel_symm y y' hyy'_orig) h_case.1, h_case.2⟩
      · cases' hy'' with hy''_orig hy''_contract
        · right
          obtain ⟨u, v, hlink_e, hrel⟩ := hyy'_contract
          use u, v, hlink_e
          cases' hrel with h_case h_case
          · right
            exact ⟨h_case.2, G.vertexRel_trans y'' y u (G.vertexRel_symm y y'' hy''_orig) h_case.1⟩
          · left
            exact ⟨h_case.2, G.vertexRel_trans y'' y v (G.vertexRel_symm y y'' hy''_orig) h_case.1⟩
        · obtain ⟨u₁, v₁, hlink₁, hrel₁⟩ := hyy'_contract
          obtain ⟨u₂, v₂, hlink₂, hrel₂⟩ := hy''_contract
          have huv_eq : G.vertexRel u₁ u₂ ∧ G.vertexRel v₁ v₂ :=
            G.rel_of_isLink e u₁ v₁ u₂ v₂ hlink₁ hlink₂
          cases' hrel₁ with h₁ h₁ <;> cases' hrel₂ with h₂ h₂
          ·  sorry

[Alex Kontorovich]

Idea: I’m trying to do too much at once; in a general (not necessarily simple) graph, when you contract two vertices, you don’t have to remove the edge between them, you can leave it as a loop. (And then later if you like, remove that edge, since we already have edge deletion.) I’ll come back to this tomorrow (have to go to bed; teaching middle schoolers Euclidean geometry in the morning…)

[Philippe Duchon]

Alex Kontorovich said:

Shouldn't rel_of_isLink be:

rel_of_isLink e x y z w : IsLink e x y → IsLink e z w → vertexRel x z ∧ vertexRel y w

? So if e represents an edge from x to y and also from z to w, then x had better be in the same vertex class as z and same with y and w, no?

The graph is undirected, so IsLink e x y means e is an edge between x and y and IsLink e z w means e is an edge between z and w, but that only means x must be the same vertex as z or w (with the other relation for y, which you get from the other axioms).

[Mario Carneiro]

Note that in my version, the PER thing was happening only for vertices, not for edges. (You have introduced a PER on edges using edgeRel.) Quotienting edge names is much less useful, because there is no operation of edge name contraction where you take two edges and make them have the same name, because this produces a 4-ended edge.

[Mario Carneiro]

I think the only case of edge name quotienting that makes sense is if all of the edges quotiented are parallel

[Alex Kontorovich]

Yes that’s what I had in mind, that if you have multiple parallel edges, you might want to fuse some (but not others) into one, and then you’re struggling to make a “cannonical” choice unless you also have a relation on edges, no?

[Peter Nelson]

This would allow for contraction to work in the setting of simple graphs, as well as a canonical notion of simplification.

[Peter Nelson]

On the other hand, definitions containing data now needs to respect both the edge and vertex relations.

[Peter Nelson]

Maybe this object is a Pregraph, and a Graph is a pregraph with uniquely named vertices and edges?

[Alex Kontorovich]

Interesting. I was also thinking that it could work well to have a Simplification process that takes a Pregraph and transforms it into a Pregraph satisfying Pregraph.IsSimple by removing any loop edges and identifies any parallel edges. This just might work, no?

[Mario Carneiro]

isn't that just the quotient?

[Mario Carneiro]

certainly the quotient map from Pregraph to Graph is of central importance here and you would want a good API for it

[Mario Carneiro]

actually maybe you are talking about mapping a Graph to a SimpleGraph. That also works (it doesn't need to have an IsSimple input because of that complete lattice structure I mentioned earlier)

[Alex Kontorovich]

I asked my local graph theorist friend (Swee Hong Chan) if there would be a natural application for "edge relations" similar to vertices in what we now seem to be calling a Pregraph; he said yes. So shall I proceed with developing this notion, and its API? I think it'll be the easiest way to define graph minors, and API taking Pregraphs to Graphs (and the latter to SimpleGraphs) should make it possible to do graph theory nicely? What do you all think?

[Alex Kontorovich]

PS He said that what we call Graphs would elsewhere be called Multigraphs... I guess you can't please all..?

[Philippe Duchon]

Alex Kontorovich said:

PS He said that what we call Graphs would elsewhere be called Multigraphs... I guess you can't please all..?

Terminology in graph theory is really variable; between the variants in the definition of a graph (directed or undirected, simple or multigraph, with or without loops) and the variants in what should be called a path/walk/cycle, it's really a mess.

I wouldn't worry about pleasing all, but it would really be nice to have all variants available even if it means people have to call their favorite variant by a different name.

Right now I think Mathlib defines walks and paths only for simple (loopless, undirected) graphs (SimpleGraph); adding the corresponding definitions and theorems for similar notions in simple directed graphs (loops allowed; Digraph) would probably not be difficult but would result in a lot of duplication.

And that's not even taking important notions like minors into account...

[Jun Kwon]

Hi, I am Jun Kwon, a PhD student of Peter Nelson (@Peter Nelson). I would like to revive this thread and ask for some advice on the definition of a graph (multigraph).

Here, α (or Set α) will be the type of vertices, and β will be the type of edges. Also, "graph" will mean "multigraph" here.

First, we should ask what makes a definition of a graph good. I suggest that a good definition of a mathematical object is one that facilitates the fundamental operations on the object. In the case of graphs, that means removing and adding vertices and edges, and contracting edges; or equivalently, taking subgraphs, induced subgraphs, and minors.

Similar to the definition of a matroid, deletion of elements is a fundamental operation on graphs (e.g., induced subgraphs). To facilitate this operation, Peter defined matroids such that the structure contains the ground set field. Using this, M \ e does not have type Matroid { f // f ≠ e } but simply Matroid β with e removed from the ground set. In effect, the type Matroid β contains not only the matroids on β, but also all possible submatroids.

However, contraction of edges in graphs comes with an added complexity: what should the new supervertex be labelled with? For example, if an edge e : β between u, v : α is contracted, how can we deterministically provide a new label for the vertex created by identifying u and v? From here, I will talk about vertex identification rather than contraction as edge contraction can be done by identifying the ends of edges and removing the edges afterwards.

There are many different answers to this. One approach we tried is to ask the user to decide by providing a function f such that f u = f v and labelling the supervertex as f u. However, this is not great at facilitating contraction: if you perform ten edge contractions, you will have to create and remember ten different functions just to keep track of where each vertex was merged.

Mario has suggested a PERGraph.

PERGraph

import Mathlib.Tactic

structure PERGraph (α β : Type*) where

  /-- The partial equivalence relation on the vertex set.

  If `vertexRel a b`, then `a` and `b` represent the same vertex. -/

  vertexRel : α → α → Prop

  vertexRel_symm : vertexRel a b → vertexRel b a

  vertexRel_trans : vertexRel a b → vertexRel b c → vertexRel a c

  IsLink : β → α → α → Prop

  isLink_symm : IsLink e a b → IsLink e b a

  isLink_resp : IsLink e a b → vertexRel b b' → IsLink e a b'

  rel_of_isLink : IsLink e x y → IsLink e v w → vertexRel x v ∨ vertexRel x w

  left_mem_of_isLink : IsLink e x y → vertexRel x x

Here, vertexRel is a partial equivalence relation (PER) on α, and related vertices represent the same vertex. With this definition, vertices can be identified by changing the PER on α like the example below.

def VxIdentify (G : PERGraph α β) (S : Set α) : PERGraph α β where

  vertexRel u v := vertexRel u v ∨ (u ∈ S ∧ v ∈ S)

  IsLink e u v := ∃ x y, (u = x ∨ u ∈ S ∧ x ∈ S) ∧ (v = y ∨ v ∈ S ∧ y ∈ S) ∧ G.IsLink e x y

  ...

However, this comes with some downsides.

Previously, since every object in α represented a unique vertex (or was not in the ground set), with some bijection fudging in our heads, you could imagine that u IS the vertex.

However, with this setup, u : α no longer uniquely represents a vertex, so the label u and the vertex represented by u are mathematically different objects. This is a mental overhead that does not exist in the usual graph theory.

Furthermore, having to control what happens to the vertices indirectly via the labels is not great. For example, given S : Set α, I would like to find δ(S), the edge cut of S, the set of edges with exactly one end in S. Previously, it can be defined as {e | ∃ u v, u ∈ S ∧ v ∉ S ∧ G.IsLink e u v} (the set of edges between two vertices, one in S and another outside S). With this setup, it would have to be {e | ∃ u v, u ∈ S ∧ (v ∉ S ∧ ∀ w ∈ S, ¬ vertexRel v w) ∧ G.IsLink e u v} (the set of edges between two vertices, one in S and another not only outside S but also not vertex-related to any vertex in S). Also, every time we define a new property/function on graphs, we have to prove a lemma that the outputs agree when rewriting a label with a vertex-related one. These are problems that arise repeatedly, even in parts of the API that have nothing to do with contraction/identification. I am not saying it can't be done, but these are added complexities that do not exist in the usual graph theory.

I would like to step back and talk about what exactly is needed to facilitate edge contraction. First, we should be able to do contraction in type, i.e., the type of the input graph and the output graph should be the same. Without this, a minor graph would have a vertex type that is a subtype of a quotient of the original vertex type. Then, showing that a minor relation is transitive requires that a subtype of a quotient of a subtype of a quotient has an Equiv with a subtype of a quotient. The fact that the minor relation is transitive is a very trivial lemma in graph theory, yet, without in-type contraction, I do not know a way to prove it without spending a lot of time.

Semantically, this means that Graph α β contains not only graphs with those vertices and edges, but also all possible deletions and contractions of them. For that, we need some relabelling function f returning values in α to determine how the new vertices are labelled. The question is: when should f be provided?

To the best of my knowledge, there are three different answers to this question: when contracting, when the graph is created, and when α is created. The first answer, when contracting, leads to my original solution of asking the user to provide a function every single time they want to contract an edge. It looks like this:

Old graph definition (requires function for every contraction)

structure Graph (α β : Type*) where

  /-- The vertex set. -/

  vertexSet : Set α

  /-- The binary incidence predicate, stating that `x` and `y` are the ends of an edge `e`.

  If `G.IsLink e x y` then we refer to `e` as an `edge` and `x` and `y` as the `left` and `right`. -/

  IsLink : β → α → α → Prop

  /-- The edge set. -/

  edgeSet : Set β := {e | ∃ x y, IsLink e x y}

  /-- If `e` goes from `x` to `y`, it goes from `y` to `x`. -/

  isLink_symm : ∀ ⦃e⦄, e ∈ edgeSet → (Symmetric <| IsLink e)

  /-- An edge is incident with at most one pair of vertices. -/

  eq_or_eq_of_isLink_of_isLink : ∀ ⦃e x y v w⦄, IsLink e x y → IsLink e v w → x = v ∨ x = w

  /-- An edge `e` is incident to something if and only if `e` is in the edge set. -/

  edge_mem_iff_exists_isLink : ∀ e, e ∈ edgeSet ↔ ∃ x y, IsLink e x y := by exact fun _ ↦ Iff.rfl

  /-- If some edge `e` is incident to `x`, then `x ∈ V`. -/

  left_mem_of_isLink : ∀ ⦃e x y⦄, IsLink e x y → x ∈ vertexSet

def VxIdentify (G : Graph α β) (f : α → α) : Graph α β where

  vertexSet := f '' G.vertexSet

  IsLink e x y := ∃ x' y', G.IsLink e x' y' ∧ x = f x' ∧ y = f y'

  ...

/-- This is a valid contraction iff `f` sends exactly the vertices connected by edges in `C` to the same place. -/

def contract (G : Graph α β) (f : α → α) (C : Set β) :=

  (VxIdentify G f).edgeDelete C

As mentioned before, this would require the user to create and remember a function for every single contraction. Also, for any sane use case, the user would further need to prove that the function is aligned with the edge set. That is, the vertices that are mapped to the same vertex by f are exactly the vertices connected by edges in C.

The second option is to attach the function to the graph as a structure field. This allows the contraction to be performed without supplying a function every single time. However, it would need to be supplied whenever you create a graph. When augmenting a graph, there is a solution of simply retaining the function, but creating a graph from nothing would be harder. Also, two graphs would not be the same if they have different functions attached to them, even though they are the same graphically.

[Jun Kwon]

The last option is to attach the function to α. This enforces one choice of function for all graphs defined on α. This is currently my favourite option.

Graph with Set α

import Mathlib.Order.SupIndep

structure Partition (α : Type*) [CompleteLattice α] where

  parts : Set α

  indep : sSupIndep parts

  bot_not_mem : ⊥ ∉ parts

def Partition.supp {α} [CompleteLattice α] (P : Partition α) := sSup P.parts

def Partition.flatten {α} [CompleteLattice α] (Q : Partition (Set α)) {P : Partition α}

    (hQ : Q.supp = P.parts) : Partition α where

  parts := sSup '' Q.parts

  ...

structure Graph (α β : Type*) where

  vertexPartition : Partition (Set α)

  /-- The vertex set. Note that each vertex has type `Set α` rather than `α`. -/

  vertexSet : Set (Set α) := vertexPartition.parts

  /-- The vertex set is equal to the parts of the vertex partition. -/

  vertexSet_eq_parts : vertexPartition.parts = vertexSet := by rfl

  /-- The binary incidence predicate, stating that `x` and `y` are the ends of an edge `e`.

  If `G.IsLink e x y` then we refer to `e` as `edge` and `x` and `y` as `left` and `right`. -/

  IsLink : β → Set α → Set α → Prop

  /-- The edge set. -/

  edgeSet : Set β := {e | ∃ x y, IsLink e x y}

  /-- If `e` goes from `x` to `y`, it goes from `y` to `x`. -/

  isLink_symm : ∀ ⦃e⦄, e ∈ edgeSet → (Symmetric <| IsLink e)

  /-- An edge is incident with at most one pair of vertices. -/

  eq_or_eq_of_isLink_of_isLink : ∀ ⦃e x y v w⦄, IsLink e x y → IsLink e v w → x = v ∨ x = w

  /-- An edge `e` is incident to something if and only if `e` is in the edge set. -/

  edge_mem_iff_exists_isLink : ∀ e, e ∈ edgeSet ↔ ∃ x y, IsLink e x y := by exact fun _ ↦ Iff.rfl

  /-- If some edge `e` is incident to `x`, then `x ∈ V`. -/

  left_mem_of_isLink : ∀ ⦃e x y⦄, IsLink e x y → x ∈ vertexSet

def VxIdentify {α β} (G : Graph α β) (P : Partition (Set (Set α))) (hP : P.supp = G.vertexSet) : Graph α β where

  vertexPartition := P.flatten (G.vertexSet_eq_parts ▸ hP)

  IsLink e x y := ∃ x' y', G.IsLink e x' y' ∧ x' ⊆ x ∧ y' ⊆ y

  ...

/-- Connected components as a partition of the set of vertices. -/

def connPartition (G : Graph α β) : Partition (Set (Set α)) := sorry

lemma supp_connPartition (G : Graph α β) : (connPartition G).supp = G.vertexSet := sorry

/-- Restrict the edge set to a subset. -/

def edgeRestrict (G : Graph α β) (E : Set β) : Graph α β where

  vertexPartition := G.vertexPartition

  vertexSet := G.vertexSet

  edgeSet := G.edgeSet ∩ E

  IsLink e u v := G.IsLink e u v ∧ e ∈ E

  ...

def contract (G : Graph α β) (C : Set β) : Graph α β :=

  edgeRestrict (VxIdentify G (connPartition (edgeRestrict G C)) (supp_connPartition G)) (G.edgeSet \ C)

The glaring issue with my claim that these three are the only options is: where does PERGraph belong? My answer is α... with an asterisk. PERGraph is very close mechanically to the second option, as it attaches some extra information in the structure field. However, it comes with a relation, not a function, and unfortunately breaks label uniqueness. Actually, the way it facilitates contraction is very close to the last option. As the name suggests, PERGraph involves partially partitioning the elements of α into several parts where elements in the same part represent the same vertex. A very simple transformation that solves the uniqueness problem is to imagine each part represents a vertex rather than the individual labels in it. The type for the vertices is now Set α, sure, but it is exactly the same thing as PERGraph without the uniqueness problem. Through this lens, we notice that PERGraph is equivalent to a graph with Set α as its vertex type, which naturally comes with a union/sUnion function: with ℕ as the vertex type, identifying vertices 1 and 2 as vertex-related is equivalent to merging {1} and {2} by relabelling them as {1} ∪ {2} = {1, 2}.

I am fairly sure that the full generality of the vertex type is not just the set structure (or CompleteAtomicBooleanAlgebra α, which is order-isomorphic to the set structure). If we stick with sup as the operation, either CompleteLattice α or Order.Frame α seem sufficient, as CompleteLattice α is required for Partition α but Order.Frame α is required for CompleteLattice (Partition α), which could be handy.

Graph with CompleteLattice α assumption

import Mathlib.Order.SupIndep

structure Partition (α : Type*) [CompleteLattice α] where

  parts : Set α

  indep : sSupIndep parts

  bot_not_mem : ⊥ ∉ parts

structure Graph (α β : Type*) [CompleteLattice α] where

  vertexPartition : Partition α

  /-- The vertex set. -/

  vertexSet : Set α := vertexPartition.parts

  /-- The vertex set is equal to the parts of the vertex partition. -/

  vertexSet_eq_parts : vertexPartition.parts = vertexSet := by rfl

  /-- The binary incidence predicate, stating that `x` and `y` are the ends of an edge `e`.

  If `G.IsLink e x y` then we refer to `e` as `edge` and `x` and `y` as `left` and `right`. -/

  IsLink : β → α → α → Prop

  /-- The edge set. -/

  edgeSet : Set β := {e | ∃ x y, IsLink e x y}

  /-- If `e` goes from `x` to `y`, it goes from `y` to `x`. -/

  isLink_symm : ∀ ⦃e⦄, e ∈ edgeSet → (Symmetric <| IsLink e)

  /-- An edge is incident with at most one pair of vertices. -/

  eq_or_eq_of_isLink_of_isLink : ∀ ⦃e x y v w⦄, IsLink e x y → IsLink e v w → x = v ∨ x = w

  /-- An edge `e` is incident to something if and only if `e` is in the edge set. -/

  edge_mem_iff_exists_isLink : ∀ e, e ∈ edgeSet ↔ ∃ x y, IsLink e x y := by exact fun _ ↦ Iff.rfl

  /-- If some edge `e` is incident to `x`, then `x ∈ V`. -/

  left_mem_of_isLink : ∀ ⦃e x y⦄, IsLink e x y → x ∈ vertexSet

Of course, you could go further and create a bespoke class that contains the operation and the exact axioms we need for contraction—something like the following:

Graph with bespoke class

import Mathlib.Order.SupIndep

class contractFun (α : Type*) where

  f : Set α → α

  /-- This is not strictly necessary for identification, but this is required for the property

    `G / (C ∪ D) = G / C / D`. -/

  partialEval : ∀ S T : Set α, S ⊆ T → f T = f (T \ S ∪ {f S})

  singleton : ∀ a : α, f {a} = a

variable {α β : Type*} [contractFun α]

structure Graph (α β : Type*) [contractFun α] where

  vertexSet : Set α

  /-- When identifying vertices, the new label should not clash with other labels. -/

  contractable : ∀ S T : Set α, S ⊆ vertexSet → T ⊆ vertexSet → Disjoint S T → contractFun.f S ≠ contractFun.f T

  IsLink : β → α → α → Prop

  edgeSet : Set β := {e | ∃ x y, IsLink e x y}

  isLink_symm : ∀ ⦃e⦄, e ∈ edgeSet → (Symmetric <| IsLink e)

  eq_or_eq_of_isLink_of_isLink : ∀ ⦃e x y v w⦄, IsLink e x y → IsLink e v w → x = v ∨ x = w

  edge_mem_iff_exists_isLink : ∀ e, e ∈ edgeSet ↔ ∃ x y, IsLink e x y := by exact fun _ ↦ Iff.rfl

  left_mem_of_isLink : ∀ ⦃e x y⦄, IsLink e x y → x ∈ vertexSet

structure Partition (α : Type*) [CompleteLattice α] where

  parts : Set α

  indep : sSupIndep parts

  bot_not_mem : ⊥ ∉ parts

def Partition.supp {α} [CompleteLattice α] (P : Partition α) := sSup P.parts

def VxIdentify (G : Graph α β) (P : Partition (Set α)) (hP : P.supp = G.vertexSet) : Graph α β where

  vertexPartition := {parts := f '' P.parts, ...}

  IsLink e x y := ∃ x' y', G.IsLink e x' y' ∧ x' ≤ x ∧ y' ≤ y

  ...

/-- Connected components as a partition of the set of vertices. -/

def connPartition (G : Graph α β) : Partition (Set α) := sorry

lemma supp_connPartition (G : Graph α β) : (connPartition G).supp = G.vertexSet := sorry

/-- Restrict the edge set to a subset. -/

def edgeRestrict (G : Graph α β) (E : Set β) : Graph α β where

  vertexSet := G.vertexSet

  edgeSet := G.edgeSet ∩ E

  IsLink e u v := G.IsLink e u v ∧ e ∈ E

  ...

def contract (G : Graph α β) (C : Set β) : Graph α β :=

  edgeRestrict (VxIdentify G (connPartition (edgeRestrict G C)) (supp_connPartition G)) (G.edgeSet \ C)

My worry is something like this happening:\

Graph theorist: Oh, I heard Lean is cool! Let me try doing some graph theory with it!\

Lean: Okay, do you want to create a graph?\

Graph theorist: Yes!\

Lean: Sure, just give me a proof that your vertex type is a CompleteLattice.\

Graph theorist: ?????

However, I do not have a better idea than requiring the vertex type to be either Set α or requiring an instance of CompleteLattice α. If you have a suggestion, please let me know. I would very much appreciate it.

[Alex Kontorovich]

Whatever definition you decide to go with, you can test it on defining graph minors -- how will you handle edge contraction? (That was my "white whale" for the few moments I spent thinking about this, trying to state Hadwiger's conjecture...) Try to get some good API and you'll see what works or doesn't...