How to return Walk

Stream: graph theory

[Jakub Nowak]

How do you recommend returning Walk from a function, when its endpoints cannot be (easily) derived from the arguments?
I couldn't find an example in mathlib of this. Maybe partially because people usually work around this somehow, or just give up on contributing. Here's a function I have (for a context, I want to contribute proof of has odd cycle iff not bipartite):

def odd_cycle_of_odd_walk [DecidableEq V] (p : G.Walk u u) : (v : V) × G.Walk v v

The problem is that returning a dependant pair from a function is usually discouraged and I can confirm that working with this function is a bit painful.
Do you have some ideas what would be the best thing to do in this case?

In my opinion, the problem stems from how Walk is defined. IMO, endpoints should be fields and not part of its type signature. Would it be desirable for mathlib to introduce something like SimpleGraph.Walk' : Type* or SimpleGraph.GenericWalk : Type* (with some API)?
Although, maybe something like this shouldn't be introduced to SimpleGraph and it should be introduced to Graph instead, where (I suspect one reason being similar) also vertex set is a field of Graph instead of part of its type signature.

[Jakub Nowak]

One other weird idea I have, is to maybe have SimpleGraph.Walk' : Set V → Set V → Type*. And have two fields with proofs that the first vertex belongs to the first set, and the last vertex belongs to the second set. Then, SimpleGraph.Walk' {u} {v} would be logically equivalent to SimpleGraph.Walk u v and SimpleGraph.Walk' ⊤ ⊤ would be logically equivalent to the version without any arguments.

[Snir Broshi]

Jakub Nowak said:

for a context, I want to contribute proof of has odd cycle iff not bipartite

This already exists as docs#SimpleGraph.two_colorable_iff_forall_loop_even (G.IsBipartite is defined to be G.Colorable 2), unless you're talking about this TODO which formulates the statement a bit differently.
If you're planning to solve that TODO and docs#SimpleGraph.two_colorable_iff_forall_loop_even isn't helping, you can try using docs#finTwoEquiv to convert G.IsBipartite which is Nonempty (G.Coloring (Fin 2)) to Nonempty (G.Coloring Bool) and then use docs#SimpleGraph.Coloring.even_length_iff_congr or docs#SimpleGraph.Coloring.odd_length_iff_not_congr.
Additionally, theorems from #29579 (e.g. docs#SimpleGraph.chromaticNumber_eq_two_iff) might be relevant, not sure.
Why do you need the def above to prove this theorem?

[Snir Broshi]

As for the walk suggestions, I think Walk is good as it is now, but the set suggestion sounds quite good tbh (as long as we're not replacing the existing Walk), as it might be helpful for working with cuts in graphs.

[Snir Broshi]

Concrete suggestion: you can maybe split the function in two, one that returns a vertex and then another that returns a closed walk on that vertex.
I'm interested to learn how you managed to get an odd cycle from an odd walk, can you share the body of that function? This might enhance #31217

[Jakub Nowak]

Snir Broshi said:

This already exists as docs#SimpleGraph.two_colorable_iff_forall_loop_even (G.IsBipartite is defined to be G.Colorable 2), unless you're talking about this TODO which formulates the statement a bit differently.

I wanted to make this topic to just focus the discussion on Walk API. You can check the discussion here to discuss the theorem: #Is there code for X? > bipartite iff does not contain an odd cycle. The theorem in mathlib is not exactly the same, see this message. As for the TODO, I have one implication. I strongly suspect the second implication is easy with the stronger version of docs#SimpleGraph.two_colorable_iff_forall_loop_even (and I have this mostly completed, I'm struggling with Lean, the problem with Walk being main blocker).

Snir Broshi said:

Why do you need the def above to prove this theorem?

Specifically to have the stronger version with cycles, not any walk.

Snir Broshi said:

Concrete suggestion: you can maybe split the function in two, one that returns a vertex and then another that returns a closed walk on that vertex.

The problem is, that this would be basically duplicating most of the code. Although, maybe I could try defining a private function that returns a pair, and then use it to define the two separate functions. Not sure if that would fix any problems. But it might only contain them to theorems regarding just this function.

Snir Broshi said:

As for the walk suggestions, I think Walk is good as it is now, but the set suggestion sounds quite good tbh (as long as we're not replacing the existing Walk), as it might be helpful for working with cuts in graphs.

I don't know what example specifically you have in mind, but I think that both the Set arguments version, and version without any arguments, will help in every case when working with docs#Walk where the endpoints have to change in some non-trivial way. Not sure if the Set idea is good. Basically instead of G.Walk' s t you can have smth like (w : G.Walk') → w.fst ∈ s → w.last ∈ t, in the case where G.Walk' s t is argument. And if G.Walk' s t is being returned, than you can prove w.fst ∈ s and w.last ∈ t in separate theorems. The fields-instead-of-arguments version is more flexible, you can easily plug-in any statement about the vertices, not just Set membership. Although, with the Set version, you can still do smth like (w : G.Walk' ⊤ ⊤) → p w.fst → q w.last, to use some non-trivial statements about vertices. I think the Set version only makes sense if the Set membership covers most of typical use-cases.

[Jakub Nowak]

Sounds like a similar problem, although with docs#NFA.Path: #mathlib4 > dependent product as return type

[Snir Broshi]

I changed my mind, I now support adding a version of Walk with no endpoints (and no sets).
Something like:

structure Walk' extends V × V where
  toWalk : G.Walk fst snd

but with a better name. G.Walk' is to G.Walk what G.Dart is to G.Adj.
Though I prefer adding a generic wrapper for these kinds of unbundled structures:

import Mathlib

structure ProdWithData {α β : Type*} (F : α → β → Sort*) extends α × β where
  inner : F fst snd

namespace SimpleGraph
variable {V : Type*} {G : SimpleGraph V}

def Walk' := ProdWithData G.Walk
def Walk'.toWalk (w : G.Walk') := w.inner

ProdWithData can then be used on SimpleGraph.Walk, SimpleGraph.Adj (for Dart), docs#Path (topology), docs#NFA.Path that you mentioned, and probably many path-y things.

[Snir Broshi]

See #30293 for another possible use-case of a generic Walk

[Aaron Liu]

Snir Broshi said:

I changed my mind, I now support adding a version of Walk with no endpoints (and no sets).
Something like:

structure Walk' extends V × V where
  toWalk : G.Walk fst snd

but with a better name.

You probably shouldn't extends V × V

[Jakub Nowak]

What's the point of extending product, instead of just having structure with two additional fields? And what's the point of ProdWithData?

[Jakub Nowak]

You would still need to write boilerplate for the API with ProdWithData. I guess it might be slightly less work if we have this generic structure.

[Jakub Nowak]

Not sure if match allows somehow writing custom @[match_pattern] for structure pattern syntax? If not, then I think you lose potentially useful feature of having custom names for the elements of the product in structure pattern.

E.g. this

structure Walk' where
  first : V
  last : V
  toWalk : G.Walk first last

you can match like this:

match w where
| { first, last, toWalk } => _

But ProdWithData G.Walk you would have to match as

match w where
| { fst, snd, inner } => _

And, afaik, Lean currently doesn't give any way to change this.

Also, when F in the definition of ProdWithData is a conjunction, then it would likely be simpler to have it as a two separate fields.

[Jakub Nowak]

If you think generalizing this would be useful to avoid work in the future, then maybe having prod_with_data as macro would be a better approach? E.g. something like:

structure Walk' where
  first : V
  last : V
  toWalk : G.Walk first last

prod_with_data Walk' extends Walk

or

@[prod_with_data Walk]
structure Walk' where
  first : V
  last : V
  toWalk : G.Walk first last

And prod_with_data macro would take care of creating some common API.

[Jakub Nowak]

But having macros that generate code is potentially sketchy. Lean ensures correctness of proofs, so it's fine to generate proofs with tactics. But Lean doesn't ensure correctness of your definitions. You must still read them carefully. Generating them through macros, means, you either need to prove correctness of your macro somehow (sound very hard, Lean semantics aren't even formalized), or just read the code generated my macro.

[Shreyas Srinivas]

You could actually kick out the indices and you would lose nothing in the current definition of a walk. The end points could simply be deduced from it

EDIT: I mean you can deduce the Walk (and its indices) by returning something else. See below.

[Shreyas Srinivas]

I actually tried this for Digraphs.

[Jakub Nowak]

@Shreyas Srinivas I couldn't understand what do you mean.

[Jakub Nowak]

Isn't kicking out indices the point of this whole Walk' discussion?

[Shreyas Srinivas]

There is a function in mathlib to convert walks to edgelists

[Shreyas Srinivas]

you can simply reconstruct the walk from the edge list.

[Shreyas Srinivas]

the List (Sym2 V) requires no indices, so you can return that from your function.

[Shreyas Srinivas]

Or since you are using SimpleGraph, you could also just return docs#SimpleGraph.Walk.support

[Shreyas Srinivas]

Jakub Nowak said:

Shreyas Srinivas I couldn't understand what do you mean.

Sorry I am focused on the function you initially described

[Shreyas Srinivas]

So you don't really need indices and dependent sums to return a walk

[Shreyas Srinivas]

For the wider discussion, here's a more abstract definition of a walk:

import Mathlib

open SimpleGraph

structure SimpleGraph.AltWalk (G : SimpleGraph V) where
  st : V
  en : V
  len : ℕ
  len_atleast_1 : len > 0
  seq : Fin len → V
  st_prop : seq ⟨0, by grind⟩ = st
  en_prop : seq ⟨len - 1, by grind⟩ = en
  adj_prop : ∀ i : Fin len, (h : i < (len - 1)) → G.Adj (seq i) (seq ⟨i + 1, by grind⟩ )

[Shreyas Srinivas]

or better yet:

structure SimpleGraph.ListWalk (G : SimpleGraph V) where
  support : List V
  len_prop : support.length > 0
  adj : ∀ i : Fin (support.length), (h : i < (support.length - 1)) →  G.Adj (support.get i) (support.get ⟨i+1, by grind⟩)

[Shreyas Srinivas]

Even better:

structure SimpleGraph.ListChainWalk (G : SimpleGraph V) where
  support : List V
  chainAdj : List.IsChain G.Adj support

[Shreyas Srinivas]

From this, you get the adjacency relation in terms of indices for free

[Shreyas Srinivas]

I prefer one of the last two definitions for the reason that sometimes you want to return the equivalent of Walk.nil which is of type G.Walk u u and your function has a generic return type G.Walk u v and now you have to insert an extra Eq.subst to prove to lean that u = v, which is tedious. This doesn't seem to happen with IsChain since it has only one index.

[Shreyas Srinivas]

and of course a bunch of the current API just duplicates the theorems of IsChain and Lists anyway. So the last definition is the ideal definition of a walk (perhaps with a support \neq [] condition)

[Jakub Nowak]

The inductive definition does have some benefit of simplicity, in terms that many basic definition are simple to define too. Though, we can still get the recursor for induction/cases even with non-inductive definition. Non-inductive definition might be better in the long run.

Shreyas Srinivas said:

the List (Sym2 V) requires no indices, so you can return that from your function.

You can't recover Walk from List (Sym2 V) in some (infinite number of) cases. Although, it's not case for this particular function, which always returns a cycle.

Shreyas Srinivas said:

I prefer one of the last two definitions for the reason that sometimes you want to return the equivalent of Walk.nil which is of type G.Walk u u and your function has a generic return type G.Walk u v and now you have to insert an extra Eq.subst to prove to lean that u = v, which is tedious. This doesn't seem to happen with IsChain since it has only one index.

I also often have problems witch matching .nil. Being tedious because of having to add subst in proofs is one thing. But in definitions match will just fail in the .nil case which just blocked me from writing what I needed multiple times. But with bundled data I think that problem with match won't manifest?

Shreyas Srinivas said:

or better yet:

structure SimpleGraph.ListWalk (G : SimpleGraph V) where
  support : List V
  len_prop : support.length > 0
  adj : ∀ i : Fin (support.length), (h : i < (support.length - 1)) →  G.Adj (support.get i) (support.get ⟨i+1, by grind⟩)

Do we want to enforce support.length > 0? Maybe it would make sense to support walk that has vertex-length equal to zero as well as walks that have vertex-length equal to one?

Shreyas Srinivas said:

Even better:

structure SimpleGraph.ListChainWalk (G : SimpleGraph V) where
  support : List V
  chainAdj : List.IsChain G.Adj support

I agree, this one seems the best from your propositions. I also already did some experiments with exactly the same definition using List.IsChain.

[Shreyas Srinivas]

Basically when it comes to multiple indices of the same type, match, cases and everything else will just give up trying to check it they are equal

[Shreyas Srinivas]

With cases you get a “dependent elimination failed” error

[Aaron Liu]

Jakub Nowak said:

I also often have problems witch matching .nil. Being tedious because of having to add subst in proofs is one thing. But in definitions match will just fail in the .nil case which just blocked me from writing what I needed multiple times. But with bundled data I think that problem with match won't manifest?

Does it work if you add the indices as match discriminants?

[Jakub Nowak]

Aaron Liu said:

Does it work if you add the indices as match discriminants?

That's what I always try, and sometimes it does, sometimes it doesn't.

[Jakub Nowak]

Shreyas Srinivas said:

With cases you get a “dependent elimination failed” error

cases doesn't fail I think? It just won't do a substitution, but won't fail. You can use cases h : w and then rw! [h], cause rw! does better job then cases.

[Shreyas Srinivas]

For the general case of multigraphs, instead of using G.Adj as the chain relation you have a list of (v : V) x (e : E) x (w : V) x (Adj v e w) and the chain relation is something like fun x y => x.snd.snd = y.fst

[Jakub Nowak]

Shreyas Srinivas said:

For the general case of multigraphs, instead of using G.Adj as the chain relation you have a list of (v : V) x (e : E) x (w : V) x (Adj v e w) and the chain relation is something like fun x y => x.snd.snd = y.fst

That won't admit 1-vertex-length walks I think?

[Shreyas Srinivas]

Sadly yes.

[Shreyas Srinivas]

But that’s the Diestel definition.

Anyway, I am currently interested in something I can use with SimpleGraph and Digraph. I think it is a mistake to try to aim for a common API via docs#Graph

[Jakub Nowak]

Shreyas Srinivas said:

But that’s the Diestel definition.

Diestel's definition does admit 1-vertex-length walks:

A walk (of length k) in a graph G is a non-empty alternating sequence v0e0v1e1 . . . ek−1vk of vertices and edges in G such that ei = { vi, vi+1 } for all i < k.

[Shreyas Srinivas]

Yeah but the problem is you want to fit diestels definition without getting into dependent type hell or heterogenous lists.

[Shreyas Srinivas]

I just modified the basic defs file of my Digraph.Walk and Path API to this definition. Lemmas still need changing. Feel free to use this with changes. It might be easier to add the Digraph API fresh and then retrofit only the necessary pieces of SimpleGraph API (and delete the rest)

Just give the required license/author attribution if you plan to make a PR.

Digraph.Walk basic defs only

/-
Copyright (c) 2025 Shreyas Srinivas. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Shreyas Srinivas
-/

import Mathlib

open Digraph

structure Digraph.Walk (G : Digraph V) where
  support : List V
  chainAdj : List.IsChain G.Adj support



def IsCircuit {G : Digraph V} (W : G.Walk) : Prop :=
  W.support.length > 2 ∧ W.support.head = W.support.getLast


structure Digraph.Path (G : Digraph V) extends Walk G where
  nodup : List.Nodup support

def IsCycle (G : Digraph V) (P : G.Path) : Prop :=
  IsCircuit P.toWalk

def Digraph.Walk.Length {G : Digraph V} (W : G.Walk) :=
  W.support.length

def Digraph.Walk.Single {G : Digraph V} (u : V) : G.Walk where
  support := [u]
  chainAdj := by
    apply List.IsChain.singleton

def Digraph.Path.Single {G : Digraph V} (u : V) : G.Path where
  support := [u]
  chainAdj := by
    apply List.IsChain.singleton
  nodup := by
    simp_all

def Digraph.Walk.cons {G : Digraph V}
  (u : V) (W : G.Walk)
  (hAdj : (hnempty : W.support ≠ [])
    → G.Adj u (W.support.head hnempty))
  : G.Walk where
  support :=
    match W.support with
    | [] => [u]
    | v :: vs => u :: v :: vs
  chainAdj := by
    have hchainW := W.chainAdj
    cases hW : W.support with
    | nil =>
        simp
    | cons head tail =>
        simp
        rw [hW] at hchainW hAdj
        constructor
        · simp_all only [ne_eq, reduceCtorEq, not_false_eq_true, List.head_cons, forall_const]
        · assumption

def Digraph.Walk.tail {G : Digraph V} (W : G.Walk) : G.Walk where
  support := W.support.tail
  chainAdj := by
    apply List.IsChain.tail
    exact W.chainAdj

def Digraph.Path.cons {G : Digraph V}
  (u : V) (W : G.Path)
  (hnewvertex : List.Nodup (u :: W.support))
  (hAdj : (hnempty : W.support ≠ [])
    → G.Adj u (W.support.head hnempty))
  : G.Path where
  support :=
    match W.support with
    | [] => [u]
    | v :: vs => u :: v :: vs
  chainAdj := by
    have hchainW := W.chainAdj
    cases hW : W.support with
    | nil =>
        simp
    | cons head tail =>
        simp
        rw [hW] at hchainW hAdj
        constructor
        · simp_all only [ne_eq, reduceCtorEq, not_false_eq_true, List.head_cons, forall_const]
        · assumption
  nodup := by
    induction hW : W.support with
    | nil =>
        simp
    | cons head tail ih =>
        simp_all

def edgeList {G : Digraph V} (W : G.Walk) : List (V × V) :=
  match hW : W.support with
  | []
  | [_] => []
  | v :: w :: _ =>
      (v,w) :: edgeList W.tail
  termination_by W.support.length
  decreasing_by
    simp [Walk.tail, hW]

[Shreyas Srinivas]

We should probably ask the graph theory maintainers/reviewers : CC @Kyle Miller

[Shreyas Srinivas]

The inductive definition does have some benefit of simplicity, in terms that many basic definition are simple to define too. Though, we can still get the recursor for induction/cases even with non-inductive definition. Non-inductive definition might be better in the long run.
``````

[Shreyas Srinivas]

The List.IsChain based definition is inductive. See how IsChain is defined

[Shreyas Srinivas]

It just has one index. The list itself.

[Shreyas Srinivas]

Update : I have started work on formalising combinatorial flow algorithms. The repository is here. It is still an early WIP, but it uses my definition of walks. I still think some refining is needed in the ford Fulkerson description (which is largely because I haven’t actually implemented Edmond’s Karp path selection and I haven’t checked the start and terminal vertices of paths. But these are trivial to fix

Repo : https://github.com/Shreyas4991/LeanFlows

[Shreyas Srinivas]

The goal is to finish push relabelling. Then it can be extended (with a lot of additional graph theory to the recent FOCS 2025 paper albeit only for correctness).

[Shreyas Srinivas]

Also CC : @Sorrachai Yingchareonthawornchai you might be interested.

[Sorrachai Yingchareonthawornchai]

I have different definitions in mind, but please go ahead, and let us know how it goes. The design space is quite large. It is good to have attempts and discuss the strengths/weaknesses of the design.

[Shreyas Srinivas]

Sorrachai Yingchareonthawornchai said:

I have different definitions in mind, but please go ahead, and let us know how it goes. The design space is quite large. It is good to have attempts and discuss the strengths/weaknesses of the design.

Apologies for the late reply. I have been travelling. I already wrote one half of the max flow-min cut theorem 1.5 years ago using the definitions available in mathlib at that time ( I am not recovering that code now, it was written before lean4 had the notion of stable versions). Since then lean and its tactics have come a long way. Part of my motivation is to see how far I can go this time and to test my definition of a walk over the mathlib simplegraph version

[Shreyas Srinivas]

(deleted)

[Shreyas Srinivas]

small update : This definition of walks is a breeze to work with. I am missing the code action with fun_induction though.