paths

Stream: graph theory

[Jalex Stark]

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]

the code is in this repo
https://github.com/apurvnakade/mc2020-projects

[Jalex Stark]

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]

so then we made an implementation with lists at the core

[Jalex Stark]

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

[Jalex Stark]

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]

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

[Jalex Stark]

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]

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]

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]

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]

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

[Aaron Anderson]

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)

[Alena Gusakov]

Ohhh okay gotcha

[Alena Gusakov]

Interesting

[Aaron Anderson]

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

[Alena Gusakov]

Makes sense

[Aaron Anderson]

and there are some ok lemmas for functions from fin

[Alena Gusakov]

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

[Aaron Anderson]

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]

*make induction easier for me to follow lol

[Aaron Anderson]

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

[Aaron Anderson]

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

[Aaron Anderson]

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

[Aaron Anderson]

(deleted)

[Jalex Stark]

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]

starting with induction_on

[Alena Gusakov]

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

[Alena Gusakov]

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

[Aaron Anderson]

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

[Aaron Anderson]

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

[Aaron Anderson]

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

[Aaron Anderson]

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

[Alena Gusakov]

Yeah that makes sense

[Alena Gusakov]

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]

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

[Alena Gusakov]

Yeah true

[Jalex Stark]

from my point of view, nat subtraction is never convenient

[Aaron Anderson]

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]

this is the road to dependent type hell

[Aaron Anderson]

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

[Jalex Stark]

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]

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

[Jalex Stark]

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]

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

[Aaron Anderson]

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

[Jalex Stark]

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

[Aaron Anderson]

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

[Aaron Anderson]

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]

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

[Aaron Anderson]

Jalex Stark said:

starting with induction_on

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

[Jalex Stark]

I think so

[Kyle Miller]

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]

Oof, that’s a good point

[Kyle Miller]

(moving discussion back to paths from maximal path)

[Kyle Miller]

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]

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

[Kyle Miller]

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

[Alena Gusakov]

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]

@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]

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

[Aaron Anderson]

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

[Kyle Miller]

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]

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]

But I think path is really a multigraph definition

[Aaron Anderson]

Because of edge injectivity

[Aaron Anderson]

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

[Kyle Miller]

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

[Kyle Miller]

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]

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

[Aaron Anderson]

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

[Aaron Anderson]

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

[Kyle Miller]

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]

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