Do we need SimpleGraph.Path?

Stream: graph theory

[Jakub Nowak]

We have SimpleGraph.IsPath and SimpleGraph.Path is a structure that bundles this property. When using it I often find myself converting between path and walk. This can be greatly improved by adding more defs and theorems for SimpleGraph.Path (e.g. Path.length). But, do we really need Path? What gains do we get from it, instead of having just Walk and IsPath as assumption?

[Vlad Tsyrklevich]

I didn't realize we had a SimpleGraph.Path, it does seem unnecessary to me, though perhaps I'm missing something. I'd vote for deprecating it.

[Iván Renison]

I did some things with paths, and I used everywhere Walk with IsPath assumption precisely because all the definitions and lemmas that are only available for Walk. I also thought that Path in its current form is unnecessary

[Jakub Nowak]

I think, if someone were to make an effort, to make API for Path, it could be usable. I wanted to ask, whether it's worth the effort at all. I.e., imagine there's a full API for Path, what would we gain from it?

I think that abstracting away definition makes sense, when the definition is an implementation detail, or when you treat your new object as something separate.
But I don't see any need to hide the fact that Path is a Walk.

[Jakub Nowak]

@Niklas Mohrin
I'm looking at the possibility of deprecating docs#SimpleGraph.Path. Not sure what to do with docs#SimpleGraph.Path.instFintype. Would Fintype { w : G.Walk u v // w.IsPath } be ok four your usage?
We might also want to have instFinite that doesn't require DecidableRel and DecidableEq.

[Shreyas Srinivas]

I am using SimpleGraph.Path because in one of my repos. It is actually quite useful in keeping things succinct

[Shreyas Srinivas]

If it didn't exist, I would reinvent it.

[Jakub Nowak]

Would you like to contribute API for Path? Currently, I find it very lacking for it to be useful.

[Jakub Nowak]

Other people said, they're ok with using Walk and IsPath, have you tried it?

[Shreyas Srinivas]

using the walk API in Path is not super hard since Path is just a subtype of Walk. It works with a coercion. The default coercion is to Walk.

[Jakub Nowak]

Yes, but then any definition will return Walk, not Path. So you're back with Walk and you have to prove IsPath if you want to get back to having Path.

[Jakub Nowak]

I have trouble with the coercion approach.

import Mathlib

variable {V : Type*} [Fintype V] {G : SimpleGraph V}
open SimpleGraph

example {u v : V} (p : G.Path u v) : ∃ n, Walk.length p < n := sorry

Neither Walk.length p nor p.length works here. Doing coercion manually, i.e. p.val.length works.

[Snir Broshi]

FWIW I also vote for deprecating Path

[Niklas Mohrin]

Thanks for reaching out, I can provide my thoughts: I always found that passing walks together with their Path-ness makes nicer signatures; it more closely resembles how I think about a definition. I do agree though that trying to always bundle the IsPath (or further hypotheses) does make the code awkward sometimes. Maybe, in our project back then, it would have actually been better to not bother about packing facts up, but I don't know. I did end up just adding convenience definitions like Path.transfer here: https://github.com/niklasmohrin/lean-seminar-2023/blob/5a53c8e067632017bded4fbf24b346b2ffddb84d/FlowEquivalentForest/SimpleGraph/Path.lean#L123

Ultimately, I don't care much about the decision, since I am not working with Lean at the moment. I think any work to improve ergonomics around paths would be nice and either having a more thorough Path api or having IsPath instances easily synthesized (or by simp or whatever) when needed would help on that front. Changing the fintype instance to match the rest seems sensible :+1:

[Niklas Mohrin]

(of course, the project code would break, but that is totally expected; it is not maintained anyways)

[Shreyas Srinivas]

I can see some advantages in this deprecration since one can carry IsPath around. But if we do this, I would like to reserve the name Path for an inductive definition of paths. Something roughly like

inductive Path (G : SimpleGraph V) : V -> V -> Type u where
        | nil {v} => Path v v
        | cons {u v w} : (e : G.Adj u v) (p_ind : Path v w) (new_u : u \notin p_ind) : Path u w

[Jakub Nowak]

That's pretty much the same as what Path is now. With sufficient API definition doesn't matter in most case. E.g. you can have the cases and induction tactic work just as with the structure you wrote above, by writing custom recursor like this: #new members > Custom recursor in term mode @ 💬
For match you need to create @[match_pattern].