Tutte's theorem

Stream: mathlib4

[Pim Otte]

I have a proof of Tutte's theorem that compiles. This topic will serve as a tracker for upstreaming it into mathlib.

Merged PRs:

• #11667
• #14622
• #12960
• #14623
• #14977
• #15237
• #15357
• #15539
• #16352
• #15652
• #17436
• #19094
• #18905
• #19250
• #19611
• #20023
• #19373
• #19377
• #20602
• #20800
• #20024
• #20830
• #20398
• #18878
• #20705 (not mine, but needed)
• #21250
• #21981
• #22034
• #22125

Open PRs, in dependency order:

• #22119
• #22915

Closed, unmerged PRs:

• #14976
• #16610
• #15666
• #21097

[Yaël Dillies]

Hey, thanks for the good work! Please ask for my review on github when you open a combinatorics PR :smile:

[Pim Otte]

There's a couple of things that I suspect are a bit wonky, so I'm looking for some feedback on how to improve that, or an indication that the direction I took is likely fine.

• Extending a matching free graph to a maximal one
• Definition of alternating subgraph
• Explicit construction of a path in a subgraph that's a cycle
• Explicit construction of matching-alternating path that yields contradiction matching

These are kind of major things that I'm not entirely sure I went the right way on, so if anyone has pointers for better ways to approach these I'd love to hear them. I have a lot of time the coming month and a half, so I could put some time into working out vague ideas too, anything helps:)

[Peter Nelson]

Tutte’s theorem is a good project!

You are doing quite a bit of work considering maximal objects with definitions from scratch. i think you could tighten things by using the material in Order.minimal.

[Pim Otte]

@Yaël Dillies As follow-up to this discussion I started a rewrite of sndOfNotNil to getVert

Is this a sane definition of tail, or is this going to cause problems down the road?

/-- The walk obtained by removing the first dart of a non-nil walk. -/
def tail (p : G.Walk u v) (hp : ¬ p.Nil) : G.Walk (p.getVert 1) v :=
  p.notNilRec (@fun _ _ _ _ q => getVert_zero _ ▸ (getVert_zero q ▸ q)) hp

[Yaël Dillies]

Looks sensible

[Yaël Dillies]

You might even want to generalise it to drop first

[Yaël Dillies]

The ¬ p.Nil assumption looks like it can now go away

[Pim Otte]

Yaël Dillies said:

You might even want to generalise it to drop first

I don't quite get this, what are you suggesting here?

[Yaël Dillies]

Here is a parallel: docs#List.tail is a special case of docs#List.drop. It looks like your new definition straightforwardly generalises to drop (by replacing the 1 by an arbitrary number), meaning that you can define it first then recover tail as drop 1

[Pim Otte]

Gotcha, I think this does feel okay, I'll go down this path:

/-- The walk obtained by removing the first n darts of a walk. -/
def drop {u v : V} (p : G.Walk u v) (n : ℕ) : G.Walk (p.getVert n) v :=
  match p, n with
  | .nil, _ => .nil
  | p, 0 => getVert_zero _ ▸ (getVert_zero p ▸ p)
  | .cons h q, (n + 1) => cons_getVert_succ _ h ▸ q.drop n

/-- The walk obtained by removing the first dart of a non-nil walk. -/
def tail (p : G.Walk u v) : G.Walk (p.getVert 1) v := p.drop 1

[Pim Otte]

Thanks!

[Pim Otte]

@Yaël Dillies Another small query. Is the thing below legal? I don't think I've ever seen a hole in a statement, but I don't quite know what would fill it:

@[simp]
lemma cons_tail_eq (h : G.Adj u v) (p : G.Walk v w) : (p.cons h).tail = getVert_zero _ ▸ p := by
  match p with
  | nil =>
    simp only [cons_getVert_succ]
    rfl
  | cons h q =>
    simp only [cons_getVert_succ]
    rfl

[Yaël Dillies]

Oh you should use Walk.copy rather than ▸ here

[Pim Otte]

In the drop definition or just in the lemma?

[Yaël Dillies]

Both

[Pim Otte]

@Yaël Dillies I'm having trouble proving the lemma below and now I'm doubting if it's even true. The documentation mentions that Subgraphs are not boolean algebra because of verts. I feel like I'm overlooking something to do with that. Any thoughts?

import Mathlib.Combinatorics.SimpleGraph.Subgraph

namespace SimpleGraph.Subgraph

theorem sdiff_adj' {V} {a b : V} {G : SimpleGraph V} {G₁ G₂ : Subgraph G}: (G₁ \ G₂).Adj a b ↔ G₁.Adj a b ∧ ¬G₂.Adj a b := by
  constructor
  · intro h
    refine ⟨h.1 (le_sup_right : G₁ ≤ G₂ ⊔ G₁), ?_⟩
    intro h'
    have := h.1
    sorry
  · intro ⟨h₁, h₂⟩

    sorry

[Peter Nelson]

I am still trying to wrap my head around how sdiff is defined for SimpleGraph.Subgraph, but your statement looks like it might be false because if a and b are vertices of both graphs, they are not vertices of the difference, so the RHS can hold without the LHS holding.

[Yaël Dillies]

Yes, Peter is exactly right

[Pim Otte]

Ok, so in that case, does it make sense to revisit this PR ? The current definition of symmDiff builds on the sdiff from the Lattice instance, but for augmenting matchings we definitely do need to be more inclusive of vertices.

[Peter Nelson]

Yes, this notion of difference isn’t the right one for augmenting paths. But perhaps it is useful for other things.

Augmenting path arguments are probably more at home with the boolean algebra on SimpleGraph V rather than on subgraphs. In proving something like Tutte’s theorem, do you ever need to consider a graph with strictly fewer vertices?

[Peter Nelson]

Specifically, the coercion of Iic G to a type is essentially the type of spanning subgraphs of G - probably a proof of Tutte will go smoothly if you stay in that setting.

[Pim Otte]

I sort of ended up with Subgraphs because that's where IsMatching is, but I think what you're saying makes sense, so I'll try that route:)

[Pim Otte]

Peter Nelson said:

Tutte’s theorem is a good project!

You are doing quite a bit of work considering maximal objects with definitions from scratch. i think you could tighten things by using the material in Order.minimal.

I just realized that the reason I ended up doing something specific is that I needed [Decidable G.Adj] for the resulting graph.
A general approach using order on a set of graphs that's matching-free won't get me [Decidable G.Adj] for a maximal element, and adding the decidability as a constraint might mean the maximal in the set is not maximal from a matching-free point of perspective.

Am I missing something? Is there a cleaner way to do this, making use of existing theory?

[Yaël Dillies]

Why don't you just use classical?

[Pim Otte]

For some reason I thought that wasn't possible, but reflecting on it I think I know how to do that now, thanks:)

[Pim Otte]

@Yaël Dillies I had set up some infrastructure for graphs consisting of a single edge: def, example usage

Is that something that makes sense to PR or did I miss a more idiomatic way to handle that?

[Yaël Dillies]

That sounds reasonable, but I think I remember @Jeremy Tan doing something similar? so maybe coordinate

[Pim Otte]

Jeremy pointed me to https://github.com/leanprover-community/mathlib4/blob/dc72d4cff3bc92208c623e848ba1e493ed474f5d/Mathlib/Combinatorics/SimpleGraph/Operations.lean#L145, so I'll build on that:)

[Pim Otte]

I've split off a somewhat coherent part of the argument, but I'm doubting how to move forward in polishing it for mathlib. See here for the work in progress.

A lot of the proof of Tutte as a whole works with the following stuff:

• {v : V | ∀ w, v ≠ w → G.Adj w v} the nodes connected to all other nodes
• ((⊤ : Subgraph G).deleteVerts {v : V | ∀ w, v ≠ w → G.Adj w v}).coe the graph created by deleting these nodes.

In addition I have:

let rep := fun (c : ConnectedComponent Gsplit.coe) => c.exists_vert.choose
let oddVerts := Subtype.val '' (rep '' {(c : ConnectedComponent Gsplit.coe) | Odd (c.supp.ncard)})

which is specific to this part of the proof, a subset of nodes, one from each odd component.

I currently have some sub-results in "haves", but this function is growing way too long and the compiler feedback loop is a bit long.

I see a couple of options:

• Keep it like this
• Extract the haves to lemmas, not abstracting the names
• Introduce definitions with names for the objects above and then prove lemmas about them. (I'm not aware of commonly used names for above objects, so I'd make something up)

In the end I'm tempted to put all of this in a file specifically for Tutte's theorem.

@Yaël Dillies Any thoughts on the above, as big-picture stuff? (I'm aware there's probably a lot to be golfed and polished on the detailed level, but I'd love to do that in a proper global structure.)

[Kim Morrison]

I think you should come up with names for those things, and prove lemmas about them. It's the mathlib way. :-)

allConnectedVerts and deleteAllConnectedVerts?

[Etienne Marion]

Hi! @Pim Otte you opened #20024 and #21097 which I think define the same thing, but the former being specific to connected components while the latter working for any quotient. It seems reasonable to me to have a SetLike instance for equivalence classes but in that case I think ConnectedComponent should be reworked for that change? In particular couldn't there be a conflict between the two SetLike instances? (there is already one for ConnectedComponents) Tagging @Yaël Dillies and @Bhavik Mehta who reviewed #20024.

[Pim Otte]

@Etienne Marion yes, there's a related question I've asked in #20024 too, about the usage of explicit calls to .supp rather than using coercion.

Since #21097 is in a new file, there's no immediate problems, and I'd be happy to do a follow-up PR refactoring to switch to the new instance (and possibly coercion instead of explicit supp), or include it in #21097 if that's preferable

I'm not sure which one is preferable from a strategic point, so that's something that I also look to @Bhavik Mehta for (or maybe @Kyle Miller ?)

[Bhavik Mehta]

I'll take a look at this tomorrow, unless someone beats me to it!

[Bhavik Mehta]

I agree it seems reasonable to have a SetLike instance for equivalence classes, and that ConnectedComponent should be reworked for that. Probably the best way forward is to get #21097 merged, then follow up amending ConnectedComponent, and then adapt #20024 to adjust (or maybe it'll be redundant by that point).

[Pim Otte]

Sounds good:) I'm pretty sure that #20024 will be redundant, I tested one of the earlier variations and they were all defeq, so I'll close that one and follow up once #21097 is merged