Construct path from walk?

Stream: graph theory

[Chase Norman]

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]

I have tried proving it and it is insanely obnoxious

[Alena Gusakov]

My attempt was also based on the idea of duplicate elements

[Alena Gusakov]

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]

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

[Alena Gusakov]

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

[Chase Norman]

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

[Alena Gusakov]

I think it's there yeah

[Alena Gusakov]

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

[Alena Gusakov]

I have the obvious direction down, path -> walk

[Chase Norman]

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

[Alena Gusakov]

Ah yeah that must be it

[Alena Gusakov]

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

[Chase Norman]

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

[Alena Gusakov]

I've always seen graph theory and combinatorics linked together

[Aaron Anderson]

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]

Is this the transitive closure? eqv_gen?

[Aaron Anderson]

Yes

[Aaron Anderson]

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

[Chase Norman]

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]

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]

sounds like a walk

[Mario Carneiro]

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

[Mario Carneiro]

I feel like this question has come up before on zulip

[Chase Norman]

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]

you aren't inducting on the length of the path

[Mario Carneiro]

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

[Mario Carneiro]

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]

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]

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

[Mario Carneiro]

the base case is of course |S| = 0

[Chase Norman]

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

[Mario Carneiro]

?

[Mario Carneiro]

We just add an arbitrary vertex to S

[Chase Norman]

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]

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

[Chase Norman]

I feel like I'm missing some obvious step.

[Mario Carneiro]

hm, you're right

[Mario Carneiro]

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]

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]

what is the formal definition of connected in your view?

[Mario Carneiro]

eqv_gen?

[Aaron Anderson]

eqv_gen G.adj

[Aaron Anderson]

The transitive closure of adjacency

[Mario Carneiro]

walk -> connected is easy

[Chase Norman]

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

[Mario Carneiro]

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

[Chase Norman]

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]

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]

induction on walks

[Mario Carneiro]

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]

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

[Kyle Miller]

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]

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!

[Julian Berman]

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

[Kyle Miller]

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.