Formalization of Vizing's theorem

Stream: graph theory

[arohee]

I just finished formalizing a constructive proof of Vizing's theorem in Lean:

Every simple undirected graph can be edge colored using a number of colors that is at most one greater than the maximum degree of the graph.

In particular, my proof is a verified implementation of the Misra and Gries edge coloring algorithm, which is also polynomial time.

My formalization can be found here: https://github.com/aroheebhoja/vizing/blob/main/Vizing/Main.lean

I plan to write up this result, as well as submit some auxiliary lemmas (mostly about lists and arrays) as contributions to Mathlib.

Would appreciate any comments or advice!

[Vlad Tsyrklevich]

Nice work! I looked at the upsteaming file, some quick notes:

• For mathlib style, numerical indices like h1 should subscripts, e.g. h\1
• You can use dot notation to shorten some proofs, e.g. if foo has type List, you can use foo.bar instead of List.bar foo.
• For chain'_mem_notMem_of_nodup_prefix_length_lt, there's two things proved and the first doesn't have to do with List.Chain' so those should be separate, and the second conclusion seem like it may just be a form of chain'_rel_of_idx_consec so perhaps it is subsumed at that
• Incidentally, I have a form of chain'_rel_of_idx_consec under review at #25812
• pop_size_lt can be proved by grind, which means perhaps it should just be inlined wherever it's used as such.

[Vlad Tsyrklevich]

• length_le_length_of_nodup_of_subset can be proven using the term L.subperm_of_subset hl hsubset |>.length_le. Since you only use it in one place, it may be worth inling.
• Instead of back_of_back? being an existential, perhaps it should be a lemma relating back? to back like List.getLast?_eq_getLast is for Lists

[Snir Broshi]

Incredible! Do you plan to submit the Vizing proof to Mathlib?

[Chris Wong]

You might like to use docs#Sym2, which handles the symmetry condition for you. Though I'm not sure how that would work with your array representation.