simple_graphs2

Stream: graph theory

[Alena Gusakov]

I pushed an error fix that Kevin helped me out with

[Alena Gusakov]

Basically just got rid of the problem in degree_le where Lean didn't know why we were allowed to compare the degrees because it didn't know degree (G'.in_subgraph hv) is a fintype

[Alena Gusakov]

just kidding, somehow there's still an error somewhere

[Kyle Miller]

I'm going to take a look -- I had some troubles with these instances because they caused class resolution to not terminate. (I'm trying to get my own changes to the branch in order so I can merge yours.)

[Kyle Miller]

Alena Gusakov said:

just kidding, somehow there's still an error somewhere

These instances are tricky, and I've been struggling with how to define these off and on for a while, but they might finally now be OK. It turns out you can't actually have them as instances because they "introduce metavariables", which are caused by variables on the LHS of the colon that cannot be totally inferred by either class resolution or the usual implicit argument elaboration.

Anyway, degree_le is now a lemma (with proof!), and it makes use of some new lemmas involving graph embeddings. The idea is that it's not hard to prove that the neighbor set of a vertex in a subgraph embeds in the neighbor set of that vertex in a supergraph, and then fintype.card_le_of_injective does the rest.

If you wanted, you could follow the same strategy with embedding.map_edge_set to show that the cardinality of an edge set of a subgraph is less than or equal to the cardinality of the supergraph's edge set.

[Kyle Miller]

A couple of other sorry's:

• complete_graph_min_colors is that a complete graph on n vertices needs at least n colors in a proper coloring.
• exists_path_eq_eqv_gen should follow from a lemma that if there is a walk between two vertices then there is a path between them.

[Alena Gusakov]

it seems like there are other errors now though - namely in the proofs of all of the map_edge_set definitions oops, restarted lean and the errors went away

[Kyle Miller]

After some discussion with @Alena Gusakov, the branch now has what seems to be an easier-to-work-with definition of subgraphs:

structure subgraph :=
(V' : set (V G))
(adj' : V G → V G → Prop)
(adj_sub : ∀ ⦃v w : V G⦄, adj' v w → v ~g w)
(edge_vert : ∀ ⦃v w : V G⦄, adj' v w → v ∈ V')
(symm' : symmetric adj')

(It has the correct extensionality property, which I had trouble getting right with this sort of formulation, that there is exactly one term per subgraph. That's why the earlier definition used a subset of edges.)

As an experiment in a technique to show two definitions are equivalent, I kept the old definition as a protected definition in the simple_graph.subgraph namespace:

protected structure of_edge_set' (G : α) :=
(V' : set (V G))
(edge_set' : set (sym2 (V G)))
(edge_sub : edge_set' ⊆ edge_set G)
(has_verts : ∀ ⦃e : sym2 (V G)⦄ ⦃v : V G⦄, e ∈ edge_set' → v ∈ e → v ∈ V')

Then I gave it a simple_graphs instance and proved two statements:

protected def equiv_of_edge_set' : subgraph G ≃ of_edge_set' G

def iso_of_edge_set' (G' : subgraph G) : G' ≃g subgraph.equiv_of_edge_set' G'

That is to say, the types are equivalent, and that equivalence carries graphs to isomorphic graphs. (This is what I meant in the matroids topic -- matroids have multiple definitions, and this seems to be a structured way to formalize that the definitions are equivalent.)

[Kyle Miller]

I've added formalizations of the first two theorems in Bollobas's book in this branch.

-- The type of all embedded cycles in a given graph
def cycles (G : α) := Σ (n : {n : ℕ // 3 ≤ n}), cycle_graph n.1 n.2 ↪g G

/--
Veblen 1912 (theorem 1 in book).  Every vertex has even degree iff there is a
partition of the graph into edge-disjoint cycles.
-/
theorem edge_partition_cycles (G : α) [fintype (V G)] :
  (∀ v : V G, degree v % 2 = 0) ↔ (∃ partition : set (cycles G),
                                     ∀ (e : edge_set G), !∃ (c : cycles G), c ∈ partition ∧
                                       e ∈ set.image (embedding.map_edge_set c.2) set.univ) :=
sorry

/--
Mantel 1907 (theorem 2 in book). If a graph with n vertices and m edges satisfies
floor(n^2 /4) < m, then it contains a triangle.
-/
theorem has_triangle (G : α) [fintype (V G)] (h : (fintype.card (V G))^2 / 4 < (edge_finset G).card) :
  nonempty (cycle_graph 3 (by linarith) ↪g G) :=
sorry

(Proving these will take a good amount of theory building still.)

For the first theorem, it's probably better to formalize cycles as being subgraphs that are isomorphic to a cycle graph, since with the current formulation every cyclic shift of a cycle is considered to be a different cycle. It's probably also good to formalize the idea of edge-disjoint partitions by subgraphs.

[Kyle Miller]

Changed it to be in terms of subgraphs that are cycles:

/--
Veblen 1912 (theorem 1 in book). Every vertex has even degree iff there is a
partition of the graph into edge-disjoint cycles.
-/
theorem edge_partition_cycles (G : α) [fintype (V G)] :
  (∀ v : V G, degree v % 2 = 0) ↔ (∃ partition : set (subgraph G), (∀ G' ∈ partition, subgraph.is_cycle G') ∧
                                     ∀ (e ∈ edge_set G), !∃ (c : subgraph G), c ∈ partition ∧
                                       e ∈ c.edge_set') :=
sorry

[Alena Gusakov]

so for the second implication here

lemma exists_path_eq_exists_walk : exists_path G = exists_walk G :=
begin
  ext v w,
  split,
  intro h,
  rcases h with ⟨n, ⟨f, hf⟩⟩,
  split,
  use n,
  rw walk,
  use f.to_homomorphism,
  exact hf,

  intro h,
  rcases h with ⟨n, ⟨f, hf⟩⟩,
  sorry,
end

would having open_locale classical and then contracting edges between repeated vertices be a good strategy? i'm kind of stumped with this one

[Alena Gusakov]

also, i wonder if it might be useful to define some notion of the image of a graph homomorphism (unless i'm missing something that's already defined)

[Kyle Miller]

Feel free to make the lemma noncomputable and use the classical tactic for now. (I think classical does the equivalent of open_locale classical inside a proof, but I'll have to check)

[Kyle Miller]

I was imagining doing strong induction on the length of a walk. If a walk isn't a path, then there must be a repeated vertex, and then if you cut out the portion of the walk that occurred between the two vertices, the walk length gets shorter, hence it has a corresponding path by induction

[Aaron Anderson]

Do you even need noncomputable if you're just using classical inside a proof of a Prop?

[Kyle Miller]

Probably not

[Alena Gusakov]

also, is it possible to like, "concatenate" functions? like make a new function out of two that you already have

[Kyle Miller]

The easiest-to-remember way is using lambda expressions

[Kyle Miller]

There's a whole bunch of function combinators in the function namespace, too, but they don't seem to be used much

[Kyle Miller]

I tried using combine in the definition of graph homomorphisms, but there were some type errors (I think because it involved Prop?) and I reconsidered. It even has fancy notation: (f -[h]- g) x y = h (f x y) (g x y)

[Alena Gusakov]

I don't know if combine is what I'm looking for - it looks like it takes functions with two arguments

[Alena Gusakov]

I'm currently working on the concatenation of walks definition

[Kyle Miller]

combine was just one of the many examples of combinators. i don't think it's useful for what you're doing.

for walks, this is gluing walks together, right? I'm not sure how gluing functions together works elsewhere in mathlib (how do the sheaf axioms glue functions? maybe that's to general to be useful here)

(When you said "contract" earlier, this might be where it'd be nice to actually have a quotient construction, using the expanded notion of graph homomorphism that was in the ncatlab article)

[Alena Gusakov]

I think I might've found a way to do it, does this look legit?
to_fun := λ x, if x ≤ n then p.1.to_fun x else q.1.to_fun x,

[Alena Gusakov]

context:

def walk.concat {n : ℕ} {m : ℕ} {v w u : V G} (p : walk G n u v) (q : walk G m v w) :
  walk G (n + m) u w :=
  { val :=
    { to_fun := λ x, if x ≤ n then p.1.to_fun x else q.1.to_fun x,
    map_adj' := sorry},
  property := sorry, }

[Alena Gusakov]

wait no it's not cause x is a vertex. I'll smooth that out I guess

[Alena Gusakov]

It seems like it would just be to_fun := λ x, if x.1 ≤ n then p.1.to_fun x else q.1.to_fun x,

[Kyle Miller]

I just realized that I have this partially defined in that file already, it's just too big and disorganized, sorry. Take a look at walk_join

[Kyle Miller]

It still lacks the proof that the result is a walk

[Kyle Miller]

(I'm assuming you're using simple_graphs2 based on the exists_path_eq_exists_walk lemma)

[Alena Gusakov]

ohhh okay, ty

[Alena Gusakov]

we can't have paths on a single vertex right? that contradicts the definition of path

[Alena Gusakov]

should we have a lemma that explicitly states that?

[Kyle Miller]

Are zero-length paths not ok?

[Kyle Miller]

for compositions of walks, I thought those would be identity elements

[Kyle Miller]

walks themselves should form a category (I forget the exact terminology, maybe a dagger category? some kind of category where objects are self-dual and morphisms have duals). objects of the category are vertices of the graph, morphisms are walks from a vertex to another vertex, composition of walks is the concatenation of the walks, identities are the zero-length walks, and duals are parameterization reversal

[Kyle Miller]

once you have all this set up, then "there exists a morphism from x to y" is an equivalence relation on objects of the category

[Kyle Miller]

i.e., "there exists a walk of any length from x to y" is an equivalence relation.

[Jalex Stark]

I remember writing path code that used path.empty v to be the empty path rooted at vertex v

[Alena Gusakov]

I'm having trouble working with simple_graph_from_rel - specifically, I can't seem to figure out how to treat the vertices in the graph as the original objects they were defined as

[Kyle Miller]

One trick is you can use the change tactic to change the type to whatever it's actually equal to.

Another is to add this missing lemma and use it to rewrite V G:

lemma simple_graph_on.verts_eq (α : Type u) (G : simple_graph_on α) : V G = α := rfl

Yet another thing you could do, I think, is to use erw rather than rw.

[Alena Gusakov]

now i'm getting hung up on trying to coerce the numbers from fin to nat

[Alena Gusakov]

should we add nontrivial to the definition of connected?

[Alena Gusakov]

actually wait no, i guess it's trivially true for...the trivial case

[Alena Gusakov]

I'm trying to prove that in a nontrivial connected graph, every vertex has degree at least one

[Alena Gusakov]

but it's an absolute nightmare

[Aaron Anderson]

I'm maybe behind the times on what definition of connected you're using, but perhaps it'd actually be easier to prove something more general: if you have a set of vertices, and no vertex in the set is adjacent to any vertex outside the set, then no vertex in the set is path-connected to any vertex outside the set

[Alena Gusakov]

My definition of connected is there exists a path between every vertex, but what I want to prove is that this means every vertex has at least one edge to it

[Alena Gusakov]

also currently having trouble proving that a subgraph of an acyclic graph is also acyclic

[Aaron Anderson]

Alena Gusakov said:

also currently having trouble proving that a subgraph of an acyclic graph is also acyclic

This should be at least pretty easy if we're using an embedding or subgraph definition of acyclic

[Aaron Anderson]

I'm going over to simple_graphs2 to check out what I've missed

[Alena Gusakov]

My current problem is when I say is_acyclic (subgraph G) it doesn't recognize the subgraph as a simple graph

[Alena Gusakov]

sorry, I should've said I'm having trouble stating it

[Aaron Anderson]

One note: @Kyle Miller, I know that we have good reasons to doubt whether graph homomorphisms should be modeled with rel_homs, but I'm confused why simple_graphs2 uses rel_iso to define isomorphisms, but doesn't use rel_embedding to define embeddings, when I'm pretty sure the custom structure for embeddings has the exact same information as rel_embedding

[Kyle Miller]

I was going to change it back eventually. Your new PR wasn't there yet

[Kyle Miller]

though my embedding was a mono, vs regular mono

[Aaron Anderson]

Kyle Miller said:

though my embedding was a mono, vs regular mono

Ah right, sorry

[Aaron Anderson]

Anyway, the main advantage of a non-regular mono is that an arbitrary subgraph has an inclusion embedding

[Aaron Anderson]

Have we put that in lean yet?

[Aaron Anderson]

Because I'd imagine that's how you'd prove that a subgraph of an acyclic graph is acyclic

[Aaron Anderson]

or I guess you redefine/show that it's equivalent to nonexistent of a subgraph which is a cycle

[Aaron Anderson]

in which case you want to use transitivity of subgraph

[Aaron Anderson]

Alena Gusakov said:

I'm trying to prove that in a nontrivial connected graph, every vertex has degree at least one

I think I have a sketch if you're willing to use the eqv_gen version, which is defined on simple_graphs2, but the equivalence is currently sorry

[Aaron Anderson]

Say you have a set S of vertices. Then you define an equivalence relation (actually a setoid) where two vertices are equivalent iff they're both in S or both not in S.

[Aaron Anderson]

Then you want to use https://leanprover-community.github.io/mathlib_docs/data/setoid/basic.html#setoid.eqv_gen_le

[Aaron Anderson]

What this tells you is that if (for all x y : V, x ~g y implies s.rel x y), where s.rel is our new equivalence relation

[Aaron Anderson]

then (eqv_gen G.adj) x y implies s.rel x y

[Aaron Anderson]

In other words, x being connected to y implies x and y are both in S or both not in S

[Kyle Miller]

Aaron Anderson said:

Have we put that in lean yet?

This is in there:

def subgraph.map {x y : subgraph G} (h : x ≤ y) : x ↪g y

[Aaron Anderson]

This basically proves the lemma that if a set S is closed under adjacency, that its vertices are not connected to outside vertices

[Aaron Anderson]

and to prove the exact theorem you wanted, @Alena Gusakov , the only remaining step is to let S be a singleton. Then you find that if your singleton has degree 0, then it's closed under adjacency, so its one element is not connected to anything else, the contrapositive of what you wanted.

[Aaron Anderson]

Does that make sense?

[Aaron Anderson]

Kyle Miller said:

Aaron Anderson said:

Have we put that in lean yet?

This is in there:

def subgraph.map {x y : subgraph G} (h : x ≤ y) : x ↪g y

Ok, so then it should be relatively easy to prove at least that if a subgraph S is NOT acyclic, then there is an embedding from a cycle graph into S, which you can then compose with subgraph.map to get an embedding from the cycle graph into the subgraph top

[Aaron Anderson]

Then it's a matter of showing that a graph isomorphic to an acyclic graph is acyclic, which can also work by composing embeddings

[Kyle Miller]

(Speaking of eqv_gen G.adj, one thing @Alena Gusakov is helping with is showing that three different definitions of connectivity are equal: there exists a path between vertices, there exists a walk between vertices, and eqv_gen G.adj.)

[Alena Gusakov]

yeah i've been poking around those lemmas, they're also a nightmare

[Kyle Miller]

I'm sure we'll figure out how to make it nice eventually :smile:

[Kyle Miller]

@Aaron Anderson I was considering replacing f : G ↪g G' with f : G →g G' having some kind of mono instance, not sure the right name. It's can't be the category theory one, unfortunately, for some of the usual reasons. It would be nice if injective were a typeclass here, because injective f ends up being the correct notation, given the has_coe_to_fun instance for graph homomorphisms.

[Kyle Miller]

I hesitate to do this, though, because ↪g seems to have been convenient so far to mean monomorphism since it extends function.embedding so can find some immediate use in some cardinality arguments. However, it seems possible to define a cast of a function with a mono-like instance to get a function.embedding as needed.

[Kyle Miller]

I've reorganized the simple_graphs2 repository in a number of ways:

• Now a simple graph is merely a term of simple_graph. This is a bundled simple_graph_on α term, for simple graphs with vertex type α.
• To give the terms of a type the structure of a simple graph, one implements has_coe_to_simple_graph. This gives you access to a new coercion arrow, ↟, which coerces graph-like things to simple graphs. This circumvents an issue where typeclass resolution won't assert two universe metavariables are equal, so has_coe cannot work, but perhaps in a future version of Lean this will be resolved. Until then, ↟ works well enough.
• The code has been broken up into multiple files in https://github.com/leanprover-community/mathlib/tree/simple_graphs2/src/combinatorics/simple_graph so hopefully it's easier to follow now!
• Graph homomorphisms have been changed to use order.rel_iso exclusively. Monomorphisms are graph homomorphisms that implement thesimple_graph.hom.mono typeclass.

More about ↟: Of the many ways of organizing the simple graph library so that derived objects like subgraphs can be graphs, too, this seems to be the least-bad of all of them, and it has the benefit that, in the future, these arrows might disappear entirely. While you might need to specify universe variables, like (G : simple_graph.{u}), so far I don't think I've been required to do this and have only done so for clarity in definitions.

When writing theorems about graphs in general, make sure to do it for terms of type simple_graph. I think the way new types of graphs should work is, after defining the coercion, there needs to be a number of simp lemmas that specialize the generic definitions.

I've also added walks to the library. There are two ways they are represented, either as an inductive type that's essentially a list of adjacent vertices or as graph homomorphisms from path graphs into the graph. There is a proof that these are structurally equivalent (I visited heq on the way, one of the circles of dependent typed hell, but that's all gone now, thankfully -- I have a special version of heterogeneous equality in the library still, which seems like it could be useful, but if it finds no use it'll be removed). The walk type is essentially defining a category of walks, and it might be nice to actually give it a category structure, too.

Warning: not every definition makes sense and not every lemma with a sorry is provable -- I also, unfortunately, haven't necessarily fixed all errors. The documentation is probably not up to date either!

[Kyle Miller]

(The coercion arrow, by the way, didn't change the code much. The previous version still was about coercions, and it was just a matter of changing who is responsible for inserting them, so to speak.)

[Jalex Stark]

Wow! I guess there's a lot of shovel-ready work for filling in sorries and carving off PRs to mathlib.

[Jalex Stark]

Do you think that the current definition of simple graphs in mathlib should be replaced or just given an instance of the new coercion arrow?

[Jalex Stark]

Kyle Miller said:

When writing theorems about graphs in general, make sure to do it for terms of type simple_graph. I think the way new types of graphs should work is, after defining the coercion, there needs to be a number of simp lemmas that specialize the generic definitions.

I guess this implies that you think the current theorem statements should be rejiggered to be about terms of type simple_graph. But if we give the old simple graph type an instance of the new coercion arrow, then e.g. the proof of freek 83 in the mathlib archive won't need changes, except maybe to add some arrows?

[Jalex Stark]

I am like 8000 messages in the hole in terms of staying up to date on the server... have you advertised this stuff on #maths or are you waiting until more of the sorries and errors are fixed?

[Jalex Stark]

(small meta note, hopefully this is more helpful than annoying. if your big message were broken up into smaller messages, it would be easier to quote / emoji for more specific things)

[Kyle Miller]

Jalex Stark said:

(small meta note, hopefully this is more helpful than annoying. if your big message were broken up into smaller messages, it would be easier to quote / emoji for more specific things)

Like this? (Good point :smile:)

[Jalex Stark]

Kyle Miller said:

Graph homomorphisms have been changed to use order.rel_iso exclusively. Monomorphisms are graph homomorphisms that implement thesimple_graph.hom.mono typeclass.

I guess @Aaron Anderson will be happy to hear this

[Kyle Miller]

The conversion to using simple_graph is almost entirely just removing vertex type arguments and then doing v : V G. It's pretty much painless.

[Jalex Stark]

What do you think the next PR from this branch should be?

[Kyle Miller]

It would be nice to sort out the coercion. There's a little discussion in #Is there code for X? (the auto-coercions thread) about how has_coe is almost but not quite sufficient, but it seems fixing this involves modifying Lean itself.

[Kyle Miller]

But maybe making the arrow a local notation is good enough for now.

[Kyle Miller]

Jalex Stark said:

What do you think the next PR from this branch should be?

Most of simple_graph/basic.lean seems good, except for the incomplete stuff about graph operations. Some simp lemmas relating simple_graph_on to simple_graph might not make sense. Also simple_graph_from_rel_adj can probably wait.

The definitions in simple_graph/hom.lean seem fine, but the lemmas should be reviewed since the api is underutilized and seems somewhat incomplete.

simple_graph/subgraph.lean seems good, except for things about cycles and maybe induced graphs. Cardinality results should be reviewed -- there's no application of them yet so the design might not be good.

simple_graph/simple_graph_on.lean is fine enough. It could certainly be expanded, but it at least has a bounded_lattice instance.

simple_graph/degree_sum.lean is close, but I think it can still be simplified a lot given a person sufficiently competent with big_operators. It also would be nice to have an explicit handshake lemma.

[Kyle Miller]

simple_graph/adj_matrix.lean is just the current adj_matrix.lean but modified to use this new simple_graph type.

[Alena Gusakov]

I think I completed the edge contraction definition

[Alena Gusakov]

I also created an edge deletion definition

[Alena Gusakov]

I tried messing around with paths and walks after that, as well as trees, but really didn't get anywhere

[Alena Gusakov]

I managed to prove the first direction of the statement map_rel_iff' in fin.flip.invol

[Alena Gusakov]

but the other direction has me stumped

[Bhavik Mehta]

Since it's an involution can't you just use the first direction and some equivalence properties?

[Bhavik Mehta]

I might be misremembering what you're trying to prove though

[Alena Gusakov]

i think i got stuck trying to do exactly that

[Alena Gusakov]

Trying to figure out how to define matchings currently. I'm thinking some structure like

structure matching_on (G : simple_graph) :=
(disjoint : )

[Alena Gusakov]

where disjoint is the property that the edges are disjoint

[Alena Gusakov]

but I'm not quite sure how to get there

[Alena Gusakov]

maybe a class? something like

class matching (M : set (sym2 (V G))) :=
(disjoint : ∀ e f ∈ M, ∀ v : V G, v ∈ e → v ∉ f)

[Kyle Miller]

A class seems like a reasonable approach. I haven't tested it, but maybe this definition?

class matching (M : set (sym2 (V G))) :=
(sub_edges : M ⊆ E G)
(disjoint : ∀ (e f ∈ M) (v : V G), v ∈ e → v ∈ f → e = f)

class perfect_matching (P : set (sym2 (V G))) extends matching P :=
(cover : ∀ v : V G, ∃ e ∈ P, v ∈ e)

[Kyle Miller]

There are upsides and downsides to classes for this, so you might need to experiment. Structures would be fine too, but if you had a perfect matching, you'd need to use its to_matching function to turn it into a matching when necessary.

Another thing to consider is predicates

def matching {G : simple_graph} (M : set (sym2 (V G)) := M ⊆ E G ∧ ∀ (e f ∈ M) (v : V G), v ∈ e → v ∈ f → e = f
def perfect_matching {G : simple_graph} (P : set (sym2 V G)) := matching P ∧ ∀ v : V G, ∃ e ∈ P, v ∈ e

but a downside here is that you can't access the sub-properties as easily.

[Alena Gusakov]

ah yeah thank you, the class definition you gave makes more sense

[Alena Gusakov]

forgot to add the part where the edges come from G

[Bhavik Mehta]

I feel like you want a structure rather than a class (they can also extend) since you might want to consider multiple matchings on the same set

[Kyle Miller]

I was thinking that too, but then I realized Alena's class was the matching itself, and all the fields are just propositions so the class is a subsingleton. It seems like it's similar to using mono.

[Bhavik Mehta]

I think mono should be a proposition though :) I think that change is gonna happen in the category theory library as soon as someone actually puts in the effort to make it

[Alena Gusakov]

Is there something we can do about the builds failing?

[Alena Gusakov]

I've been away for a bit so I'm a bit out of the loop, are we still trying to go with the definition simple_graph_on where we turn it into simple_graph later? Just looking at the file in mathlib and it doesn't seem to be the case right now

[Alena Gusakov]

If we are going to do that then I can start slicing off simple_graphs2 into PRs

[Alena Gusakov]

Btw I think when I was initially trying to figure things out I muddled up a lot of the code in simple_graphs2 so I'm sorry if that caused anyone to step back

[Jalex Stark]

I think the simple_graph_on proposal is still the best one, and I'd support you in making PRs about it

[Aaron Anderson]

I’d be happy to help a PR to refactor to simple_graph_on etc. if someone else gets it started

[Aaron Anderson]

(Mostly I’m volunteering to translate over the friendship graph material)

[Alena Gusakov]

I think we pretty much do have everything refactored ah wait, forgot that we need to catch up to all of the mathlib changes since september

[Alena Gusakov]

Like, I didn't even need to do the work, it's already there in simple_graphs2

[Alena Gusakov]

But I'll pull the file into its own PR

[Alena Gusakov]

So I managed to adapt some of the lemmas and definitions from simple_graphs2 into a branch that doesn't rely on simple_graph_on

[Alena Gusakov]

@Bhavik Mehta just gonna pull you into this conversation cause I'm probably not going to be able to explain why I wasn't using simple_graph_on very well

[Alena Gusakov]

Also @Eric Wieser

[Aaron Anderson]

I think it still makes sense to eventually have a PR that adds no new features, and just converts to simple_graph_on, because I think that conversion will cause enough discussion by itself.

[Aaron Anderson]

You could always have another PR that is blocked by that simple_graph_on PR, adding features on top of simple_graph_on, if you think that those features would be a good demonstration of why simple_graph_on is good.

[Alena Gusakov]

So far I haven't had any trouble switching everything from simple_graphs2 to the definition we currently have in mathlib

[Alena Gusakov]

The one annoying thing is not using simple_graph_on means we don't have the special notation for adjacency

[Alena Gusakov]

But if I do find problems/advantages I'll try to do that

[Kyle Miller]

Alena Gusakov said:

So far I haven't had any trouble switching everything from simple_graphs2 to the definition we currently have in mathlib

We haven't gotten to subgraphs in mathlib yet is why :smile:

I think it's better to leave it as simple_graph for now and then do the refactor later when a simple_graph_on is clearly needed -- and since putting it off might cause more work, I'm willing to do it when it comes to that. (I think it will actually be less work long-term to not change it now.)

[Alena Gusakov]

Got it, I'll try to do subgraphs in the next PR (assuming this first one gets approved)

[Hunter Monroe]

@Alena Gusakov can I do a pull request with subgraph.lean and hom.lean from the simple_graph_subgraph branch? I would add a definition of graph isomorphism.

abbreviation iso (G : simple_graph V) (G' : simple_graph W) : Type (max u v) :=
rel_iso (G.adj) (G'.adj)

[Alena Gusakov]

Go for it!

[Alena Gusakov]

I don't remember how much I did with that branch tbh

[Kyle Miller]

For what it's worth, @Aaron Anderson had written the following for a PR a while back. It seems fine, though I think the definition of embedding is surprising for graphs (I think you'd want a result that every subgraph of $G$ embeds in the graph $G$ -- so an embedding would be an injective homomorphism). I think the terminology comes from model theory -- it's a useful concept, but I don't know the proper graph-theoretic terminology for it.

section maps

variables {W : Type*} (G) (H : simple_graph W)

/-- A graph homomorphism maps adjacent vertices to adjacent vertices -/
abbreviation hom := rel_hom G.adj H.adj

infix ` →g ` : 50 := hom

/-- A graph embedding is an embedding `f` such that for vertices `v w : V`,
  `G.adj f(v) f(w) ↔ G.adj v w `-/
abbreviation embedding := rel_embedding G.adj H.adj

infix ` ↪g ` : 50 := embedding

/-- A graph isomorphism is an equivalence that preserves adjacency-/
abbreviation iso := rel_iso G.adj H.adj

infix ` ≃g ` : 50 := iso

end maps

[Alena Gusakov]

(deleted)

[Hunter Monroe]

A relationship embedding rel_embedding maps G to an induced subgraph of H (a bijection for all edges of the involved vertices of H), right? Also, I want to be certain that all of these maps are injective, which is my reading of the definitions.

Kyle Miller said:

abbreviation embedding := rel_embedding G.adj H.adj

[Hunter Monroe]

I will leave out embedding which is an obscure concept within graph theory. The only reference I could find was to "induced subgraph isomorphism" within complexity theory.

[Yakov Pechersky]

Embedding is by definition injective. An injective map can be called an embedding. Not all rel_homs will be injective.

[Kevin Buzzard]

In topology an embedding is a specific kind of injective map -- the words aren't entirely interchangeable

[Bhavik Mehta]

Hunter Monroe said:

I will leave out embedding which is an obscure concept within graph theory. The only reference I could find was to "induced subgraph isomorphism" within complexity theory.

embeddings essentially let you define induced subgraphs, which I'd argue aren't at all obscure, I think they should definitely be added

[Kyle Miller]

Yeah, I didn't mean to suggest that rel_embedding was obscure, just that calling it an "embedding" seems to be. I personally think hook arrow for "injectively maps onto an induced subgraph" would be surprising, but I'm happy to follow consensus.

@Kevin Buzzard At least in this case, injective homomorphisms induce topological embeddings for the graphs' geometric realizations as CW complexes.

[Kevin Buzzard]

There is a more general concept of injection where you're allowed to send adjacent vertices to non-adjacent vertices which are connected by a path I guess. I remember learning the statement (but not proof) of a theorem of perhaps Kuratowski saying that topological K5's and K(3,3)'s are the only obstruction to planarity

[Kyle Miller]

The rel_embedding definition is a regular monomorphism, but the injective rel_hom definition is a monomorphism, in the category of simple graphs where maps have to preserve adjacency. There are at least two different ways to define this category, however (and ncatlab describes both). In the other one, maps can send adjacent pairs to adjacent pairs, or collapse them to a single vertex.

[Kyle Miller]

Maybe this is why they deserve to be called embeddings, now that I've thought it through again in front of everyone.

[Hunter Monroe]

I have created a pull request for subgraph and maps (homomorphism, isomorphism, embedding).

[Johan Commelin]

@Hunter Monroe Just fyi, if you type #8223 in Zulip, it will render as #8223 and also link to your PR.

[Hunter Monroe]

I have incorporated review comments and reverted the formatting. Note one substantive change at @Bhavik Mehta's suggestion: hom and iso no longer assume that G and G' have vertices of the same type.

[Bhavik Mehta]

Note that Kyle's suggestion above also did not have this assumption

[Kyle Miller]

How do we want naming of lemmas for subgraphs to work? There are a number of useful definitions and lemmas for subgraphs that reflect lemmas about simple graphs. Right now in the PR, they use ' to distinguish them. For example, simple_graph.edge_set versus subgraph.edge_set'. It seems like it would be sensible going for subgraph.edge_set since namespaces or dot notation can distinguish them.

[Kyle Miller]

I'm also wondering about where subgraph should live. It seems like the name will conflict with subgraphs of other types of graphs, like multigraphs. Should it be put into the simple_graph namespace?

[Hunter Monroe]

My thought was to put subgraph under simple_graph, and in the next PR generalize to allow directed graphs, etc.

[Kyle Miller]

Right now subgraph is not in the simple_graph namespace -- it might be the combinatorics.simple_graph.subgraph module, but inside the file you have to manage namespaces yourself. I'm essentially suggesting that inside this module, there should be namespace simple_graph rather than open simple_graph, but I'm wondering what other graph theorists think.

[Kyle Miller]

Hunter Monroe said:

in the next PR generalize to allow directed graphs, etc.

Would you mind discussing this in a new topic here in the #graph theory stream? Even simple_graph went through a good amount of redesign before it made it into mathlib.

[Hunter Monroe]

@Kyle Miller I see two options for pursuing that issue: (1) put this version of subgraph in the simple_graph namespace since it clearly only applies to simple graphs given the presence of sym', and delay broader discussions about a broader structure that encompasses multigraphs and directed graphs while wrapping up this PR (this is my preference), or (2) consider the broader structure including how subgraph fits in before wrapping up this PR. I am worried that we could get bogged down this way, and there is some history of that. We could get lost trying to build a subgraph concept for directed multi hypergraphs. If I have misunderstood the question you are asking, let me know.

[Kyle Miller]

@Hunter Monroe (1) is what I meant. I had been expecting each notion of graph will have its own notion of subgraph, which is why I bring this up.

[Kyle Miller]

(For some context, I had written about three or four different definitions of subgraph, and after some experimentation the one you've kindly PR'd seemed to be the best one. There wasn't really anything that used subgraphs yet, so the work to polish it and PR it hadn't happened...)

[Kyle Miller]

By the way, I knew that there was some place where I had developed it more (like when I mentioned there was a version when I had removed all the primes), and I just found it: https://github.com/leanprover-community/mathlib/blob/simple_graph_matching/src/combinatorics/simple_graph/subgraph.lean (sorry)

[Kyle Miller]

I also understand the purpose of adj_symm now. It's that symmetric is a one-way implication, but it's nice to have it as an iff.

[Kyle Miller]

@Hunter Monroe By the way, I'm happy to help with merging this subgraph.lean with yours for the PR.

[Hunter Monroe]

I will give it a try.

[Kyle Miller]

Feel free to defer as much as you want to a later PR. ( Also, I'm not sure all of it makes sense.)

It turns out there's also a bunch of stuff about homomorphisms here https://github.com/leanprover-community/mathlib/blob/simple_graph_matching/src/combinatorics/simple_graph/hom.lean (This can also wait)

[Yaël Dillies]

Kyle Miller said:

I also understand the purpose of adj_symm now. It's that symmetric is a one-way implication, but it's nice to have it as an iff.

Then it should be called adj_comm

[Yaël Dillies]

The rule is unfortunately quite lax, but having symmlemmas to be one-way and comm lemmas to be two-ways (so including equality) is pretty useful to the ear.

[Kyle Miller]

I wasn't aware of this convention -- this should be fixed in simple_graph/basic.lean then with edge_symm, which probably should be called adj_comm. (I don't remember how it got the name edge_symm exactly.)

[Kyle Miller]

Maybe it would make sense to rename sym in the simple_graph structure to adj_symm, add the @[symm] attribute to it, and delete the edge_symm' lemma. (This might not all work due to the obviously autoparam.)

(If I recall, it's sym rather than symm so it doesn't conflict with the symm in the root namespace, which isn't actually used by the library.)

[Hunter Monroe]

@Kyle Miller actually yes could you help with this? Merging subgraph.lean would also affect basic.lean including additional code from hom.lean.

Kyle Miller said:

Hunter Monroe By the way, I'm happy to help with merging this subgraph.lean with yours for the PR.

[Kyle Miller]

Thanks for your work, @Hunter Monroe, to get this PR together. I think I'm done editing now.

[Kyle Miller]

Oh, there are some linter errors and other errors to fix still. I'll try to take care of those

[Kyle Miller]

#8223 seems ready for more review

Part of this, I changed edge_symm to adj_comm, as suggested by @Yaël Dillies

[Hunter Monroe]

Looks good, let's see what the reviewers think.

Here is an approach for handling any type of graph in one framework. A typeclass graph has a set of vertices V, a type E for edges which is a multiset, and a function incidence that maps each edge to a subset of V. This is enough to define a generic approach to subgraphs and maps. An instance specifies what an edge is: an unordered pair of V without loops and without duplication (graph), an ordered pair of V with the same constraints (direct graph), edges with more than two vertices with the same constraints with permuting those vertices gives the same edge (hypergraph), without such permuting (directed hypergraph), and allow duplication (multigraph), etc. The condition for G' to be a subgraph of G is generic: given any subset VS of V, the multiset of edges of G' incident on VS is a submultiset of the multiset of edges of G incident on VS. The maps can also be defined generically. All the action happens in the definition of edge. The constraints can be stated generically: has_symm (permuting the vertices gives the same edge), no_loops, 2_edge (two vertices per edge), n_edge (hypergraphs), no_dups (does not hold for multigraphs).

[Kyle Miller]

Here's a proposal along those lines (and similar to something I worked on for a while to try to make it so that submultigraphs could be used as if they were multigraphs):

class graph_like (α : Type*) :=
(V : α → Type*)
(E : α → Type*)
(incidence : Π (G : α), E G → set (V G))

-- Example instance
instance (V : Type*) : graph_like (simple_graph V) :=
{ V := λ G, V,
  E := λ G, G.edge_set,
  incidence := λ G e, {v : V | v ∈ (e : sym2 V)} }

A tradeoff with this is that you lose dot notation if you only have generic code.

There's also a question about whether having generic code will result in less code overall.

[Kyle Miller]

Before the definition of subgraph that was in this PR, there was a definition involving a subset of the edge set of the simple graph, rather than a sub-relation of the adjacency relation. This wasn't so easy to work with because there were levels of stuff you had to get through (like sym2).

[Kyle Miller]

To be clear, I do like this idea of having something that would let there be generic definitions, and I like the ideas you have. The design trick is figuring out how to do this in a way that is ergonomic and that definitely makes things simpler. It's worth designing something generic, even right now, but also I think in the short term making non-generic things is a good way to inform a generic design.

Re ergonomics: if anyone looks at that directed_graph definition I made, one annoying problem is that the adjacency relation G.adj v w renders as G.to_directed_graph.adj v w. Maybe a reducible definition can fix this? I was wanting to avoid a notation, but perhaps there will eventually a v ~[G] w defined by something like

notation v `~[` G `]` w := ∃ (e : graph_like.E G), graph_like.incidence G e = {v, w}

[Yaël Dillies]

Hunter are you sure this works that great with hypergraphs? Hypergraphs want set V → Prop and multigraphs want V → V → Prop.

[Yaël Dillies]

Kyle Miller said:

Here's a proposal along those lines (and similar to something I worked on for a while to try to make it so that submultigraphs could be used as if they were multigraphs):

I actually kind of like this presentation! Not being a multigraph then becomes injective incidence. The problem I see is that set (V G ) doesn't allow you to express oriented edges. Also, we don't have to use only generic code. We can redefine functions for every kind of graphs we care about and use the common API to avoid boilerplate.

[Kyle Miller]

An unspoken idea here is that this is only giving a common interface. A directed graph is free to peer into the E type, for example.

[Kyle Miller]

I'm curious what you mean about set V -> Prop and V -> V -> Prop. What's the objection?

[Kyle Miller]

Here's another multigraph definition along with a graph_like instance:

/-- Multigraphs as graphs with labeled edges. An edge is identified with the
unordered pair of endpoints and the label. -/
structure multigraph (V : Type*) (α : Sort*) :=
(links : set (α × V × V))
(sym : prod.map id prod.swap '' links = links)

def multigraph.is_simple {V : Type*} {α : Sort*} (G : multigraph V α) :=
∀ {a : α} {v w : V}, (a,v,w) ∈ G.links → v ≠ w

def multigraph.edges {V : Type*} {α : Sort*} (G : multigraph V α) : set (α × sym2 V) :=
(λ (l : α × V × V), (l.1, ⟦(l.2.1, l.2.2)⟧)) '' G.links

instance (V : Type*) (α : Sort*) : graph_like (multigraph V α) :=
{ V := λ _, V,
  E := λ G, G.edges,
  incidence := λ G e, {v : V | v ∈ e.1.2}}

[Kyle Miller]

I like how this definition of multigraph exposes some useful parameters, lets you give edges identity, and is fairly simple. It even would have a lattice instance. (The seemingly unattainable property is to also have it so that the degree-sum formula will work with loop edges without special casing or having a significantly more complicated definition. Here, there is a single element of links for loop edges, and two elements for non-loop edges.) The "links" terminology comes from a paper by Chou, "A formal theory of undirected graphs in higher-order logic", 1994. In that paper, there are additional constraints that each edge has its own unique label and all the labels are used. I think that can be relaxed.