New Walk definition without index parameters

Stream: graph theory

[Shreyas Srinivas]

I would actually like to PR that definition if there is support

[Shreyas Srinivas]

Since posting that definition I have developed nice API for both that and the digraph version

[Shreyas Srinivas]

And given how similar they are, it suggests that a common typeclass Adj with a binary adjacency relation would be useful here and for any future graph definitions. This is then sufficient for walks

[Shreyas Srinivas]

The current version is (ascii-ed out the last because I am typing on a phone).

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

[Shreyas Srinivas]

Bundling the non empty support allows us to use list defs that require the list to be nonemoty.

[Shreyas Srinivas]

I also have an induction principle for consing vertices and two different definitions of appending walks

[Notification Bot]

6 messages were moved here from #graph theory > `p.getVert n` vs `p.support[n]` by Jakub Nowak.

[Shreyas Srinivas]

And the great news is, I also have it for subgraphs (which unfortunately exists in mathlib as a separate definition in mathlib).

[Shreyas Srinivas]

important : The reason I suggest an Adj typeclass is because adjacency is the only relevant parameter and the definition of Walks for SimpleGraph, Subgraphs, and Digraphs is identical

[Jakub Nowak]

I think we should modify definition of docs#SimpleGraph to have set of vertices, instead of further developing docs#SimpleGraph.Subgraph API.

[Jakub Nowak]

We might want to have typeclass for different graph definitions. Which would include .Adj.

[Jakub Nowak]

Hm, actually, it would include .Adj and nothing else. Cause we probably want assumption symmetric to be in separate typeclasses.

[Shreyas Srinivas]

Yeah that’s a major refactor. That @Bhavik Mehta and @Yaël Dillies are also planning.

[Shreyas Srinivas]

I have wanted a vertex set since early last year

[Shreyas Srinivas]

But because the situation is trivial for Digraphs I started mathlib4#33466 It is ready for review and if someone wants to add some commits that’s also welcome

[Shreyas Srinivas]

The next step would be to make SimpleGraph extend Digraph

[Shreyas Srinivas]

Or just add vertex sets there

[Shreyas Srinivas]

And typeclass instances related to order relations will change a bit

[Jakub Nowak]

Shreyas Srinivas said:

The next step would be to make SimpleGraph extend Digraph

I think we don't want that. In SimpleGraph edges are Sym2 V, and in Digraph edges are V × V. We don't want to leak definitions about edges from Digraph to SimpleGraph.

[Shreyas Srinivas]

Anyway. I’d focus on getting mathlib4#33466 merged first

[Ilmārs Cīrulis]

Does this big planned refactor means something for bystanders too? I mean, would it force us (or someone else) to reprove proofs already done?

I hope this isn't a dumb question. :sweat_smile:

[Jakub Nowak]

It depends on whether will current docs#SimpleGraph.Walk be deprecated. That wasn't discussed.

[Shreyas Srinivas]

I just wanted to let you all know that I posted the digraph version as a PR to my fork of mathlib for demo purposes. It's not done yet, but you can see where it is headed:
https://github.com/Shreyas4991/mathlib4/pull/1/changes

[Shreyas Srinivas]

(deleted)

[Shreyas Srinivas]

(deleted)

[Shreyas Srinivas]

(deleted)

[Bhavik Mehta]

Shreyas Srinivas said:

I would actually like to PR that definition if there is support

What's the motivation for the new definition? From what I've seen, the proposed API is quite a bit more limited, and is quite a bit more involved to use in practice, and we don't get many benefits in application.

[Shreyas Srinivas]

Index headaches disappear. Also I dispute the claim that it is more involved to use.

[Shreyas Srinivas]

You don't have to do substs to return Walk.nil in a function that has a return type G.Walk u v

[Bhavik Mehta]

What kind of index headaches?

[Shreyas Srinivas]

Shreyas Srinivas said:

You don't have to do substs to return Walk.nil in a function that has a return type G.Walk u v

this

[Shreyas Srinivas]

I have put this to use in my berge lemma formalization and it substantially simplified proofs of theorems

[Shreyas Srinivas]

By reducing them to list theorems

[Bhavik Mehta]

I dispute the claim that this is a headache!

[Shreyas Srinivas]

Having used them in three different places, I prefer my definition

[Bhavik Mehta]

Interesting, do you have a before and after?

[Shreyas Srinivas]

Private repo.

[Bhavik Mehta]

The reason I ask is that I'd seen a proof of Berge in a student project a while ago, and it was relatively short and clean from what I remember.

[Shreyas Srinivas]

There was no proof in any of the publicly posted projects here.

[Shreyas Srinivas]

There were attempts that never showed up as public repos or mathlib PRs.

[Bhavik Mehta]

Indeed, this was also a private repo for assessed coursework

[Shreyas Srinivas]

Fair enough. But I have done quite a bit of background work with TCS formalization, and I find the list approach better. List.IsChain already has all the lemmas and inductiveness we need. G.Walk is just too tedious. The fact that a nil and cons walk have two difrerent types is a big enough headache.

[Bhavik Mehta]

And, to be clear, that's why I'd like some more concrete evidence for why a definition without index parameters is better. The current definition has been used in fairly substantial projects in mathematical graph theory and in TCS (some public and some private) and I haven't encountered any issues, and certainly not issues that would be resolved by changing the definition. So I would be interested to hear about where you got stuck.

[Shreyas Srinivas]

That's a fair point. This is why I haven't actively pushed this beyond showing my definitions in different repos. Under my current schedule making these projects public won't happen for three months (maybe even more). But I do recommend using my definitions and checking if you can simplify your proofs substantially. I have currently adopted this definition for SimpleGraph, Subgraph, and also Digraph. The latter two don't have Walk and Path API in mathlib anyway.

[Shreyas Srinivas]

And I would also make a separate argument that it is easier to work with the support list than with G.Walk u v, both cognitively and in lean. Because it's just a list.

[Bhavik Mehta]

I had tried an index-free definition, and the proofs were not substantially better (most got very slightly worse, but not significantly), that's why I could confidently claim that the issues weren't resolved by changing the definition!
As always, I can believe that there are missing lemmas and constructors for the current definition, and if you can identify them then we can discuss adding them. But much better evidence and arguments would be needed to re-do the definition, in particular because it also changes the type of the definition.

[Bhavik Mehta]

Shreyas Srinivas said:

And I would also make a separate argument that it is easier to work with the support list than with G.Walk u v, both cognitively and in lean. Because it's just a list.

Firstly this is subjective (and also personally feel the exact opposite: my mental model of a walk is as a sequence of edges, not just a bare sequence of vertices), but secondly don't forget that you can always take the list of vertices from a walk (docs#SimpleGraph.Walk.support), and perform operations there. So it's not like you're banned from thinking about the vertex list, we have API for that point of view for those who prefer it.

[Shreyas Srinivas]

I know of the support list, I just don't think most graph walk lemmas are stated in terms of support

[Shreyas Srinivas]

also sometimes you just want to manipulate walks and paths as vertex sequences in algorithms on simplegraphs.

[Shreyas Srinivas]

So you have a path, you add or remove some vertices. You get a new path.

[Shreyas Srinivas]

This is painless in my definition

[Bhavik Mehta]

And not all graph walk lemmas should be stated in terms of support, for those of us who prefer thinking about the walk in terms of its edges. But there are over 200 declarations about the support of graph walks, so you already can manipulate walks and paths as vertex sequences in mathlib.

[Shreyas Srinivas]

I know that, but if you walk is just a list of vertices, then this manipulation is far more trivial

[Shreyas Srinivas]

Note that I am not opposed to what mathlib calls defeq abuse in my projects. If a proof follows from reduction, that's sometimes a plus in my book.

[Kyle Miller]

@Shreyas Srinivas For what it's worth, using List.IsChain was already considered when we defined the current Walk.

I think it's valid to want to work with lists of vertices, but this its own type. As I'm sure you know from TCS, there's rarely a one-size-fits-all type that handles all possible use cases.

I would suggest the following:

1. Create a structure wrapping up endpoints plus a SimpleGraph.Walk, for the very useful case of a walk without vertex endpoints.
2. Create a constructor for this structure that uses the List.IsChain list interface.
3. Implement supporting API to be able to do induction using this interface.

[Iván Renison]

Creating a structure wrapping up endpoint isn't going to cause a lot of duplication?

[Shreyas Srinivas]

Fwiw, I am not claiming that my approach is perfect for mathlib. But it maps better to my mental model of walks and paths and I get them from the algorithms side of TCS.

[Shreyas Srinivas]

and the avoidance of index issues, especially during cases/induction makes it even better.

[Shreyas Srinivas]

The place I encountered the most annoying index issues was inducting on walks.

[Bhavik Mehta]

Kyle Miller said:

As I'm sure you know from TCS, there's rarely a one-size-fits-all type that handles all possible use cases.

Yes, this is really the key point. The indexed version makes it easy to talk about the non-indexed version, but not vice versa. And since mathlib should be allowing one to talk about whichever version they prefer, we should take the primary definition as the one which allows making all the others conveniently.
My objection isn't to allowing the perspective of walk-as-vertex-list, I instead object to disallowing the perspective of walk-as-matched-edge-list.

[Kyle Miller]

We likely need to restate results @Iván Renison, but we can't be allergic to the appearance of duplication. I don't think there's any way around this. I've seen the need for both indexed walks and non-indexed walks.

[Shreyas Srinivas]

I don't wish to disallow anything. A couple of years ago I mentioned that in TCS we don't go for "most abstract definition" in our theory building, we go for collections of definitions and lemmas that let us move between them as required.

[Bhavik Mehta]

Shreyas Srinivas said:

The place I encountered the most annoying index issues was inducting on walks.

I'm very surprised to hear this, since induction on walks is used super commonly in mathlib already, whereas the statement of induction for walks in the PR linked for HasAdj with the non-indexed definition is shockingly long, and the usages are also not very pleasant.

[Shreyas Srinivas]

Fwiw, in my case you can also work with edgeLists

[Shreyas Srinivas]

It's fairly straightforward to generate the edge list of a walk from that List based definition

[Shreyas Srinivas]

https://github.com/Shreyas4991/mathlib4/pull/1/changes#diff-b55a9b9aa0920cc83b0887bfa90b6cddc3fd4113c6736931da7f7cb75497db5eR147

[Shreyas Srinivas]

In Berge's lemma I use edge lists.

[Shreyas Srinivas]

Which btw also suggests a non-indexed edgeList based definition of walks. Instead of List.IsChain G.Adj you have List.IsChain ... where ... is a relation on two edges that says that the second component of the first edge equals the first component of the second edge. At least, this walks for directed walks even on SimpleGraph.

[Kyle Miller]

@Shreyas Srinivas Please read what I wrote carefully, since I didn't say anything about whether yours was better or not. It's simply a different approach (and also one we evaluated). A big reason List.IsChain is so well developed was in case it was ever used for formalizing some aspect of walks. Edit: I'd give credit to Yakov Pechersky here for using List.IsChain for walks.

For this discussion, can I ask that we avoid making broad claims like "it's better/worse" and instead illustrate points with concrete examples?

[Shreyas Srinivas]

I am not claiming something is better or worse in general. I am describing what worked better or worse for me

[Bhavik Mehta]

Comparing your file with indexed walks:

• the definition of cons (which I'm sure you'll agree is a fundamental operation on walks) is 16 lines long, whereas in mathlib it's definitional
• support is definitional in yours but it's 2 lines in mathlib
• the definition of edge list is 8 lines long in yours but 2 lines in mathlib
• most of the proofs in your example file are quite a bit longer and more intricate than the equivalent mathlib proofs
• cons_induction takes what looks like 40 lines with your definition, but is definitional in mathlib. it's not used in the file you sent, so it's hard to judge how nice it is to use, but the mathlib one is used 18 times and the "setup" before getting to one of the cases is one line

So I'm still interested if you can share a full concrete example where your definition worked better.

[Shreyas Srinivas]

Concretely, I like vertex and edge list definitions because I want to traverse them easily, update weight assignments on them, induct on them and so on in flows. In Berge's lemma I am taking two walks and xoring them. In all these cases, I personally found the fact that each walk has a different type, made things difficult. Maybe there is an optimal path through Mathlib's API I missed. But by quickly hashing out this API, I got rid of those problems.

[Shreyas Srinivas]

Bhavik Mehta said:

Comparing your file with indexed walks:

• the definition of cons (which I'm sure you'll agree is a fundamental operation on walks) is 16 lines long, whereas in mathlib it's definitional
• support is definitional in yours but it's 2 lines in mathlib
• the edge list is 8 lines long in yours but 2 lines in mathlib
• most of the proofs in your example file are quite a bit longer and more intricate than the equivalent mathlib proofs
• cons_induction takes what looks like 40 lines with your definition,
  So I'm still interested if you can share a full concrete example where your definition worked better.

I didn't invest any effort in golfing proofs or definitions of API.

[Bhavik Mehta]

Shreyas Srinivas said:

I know that, but if you walk is just a list of vertices, then this manipulation is far more trivial

I would argue that a "far more trivial" definition or proof shouldn't be this much longer, even if ungolfed

[Shreyas Srinivas]

It's more well structured to me, readability wise. But I rest my case. I am not pushing for any change upstream right now, since I have a lot on my plate. Maybe I will return to this in half a year.

[Iván Renison]

I think that we should considered the HasAdj refactorization and this possible change as separate things. I was going to make HasAdj.Walk with the support because it was suggested in #graph theory > Digraphs @ 💬, but better not to mix things.
So, unless you think I should do something different, for HasAdj.Walk I will mirror SimpleGraph.Walk, and then if the decision is to make some change we do it

[Snir Broshi]

Here's a concrete example where I believe defining a walk in terms of its support would be vastly superior:
(ignore the list lemmas at the beginning)

import Mathlib

namespace List

theorem tail_take {α : Type*} (l : List α) (n : ℕ) :
    (l.take n).tail = l.tail.take (n - 1) := by
  simp [← List.drop_one, List.drop_take]

theorem dropLast_take' {α : Type*} (l : List α) (n : ℕ) :
    (l.take n).dropLast = l.dropLast.take (n - 1) := by
  simp [List.dropLast_eq_take, List.take_take, Nat.sub_min_sub_right]

theorem tail_drop' {α : Type*} (l : List α) (n : ℕ) :
    (l.drop n).tail = l.tail.drop n := by
  simp

theorem dropLast_drop {α : Type*} (l : List α) (n : ℕ) :
    (l.drop n).dropLast = l.dropLast.drop n := by
  simp [List.dropLast_eq_take, Nat.sub_right_comm, List.drop_take]

theorem eq_of_head?_eq_of_tail_eq {α : Type*} (l₁ l₂ : List α) (hh : l₁.head? = l₂.head?)
    (ht : l₁.tail = l₂.tail) : l₁ = l₂ := by
  by_cases hnil₁ : l₁ = []
  · grind [List.head?_eq_none_iff]
  have hnil₂ : l₂ ≠ [] := by grind [List.head?_eq_none_iff]
  rw [← List.cons_head_tail hnil₁, ← List.cons_head_tail hnil₂]
  grind

theorem tail_eq_nil_iff {α : Type*} {l : List α} : l.tail = [] ↔ l.length ≤ 1 := by
  grind [List.length_tail, List.length_eq_zero_iff]

theorem dropLast_eq_nil_iff {α : Type*} {l : List α} : l.dropLast = [] ↔ l.length ≤ 1 := by
  grind [List.length_dropLast, List.length_eq_zero_iff]

theorem eq_of_tail_eq_of_dropLast_eq {α : Type*} {l₁ l₂ : List α} (h : 1 < l₁.length)
    (ht : l₁.tail = l₂.tail) (hd : l₁.dropLast = l₂.dropLast) : l₁ = l₂ := by
  have hnil₁ : l₁ ≠ [] := by grind
  have hnil₂ : l₂ ≠ [] := by grind [dropLast_eq_nil_iff]
  rw [← List.cons_head_tail hnil₁, ← List.cons_head_tail hnil₂, ht]
  have hdnil₁ : l₁.dropLast ≠ [] := by grind [dropLast_eq_nil_iff]
  have hdnil₂ : l₂.dropLast ≠ [] := by grind [dropLast_eq_nil_iff]
  simp [← List.head_dropLast hdnil₁, ← List.head_dropLast hdnil₂, hd]

end List

namespace SimpleGraph.Walk

theorem support_eq_iff_darts_eq {V : Type*} {G : SimpleGraph V} {u₁ v₁ u₂ v₂ : V}
    {p₁ : G.Walk u₁ v₁} {p₂ : G.Walk u₂ v₂} (hnil : ¬p₁.Nil) :
    p₁.support = p₂.support ↔ p₁.darts = p₂.darts := by
  refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
  · refine Dart.toProd_injective.list_map <| List.rightInverse_unzip_zip.injective ?_
    have : Prod.fst ∘ Dart.toProd = fun d : G.Dart ↦ d.fst := rfl
    have : Prod.snd ∘ Dart.toProd = fun d : G.Dart ↦ d.snd := rfl
    grind [map_fst_darts, map_snd_darts]
  · rw [← cons_map_snd_darts, ← cons_map_snd_darts, h]
    have : ¬p₂.Nil := by grind [darts_eq_nil]
    suffices p₁.firstDart hnil = p₂.firstDart this from congrArg (·.fst :: _) this
    grind [firstDart_eq_head_darts]

theorem support_infix_iff_darts_infix {V : Type*} {G : SimpleGraph V} {u₁ v₁ u₂ v₂ : V}
    {p₁ : G.Walk u₁ v₁} {p₂ : G.Walk u₂ v₂} (hnil : ¬p₁.Nil) :
    p₁.support <:+: p₂.support ↔ p₁.darts <:+: p₂.darts := by
  rw [List.infix_iff_getElem?, List.infix_iff_getElem?]
  refine ⟨fun ⟨k, hk, h⟩ ↦ ⟨k, by grind, fun i hi ↦ ?_⟩,
    fun ⟨k, hk, h⟩ ↦ ⟨k, by grind, fun i hi ↦ ?_⟩⟩
  · rw [getElem?_pos _ _ <| by grind, Option.some_inj]
    ext <;> grind [fst_darts_getElem, snd_darts_getElem]
  · rw [getElem?_pos _ _ <| by grind, Option.some_inj]
    by_cases hi' : i = p₁.length
    · have := h <| i - 1
      grind [not_nil_iff_lt_length, snd_darts_getElem]
    have := h i
    grind [fst_darts_getElem]

theorem support_prefix_iff_darts_prefix {V : Type*} {G : SimpleGraph V} {u₁ v₁ u₂ v₂ : V}
    {p₁ : G.Walk u₁ v₁} {p₂ : G.Walk u₂ v₂} (hnil : ¬p₁.Nil) :
    p₁.support <+: p₂.support ↔ p₁.darts <+: p₂.darts := by
  rw [List.prefix_iff_eq_take, List.prefix_iff_eq_take]
  refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
  · have := congrArg List.dropLast h
    rw [List.dropLast_take', ← map_fst_darts, ← map_fst_darts] at this
    have := congrArg List.tail h
    rw [List.tail_take, ← map_snd_darts, ← map_snd_darts] at this
    refine Dart.toProd_injective.list_map <| List.rightInverse_unzip_zip.injective ?_
    have : Prod.fst ∘ Dart.toProd = fun d : G.Dart ↦ d.fst := rfl
    have : Prod.snd ∘ Dart.toProd = fun d : G.Dart ↦ d.snd := rfl
    grind [List.map_take]
  · apply List.eq_of_tail_eq_of_dropLast_eq <| by grind [nil_iff_length_eq]
    · rw [List.tail_take, ← map_snd_darts, ← map_snd_darts, h]
      simp
    · rw [List.dropLast_take', ← map_fst_darts, ← map_fst_darts, h]
      simp

theorem support_suffix_iff_darts_suffix {V : Type*} {G : SimpleGraph V} {u₁ v₁ u₂ v₂ : V}
    {p₁ : G.Walk u₁ v₁} {p₂ : G.Walk u₂ v₂} (hnil : ¬p₁.Nil) :
    p₁.support <:+ p₂.support ↔ p₁.darts <:+ p₂.darts := by
  rw [List.suffix_iff_eq_drop, List.suffix_iff_eq_drop]
  refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
  · have := congrArg List.dropLast h
    rw [List.dropLast_drop, ← map_fst_darts, ← map_fst_darts] at this
    have := congrArg List.tail h
    rw [List.tail_drop', ← map_snd_darts, ← map_snd_darts] at this
    refine Dart.toProd_injective.list_map <| List.rightInverse_unzip_zip.injective ?_
    have : Prod.fst ∘ Dart.toProd = fun d : G.Dart ↦ d.fst := rfl
    have : Prod.snd ∘ Dart.toProd = fun d : G.Dart ↦ d.snd := rfl
    grind [List.map_drop]
  · apply List.eq_of_tail_eq_of_dropLast_eq <| by grind [nil_iff_length_eq]
    · rw [List.tail_drop', ← map_snd_darts, ← map_snd_darts, h]
      simp
    · rw [List.dropLast_drop, ← map_fst_darts, ← map_fst_darts, h]
      simp

end SimpleGraph.Walk

[Snir Broshi]

Basically anything that uses Walk.support / Walk.edges / Walk.darts will probably become much shorter.

[Snir Broshi]

Also we'd finally be able to deprecate getVert in favor of support.get (or getD)

[Bhavik Mehta]

Interesting... it's not clear to me that these ones would change much at all, since these are theorems about lists and are essentially agnostic to the way Walk is defined. Can you say more about why you think these would get better?

[Snir Broshi]

Oh and Walk.copy of course. But Walk.append would become a bit harder – we would probably require a proof that the walks match.

[Snir Broshi]

Bhavik Mehta said:

Can you say more about why you think these would get better?

It would certainly save these 2 lines that appear in 3 proofs above:

    have : Prod.fst ∘ Dart.toProd = fun d : G.Dart ↦ d.fst := rfl
    have : Prod.snd ∘ Dart.toProd = fun d : G.Dart ↦ d.snd := rfl

because Walk.darts would presumably be of type List (V × V), and the .Adj proof would be a separate theorem.
But you might be right, maybe the problem in these proofs is just that List.zip has poor API.