David Philipps

Stream: new members

[David Philipps]

Hi there, my Name is David and I am thinking about starting to use Lean in my mathematical work. I wrote paper in Structural Graph Theory (https://arxiv.org/abs/2502.15396), featuring versions of the Cops and Robbers game and some monotonicity results, that I would like to formalize. My goal is to learn Theorem Proving in the process and I have some questions from the start:

1. Is Lean the right tool? Should I look into alternatives like Coq before starting?
2. How much combinatorical game theory etc. is already formalized that would be useful?
3. Is that a realistic undertaking?
4. How to start?

I hope someone can give me some insight in this community to help me get going! Thanks in advance!

Kind regards,
David Philipps

[Luigi Massacci]

Taking a look at #general > Combinatorial game theory repository and related conversations in that channel should be a good start on question 2, as for graph theory itself, there's plenty in mathlib.

[Luigi Massacci]

For question 4, see the community page for learning lean

[David Philipps]

I started my journey but now I am stuck on a thing: I have this definition for degeneracy

noncomputable def degeneracy {V : Type*} [Fintype V] (G : SimpleGraph V) [G.LocallyFinite] : Nat :=
  sInf {n : ℕ | ∃ L : Layout V, isValidDegeneracy G L n}

, but i also saw Nat.find and seems to be more useful? How can I rewrite this with Nat.find? All my approaches fail :/

[Kevin Buzzard]

Can you edit your post to make it into a #mwe using #backticks ? It's not completely essential for understanding in this case but it's good practice so we gently encourage it :-)

[David Philipps]

Edit: here my full code and where I am going with it:

import Mathlib.Combinatorics.SimpleGraph.Basic
import Mathlib.Combinatorics.SimpleGraph.Finite
import Mathlib.Order.Defs.LinearOrder
import Mathlib.Data.Nat.Lattice
import Mathlib.Data.Fin.Basic
import Mathlib.Order.Basic
import Mathlib.Data.Set.Basic
import Mathlib.Data.Finset.Basic

namespace SimpleGraph

def Layout (V : Type*) := LinearOrder V

def countAdjPred {V : Type*} (G : SimpleGraph V) [G.LocallyFinite] (L : Layout V) (v : V) : Nat :=
  Finset.card { w ∈ G.neighborFinset v | L.lt w v }

def isValidDegeneracy {V : Type*} (G : SimpleGraph V) [G.LocallyFinite] (L : Layout V) (k : Nat) : Prop :=
  ∀ v : V, countAdjPred G L v ≤ k

noncomputable def degeneracy {V : Type*} [Fintype V] (G : SimpleGraph V) [G.LocallyFinite] : Nat :=
  sInf {n : ℕ | ∃ L : Layout V, isValidDegeneracy G L n}

theorem clique_has_deg_n (n : ℕ) : degeneracy (completeGraph (Fin (n+1))) ≥ n := by
  unfold degeneracy
  apply LE.le.ge
  apply le_sInf

the last line does not work, but I dont understand the error and how to resolve it. Transitioning to Nat.find is one apporach that I am trying out.

[Luigi Massacci]

Ahhh, I feel like this is a part of mathlib where it's easy to get papercuts. Do you know what a complete lattice is? le_sInf doesn't apply because the natural numbers don't form one. You should use le_csInf instead

[David Philipps]

Works like a charm :))

[David Philipps]

Okay I now have 99% of the proof through trial and error but the last thing confuses me.

import Mathlib.Combinatorics.SimpleGraph.Basic
import Mathlib.Combinatorics.SimpleGraph.Finite
import Mathlib.Order.Defs.LinearOrder
import Mathlib.Data.Nat.Lattice
import Mathlib.Data.Fin.Basic
import Mathlib.Order.Basic
import Mathlib.Data.Set.Basic
import Mathlib.Data.Finset.Basic
import Mathlib.Data.Fin.Basic

namespace SimpleGraph

/-- A layout is represented as a linear ordering of vertices -/
def Layout (V : Type*) := LinearOrder V


/-- Count of adjacent predecessors for a vertex v in a given layout -/
def countAdjPred {V : Type*} (G : SimpleGraph V) [G.LocallyFinite] (L : Layout V) (v : V) : Nat :=
  Finset.card { w ∈ G.neighborFinset v | L.lt w v }

/-- Verifies if a number k satisfies the degeneracy condition for a given layout -/
def isValidDegeneracy {V : Type*} (G : SimpleGraph V) [G.LocallyFinite] (L : Layout V) (k : Nat) : Prop :=
  ∀ v : V, countAdjPred G L v ≤ k

/-- The degeneracy (δ*) of a graph is the minimal k over all possible layouts such that
    for each vertex v, there are at most k vertices w ≺ v that are adjacent to v -/


noncomputable def degeneracy {V : Type*} [Fintype V] (G : SimpleGraph V) [G.LocallyFinite] : Nat :=
  sInf {n : ℕ | ∃ L : Layout V, isValidDegeneracy G L n}


theorem clique_has_deg_n (n : ℕ) : degeneracy (completeGraph (Fin (n+1))) = n := by
  unfold degeneracy
  have nonEmpty : n ∈ {n_1 | ∃ L, (completeGraph (Fin (n + 1))).isValidDegeneracy L n_1} := by
    simp
    let L : LinearOrder (Fin (n+1)) :=  inferInstance
    use L
    unfold isValidDegeneracy
    intro v
    refine le_trans ?_ (Nat.le_pred_of_lt v.prop)
    unfold countAdjPred

    trans {w | w < v}.toFinset.card
    · apply Finset.card_le_card
      intro w hw
      simp only [Finset.mem_filter] at hw
      exact Set.mem_toFinset.mpr hw.2
    · calc
      -- There are at most v elements less than v
      _ = ({w | w < v}.toFinset.map ⟨Fin.val, Fin.val_injective⟩).card :=
        (Finset.card_map _).symm
      _ = ({w : ℕ | w < v.val }).toFinset.card := by
        congr 1
        simp
        ext w
        simp
        constructor <;> intro h
        · obtain ⟨a, ha, rfl⟩ := h
          exact_mod_cast ha
        · use ⟨w, ?_⟩, ?_
          · apply h.trans v.prop
          · exact_mod_cast h
      _ = (Finset.range v.val).card := by
        congr
        exact Set.toFinset_ofFinset (Finset.range ↑v) (Set.fintypeLTNat._proof_34 ↑v)
      _ ≤ _ := by
        apply le_of_eq
        exact Finset.card_range ↑v

  apply le_antisymm
  · -- Show degeneracy ≤ n-1
    apply Nat.sInf_le
    exact nonEmpty

  · apply le_csInf
    · exact Set.nonempty_of_mem nonEmpty
    · simp only [Set.mem_setOf_eq]
      simp only [forall_exists_index]
      intro n' L
      intro hvalid
      unfold isValidDegeneracy at hvalid
      specialize hvalid n
      unfold countAdjPred at hvalid
      unfold neighborFinset at hvalid
      unfold neighborSet at hvalid
      unfold Adj at hvalid
      apply le_trans _ hvalid
      apply le_of_eq
      symm
      simp only [completeGraph_eq_top, top_adj, ne_eq, Set.toFinset_setOf]
      rw [Finset.filter_filter]

The final goal is

{a | ¬↑n = a ∧ a < ↑n}.card = n

How can i translate between sets and types like Fin n?

[Aaron Liu]

Are you sure this is true? Can you provide an informal proof?

[Kevin Buzzard]

Informally it looks good to me: we have a : Fin (n + 1) and both of the criteria defining the finset say that it's not n, so you have 0,1,...,n-1 left. What am I missing?

[Aaron Liu]

The < is not the normal Fin <

[Kevin Buzzard]

Lol what the heck?

[Kevin Buzzard]

How can let L : LinearOrder (Fin (n+1)) := inferInstance give a < which is not the normal one?

[Kevin Buzzard]

Adding

theorem extracted (n : ℕ) : (Finset.filter
  (fun a : Fin (n + 1) ↦ ¬(n : Fin (n + 1)) = a ∧ a < (n : Fin (n + 1)))
  Finset.univ).card = n := sorry

(I don't know what notation for Finset.filter is) then indeed exact extracted n fails and convert extracted n gives

⊢ Preorder.toLT = instLTFin

[Aaron Liu]

Kevin Buzzard said:

How can let L : LinearOrder (Fin (n+1)) := inferInstance give a < which is not the normal one?

That's not where the L comes from, that's a different L in a different context

[Aaron Liu]

The L that is not the normal linear order comes from intro n' L

[Aaron Liu]

And specialize hvalid n made the goal unprovable

[David Philipps]

Ahh I see, so I need to access the maximal element according to L. Currently trying to figure our how one does that, open for tipps

[Kevin Buzzard]

There's Finset.max' which you could apply to Finset.univ and there's also \top if the instances are there (a finite linear order is a complete lattice).

[Aaron Liu]

I'm guessing the instance is not there because you would be synthesizing data

[David Philipps]

What does synthesizing data mean? I read it multiple times in errors, but what is it about?

[Kevin Buzzard]

Typeclass inference (the square bracket system) works best when there's at most one instance of everything. You might have run into this already in your argument because you've been putting more than one < on Fin (n + 1). The problem with typeclass inference creating data is that then you might end up with two different instances pointing at the same thing. And by "different" I include the case where actually the objects are the same but the proof that they're the same isn't rfl. So if you choose a total order on Fin n then there's a danger if you get typeclass inference to start making a top element in the sense that even though there's only one top element, there's more than one way to make it, and this might confuse the system.