Zulip Chat Archive

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

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

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

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

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

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

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

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

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

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

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

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

Ohh okay phew

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

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

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

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

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

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

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

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

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

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

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

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