Potential submission to Formal Conjectures

Stream: new members

[Timothy Chow]

I'm considering submitting a conjecture of mine to the Formal Conjectures project. With some help from Lean Finder, I have managed to construct a pretty short and (I believe) correct formalization of the conjecture. However, there is a feature of the formalization that feels kludgy to me, and I'm wondering if there's a cleaner approach.

The code is short enough that I think it's not too obnoxious to post it here in its entirety.

import Mathlib
variable {α : Type*} [DecidableEq α]

/- The union of k finsets supplied by a function `Fin k → Finset α`. -/
def unionOfFinK (k : Nat) (f : Fin k → Finset α) : Finset α :=
  Finset.biUnion (Finset.univ : Finset (Fin k)) f

namespace SimpleGraph

/- The maximum size of the union of k independent sets. -/
noncomputable def independenceNumK (G : SimpleGraph α) (k : Nat) : Nat :=
  sSup { n | ∃ f : Fin k → Finset α, (∀ i, G.IsIndepSet (f i)) ∧ ((unionOfFinK k f).card = n) }

/- A finite graph is cdsColorable if it has a proper coloring
  by natural numbers such that for all k > 0, the number of
  vertices with color < k equals the maximum size of
  the union of k independent sets. -/
def cdsColorable [Fintype α] {G : SimpleGraph α} : Prop :=
  ∃ (C : G.Coloring Nat), ∀ k : Nat, k > 0 →
  ∑ i ∈ Finset.range k, (C.colorClass i).ncard = independenceNumK G k

open YoungDiagram

def YoungDiagram.Cell (μ : YoungDiagram) : Type := Subtype fun c : ℕ × ℕ => c ∈ μ

/- The simple graph of a Young diagram: two distinct cells are
  adjacent iff they lie in the same row or in the same column. -/
def YoungDiagram.toSimpleGraph (μ : YoungDiagram) : SimpleGraph (YoungDiagram.Cell μ) :=
  SimpleGraph.fromRel fun a b =>
    (Prod.fst a.val = Prod.fst b.val) ∨ (Prod.snd a.val = Prod.snd b.val)

/- The Latin Tableau Conjecture: If G is the simple graph
  of a Young diagram, then G is cdsColorable. -/
theorem LatinTableauConjecture (μ : YoungDiagram) [Fintype (YoungDiagram.Cell μ)]
   [DecidableEq (YoungDiagram.Cell μ)] :
     (YoungDiagram.toSimpleGraph μ).cdsColorable := by sorry

The part that feels kludgy is taking the union of k finite sets. I was a bit surprised that this didn't seem to be explicitly in mathlib. Did I miss something? The code for unionOfFinK was generated by Lean Finder and seems to be correct, but is there a cleaner approach?

[Snir Broshi]

What about defining independenceNumK using Sets? Since you're only dealing with finite graphs that should be equivalent, though the independence number for infinite graphs might change.

noncomputable def independenceNumK (G : SimpleGraph α) (k : Nat) : Nat :=
  sSup { n | ∃ f : Fin k → Set α, (∀ i, G.IsIndepSet (f i)) ∧ (iSup f).ncard = n }

[Snir Broshi]

You can also do:

noncomputable def independenceNumK (G : SimpleGraph α) (k : Nat) : Nat :=
  sSup { (iSup (Subtype.val ∘ f)).ncard | f : Fin k → Subtype G.IsIndepSet }

[Timothy Chow]

Thanks! I like your first solution. I would likely have typed \bigcup i, f i rather than iSup f. Is there a difference?

[Kevin Buzzard]

import Mathlib

example {k α} (f : Fin k → Set α) : ⋃ i, f i = iSup f := rfl -- works
example {k α} (f : Fin k → Set α) : ⋃ i, f i = iSup f := by with_reducible_and_instances rfl -- fails

Seems like they're definitionally equal if we allow unfolding, but not if we don't.

set_option pp.notation false
example {k α} (f : Fin k → Set α) : ⋃ i, f i = iSup f := by
  unfold Set.iUnion
  -- ⊢ Eq (iSup fun i ↦ f i) (iSup f)
  with_reducible_and_instances rfl

So the difference is (1) Set.iUnion is a def, so some things (e.g. exact, rfl) can see through it and other things (e.g. rw, simp, typeclass inference) can't and (2) zeta reduction or whatever it's called: fun i ↦ f i reduces to f because of some reduction rule in type theory.