What kind of graphs are in Mathlib already?

Stream: graph theory

[Pieter Cuijpers]

Hi, I'm trying to figure out which types of graphs are defined already in Mathlib and where to find them, and which ones are not.

So far, I've seen SimpleGraph, Digraph, and Quiver. These give rise to two questions.

1) In the first two definitions, I would have expected that SimpleGraph would extend Digraph, and that things like walk would be defined on Digraph, but that seems not to be the case. Is this just a matter of did not happen yet or is there a rationale behind that? And how does this community go about refactoring efforts - if it is indeed a matter of did not happen yet?

2) The definition of Quiver is the next step up from Digraph and generalizes Prop to sort as a way of generating different edges between vertices. I understand that this is helpful as a step towards defining Category later, but in some of the graph theoretic work that I encounter considering a MultiGraph (I think it would be called) as:

class MultiGraph (Vertex : Type*) (Edge: Type*) where
   source : Edge -> Vertex
   destination : Edge -> Vertex

seems helpful, in that it seems a lot easier to me when I want to consider all the edges in the graph at the same time. When I use Quiver I always have to first identify the source and destination explicitly, which is sometimes cumbersome. Does that definition (or similar) exist under a different name perhaps? Is there a reason not to have it? And if not to both, should I try setting up a PR for it?

[Rida Hamadani]

Regarding part (1), it is a case of "nobody did it yet". It shouldn't be too hard, feel free to do it!

[Rida Hamadani]

Actually "nobody did it" is technically wrong, @Jeremy Tan did it here #16018, but that PR got closed and nobody worked on it after that.

Digraphs are relatively recent compared to simple graphs, and that part is still lacking, I wanted to port parts of simple graph to digraphs but got too busy with other things, I would be happy to help if somebody else starts working on it.

I think this is worth it because there are a lot of important results on, for instance, tournaments, directed SRGs, flow networks, etc and this part of the library can be the foundation for formalizing them.

[Rida Hamadani]

cc. @Peter Nelson regarding point (2).

[Kyle Miller]

With 1, it's that it's not necessarily useful to have it literally extend Digraph. If you're thinking about this in terms of object-oriented programming and subtyping, Lean doesn't work the same way. You wouldn't be able to pass a SimpleGraph to a function expecting a Digraph, except in special cases (via dot notation), and you can't use dot notation to make Digraph functions that operate on SimpleGraphs that return SimpleGraphs.

#4127 has a class-based approach to unify the API, but as you can see it's quite an old PR. I think I have a branch somewhere with a more updated version, but it might be on my desktop computer...

[Pieter Cuijpers]

@Kyle Miller I do get that the subtyping doesn't work in exactly the same way, but if the notion of 'walk' was defined on Digraphs, it would automatically be defined on SimpleGraphs, so it would prevent duplication of code - right?

The tricky part, I think, that in some cases the concepts may generalize, but the proofs would go via a different route. Worse, the formulation of the concepts may be different. For example my question on Multigraphs vs Quivers is an example of that. The two definitions may - up to some details - be equivalent (up to some type-theoretic differences), but the proofs of some theorems will be awkward on one, while going smoothly on the other, and vice versa. In such a situation, people may prefer one basic definition over another, and there is no clear decision anymore on how the inheritance should go.

[Pieter Cuijpers]

Rida Hamadani said:

Actually "nobody did it" is technically wrong, Jeremy Tan did it here #16018, but that PR got closed and nobody worked on it after that.

Digraphs are relatively recent compared to simple graphs, and that part is still lacking, I wanted to port parts of simple graph to digraphs but got too busy with other things, I would be happy to help if somebody else starts working on it.

I think this is worth it because there are a lot of important results on, for instance, tournaments, directed SRGs, flow networks, etc and this part of the library can be the foundation for formalizing them.

Hm... that is not too encouraging... hence my question "how does refactoring work" in this community? Is there a way to avoid that such an effort "fails" (if that is the right word).

[Kyle Miller]

Pieter Cuijpers said:

it would automatically be defined on SimpleGraphs, so it would prevent duplication of code - right?

No, not exactly. If G : SimpleGraph V, you can't write Digraph.Walk G u v. However, the dot notation elaboration would let you write G.Walk u v to get Digraph.Walk G.toDigraph u v.

The class system I mentioned in the PR I linked to is the way to go to get the unified interface you want (or maybe not done exactly like in the PR, but the general idea). That's how homomorphisms work in mathlib; they have similar issues, since you want, for example, a homomorphism that's both multiplicative and additive to "be" a multiplicative homomorphism and an additive homomorphism.

[Kyle Miller]

extends is a very very weak concept, and it's not worth it here I think. That's not to say that no one wants a unified interface for graphs! It's just that extends isn't the correct mechanism.

[Kyle Miller]

extends works a lot better for class than structure, since the parents each give a projection instance, and that simulates the OO-like subtyping. For graphs, what we want are classes that provide the interface for what it means to be a graph with certain kinds of features, and then definitions can make use of these classes. They would not be in terms of a concrete data type.

[Kyle Miller]

The reason I stopped pursuing #4127 is (1) I wasn't sure about some of the interface I was developing (e.g. should the vertex type of a graph type be allowed to vary with the graph? or does the graph type itself fix the vertex type? I ran into some Lean bugs here, and they might be fixed by now) and (2) I like dot notation and don't want to give it up, which the class-based system requires, and in the meantime I've been working on Lean features to preserve dot notation.

[Pieter Cuijpers]

I'm a bit lost on why extends does not work on structure, but that aside I think it is indeed the unified interface that I'm looking for, which usually is created either by extends or by an instance theorem (which is also fine with me). And both give the dot notation elaboration, which is I think quite an okay way to achieve the interface we need.

(I'm probably not enough of a programmer to use all the jargon correctly.)

[Pieter Cuijpers]

Kyle Miller said:

The reason I stopped pursuing #4127 is (1) I wasn't sure about some of the interface I was developing (e.g. should the vertex type of a graph type be allowed to vary with the graph? or does the graph type itself fix the vertex type? I ran into some Lean bugs here, and they might be fixed by now) and (2) I like dot notation and don't want to give it up, which the class-based system requires, and in the meantime I've been working on Lean features to preserve dot notation.

You have my full support on liking dot notation and prioritizing that :-)

What you mention about #4127 sounds like the decision between Multigraph as I proposed it above and Quiver as it is in the library to me, or am I mistaken? There may be value to both. And strictly speaking, a Multigraph would be a Quiver, but not necessarily the other way around?

[Pieter Cuijpers]

I may be overlooking important details here.

[Kyle Miller]

I'm a bit lost on why extends does not work on structure

I invite you to experiment here with using extends on structure. It "works", but there are some deep usability problems, because you don't get a coercion from SimpleGraph to Digraph that actually works. This is why I point out that it's not like the OO concept of extension — the OO one is how people think it will work, even if they aren't consciously thinking about it that way.

There's also a fundamental conceptual issue: a simple graph isn't a digraph. Sure, you can model a simple graph as a symmetric irreflexive relation, but that doesn't mean that there are edges going in both directions. For simplicity's sake we may as well take the perspective that simple graphs are digraphs, but I think it's worth keeping this in mind. It has a big impact on how you name functions. E.g., you want the neighbor set of a vertex, right? Is that the set of heads or tails from a given vertex?

[Kyle Miller]

What you mention about #4127 sounds like the decision between Multigraph as I proposed it above and Quiver as it is in the library to me, or am I mistaken?

It's different. With Quiver/MultiGraph, you're putting a fixed structure on a given Vertex and Edge type. With my PR, you have an actual type of graphs under consideration, and each term of that type has a graph structure.

We care about the lattice structure on SimpleGraph and Digraph for example, and we might have general theorems about it.

Multigraphs generally don't have a good lattice structure however, so your MultiGraph type could be workable. You just need to keep in mind that you should never have two graphs with the same Vertex and Edge types. (It's possible to have a Multigraph type with a lattice structure; recall that there are two definitions of a multigraph, one is that the edge set is a multiset of unordered pairs, and the other is what you have. That is, indistinguishable vs distinguishable multiedges. They're slightly different, and I think we should be able to support both.)

[Peter Nelson]

You just need to keep in mind that you should never have two graphs with the same Vertex and Edge types

I disagree on this point. For instance, I could remove an edge from multigraph, and add it back somewhere else.

[Kyle Miller]

What are you disagreeing with? I'm pointing this out as a problem with the arrangement.

[Peter Nelson]

I interpreted 'should' as a design mandate. If it's not that, I have no disagreement.

[Kyle Miller]

It's a "should" as in "class instances are supposed to be canonical, so you shouldn't violate that"

[Peter Nelson]

This goes against the design of matroids that seems to be working very well - for instance, operations like truncation, and results like the matroid intersection theorem, use different matroids on the same ground set (type).

[Peter Nelson]

Ah, the difference is the 'class' part.

[Kyle Miller]

Yes, I'm saying why the MultiGraph class from the beginning of this thread has some difficulties. It's workable, and I'm sure it's great for certain applications, but it's not necessarily what everyone would want.

[Kyle Miller]

We want a class (or a system of classees) that describes a generic Multigraph interface. Concrete implementations of multigraphs would then implement these classes, and each person can use their favorite kind of multigraph with the generic library.

[Pieter Cuijpers]

Got that, but I would be fine with making MultiGraph a structure as well. I was not aware of a cannonical "lattice of Digraphs", but it makes sense to consider it as a structure too.

[Kyle Miller]

Digraph V and SimpleGraph V have lattice structures, via edge containment

[Peter Nelson]

The plan my student and I have at the moment is something like the following:

structure Graph (α β : Type*) where
-- vertex set
  V : Set α
-- edge set
  E : Set β
-- edge-vertex incidence
  Inc : β → α → Prop
  vertex_support : ∀ e v, Inc e v → v ∈ V
  edge_support : ∀ e v, Inc e v → e ∈ E
-- extra propositional stuff, such as the fact that each edge is incident with at most two vertices.

[Peter Nelson]

This uses the 'embedded set' design that has worked well for matroids. I am growing more and more convinced that this will be the best way to formalize real-world proofs involving minors.

If contracting an edge of a graph forces passing to a new graph with a different vertex type, then any vaguely complicated 'contract an edge, apply induction'-type proof will descend to DTT hell.

[Kyle Miller]

Seems reasonable. I think this basically what's in https://link.springer.com/chapter/10.1007/3-540-58450-1_40, but with types for the elements of the V and E sets. (I can't check right now.)

[Kyle Miller]

Here's another definition I experimented with: https://github.com/leanprover-community/mathlib3/blob/3c940418e050f85795b91778aa17fdf7c354c700/src/combinatorics/multigraph/basic.lean#L58-L60

I think it might be equivalent; it uses, basically, a set of triples V x V x E that's symmetric in the first two components, rather than an Inc relation.

[Kyle Miller]

(As always, you'll have to decide how you want to define the degree of a vertex that has a loop. The topologist in me wants it to be 2, but with all these proposals the easiest answer is 1.)

[Peter Nelson]

It's 2!

[Peter Nelson]

(Provided you want a handshake theorem, at least)

[Peter Nelson]

(and nice linear algebra over Z2)

[Kyle Miller]

How do you define degree to get 2 though?

[Peter Nelson]

edit : nevermind

[Peter Nelson]

Yeah, it's annoying. Define a function f from edges to Sym2; then the degree of a vertex is obtained by the sum over e of the sum over f e of an indicator function.

[Peter Nelson]

But the rewards are obvious!

[Peter Nelson]

This might be look a bit heavy-handed, but I think it works.

structure Graph (α β : Type*) where
  V : Set α
  E : Set β
  inc : β → α →₀ ℕ
  sum_eq : ∀ e ∈ E, (inc e).sum (fun _ x ↦ x) = 2
  vertex_support : ∀ e v, inc e v ≠ 0 → v ∈ V
  edge_support : ∀ e v, inc e v ≠ 0 → e ∈ E

def Graph.IsLoopAt (G : Graph α β) (e : β) (x : α) : Prop := G.inc e x = 2

def Graph.IsNonloopAt (G : Graph α β) (e : β) (x : α) : Prop := G.inc e x = 1

[Peter Nelson]

The handshake theorem should naturally be true with no fussing with loops, and I think even contractions will work nicely.

[Aaron Liu]

What is sum_eq : ∀ e ∈ E, (inc e).sum (fun _ x ↦ x) = 2 for?

[Aaron Liu]

Why not just have inc : β → Sym2 α instead?

[Peter Nelson]

The sum of the incidences for the vertices at each edge e is either 1+1=2 (for a nonloop e) or 2=2 (for a loop e)

[Peter Nelson]

Aaron Liu said:

Why not just have inc : β → Sym2 α instead?

Because that will be ugly for nonelements of E.

[Peter Nelson]

(In my opinion) the design should allow for deleting edges in a Graph a b to get another Graph a b, without changing the edge type.

[Aaron Liu]

You could also go hypergraph and drop it and then edges connect arbitrarily many vertices

[Peter Nelson]

You can also allow for digraphs by having the incidence function be Int-valued (plus or minus 1) and summing absolute values.

[Peter Nelson]

The annoyance is that this will require Decidable in places that Prop-valued predicates won’t

[Peter Nelson]

I believe there is no way to avoid the decidability assumption in the following :

def Graph.edgeDel (G : Graph α β) (D : Set β) [DecidablePred (· ∈ D)] : Graph α β where
  V := G.V
  E := G.E \ D
  inc := fun e ↦ if e ∈ D then 0 else G.inc e
  sum_eq e he := by simp [he.2, G.sum_eq e he.1]
  vertex_support e v h := G.vertex_support e _ <| by aesop
  edge_support e v h := ⟨G.edge_support _ v (by aesop), by aesop⟩

[Peter Nelson]

Ok, I was wrong; you can make it mostly invisible this way.

noncomputable def Graph.edgeDel (G : Graph α β) (D : Set β) : Graph α β where
  V := G.V
  E := G.E \ D
  inc e :=
    haveI := Classical.dec (e ∈ D)
    if e ∈ D then 0 else G.inc e
  sum_eq e he := by simp [he.2, G.sum_eq e he.1]
  vertex_support e v h := G.vertex_support e _ <| by aesop
  edge_support e v h := ⟨G.edge_support _ v (by aesop), by aesop⟩

[Peter Nelson]

This file uses the above to define multigraphs, edge deletions, extensionality with prop-valued incidence, loops, nonloops, images under maps that merge vertices, and the handshake theorem (with no special-casing for loops) in just over 200 lines.

[Pieter Cuijpers]

Ahh! The discussion is spiralling in quite a different direction then I would have expected, but it does give me some answer as to why there is no clear-cut definition yet :sweat_smile: . I was just being happily naive.

[Pieter Cuijpers]

But why the explicit addition of having sets of vertices and edges?
Would something like:

structure Graph (V E : Type*) where
  inc : E → V → ... whatever needs to be here

already give you enough structure to work with?

From the remarks you're making, you have experience with how the proofs will go further down the line.
I'm trying to understand why you make the choices the way you do here.

[Peter Nelson]

Yes, there is a reasonable discussion to be had about design here, and on this matter I’m expressing one particular point of view, which is informed by my work on matroids. I discuss this at length in this post: https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/The.20design.20of.20matroids

The issues in graph theory aren’t the same, but the analogies are there.

The shorter version: in real-world graph theory proofs, you might do something like contract an edge e, delete a vertex x, and consider the role of a vertex v and a path P, before and after the contractions and deletions were performed. If the graphs $G$, $G-x$, $G / e$ and $(G-x)/e$ are all modeled using different types, then there are already four ‘versions’ of v and P, related by a mess of invisible canonical maps. The more involved the proof, the worse this picture gets, and in my opinion this is a road to disaster.

To avoid this, you want the four graphs to have the same type. I don’t know a better choice for this type than simply Graph a b with vertex and edge sets as structure fields.

[Pieter Cuijpers]

I see. Would there, alternatively, be a way to turn the bookkeeping over all these invisible canonical maps into a tactic?

Personally, I like it when the definitions are kept as simple as possible, sometimes at the cost of a bit of bookkeeping in the proofs. In my work on process algebras (computer science) the bookkeeping is usually unavoidable, which is the very reason I like theorem provers. They do that bookkeeping for me. But it's only fun if it remains readable indeed.

[Pieter Cuijpers]

I see that in the other discussion, there were also people who usually have fixed graphs they are studying, in which case my definition seems preferable.

[Pieter Cuijpers]

Perhaps there is a general trend here... "fixed structures" versus "mutable structures", requiring different definitions even while they belong to the same branch of mathematics.

[Aaron Liu]

Peter Nelson said:

To avoid this, you want the four graphs to have the same type. I don’t know a better choice for this type than simply Graph a b with vertex and edge sets as structure fields.

You could bundle the type, so you have Graph.{v, u} : Type max u v, and for g : Graph you would talk about g.Vertex and g.Edge.

[Peter Nelson]

Maybe a bookkeeping tactic is possible. But it is hard to even precisely delineate the intended scope of such a tactic, and often it is the statements rather than the proofs of theorems that become horrible. Think about statements of the form 'minor operations commute' for example.

In my approach, the bookkeeping tactic needed is one that is capable of proving using existing assumptions that things are 'real' vertices and edges (members of G.V and G.E respectively). This is much more limited in scope, and can be implemented in practice.

Also, the model where the edges and vertices are types are easy to describe in terms of the more general one. Have propositional typeclasses [FullVertex G] and [FullEdge G] for G : Graph a b that state G.V = Set.univ and G.E = Set.univ. A lot of the API can be shared with the general case, and there can be specialized sugar API for the FullVertex/FullEdge cases where it is needed.

[Peter Nelson]

Aaron Liu said:

Peter Nelson said:

To avoid this, you want the four graphs to have the same type. I don’t know a better choice for this type than simply Graph a b with vertex and edge sets as structure fields.

You could bundle the type, so you have Graph.{v, u} : Type max u v, and for g : Graph you would talk about g.Vertex and g.Edge.

If I remove a vertex v, then how do the types G.vertex and (G-v).vertex relate?

[Aaron Liu]

Peter Nelson said:

Think about statements of the form 'minor operations commute' for example.

This seems relatively pain-free to write out, what problem are you seeing?

[Peter Nelson]

Suppose I have two edges e, f, and I want to contract them in one order versus another. How do I state that I have 'the same' graph both ways?

[Aaron Liu]

This is a def contractCommIso : (g.contract e).contract (map (contractGraphHom g e) f) ≃g (g.contract f).contract (map (contractGraphHom g f) e)

[Aaron Liu]

hmmm, this turned out longer than I thought it would be

[Peter Nelson]

And it's the beginning of DTT hell. Now you are pushing forward paths along that map, taking initial subsegments of the paths, etc etc.

[Peter Nelson]

It should be an = if at all possible, and for this example, = is possible.

[Aaron Liu]

I don't see how using = makes it any better though...

[Peter Nelson]

It means that pushforward/pullback API stops being API, and becomes rw.

[Pieter Cuijpers]

(newb question: what is DTT?)

[Peter Nelson]

Dependent type theory.

[Peter Nelson]

To give a concrete example on this point, I was recently looking at the definition docs#SimpleGraph.Subgraph.Connected . There is roughly 500 lines of API for it (and it's still incomplete), even though it is just SimpleGraph.Connected modulo some mathematically invisible maps.

If the vertex set for SimpleGraph were aSet, there would have been no need to have separate SimpleGraph and Subgraph types at all, and this kind of API nearly disappears.

[Peter Nelson]

#24122

[Eric Wieser]

Peter Nelson said:

I believe there is no way to avoid the decidability assumption in the following :

def Graph.edgeDel (G : Graph α β) (D : Set β) [DecidablePred (· ∈ D)] : Graph α β where
  V := G.V
  E := G.E \ D
  inc := fun e ↦ if e ∈ D then 0 else G.inc e
  sum_eq e he := by simp [he.2, G.sum_eq e he.1]
  vertex_support e v h := G.vertex_support e _ <| by aesop
  edge_support e v h := ⟨G.edge_support _ v (by aesop), by aesop⟩

I don't see any harm in keeping it? Decidability isn't inherently evil, but inserting Classical.decEq can cripple decide and #eval downstream

[Jakub Nowak]

I was thinking about definition of docs#Graph specifically for application in minors. I feel like the definition still isn't good for that purpose, as this doesn't allow for a natural definition of contraction. I think, to be able to define contraction, we would want Quotient α, and to allow contraction and subgraphs, probably Set (Quotient α) (I don't think we have partial quotient in mathlib?).
With just Set you need to arbitrarily chose one of two vertices to keep.

[Peter Nelson]

I think there is a case to be made that choosing one of the two ends as the contracted vertex is natural, a la retracts in topology. What practical issues do you see with defining a minor this way?

I am concerned that quotients, which change the vertex type every time an edge is contracted, will just be too hard to work with.

[Kevin Buzzard]

One problem with using Quotient directly is that you will end up in a situation where you quotient and then remove a vertex and will get a type which is canonically isomorophic, but not equal, to the type you get by removing a vertex and then quotienting. This is constant problem when doing graph theory in Lean's dependent type theory. Another example: quotienting to identify a and b, and then quotienting again to identify c and d, will not be equal to quotienting to identify c and d, and then a and b.

It almost feels like one needs different definitions of graphs depending on what you want to do with them, but this would very much go against Mathlib's design principles ("one definition for everything"). Perhaps Peter's suggestion is worth experimenting with.

[Jakub Nowak]

Kevin Buzzard said:

quotienting to identify a and b, and then quotienting again to identify c and d, will not be equal to quotienting to identify c and d, and then a and b.

This will result in a different relation, but orbits will be the same in both cases. And equality of functions is pointwise in Lean, so actually both relations would be equal.

[Jakub Nowak]

Peter Nelson said:

What practical issues do you see with defining a minor this way?

I'm not sure if this would result in practical issues or not. I was thinking about the case, where you have a graph G, its vertex v, and its minor G'. Now, you want to get the vertex in G' that came from v. With Set approach, you would have to go through each contraction one-by-one, check if one of the contracted vertices is v, and choose the correct one of two. With Quotient approach you would take representative of a class of v, and take its class in G'. In other words, the difference is, that Quotient doesn't forget either of the two contracted vertices. But of course, this operation of taking vertex from a graph to its minor can be implemented as part of API, so I don't know it this is a practical issue or not.

[Jakub Nowak]

Actually, maybe it is a problem, because, where would you get the list of contracted pairs from, in a Set approach?

[Jakub Nowak]

You would have to define another type for minors, to keep the list of contractions around, and now we again have the same problem as with Subgraph, that the type of minors is different than that of an original graph.

[Jakub Nowak]

Kevin Buzzard said:

It almost feels like one needs different definitions of graphs depending on what you want to do with them.

Indeed. One other useful graph operation, is duplicating the vertex in two. To support that, and keep the same type for the graph, we probably want to have Multiset, insteaf of a Set. (though, Multiset is finite, is there an infinite Multiset in mathlib?)

[Jakub Nowak]

One could probably come with something else, that would require adjusting definition of a Graph further. So maybe, adjusting the definition of a graph to suit all the operations any graph theorist would ever need is not feasible approach? And instead we should learn how to design the API to work with different types of graph.

[Jakub Nowak]

Peter Nelson said:

I am concerned that quotients, which change the vertex type every time an edge is contracted, will just be too hard to work with.

You can't really take a vertex from a graph and treat it like it's a vertex of its minor anyway. Actually, maybe having different type would even be helpful, cause it would avoid doing accidental confusion like this.

[Peter Nelson]

Jakub Nowak said:

Peter Nelson said:

I am concerned that quotients, which change the vertex type every time an edge is contracted, will just be too hard to work with.

You can't really take a vertex from a graph and treat it like it's a vertex of its minor anyway. Actually, maybe having different type would even be helpful, cause it would avoid doing accidental confusion like this.

This kind of thing is quite common - see Lemma 3.2.4 from Diestel’s book, for example: https://www.math.uni-hamburg.de/home/diestel/books/graph.theory/preview/Ch3.pdf

Of course one needs a proof that the vertex of the minor is actually there in the graph, but in many contexts this will be clear, such as when it is neither end of a single contracted edge.

[Peter Nelson]

Jakub Nowak said:

Peter Nelson said:

What practical issues do you see with defining a minor this way?

I'm not sure if this would result in practical issues or not. I was thinking about the case, where you have a graph G, its vertex v, and its minor G'. Now, you want to get the vertex in G' that came from v. With Set approach, you would have to go through each contraction one-by-one, check if one of the contracted vertices is v, and choose the correct one of two. With Quotient approach you would take representative of a class of v, and take its class in G'. In other words, the difference is, that Quotient doesn't forget either of the two contracted vertices. But of course, this operation of taking vertex from a graph to its minor can be implemented as part of API, so I don't know it this is a practical issue or not.

You don’t need to do anything one by one. If H is a minor of G in my sense, then there is an associated idempotent function from V to V that says where every vertex of G ends up, and is the identity on V(H).

In practice, the cost of changing types when taking minors is huge. (I learnt this from working with matroids, even though their minor operation is less technical - I experienced a lot of pain before switching designs). The Set approach allows for actual DTT-free Eq looking at a graph G and all sorts of mutations of G, whether they be minors or something else. It comes with tradeoffs, of course, but this advantage is substantial.

[Peter Nelson]

Vertex duplication, which you bring up, is a little more annoying, but can be done without changing types if one adds an assumption that the vertex set of G is not the whole vertex type. So G.Dup u v creates a copy of vertex u with label v, and behaves well if it is known that v is not a member of V(G).

[Jakub Nowak]

Peter Nelson said:

Of course one needs a proof that the vertex of the minor is actually there in the graph, but in many contexts this will be clear, such as when it is neither end of a single contracted edge.

Yes, but when neither vertex is an end of a single contracted edge, then you get equality of elements in the Quotient approach too.
Ah, nvm, I see, you're point is that these are different types, because there are elements of Quotient with different Setoid.

[Jakub Nowak]

Hmm, maybe then, instead of using Quotient, we should use sets as vertices (and these sets would represent equivalence classes). Or Finset or Multiset?

[Jakub Nowak]

(deleted)

[Peter Nelson]

Forcing vertices to be sets works, and gives canonical contraction, but leads to weird syntax and theorem statements, and awkward things like enforcing disjointness. I think that the way to go is allowing an arbitrary vertex type with a more permissive notion of contraction, that allows for a notion of contraction the setting where vertices are secretly sets , as well as a retraction-like one where you pick an end of the edge.

My student @Jun Kwon has been working on this, and has been quite successful in working with nontrivial proofs involving minors.

[Jakub Nowak]

Peter Nelson said:

My student Jun Kwon has been working on this, and has been quite successful in working with nontrivial proofs involving minors.

That's interesting. Which of the two approaches to contraction does he work with?

[Peter Nelson]

I’m not sure exactly where he is at with definitions at this minute, so I’ll let him weigh in. He is certainly more familiar than me with the practical issues here.

[Jakub Nowak]

I also have a question, was such definition considered?

structure Graph where
  V : Type*
  E : Type*
  IsLink : E → V → V → Prop
  isLink_symm : ∀ ⦃e⦄, (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

[Jun Kwon]

Jakub Nowak said:

Peter Nelson said:

My student Jun Kwon has been working on this, and has been quite successful in working with nontrivial proofs involving minors.

That's interesting. Which of the two approaches to contraction does he work with?

Hi! The different ways to contact has been a bit of a headache. I am working to support both ways if possible. That is, if you do not have assumptions available, then you can contract by specifying the vertex choice, but if you have more assumptions that allow a canonical contraction, you can do that too.

[Jun Kwon]

Jakub Nowak said:

I also have a question, was such definition considered?

structure Graph where
  V : Type*
  E : Type*
  IsLink : E → V → V → Prop
  isLink_symm : ∀ ⦃e⦄, (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

Are you thinking that every object of type V is a real vertex? Otherwise, how do you distinguish an isolated vertices with non-existent one?

[Jakub Nowak]

Jun Kwon said:

Are you thinking that every object of type V is a real vertex? Otherwise, how do you distinguish an isolated vertices with non-existent one?

Yes, every object of type V is a vertex. Buy you can have V : Set α if you want to be able to remove vertices.

[Shreyas Srinivas]

Jakub Nowak said:

Jun Kwon said:

Are you thinking that every object of type V is a real vertex? Otherwise, how do you distinguish an isolated vertices with non-existent one?

Yes, every object of type V is a vertex. Buy you can have V : Set α if you want to be able to remove vertices.

In that case the edge relation becomes E -> Set α -> Set α -> Prop

[Peter Nelson]

I think here V : Set a doesn’t mean the vertices are sets, it means the vertex set is modelled as a set within a type

[Jakub Nowak]

Shreyas Srinivas said:

In that case the edge relation becomes E -> Set α -> Set α -> Prop

No, that would happen if you take V = Set α. I meant V : Set α.

[Jun Kwon]

I don't think we tried with types as a structure field as supposed to an argument. My guess would be that this definition would require talking about functions, homomorphisms and isomorphisms everywhere.

[Peter Nelson]

Yes, equality of graphs would then involve ‘evil’ equality of types.

[Jakub Nowak]

That looks interesting, I might try and explore this further then.

import Mathlib

namespace GraphV2

structure Graph : Type _ where
  V : Type*
  E : Type*
  IsLink : E → V → V → Prop
  isLink_symm : ∀ ⦃e⦄, (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

structure Graph.Of (V E : Type*) (G : Graph) : Prop where
  V_eq : G.V = V
  E_eq : G.E = E

def Graph.Of.IsLink {G : Graph} {V E : Type*} (hOf : G.Of V E) : E → V → V → Prop :=
  fun e x y ↦ G.IsLink (hOf.E_eq ▸ e) (hOf.V_eq ▸ x) (hOf.V_eq ▸ y)

def Graph.Of.IsLinkSet {G : Graph} {V : Set α} {E : Set β} (hOf : G.Of V E) : β → α → α → Prop :=
  fun e x y ↦ ∃ (he : e ∈ E) (hx : x ∈ V) (hy : y ∈ V), hOf.IsLink ⟨e, he⟩ ⟨x, hx⟩ ⟨y, hy⟩

inductive Graph.IsSubgraph (G' G : Graph) : Prop where
| of_set_set {V' V : Set α} {E' E : Set β} (hOf' : G'.Of V' E') (hOf : G.Of V E)
  (verts_subset : V' ⊆ V)
  (edges_subset : E' ⊆ E)
  (isLink_impl : ∀ ⦃e x y⦄, hOf'.IsLinkSet e x y → hOf.IsLinkSet e x y)
  : IsSubgraph G' G
| of_set_type {V' : Set α} {E' : Set β} (hOf' : G'.Of V' E') (hOf : G.Of α β)
  (isLink_impl : ∀ ⦃e x y⦄, hOf'.IsLinkSet e x y → hOf.IsLink e x y)
  : IsSubgraph G' G
| of_type_type (hOf' : G'.Of α β) (hOf : G.Of α β)
  (isLink_impl : ∀ ⦃e x y⦄, hOf'.IsLink e x y → hOf.IsLink e x y)
  : IsSubgraph G' G

[Peter Nelson]

I think your type structure fields are setting you up for DTT hell.

[Jakub Nowak]

My hope for that approach is that, we can hide DTT hell inside couple API functions and not have it be exposed.

[Peter Nelson]

Say you have vertices x,y of G. How do you express the fact that (G - x) - y = (G - y) - x?

[Jun Kwon]

Can I ask if you are trying this def just cause or if you have a clear benefit over other defs in mind?

[Jakub Nowak]

Jun Kwon said:

Can I ask if you are trying this def just cause or if you have a clear benefit over other defs in mind?

My concern is that, different types of graph might be needed for different operations you would want to be able to do with the graph. I want to have one type for graph that would be flexible, and allow all operations under one graph type.

[Peter Nelson]

Can you provide examples of the operations you mean?

[Jakub Nowak]

E.g. duplicating a vertex. An operation, where you take a vertex of a graph, and you create a new graph by duplicating said vertex, and all incident edges. And there are two possible versions of this operation, depending on whether you also add an edge between duplicated vertices, or not.

[Jakub Nowak]

Or an operation, where you add a completely new vertex, connected to every other vertex.

[Jun Kwon]

I think the subgraph definition above is not transitive. For a type a, and some subtype of a, a', and some subtype of a', a'', a graph over a'' can be a subgraph of a graph over a' by 'of_set_type' and that graph over a' can be a subgraph over a. However, a graph over a'' can't be a subgraph of one over a.

[Peter Nelson]

In my experience, if you are adding a new vertex $v$ to a graph $G$ by cloning/apexing as you describe (say to get a graph $G'$), then you are probably very interested in the fact that $G' - v = G$. If that $=$ is not an =, then you are already in a very annoying place.

[Peter Nelson]

In any case, if the vertices are a type, it should still be before the colon rather than a structure field. So adding a new vertex would take Graph V E to Graph (Option V) E or whatever. This allows equality of graphs to be non-evil.

[Jakub Nowak]

Peter Nelson said:

In any case, if the vertices are a type, it should still be before the colon rather than a structure field. So adding a new vertex would take Graph V E to Graph (Option V) E or whatever. This allows equality of graphs to be non-evil.

But that would mean that $G' - v$ and $G$ have different types.

[Jakub Nowak]

I don't think $G' - v = G$ with equality is possible, unless you provide unused vertex when constructing G'.

[Peter Nelson]

I think hypothesizing an unused vertex is fine in a lemma statement, and will be easier to work with in a proof. A version with Option V can be derived from the unused vertex version at an essentially cosmetic level.

[Peter Nelson]

Jakub Nowak said:

But that would mean that $G' - v$ and $G$ have different types.

I am not sure I see the advantage in them having the same type, when the types in the structure fields are different.

[Snir Broshi]

The symmetry of having to provide a vertex when either contracting an edge or duplicating a vertex is nice
I think having slightly awkward operations is better than dealing with HEq

[Jakub Nowak]

Peter Nelson said:

I think hypothesizing an unused vertex is fine in a lemma statement, and will be easier to work with in a proof.

Yeah, I think it sounds promising. For finite graphs, you can work with [Infinite α] to always be able to find a free new vertex.