## Stream: graph theory

### Topic: Construct path from walk?

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

#### Alena Gusakov (Dec 07 2020 at 04:48):

I have tried proving it and it is insanely obnoxious

#### Alena Gusakov (Dec 07 2020 at 04:48):

My attempt was also based on the idea of duplicate elements

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

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

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

#### Chase Norman (Dec 07 2020 at 04:52):

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

#### Alena Gusakov (Dec 07 2020 at 04:52):

I think it's there yeah

#### Alena Gusakov (Dec 07 2020 at 04:52):

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

#### Alena Gusakov (Dec 07 2020 at 04:53):

I have the obvious direction down, path -> walk

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


#### Alena Gusakov (Dec 07 2020 at 04:54):

Ah yeah that must be it

#### Alena Gusakov (Dec 07 2020 at 04:55):

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

#### Chase Norman (Dec 07 2020 at 04:56):

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

#### Alena Gusakov (Dec 07 2020 at 04:56):

I've always seen graph theory and combinatorics linked together

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

#### Chase Norman (Dec 07 2020 at 05:02):

Is this the transitive closure? eqv_gen?

Yes

#### Aaron Anderson (Dec 07 2020 at 05:03):

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

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

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

#### Chase Norman (Dec 07 2020 at 06:51):

sounds like a walk

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

#### Mario Carneiro (Dec 07 2020 at 06:54):

I feel like this question has come up before 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?

#### Mario Carneiro (Dec 07 2020 at 07:02):

you aren't inducting on the length of the path

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

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

#### 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"

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

#### Mario Carneiro (Dec 07 2020 at 07:09):

the base case is of course |S| = 0

#### 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?

?

#### Mario Carneiro (Dec 07 2020 at 07:10):

We just add an arbitrary vertex to S

#### 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?

#### Chase Norman (Dec 07 2020 at 07:12):

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

#### Chase Norman (Dec 07 2020 at 07:12):

I feel like I'm missing some obvious step.

hm, you're right

#### 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 :(

#### 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)

#### Chase Norman (Dec 07 2020 at 07:21):

what is the formal definition of connected in your view?

eqv_gen?

#### Aaron Anderson (Dec 07 2020 at 07:21):

eqv_gen G.adj

#### Aaron Anderson (Dec 07 2020 at 07:21):

The transitive closure of adjacency

#### Mario Carneiro (Dec 07 2020 at 07:22):

walk -> connected is easy

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

#### Mario Carneiro (Dec 07 2020 at 07:22):

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

#### 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!

#### 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"

#### Mario Carneiro (Dec 07 2020 at 07:24):

induction on walks

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

#### Chase Norman (Dec 07 2020 at 07:35):

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

#### 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?)

#### 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!

#### 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: Aug 03 2023 at 10:10 UTC