Partial vertex colorings and (partial) edge colorings

Stream: Is there code for X?

[arohee]

Hello! Has anyone defined the notion of a partial vertex coloring or an edge coloring on a SimpleGraph? These definitions don't seem to be in Mathlib since they aren't in SimpleGraph.Coloring (docs#SimpleGraph.Coloring). If not, are there any suggestions for the most useful ways to define them? The docs suggest that a partial vertex coloring should be a Coloring of a subgraph, and I was thinking that an EdgeColoring could be a Coloring of a LineGraph but I'm not sure if that's the best way to go about it. Thanks in advance!

[Kalle Kytölä]

I am not working in combinatorics, but I have been discussing topics which involve partial graph labeling problems with @Jukka Suomela and @Henrik Lievonen and others.

I believe one useful approach is to have colorings with color set Option Color (where Color : Type is the type of actual colors you consider), and then define a "partial relaxation" of the local check of having distinct colors for each edge which will also accept an edge if at least one label is none (a missing label). Of course it depends on your use case and it will only be seen in pursuing the use case whether a given definition is good to work with. (I believe the following one is not unreasonable to work with.)

import Mathlib

/-- The local checking predicate of an edge-checkable graph problem with output label alphabet Γ. -/
structure EdgeCheck (Γ : Type*) where
  check : Γ → Γ → Prop

/-- The graph problem determined by an edge-checkable graph problem. -/
def EdgeCheck.problem {Γ : Type*} (EC : EdgeCheck Γ) {V : Type*} (G : SimpleGraph V) (φ : V → Γ) :=
  ∀ u v, G.Adj u v → EC.check (φ u) (φ v)

/-- The partial relaxation of an edge-checkable problem, allowing missing lablels and accepting
any edge where at least one of the adjacent labels is missing. -/
def EdgeCheck.partial (Γ : Type*) (EC : EdgeCheck Γ) : EdgeCheck (Option Γ) where
  check o₁ o₂ := match o₁, o₂ with
    | none, _ => true
    | some _, none => true
    | some c₁, some c₂ => EC.check c₁ c₂

/-- The edge check predicate for proper colorings. -/
def coloringEC (Γ : Type*) : EdgeCheck Γ where
  check c₁ c₂ := c₁ ≠ c₂

-- The partial 4-coloring problem for the 37-cycle:
#check ((coloringEC (Fin 4)).partial).problem (SimpleGraph.cycleGraph 37) -- Type: `(Fin 37 → Option (Fin 4)) → Prop`

/-- Sanity check bijective correspondence between the labelings that satisfy `coloringEC.problem`
and Mathlib's `SimpleGraph.coloring`. -/
def coloringEC.equiv_coloring (Γ : Type*) {V : Type*} (G : SimpleGraph V) :
    {φ // (coloringEC Γ).problem G φ} ≃ G.Coloring Γ where
  toFun φ := ⟨φ, fun h_adj ↦ φ.prop _ _ h_adj⟩
  invFun φ := ⟨φ, fun _ _ h_adj ↦ φ.valid h_adj⟩
  left_inv _ := rfl
  right_inv _ := rfl