maximal paths via zorn?

Stream: graph theory

[Alena Gusakov]

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]

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]

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

[Aaron Anderson]

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]

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]

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

[Alena Gusakov]

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]

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

[Aaron Anderson]

but I think also you could use the image API

[Aaron Anderson]

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

[Aaron Anderson]

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]

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

[Alena Gusakov]

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]

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]

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

[Alena Gusakov]

Great, thank you!

[Aaron Anderson]

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]

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]

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

[Alena Gusakov]

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]

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]

Aha, nat has a conditionally_complete_linear_order instance

[Aaron Anderson]

so you can take Sups of arbitrary bounded sets of naturals

[Alena Gusakov]

Perfect, thanks!

[Aaron Anderson]

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

[Alena Gusakov]

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]

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

[Aaron Anderson]

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]

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]

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

[Aaron Anderson]

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

[Aaron Anderson]

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

[Aaron Anderson]

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]

Right, yeah that was my thought with maximal paths

[Aaron Anderson]

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

[Alena Gusakov]

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

[Alena Gusakov]

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

[Aaron Anderson]

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

[Alena Gusakov]

I gotcha

[Aaron Anderson]

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]

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

[Alena Gusakov]

So smaller paths whose edge sets intersect with the larger path

[Alena Gusakov]

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]

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]

I think I might've just misunderstood that recipe

[Alena Gusakov]

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

[Aaron Anderson]

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

[Aaron Anderson]

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...

[Alena Gusakov]

Oh god lmao

[Aaron Anderson]

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]

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

[Aaron Anderson]

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

[Alena Gusakov]

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

[Alena Gusakov]

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]

Maximum path is easier though

[Aaron Anderson]

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]

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

[Alena Gusakov]

Gotcha

[Alena Gusakov]

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

[Aaron Anderson]

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

[Aaron Anderson]

just keep walking until you can't

[Alena Gusakov]

This is true

[Alena Gusakov]

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]

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

[Alena Gusakov]

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]

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]

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]

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

[Aaron Anderson]

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]

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

[Aaron Anderson]

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]

So what you want to show is bdd_above set_of_relevant_paths

[Aaron Anderson]

actually, what might be a better idea

[Aaron Anderson]

is to look at how that Sup is defined

[Aaron Anderson]

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

[Aaron Anderson]

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]

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

[Alena Gusakov]

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]

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]

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]

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]

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

[Aaron Anderson]

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

[Alena Gusakov]

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

[Aaron Anderson]

Uhh lists are finitely long, so these would be isomorphic

[Alena Gusakov]

Ohh okay phew

[Alena Gusakov]

Misread then

[Alena Gusakov]

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

[Kyle Miller]

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]

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

[Kyle Miller]

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]

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

[Aaron Anderson]

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

[Kyle Miller]

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]

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

[Kyle Miller]

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]

A loop is exactly a homomorphism from a cycle graph

[Kyle Miller]

We probably should move over to the paths topic

[Aaron Anderson]

Right

[Alena Gusakov]

I'm still having trouble with finding Sup

[Alena Gusakov]

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]

We have a new fintype lemma there too

[Alena Gusakov]

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]

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]

What would you recommend using?

[Bhavik Mehta]

one sec I'll type it out

[Bhavik Mehta]

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

[Alena Gusakov]

I think that's sort of what I have

[Alena Gusakov]

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

[Alena Gusakov]

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

[Bhavik Mehta]

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

[Alena Gusakov]

OH

[Bhavik Mehta]

So nothing satisfies that predicate

[Alena Gusakov]

yeah okay I gotcha

[Bhavik Mehta]

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

[Bhavik Mehta]

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]

also that should probably be called maximal not maximum

[Alena Gusakov]

It's maximum, it's a global thing

[Alena Gusakov]

For all paths in G

[Alena Gusakov]

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

[Bhavik Mehta]

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

[Alena Gusakov]

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

[Alena Gusakov]

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

[Bhavik Mehta]

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]

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]

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

[Alena Gusakov]

Yeah

[Alena Gusakov]

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

[Bhavik Mehta]

maximum length is different to maximum path though

[Bhavik Mehta]

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

[Alena Gusakov]

I am referring to maximum length

[Bhavik Mehta]

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

[Bhavik Mehta]

Ah

[Bhavik Mehta]

maybe call it is_maximum_length then

[Alena Gusakov]

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

[Alena Gusakov]

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

[Bhavik Mehta]

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

[Bhavik Mehta]

Even on a finite graph

[Alena Gusakov]

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

[Bhavik Mehta]

But under length, a maximum path does exist

[Alena Gusakov]

Like, you can have multiple maximum paths right?

[Bhavik Mehta]

Right so I'm saying change the name to is_maximum_length

[Bhavik Mehta]

Because then it matches the def you had

[Alena Gusakov]

Yeah, gotcha

[Alena Gusakov]

Yeah okay I see what you were saying

[Alena Gusakov]

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

[Alena Gusakov]

Without realizing that they're not at all interchangeable lmao

[Aaron Anderson]

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]

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

[Aaron Anderson]

so you could use that too

[Aaron Anderson]

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]

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]

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