Zulip Chat Archive

Stream: graph theory

Topic: Construct path from walk?


view this post on Zulip Chase Norman (Dec 07 2020 at 04:47):

I have a question related to graph theory formalization. I'm looking to prove that given a directed graph and a walk from vertices x to y, one can construct a path from x to y. I am formalizing my walk as a list of vertices that satisfy list.chain' on some binary relation. The path would satisfy the nodup property.

I imagine some kind of proof inducting on the number of duplicate elements in the list, however the natural human intuition seems quite hand-wavy. Does anyone here have any advice or an example of a similar proof in the WIP mathlib addition? Thanks.

view this post on Zulip Alena Gusakov (Dec 07 2020 at 04:48):

I have tried proving it and it is insanely obnoxious

view this post on Zulip Alena Gusakov (Dec 07 2020 at 04:48):

My attempt was also based on the idea of duplicate elements

view this post on Zulip Alena Gusakov (Dec 07 2020 at 04:50):

simple_graphs2 is the last branch I saw with an attempt but it's a couple of months behind mathlib, I've been slowly trying to slice it off into its own PRs

view this post on Zulip Alena Gusakov (Dec 07 2020 at 04:51):

But I'm not convinced the definitions of path/walk there lend themselves to an easy proof of that lemma

view this post on Zulip Alena Gusakov (Dec 07 2020 at 04:51):

Oh also simple_graphs2 doesn't have any directed graph stuff, you'd have to repurpose it a bit

view this post on Zulip Chase Norman (Dec 07 2020 at 04:52):

would it be in walks.lean? How far did you get in the attempt?

view this post on Zulip Alena Gusakov (Dec 07 2020 at 04:52):

I think it's there yeah

view this post on Zulip Alena Gusakov (Dec 07 2020 at 04:52):

I don't recall, it's one of the sorry'd proofs though (I think)

view this post on Zulip Alena Gusakov (Dec 07 2020 at 04:53):

I have the obvious direction down, path -> walk

view this post on Zulip Chase Norman (Dec 07 2020 at 04:54):

lemma exists_path_eq_exists_walk : exists_path G = exists_walk G :=
begin
  ext v w,
  sorry,
  sorry,
end

view this post on Zulip Alena Gusakov (Dec 07 2020 at 04:54):

Ah yeah that must be it

view this post on Zulip Alena Gusakov (Dec 07 2020 at 04:55):

Oh I guess I didn't prove the obvious direction lol, oops

view this post on Zulip Chase Norman (Dec 07 2020 at 04:56):

Why is graph theory related work in combinatorics, if I may ask.

view this post on Zulip Alena Gusakov (Dec 07 2020 at 04:56):

I've always seen graph theory and combinatorics linked together

view this post on Zulip Aaron Anderson (Dec 07 2020 at 04:57):

It might actually be easier to show that both exists_path and exists_walk are equivalent to connectedness as defined with eqv_gen

view this post on Zulip Chase Norman (Dec 07 2020 at 05:02):

Is this the transitive closure? eqv_gen?

view this post on Zulip Aaron Anderson (Dec 07 2020 at 05:03):

Yes

view this post on Zulip Aaron Anderson (Dec 07 2020 at 05:03):

I'm not sure how smooth the API for it is

view this post on Zulip Chase Norman (Dec 07 2020 at 05:10):

I feel like this just kicks the can down the road. I still feel like it would be hard to prove that there exists a path between two connected vertices.

view this post on Zulip Mario Carneiro (Dec 07 2020 at 06:48):

Prove it by induction on finsets: if every pair of elements in S is eqv_gen, then every pair or elements in S has a path

view this post on Zulip Chase Norman (Dec 07 2020 at 06:51):

sounds like a walk

view this post on Zulip Mario Carneiro (Dec 07 2020 at 06:52):

Because when you induct on finsets every new element is known to be disjoint from all the others

view this post on Zulip Mario Carneiro (Dec 07 2020 at 06:54):

I feel like this question has come up before on zulip

view this post on Zulip Chase Norman (Dec 07 2020 at 07:01):

Could you help me find this? Also I'm still misunderstanding you. If you induct on (I'm presuming) the length of the path, it's still possible you include a path that contains a node previously in the list. This would make the induction fail, as it creates a walk. Where does my logic fail?

view this post on Zulip Mario Carneiro (Dec 07 2020 at 07:02):

you aren't inducting on the length of the path

view this post on Zulip Mario Carneiro (Dec 07 2020 at 07:02):

you are inducting on the size of the set from which to select the vertices in the path

view this post on Zulip Mario Carneiro (Dec 07 2020 at 07:04):

Actually I think instead of S is pairwise eqv_gen in the hypothesis you might want every pair of elements in S has a walk in S

view this post on Zulip Mario Carneiro (Dec 07 2020 at 07:06):

oh, actually even better, to avoid having to find connected components: IH(S) = "for all x,y in S, if there is a walk from x to y in S then there is a path from x to y in S"

view this post on Zulip Chase Norman (Dec 07 2020 at 07:08):

So if x and y are the only vertices, the result is the walk is the path. n=2

view this post on Zulip Mario Carneiro (Dec 07 2020 at 07:09):

the base case is of course |S| = 0

view this post on Zulip Chase Norman (Dec 07 2020 at 07:09):

how would we restrict |S| when doing the inductive step? We would still need all the vertices to be options, right?

view this post on Zulip Mario Carneiro (Dec 07 2020 at 07:09):

?

view this post on Zulip Mario Carneiro (Dec 07 2020 at 07:10):

We just add an arbitrary vertex to S

view this post on Zulip Chase Norman (Dec 07 2020 at 07:12):

Are you saying: if there's a path that contains the added vertex s, you're done. If not, then find the path from x to s and s to y?

view this post on Zulip Chase Norman (Dec 07 2020 at 07:12):

What elements could we restrict from those paths so that we could use the IH?

view this post on Zulip Chase Norman (Dec 07 2020 at 07:12):

I feel like I'm missing some obvious step.

view this post on Zulip Mario Carneiro (Dec 07 2020 at 07:15):

hm, you're right

view this post on Zulip Mario Carneiro (Dec 07 2020 at 07:16):

I'm sure there is a simple inductive proof of this that does not need you to construct the whole vertex removing algorithm, and I'm pretty sure I posted it once on zulip but I can't find it :(

view this post on Zulip Aaron Anderson (Dec 07 2020 at 07:20):

I think the sketch I’d do is

  • path -> walk (straightforward)
  • walk -> connected (probably the hardest, but induction on the length of the walk should work)
  • connected -> path (follows from path being an equivalence relation)

view this post on Zulip Chase Norman (Dec 07 2020 at 07:21):

what is the formal definition of connected in your view?

view this post on Zulip Mario Carneiro (Dec 07 2020 at 07:21):

eqv_gen?

view this post on Zulip Aaron Anderson (Dec 07 2020 at 07:21):

eqv_gen G.adj

view this post on Zulip Aaron Anderson (Dec 07 2020 at 07:21):

The transitive closure of adjacency

view this post on Zulip Mario Carneiro (Dec 07 2020 at 07:22):

walk -> connected is easy

view this post on Zulip Chase Norman (Dec 07 2020 at 07:22):

yeah don't you just do that from transitivity? What I'm not understanding is how equivalence relation helps.

view this post on Zulip Mario Carneiro (Dec 07 2020 at 07:22):

I think the hard step in this proof is showing that path is an equivalence relation

view this post on Zulip Chase Norman (Dec 07 2020 at 07:23):

Yeah for sure. Because you can form a walk out of paths, so knowing that path is an equivalence relation is enough to do the whole proof!

view this post on Zulip Mario Carneiro (Dec 07 2020 at 07:24):

How about: IH(y,w) = "if w is a walk from x to y, then there is a path from x to every point z in w"

view this post on Zulip Mario Carneiro (Dec 07 2020 at 07:24):

induction on walks

view this post on Zulip Mario Carneiro (Dec 07 2020 at 07:29):

In the inductive step, you have x -- a - y, and if y is in x..a then you are done by the IH, and if it is not then there is a path x..a by the IH which extends to a path x..y

view this post on Zulip Chase Norman (Dec 07 2020 at 07:35):

That's more like it. That sounds powerful enough.

view this post on Zulip Kyle Miller (Dec 07 2020 at 11:36):

I just ported over some of the definitions from simple_graphs2 to use mathlib's simple graphs library, and I added a function to turn walks into paths between the same endpoints: https://github.com/leanprover-community/mathlib/blob/simple_graph_walks2/src/combinatorics/simple_graph/walks.lean#L127

This then proves that walks and paths generate the same relations: https://github.com/leanprover-community/mathlib/blob/simple_graph_walks2/src/combinatorics/simple_graph/walks.lean#L337 (I'm not sure the best way to encode relations from types -- is nonempty right?)

view this post on Zulip Chase Norman (Dec 07 2020 at 18:24):

Where can I learn more about the types of inductive definitions you used in to_path? The syntax does not make sense to me and seems very powerful. Thanks for your help!

view this post on Zulip Julian Berman (Dec 07 2020 at 20:00):

https://leanprover.github.io/reference/declarations.html#the-equation-compiler I think

view this post on Zulip Kyle Miller (Dec 14 2020 at 06:29):

I've added some more to the branch and cleaned it up somewhat: https://github.com/leanprover-community/mathlib/blob/simple_graph_walks2/src/combinatorics/simple_graph/walks.lean (this now includes, for example, that eqv_gen G.adj is equal to G.exists_walk).

It still needs some work before it's ready for a PR, but the interface seems more-or-less fine (and it includes most of hedetniemi's walk module, specialized to simple graphs). Some lemmas could stand to have more attention paid to their proofs (is_path_iff.aux for example), and a number of things could be named better.


Last updated: May 08 2021 at 22:13 UTC