## Stream: graph theory

### Topic: paths

#### Jalex Stark (Aug 12 2020 at 03:44):

Michael Hahn took a stab at defining eulerian circuits, with the intent to cross the konigsberg bridges problem off of freek's 100 theorem list

#### Jalex Stark (Aug 12 2020 at 03:45):

the code is in this repo

#### Jalex Stark (Aug 12 2020 at 03:47):

we tried for a bit using the inductive type of paths defined in the hedetniemi branch, but we felt like we were reimplementing basic list API

#### Jalex Stark (Aug 12 2020 at 03:53):

so then we made an implementation with lists at the core

#### Jalex Stark (Aug 12 2020 at 03:54):

the compatibility condition called p.adj is not quite right, maybe it's enough to separate it into three structure fields

#### Jalex Stark (Aug 12 2020 at 04:00):

Alena then started to use the same definition of path, with the goal of characterizing trees as graphs in which any pair of points has a unique path between them

#### Jalex Stark (Aug 12 2020 at 04:01):

her code is in yet another repo
https://github.com/agusakov/graph_theory_2020

#### Jalex Stark (Aug 12 2020 at 04:04):

I think michael proves that a vertex is incident to an odd number of edges in a path if and only if the path is not a cycle and the vertex is the head or tail,
up to several sorries which are somewhere between basic API and basic theorems

#### Jalex Stark (Aug 12 2020 at 04:05):

I guess both of these authors have reasons for writing in their own repo, but hopefully after the process of their first PRs, they'll see the light and want to work in branches on the mathlib repo

#### Aaron Anderson (Aug 12 2020 at 04:07):

A good test of a path definition for simple graphs would be proving that powers of adjacency matrices count paths (https://github.com/leanprover-community/mathlib/pull/3672)

#### Aaron Anderson (Aug 12 2020 at 04:10):

Jalex Stark said:

Alena then started to use the same definition of path, with the goal of characterizing trees as graphs in which any pair of points has a unique path between them

I'd be interested to see how easy it is to translate between the path-connected definition of connected that Alena is using and an inductive definition of connected

#### Aaron Anderson (Aug 12 2020 at 04:11):

where by inductive definition I guess I mean the transitive closure of adjacency

#### Aaron Anderson (Aug 12 2020 at 21:35):

This is the totally-not-battle-tested definition of a path I'm pulling out of thin air:

structure path (n : ℕ) :=
(vertex_map : fin (n + 1) → V)
(edge_map : fin n → E)
(reasonable_definition : the edges connect the right vertices)


Ohhh okay gotcha

Interesting

#### Aaron Anderson (Aug 12 2020 at 21:37):

It's less good for defining connectedness, but it'd nice to just say that the vertex map or the edge map is injective

Makes sense

#### Aaron Anderson (Aug 12 2020 at 21:37):

and there are some ok lemmas for functions from fin

#### Alena Gusakov (Aug 12 2020 at 21:38):

It might also make induction easier I think? In like, really specific cases lol

#### Aaron Anderson (Aug 12 2020 at 21:39):

I think it'd make induction marginally harder, because lists are literally an inductive type, but fin has some definitions like fin.tail and fin.init to work around that

#### Alena Gusakov (Aug 12 2020 at 21:40):

*make induction easier for me to follow lol

#### Aaron Anderson (Aug 12 2020 at 21:40):

One place I think it would be better is proving the adjacency matrix formula for counting paths

#### Aaron Anderson (Aug 12 2020 at 21:42):

@Jalex Stark, just want to invite your critique on this alternate definition of a path

#### Aaron Anderson (Aug 12 2020 at 21:43):

or maybe, I'll move to the paths stream...

(deleted)

#### Jalex Stark (Aug 12 2020 at 21:44):

Aaron Anderson said:

This is the totally-not-battle-tested definition of a path I'm pulling out of thin air:

structure path (n : ℕ) :=
(vertex_map : fin (n + 1) → V)
(edge_map : fin n → E)
(reasonable_definition : the edges connect the right vertices)


I think the right test is to reimplement the API we already have

#### Jalex Stark (Aug 12 2020 at 21:44):

starting with induction_on

#### Alena Gusakov (Aug 12 2020 at 21:45):

please make it be (vertex_map : fin n → V) and (edge_map : fin (n - 1) → E)

#### Alena Gusakov (Aug 12 2020 at 21:46):

though I guess that would be bad for cases where you don't have vertices

#### Aaron Anderson (Aug 12 2020 at 21:47):

Unfortunately, I think you really can't do that... maybe you'd have to make it path (n + 1) :='...

#### Aaron Anderson (Aug 12 2020 at 21:47):

Also, it really is pretty standard in the literature to have the length of a path be the number of edges

#### Aaron Anderson (Aug 12 2020 at 21:48):

See for instance the adjacency matrix formula. The entries of $A ^ n$ count paths with $n$ edges

#### Aaron Anderson (Aug 12 2020 at 21:48):

and if you concatenate two paths, you add the number of edges, but not vertices

#### Alena Gusakov (Aug 12 2020 at 21:48):

Yeah that makes sense

#### Alena Gusakov (Aug 12 2020 at 21:49):

For some reason I feel like the way I learned about path lengths is counting the number of vertices but maybe it's such a small detail that I didn't pay attention and have just misremembered it

#### Jalex Stark (Aug 12 2020 at 21:49):

i mean, regardless of whether you remember correctly what your prof said, we should use the definition that's most convenient

Yeah true

#### Jalex Stark (Aug 12 2020 at 21:50):

from my point of view, nat subtraction is never convenient

#### Aaron Anderson (Aug 12 2020 at 21:50):

Actually, concatenation would be even easier if you make the path definition even more dependent...

structure path_from (a b : V) (n : ℕ) :=
(vertex_map : fin (n + 1) → V)
(edge_map : fin n → E)
(reasonable_definition : the edges connect the right vertices)
(starts_at : vertex_map 0 = a)
(ends_at : vertex_map n = b)


#### Jalex Stark (Aug 12 2020 at 21:50):

this is the road to dependent type hell

#### Aaron Anderson (Aug 12 2020 at 21:50):

That'd be the definition I'd recommend if we were, say, just trying to define the fundamental group...

#### Jalex Stark (Aug 12 2020 at 21:51):

michael and I start with the G.path a b type and then I rewrote everything so that the source and sink were properties instead of part of the type

#### Jalex Stark (Aug 12 2020 at 21:51):

because i just didn't know how to prove some of the bits of the API

#### Jalex Stark (Aug 12 2020 at 21:52):

I think patrick massot and co. have put a definition of path connected topological spaces into mathlib recently, and they were trying to optimize for making it natural to define the fundamental groupoid form there

#### Aaron Anderson (Aug 12 2020 at 21:52):

If it really is infeasible that way, then my definition's just a subtype, which is not bad at all

#### Aaron Anderson (Aug 12 2020 at 21:53):

but I would recommend following whatever convention team path connected are doing

#### Jalex Stark (Aug 12 2020 at 21:54):

yes, I don't remember but maybe i can quickly find the code

#### Aaron Anderson (Aug 12 2020 at 21:54):

It looks like they do define a path as dependent on endpoints (obviously not length)

#### Aaron Anderson (Aug 12 2020 at 21:57):

I agree that defining a path in terms of source and target sounds like a pain if you're working with lists, but I think it might be nicer if you're working with fin-tuples

#### Jalex Stark (Aug 12 2020 at 21:59):

i'll think more carefully about any definition you propose after you prove path.cons and path.induction_on with it

#### Aaron Anderson (Aug 12 2020 at 21:59):

Jalex Stark said:

starting with induction_on

Did y'all ever get that working with the induction tactic?

I think so

#### Kyle Miller (Aug 13 2020 at 00:38):

Aaron Anderson said:

One place I think it would be better is proving the adjacency matrix formula for counting paths

We should probably make sure we match graph theory terminology. It bugs me as a topologist, but they call paths walks.

(I'm just quoting @Aaron Anderson's comment because somehow that's what made me remember. Counting paths is harder than counting walks.)

#### Aaron Anderson (Aug 13 2020 at 00:46):

Oof, that’s a good point

#### Kyle Miller (Aug 13 2020 at 00:56):

(moving discussion back to paths from maximal path)

#### Kyle Miller (Aug 13 2020 at 00:57):

Ok, one difference between my proposal and the structure for walks from before is that you can't specify the starting and ends points of the path. However, that's always just a subtype away

#### Kyle Miller (Aug 13 2020 at 00:58):

with walks G v w := {p : P n \graphmap G // p 0 = v /\ p n = w

#### Kyle Miller (Aug 13 2020 at 00:59):

(This would be using a coe_to_fn from graphmaps to maps on vertex sets, if that makes any sense to have.)

#### Alena Gusakov (Aug 13 2020 at 01:00):

This is how I was taught too

We should probably make sure we match graph theory terminology. It bugs me as a topologist, but they call paths walks.

#### Kyle Miller (Aug 13 2020 at 01:05):

@Alena Gusakov I'm always tempted to call them paths because of homotopy theory, which is probably the story with everyone else, too. (It's nice that "path connected" still means the same thing, since if two vertices are connected by a walk, then they are also connected by a path. If this weren't the case, I might have been inclined to use the homotopy theory terminology instead.)

#### Alena Gusakov (Aug 13 2020 at 01:06):

Ah yeah, I'm probably one of the people least familiar with homotopy theory here lol

#### Aaron Anderson (Aug 13 2020 at 01:06):

So, walks, loops, and cycles work well with homomorphisms and embeddings

#### Kyle Miller (Aug 13 2020 at 01:06):

I think this is a good test for which ever definition of walks we choose: can you prove that every pair of vertices connected by a walk is connected by a path? (Stronger: can you prove this walk uses a subset of the edges of the walk?)

#### Kyle Miller (Aug 13 2020 at 01:07):

I mean, you'll be able to prove it no matter the definition, I think, but it's a good check for whether it's a good definition.

#### Aaron Anderson (Aug 13 2020 at 01:07):

But I think path is really a multigraph definition

#### Aaron Anderson (Aug 13 2020 at 01:07):

Because of edge injectivity

#### Aaron Anderson (Aug 13 2020 at 01:08):

By the way, since we’re talking about graph homomorphisms and embeddings, check out #3750

#### Kyle Miller (Aug 13 2020 at 01:12):

@Aaron Anderson Good point about paths being a multigraph definition due to edge injectivity.

#### Kyle Miller (Aug 13 2020 at 17:42):

Aaron Anderson said:

By the way, since we’re talking about graph homomorphisms and embeddings, check out #3750

Would you mind explaining how this applies to graph homomorphisms and embeddings? I'm not familiar with order theory, but it seems like it could be useful.

#### Aaron Anderson (Aug 13 2020 at 18:26):

The definition has 0 to do with orders a priori, which is why I’m renaming it

#### Aaron Anderson (Aug 13 2020 at 18:26):

It just says basically that an embedding/equiv maps one relation to another

#### Aaron Anderson (Aug 13 2020 at 18:27):

So if you plug in two graph adjacency relations, you get graph embeddings

#### Kyle Miller (Aug 13 2020 at 18:29):

Oh, ok, that's a nice thing to have. Once you get that in, maybe I should wire sym2 up to it, too, since it has a map function. I guess relating sym2.from_rel, map, and those relation mapping functions.

#### Aaron Anderson (Aug 13 2020 at 18:41):

You could do it now with order_embedding, as long as you rename it rel_embedding` when the PR merges

Last updated: May 08 2021 at 22:13 UTC