## Stream: graph theory

### Topic: maximal paths via zorn?

#### Alena Gusakov (Aug 12 2020 at 19:34):

Question: I want to prove that, in any given graph G over vertex set V, there exists a path of maximum length. The way I want to prove it is, since path.length maps to ℕ, I want to try to use Zorn's lemma to show that there is a maximum

import .basic

universes u
variables {V : Type u}

namespace simple_graph
variables (G : simple_graph V)

/-- Morally, a path is an alternating list of vertices and edges,
with incidences between adjacent objects -/
@[ext] structure path :=
(head : V)
(tail : list V)
(edges : list G.E)
(length_eq : edges.length = tail.length)
(adj : ∀ (n : ℕ) (hn : n < edges.length),
let u := (list.cons head tail).nth_le n (by { simp; omega }) in
let v := (list.cons head tail).nth_le (n + 1) (by { simp, cc }) in
u ≠ v ∧ u ∈ edges.nth_le n hn ∧ v ∈ edges.nth_le n hn)

namespace path
variables {G}
variables (p : G.path)

/-- The ordered list of all vertices in p, starting at p.head and ending at p.sink. -/
def vertices : list V := p.head :: p.tail

/-- The number of edges in p. -/
def length : ℕ := p.tail.length
-- should probably make sure this doesn't become a problem if we run into infinite graphs?

variables {p}

/-- p.vertex_mem v holds if v is a vertex along path p. -/
def vertex_mem (v : V) (p : G.path) : Prop := v ∈ p.vertices
instance has_mem_vertices : has_mem V G.path :=
{ mem := vertex_mem }
variables (p)

/-- The empty path based at vertex v. -/
@[simps]
def empty (G : simple_graph V) (v : V) : G.path :=
{ head := v,
tail := list.nil,
edges := list.nil,
length_eq := rfl,
adj := by rintros _ ⟨_⟩ }

instance [inhabited V] : inhabited G.path := { default := empty G (arbitrary V) }

@[simp]
lemma empty_length (v : V) : (empty G v).length = 0 := by refl

/-- p.is_tour if p has no repeated vertices. -/
def is_tour : Prop := list.nodup p.vertices
-- maybe prove that is_tour → is_trail

/-- p.is_maximum if the length of p is greater than or equal to the length of every other path. -/
def is_maximum : Prop := p.is_tour ∧ ∀ (q : path G), q.length ≤ p.length

/- there exists a path, path.is_tour, s.t. path.is_maximal -/
-- CR : can be generalized to infinite graphs
lemma fin_max_tour [fintype V] [inhabited V]: ∃ (p : path G), p.is_maximum :=
begin

sorry,
end

end path

end simple_graph


#### Alena Gusakov (Aug 12 2020 at 19:35):

So this mwe is as minimal as it gets I think, as long as your definition of simple_graph isn't too far off from the one I'm using it should be fine

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

Hopefully you don't need anything as powerful as Zorn.

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

is_maximum is only based on the ranking by length, so I would look at the set of naturals that are the length of some path.

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

I sort of suspect I might :/ I think the proof of a maximum path needs to build on the existence of maximal paths (i.e. local maximum)

#### Alena Gusakov (Aug 12 2020 at 19:41):

My question is, how do I obtain that set exactly?

#### Alena Gusakov (Aug 12 2020 at 19:43):

I have the map into the naturals, it's just length, but I'm struggling to phrase the fact that there is some path that maps to the greatest number

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

one approach would be {n : ℕ | ∃ (p : G.path), p.length = n}

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

but I think also you could use the image API

#### Aaron Anderson (Aug 12 2020 at 19:44):

and say something like (length : G.path → ℕ) '' set.univ

#### Aaron Anderson (Aug 12 2020 at 19:45):

Either way, your goal is to show that set is finite/bounded. Then there should be a lemma somewhere that says it has a maximum.

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

Ahh gotcha. Didn't know I could declare sets like that

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

Yeah I'm working on another lemma that says path lengths can't go over the cardinality of V if we have fintype V

#### Aaron Anderson (Aug 12 2020 at 19:45):

Once you have that maximum, you just look back at the preimage, and any of those paths should be a maximum path by your definition

#### Aaron Anderson (Aug 12 2020 at 19:46):

I know that there exists something called finset.max and something called finset.max', which should be useful

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

Great, thank you!

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

and it'd be extra-useful to have a fintype G.path instance, because then your set of paths could be (length : G.path → ℕ) '' finset.univ, which is already a finset

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

We have that duplicate edges can't happen and we also havefintype V, that should be enough to prove fintype G.path.is_tour right? (I assume I can just say G.path.is_tour to refer to the collection of paths that don't repeat any vertices?)

#### Alena Gusakov (Aug 12 2020 at 19:50):

G.path currently allows for paths to loop back on themselves

#### Alena Gusakov (Aug 12 2020 at 19:53):

Now that I think about it, proving and then using the fact that fintype G.path.is_tour is a good way of proving the lemma, though I think both that and the fact that the lengths are bounded above by V.card are useful in their own ways

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

Knowing that a set of naturals is bounded above should be enough to show it has a maximum, I'm just not sure where in the API that is

#### Aaron Anderson (Aug 12 2020 at 20:00):

Aha, nat has a conditionally_complete_linear_order instance

#### Aaron Anderson (Aug 12 2020 at 20:01):

so you can take Sups of arbitrary bounded sets of naturals

Perfect, thanks!

#### Aaron Anderson (Aug 12 2020 at 20:02):

The order library is disturbingly powerful, but also inscrutable at first, because nobody teaches much order theory notation in regular math classes

#### Alena Gusakov (Aug 12 2020 at 20:11):

Also, if you don't mind me asking, what's wrong with using Zorn's lemma? Isn't it basically just an axiom? Or is the issue that we want to avoid assuming too much

#### Aaron Anderson (Aug 12 2020 at 20:12):

There's a general preference in math to use the minimum amount of choice you need

#### Aaron Anderson (Aug 12 2020 at 20:13):

That's extra-true in computer formalization with constructive elements, because invoking choice is clunkier on a computer than our mathematician intuitions might guess

#### Aaron Anderson (Aug 12 2020 at 20:14):

and some people in the community would probably prefer we didn't use it at all, but they've long lost that debate in mathlib

#### Aaron Anderson (Aug 12 2020 at 20:15):

But the real reason is that Zorn kind of obscures what's really going on

#### Aaron Anderson (Aug 12 2020 at 20:15):

what's really going on here is that bounded sets of natural numbers have maxima

#### Aaron Anderson (Aug 12 2020 at 20:16):

and in order to invoke Zorn for paths, you need to first show that all chains of paths have upper bounds

#### Aaron Anderson (Aug 12 2020 at 20:17):

but if you translate that into natural numbers, all sets of natural numbers are chains, so it's the same as showing your sets have maxima

#### Alena Gusakov (Aug 12 2020 at 20:17):

Right, yeah that was my thought with maximal paths

#### Aaron Anderson (Aug 12 2020 at 20:17):

and then also, the result you get is about maximal paths, which are different than maximum paths as you've defined them

#### Alena Gusakov (Aug 12 2020 at 20:17):

But I guess it is easier to just say bounded sets of natural numbers have maxima

#### Alena Gusakov (Aug 12 2020 at 20:18):

Yeah but I was saying I could use the maximal paths result for the maximum path lemma

#### Aaron Anderson (Aug 12 2020 at 20:18):

Yeah, it gets you the result you want, and you'd need to prove that anyway to invoke Zorn, so Zorn is just an extra step

I gotcha

#### Aaron Anderson (Aug 12 2020 at 20:18):

How would you get from maximal paths to maximum paths? I feel like you'd still be showing that a set of lengths has a maximum...

#### Alena Gusakov (Aug 12 2020 at 20:20):

I was thinking that the chains would be like, "sub"-paths of larger paths

#### Alena Gusakov (Aug 12 2020 at 20:20):

So smaller paths whose edge sets intersect with the larger path

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

I've was working through Dummit and Foote a couple of hours ago and there was a similar proof for maximal subgroups so I might be overcomplicating things

#### Aaron Anderson (Aug 12 2020 at 20:24):

Yeah, Zorn's lemma is a very specific recipe, which is great for making minimal and maximal algebraic widgets, because those things are a very specific sort of lattice really

#### Alena Gusakov (Aug 12 2020 at 20:25):

I think I might've just misunderstood that recipe

#### Alena Gusakov (Aug 12 2020 at 20:26):

something something if you have a hammer everything looks like a nail

#### Aaron Anderson (Aug 12 2020 at 20:26):

There's a reason it took people ages to realize it was needed as a separate axiom...

#### Aaron Anderson (Aug 12 2020 at 20:27):

I've definitely been guilty of looking for nails to hammer with Zorn, but I've also found myself on an algebra qual, trying to build a maximal widget, and then failed to find the right poset to do Zorn in, so I handwrote a 2 page transfinite induction proof instead...

Oh god lmao

#### Aaron Anderson (Aug 12 2020 at 20:28):

mercifully I'm in a department with enough logicians that that still got full credit, even if it's objectively worse than just modifying the poset slightly and hitting it with Zorn like some of my friends did

#### Alena Gusakov (Aug 12 2020 at 20:28):

Yeah I probably should've thought out the difference between maximal/maximum more before starting with this lemma

#### Aaron Anderson (Aug 12 2020 at 20:29):

That distinction between maximal and maximum-size is gonna pop up all the time in graph theory...

#### Alena Gusakov (Aug 12 2020 at 20:30):

Yeah my combinatorics professor mentioned it a lot, I probably should be more careful about it

#### Alena Gusakov (Aug 12 2020 at 20:30):

Especially since I'm now realizing that the next lemma that I wanted to prove only requires maximal paths and not maximum lol

#### Alena Gusakov (Aug 12 2020 at 20:31):

Maximum path is easier though

#### Aaron Anderson (Aug 12 2020 at 20:31):

TBH I think the easiest way to prove the existence of maximal paths here is by proving the existence of maximum paths, and observing that those are maximal

#### Alena Gusakov (Aug 12 2020 at 20:32):

The next lemma is that trees contain two vertices of degree one, which means the existence of a maximal (or maximum) path

Gotcha

#### Alena Gusakov (Aug 12 2020 at 20:32):

Yeah my professor used maximal paths in his proof but I'm not quite sure why now

#### Aaron Anderson (Aug 12 2020 at 20:33):

Verbally, it's easier to describe why maximal tours exist

#### Aaron Anderson (Aug 12 2020 at 20:33):

just keep walking until you can't

This is true

#### Alena Gusakov (Aug 12 2020 at 20:35):

I don't think we ever proved the existence of maximal/maximum paths in class but I'm probably being overly nitpicky at this point

#### Alena Gusakov (Aug 12 2020 at 20:35):

Cause it's one of those things that's "obvious" I guess

#### Alena Gusakov (Aug 12 2020 at 20:53):

If I wanted to prove that the path lengths are all bounded above by V.card, would this be the right way to go about it? Or is it still overcomplicating things

instance : has_Sup {n : ℕ | ∃ (p : G.path), p.is_tour ∧ p.length = n} :=
begin
sorry,
end


#### Alena Gusakov (Aug 12 2020 at 20:55):

I also have this lemma

/- length of path.is_tour is less than or equal to the cardinality of V -/
lemma tour_le_card [fintype V] : ∀ (p : path G) (hp : p.is_tour), p.length < fintype.card V :=
begin
intros,
unfold is_tour at hp,
sorry,
end


#### Alena Gusakov (Aug 12 2020 at 20:57):

I've seen people prove lemmas and then use those lemmas in instances so that the objects they're working with have the properties they need, so I'm trying to imitate that

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

You want to use the Sup functionality of conditionally_complete_lattice, right?

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

The Sup function is defined there for all possible sets of naturals you might want to take Sups of, but it only conditionally has the property of really being a supremum

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

If you look at the docs here https://leanprover-community.github.io/mathlib_docs/order/conditionally_complete_lattice.html

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

The relevant aspects of that structure are things like this: le_cSup : ∀ (s : set α) (a : α), bdd_above s → a ∈ s → a ≤ conditionally_complete_lattice.Sup s

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

So what you want to show is bdd_above set_of_relevant_paths

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

actually, what might be a better idea

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

is to look at how that Sup is defined

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

it's defined using nat.find, which might have even more convenient facts proved about it

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

I think you can do it with either one, so just take a look at the docs for both and see which you prefer

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

nat.find takes in an exists statement, and finds you the minimum natural number satisfying that statement

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

I don't think I get how to use either method, but I'll poke around the docs and code to see if I can figure it out

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

ok, let me know if you stay stuck, but either method should be able to get you from the lemma tour_le_card to the least upper bound, and then you prove that that least upper bound is the maximum, and that there exists a path that has that exact length, which is thus a maximum path

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

although with your naming, you might want to call that tour_lt_card, as le refers to "Less than or Equal to" while lt refers to "Less Than"

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

I keep switching back and forth between wanting to count the vertices vs the edges in the path lengths cause it seems like counting edges is the convention in the code I've copied, but I prefer vertices lol

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

Hence not updating the name when I switched to counting edges for consistency

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

hot take: maybe the definition of a path should be dependent on a natural number length

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

YEAH I've been thinking about that, I can't say I recall seeing anything that avoids infinitely long paths

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

Uhh lists are finitely long, so these would be isomorphic

Ohh okay phew

Misread then

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

I thought you were saying the definition of a path should have the condition that the length is finite

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

Alena Gusakov said:

YEAH I've been thinking about that, I can't say I recall seeing anything that avoids infinitely long paths

Speaking of infinitely long paths, one use of them is in Konig's lemma. Should we consider infinitely long paths to be fundamentally different from finite paths? It probably is nice enough having a map that gives finite truncations of an infinite path.

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

If we define paths using maps from fin n, then it’s easier to generalize to N...

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

I wonder if it's worth not defining paths per se, but instead using graph homomorphisms (to be defined) from path graphs to a given graph.

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

so you'd write (n : nat) (p : P n \embeds G) as arguments, where \embeds is some relevant arrow

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

I’m tempted, but I’m not sure all the walky definitions are easy to describe that way

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

then there'd be the infinite path graph Ray along with embeddings P n \embeds Ray for each n, and so you'd get these truncations as restrictions of Ray \embeds G

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

It’s for sure better to define infinite paths that way

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

and a walk would be a non-embedding from P n to G.

It seems like the complexity would be about the same as for the structures for walks given in the paths topic

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

A loop is exactly a homomorphism from a cycle graph

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

We probably should move over to the paths topic

Right

#### Alena Gusakov (Aug 13 2020 at 02:05):

I'm still having trouble with finding Sup

#### Alena Gusakov (Aug 13 2020 at 02:05):

Bhavik helped me out with this

lemma finset_card_le_fintype_card {α : Type*} [fintype α] (s : finset α) : s.card ≤ fintype.card α :=
finset.card_le_of_subset (finset.subset_univ _)

/- length of path.is_tour is less than the cardinality of V -/
lemma tour_lt_card [fintype V] [decidable_eq V] (p : path G) (hp : p.is_tour) :
p.length < fintype.card V :=
begin
rw [nat.lt_iff_add_one_le, ← vertices_length, ← list.to_finset_card_of_nodup hp],
apply finset_card_le_fintype_card,
end


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

We have a new fintype lemma there too

#### Alena Gusakov (Aug 13 2020 at 02:08):

But with

instance : has_Sup {n : ℕ | ∃ (p : G.path), p.is_tour ∧ p.length = n} :=
begin
sorry,
end


I wasn't really able to figure out how to use either nat.find or bdd_above

#### Bhavik Mehta (Aug 13 2020 at 02:08):

I don't think you want to be using has_Sup to express this idea, I think that'd be awkward to use in practice

#### Alena Gusakov (Aug 13 2020 at 02:09):

What would you recommend using?

#### Bhavik Mehta (Aug 13 2020 at 02:10):

one sec I'll type it out

#### Bhavik Mehta (Aug 13 2020 at 02:13):

∃ (p : G.path), p.is_tour ∧ ∀ (q : G.path), q.is_tour → q.length ≤ p.length

#### Alena Gusakov (Aug 13 2020 at 02:14):

I think that's sort of what I have

#### Alena Gusakov (Aug 13 2020 at 02:15):

I have python def is_maximum : Prop := p.is_tour ∧ ∀ (q : path G), q.length ≤ p.length

#### Alena Gusakov (Aug 13 2020 at 02:15):

And the lemma I want to prove is the existence of such a path

#### Bhavik Mehta (Aug 13 2020 at 02:15):

That definition isn't what you want, since it doesn't restrict q to be a tour

OH

#### Bhavik Mehta (Aug 13 2020 at 02:15):

So nothing satisfies that predicate

#### Alena Gusakov (Aug 13 2020 at 02:15):

yeah okay I gotcha

#### Bhavik Mehta (Aug 13 2020 at 02:16):

but you can modify it to include that, and then the lemma you want is just that such a thing exists

#### Bhavik Mehta (Aug 13 2020 at 02:16):

At the moment, you could just make a q going back and forth on two vertices (as long as there's at least one edge in the graph) so by that definition there is never a maximum

#### Bhavik Mehta (Aug 13 2020 at 02:16):

also that should probably be called maximal not maximum

#### Alena Gusakov (Aug 13 2020 at 02:17):

It's maximum, it's a global thing

#### Alena Gusakov (Aug 13 2020 at 02:17):

For all paths in G

#### Alena Gusakov (Aug 13 2020 at 02:17):

We had the back and forth over maximal/maximum earlier and decided on maximum cause it's easier

#### Bhavik Mehta (Aug 13 2020 at 02:18):

maximum vs maximal isn't about being global though, it's about uniqueness

#### Alena Gusakov (Aug 13 2020 at 02:18):

Is it? Maximum = global and maximal = local is how it was defined for me

#### Alena Gusakov (Aug 13 2020 at 02:18):

Cause you can have a path that's a local maximum

#### Bhavik Mehta (Aug 13 2020 at 02:19):

That's not how it's defined in https://en.wikipedia.org/wiki/Maximal_and_minimal_elements or https://www.math3ma.com/blog/maximal-not-maximum

#### Bhavik Mehta (Aug 13 2020 at 02:20):

In particular a graph can have multiple paths satisfying that definition, so none of them are "the maximum" but they all are maximal

#### Alena Gusakov (Aug 13 2020 at 02:20):

I think the blog has the same definitions as I do essentially nope

Yeah

#### Alena Gusakov (Aug 13 2020 at 02:20):

But we're not worried about uniqueness, we just need the existence of a path with maximum length

#### Bhavik Mehta (Aug 13 2020 at 02:21):

maximum length is different to maximum path though

#### Bhavik Mehta (Aug 13 2020 at 02:21):

Actually I guess it depends which order we're talking about

#### Alena Gusakov (Aug 13 2020 at 02:21):

I am referring to maximum length

#### Bhavik Mehta (Aug 13 2020 at 02:21):

If we're talking about the partial order on paths by inclusion, then it's maximal

Ah

#### Bhavik Mehta (Aug 13 2020 at 02:21):

maybe call it is_maximum_length then

#### Alena Gusakov (Aug 13 2020 at 02:22):

Actually you know what, I do think I have the same definitions of maximal/maximum as the blog

#### Alena Gusakov (Aug 13 2020 at 02:23):

Like if you have a maximal path p, and it's a "sub"-path of another path q, then q = p

#### Bhavik Mehta (Aug 13 2020 at 02:23):

Right, but there's no guarantee that a maximum path exists under inclusion

#### Bhavik Mehta (Aug 13 2020 at 02:23):

Even on a finite graph

#### Alena Gusakov (Aug 13 2020 at 02:23):

Sure but this isn't an inclusion argument, that's what I was trying to use before

#### Bhavik Mehta (Aug 13 2020 at 02:23):

But under length, a maximum path does exist

#### Alena Gusakov (Aug 13 2020 at 02:24):

Like, you can have multiple maximum paths right?

#### Bhavik Mehta (Aug 13 2020 at 02:24):

Right so I'm saying change the name to is_maximum_length

#### Bhavik Mehta (Aug 13 2020 at 02:24):

Because then it matches the def you had

Yeah, gotcha

#### Alena Gusakov (Aug 13 2020 at 02:25):

Yeah okay I see what you were saying

#### Alena Gusakov (Aug 13 2020 at 02:25):

I was stepping back and forth between the idea of chains of paths and the lengths of paths

#### Alena Gusakov (Aug 13 2020 at 02:27):

Without realizing that they're not at all interchangeable lmao

#### Aaron Anderson (Aug 13 2020 at 02:39):

What I was suggesting to use Sup for was not to add any new instances of has_Sup, but to show that there exists a tour of length Sup {n : ℕ | ∃ (p : G.path), p.is_tour ∧ p.length = n}

#### Aaron Anderson (Aug 13 2020 at 02:40):

This should equal nat.find (∃ n, \ (p : G.path), ∀ (p : path G), p.length ≤ n)

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

so you could use that too

#### Aaron Anderson (Aug 13 2020 at 02:47):

Let's say you use nat.find. Then what you want to show is that the output, a natural number, is actually the maximum path length.

#### Aaron Anderson (Aug 13 2020 at 02:48):

To do that, you need to show that there is no longer path, and that should come from nat.​find_spec, which basically says that your result is a witness to the ∃-statement.

#### Aaron Anderson (Aug 13 2020 at 02:49):

Then you also need to show that there is a path of that length, which you can get from nat.​find_min, which will tell you that ∀ (p : path G), p.length ≤ n - 1) is false

Last updated: Dec 20 2023 at 11:08 UTC