Proving Graph-Theoretic Properties for Quiver Paths

Stream: mathlib4

[Nicolas Rouquette]

1. Background

I'm working with Quiver.Path from Mathlib.Combinatorics.Quiver.Path.Vertices and need to establish two standard graph-theoretic results about simple paths (paths with no repeated vertices). Currently, I have these as axioms in my code, but I'd like to prove them properly or determine if they already exist in mathlib.

2. The Two Properties

A) Simple Path Length Bound

Statement: A simple path in a finite quiver has length strictly less than the number of vertices.

axiom quiver_simple_path_bound (V : Type*) [Quiver V] [Fintype V]

    {a b : V} (p : Path a b)

    (h_simple : p.vertices.Nodup) :

    p.length < Fintype.card V

Intuition: Since p.vertices has no duplicates and contains p.length + 1 elements (via vertices_length), we need p.length + 1 ≤ Fintype.card V, which gives us p.length < Fintype.card V.

B) Existence of Simple Subpath (Cycle Removal)

Statement: Every path contains a simple subpath (with no repeated vertices) connecting the same endpoints.

axiom quiver_exists_simple_subpath (V : Type*) [Quiver V]

    {a b : V} (p : Path a b) :

    ∃ (q : Path a b), q.vertices.Nodup ∧ q.length ≤ p.length

Intuition: If a path has cycles (repeated vertices), we can remove them to obtain a simple path with the same endpoints and shorter or equal length.

3. Questions

3.1. Do these results already exist in mathlib? I searched but couldn't find them. They seem like fundamental results that might be useful beyond my specific application.

3.2. What's the best approach to prove these? For the first property, I'm thinking:

- Use p.vertices.length = p.length + 1 (from vertices_length)

- Use that p.vertices.Nodup implies p.vertices.length ≤ Fintype.card V

- Combine these to get the bound

For the second property, I'm less certain. Perhaps:

- Define a function that removes cycles by detecting the first repeated vertex

- Show this produces a valid path with the same endpoints

- Show termination and preservation of properties

3.3. Would mathlib be interested in PRs for these results? They seem generally useful for anyone working with paths in quivers/graphs.

4. Context

I'm using these to prove that reachability in finite quivers can be decided by checking paths up to a bounded length (which enables computational verification). The derived result is:

theorem exists_simple_path_bounded (V : Type*) [Quiver V] [Fintype V]

    {a b : V} (p : Path a b) :

    ∃ (q : Path a b), q.vertices.Nodup ∧ q.length < Fintype.card V

Any guidance, pointers to existing lemmas, or suggestions for proving these would be greatly appreciated!

[Pim Otte]

I think it might be a good idea to look at SimpleGraph.Walk, SimpleGraph.Path, SimpleGraph.Walk.bypass (for the second property). (I'm not sure on all the answers, but hope this helps you in the right direction)

[Matteo Cipollina]

here You can find some useful API for cycles and simple paths which I'm planning to PR to mathlib, though they are not yet updated to the latest PR for SStronglyConnected quivers. With these your theorem should be easy to put together.
If you are working with undirected graphs, you may rather look at SimpleGraph APi as above. Quiver can represent undirected graphs via SymmetricQuiver, but SimpleGraph is more idiomatic for that

[Shreyas Srinivas]

I think the SimpleGraph walk api sets itself up for failure by using dependent type indices. There was a discussion on the graph theory channel for better definitions of walks and paths. You could adapt some of them for quivers and see how that works out

[Nicolas Rouquette]

Thanks, @Matteo Cipollina; your work-in-progress MCMC is very helpful in proving the two axioms I need. For now, I'm pinning my dependencies to Lean4 and Mathlib v4.25.0; I see that you're on the bleeding edge of main. So for the time being, I'm copying just the part of your MCMC/PF/Combinatorics/Quiver that I need with proper attribution to you. Please let me know when you submit a PR with your code.

[Nicolas Rouquette]

@Matteo Cipollina I've been trying to build the files you mentioned:
https://github.com/or4nge19/MCMC/blob/main/MCMC/PF/Combinatorics/Quiver/Path.lean
https://github.com/or4nge19/MCMC/blob/main/MCMC/PF/Combinatorics/Quiver/Cyclic.lean

The 1st one contains a lemma:

lemma length_lt_card_of_isStrictlySimple [DecidableEq V] [Fintype V]
    {a b : V} {p : Path a b} (hp : IsStrictlySimple p) :
  p.length < Fintype.card V

that directly corresponds to an axiom I used:

axiom quiver_simple_path_bound (V : Type*) [Quiver V] [Fintype V]
    {a b : V} (p : Path a b)
    (h_simple : p.vertices.Nodup) :
    p.length < Fintype.card V

This lemma should help me prove my 2nd axiom with [DecidableEq V].

However, I'm having problems using these files.

The MCMC repo uses the "HEAD" revision of Mathlib4; presumably this means master.
https://github.com/or4nge19/MCMC/blob/main/lakefile.toml

I am using Lean v4.25.2 and I'm running into a problem w/ undefined symbols with Mathlib4 v4.25.2:

• List.exists_mem_split
• tactic tsub_self
• List.dropLast_append_singleton
• List.ne_nil_of_head?_eq_some
• List.get_idxOf_of_mem

If I try switching to Mathlib4 master, then I get a deluge of SSL certificate problems.

Suggestions?

[Matteo Cipollina]

The problem is that I haven't yet updated the repository to the latest mathlib merged PR on Quiver, I'll try to update it today or tmr and let you know.

[Nicolas Rouquette]

Thanks @Matteo Cipollina ! I switched to v4.26.0-rc2 and used your key theorems as axioms to prove the Quiver path properties that I need for my project. You can find the details of my proofs here.