How to state this graph problem

Stream: new members

[Gareth Ma]

Me and my friend have been working on formalising a graph theory problem from his bachelor's thesis! Here are the core definitions we have been working with:

• Let $G = (V, E)$ be a finite simple undirected graph, write $e(u, v)$ for the adjacency function (so True when they're adjacent), and $n(u) = \{v \in V \colon e(u, v)\}$ be the neighbours.
• Now $V$ can be any set, so we further consider a labelling $\ell \colon V \hookrightarrow \mathbb{Z}$, i.e. label each vertex with an integer. Actually we might as well make it a V \equiv Fin n but see below. Intuitively we're literally flattening the vertices into a horizontal line preserving the edges ofc.
• Fixing such labelling, we define the "previous neighbours" to be $n_{\ell}(u) = \{v \in n(u) \colon \ell(v) < \ell(u)\}$, so only the "back edges".
• Finally, we define a function $F(G)$ to be minimum $k$ such that there exists $\ell$ such that $\forall u, n_{\ell}(u) \leq k$
• Important note: in one of our proofs, we want to construct $\ell$ by induction. More specifically the proof picks $v \in V$ (satisfying some properties), sets $\ell(v)$ to be "the maximum element" of Fin n (or for $\mathbb{Z}$ a large enough one, say $|V|$), then combine that with $\ell' \colon V \setminus \{v\} \hookrightarrow \mathbb{Z}_{< \ell(v)}$ (or to Fin (n - 1)).

From my experience, it's usually nicest when the indexing types etc. are made very generalised, so I assume G should be of type SimpleGraph ι with Fintype ι. But I am not sure about the $\ell$ function.
(1) As mentioned, we tried making it l : ι ≃ Fin (Fintype.card ι) or something but that becomes tricky when we do the induction step.
(2) We also tried l : Equiv.Perm ι, but that means we need a LinearOrder on ι directly, which isn't exactly accurate? ($V$ is not ordered). The advantage here is we can use Equiv.Perm.subtypeCongr to construct $\ell$ from $\ell'$.
(3) Finally I'm trying {ι : Type u} [Fintype ι] (α : Type u) [LinearOrder α] (l : ι ↪ α) now, but I again face issues with the induction step, and also how to pick a large element a of α and say "consider the type α - a"

I can give more details and precise Lean statements as well, but didn't want to cluster this long question :)

[Shreyas Srinivas]

are you trying to construct a dfs tree with fronds back-edges?

[Gareth Ma]

As in the final goal? No, it's not about dfs tree

[Gareth Ma]

You can see the exact statement here

[Gareth Ma]

(If $\forall \emptyset \neq U \subseteq V$, there is a vertex $u \in U$ with $|n(u) \cap U| \leq k$, then $F(G) \leq k$. Proof: we construct the $\ell$ defined above. Set $U = V$, take that $u$ and set $\ell(u) =$ something large enough. Then consider $U' = {u}^c$, take the $u' \in U'$ from hypothesis, and set $\ell(u') =$ an element less than $\ell(u)$ etc.)

[Kyle Miller]

With these $\ell$ functions, just to check, using $\mathbb{Z}$ is irrelevant, right? It would be fine to label using positive natural numbers?

If so, you might consider using ℓ : Finsupp V ℕ and declare "ℓ v > 0 means v is labeled".

Regarding your point (1), I would avoid using an explicit equivalence. Fintype V should be fine. You can do induction on the cardinality of the support of ℓ (docs#Finsupp.support).

[Kyle Miller]

That is, you might start up your induction by doing induction hcard : ℓ.support.card (You may need to make sure you are in a newer version of Lean for this syntax. Worst case you can use generalize hcard : ℓ.support.card = n followed by induction n.)

[Gareth Ma]

So to say the graph is fully labelled I would say \forall v, ℓ v > 0 and also Function.Injective ℓ?

[Kyle Miller]

Yeah, that seems right.

Or, for the first condition, you can say ℓ.support = Finset.univ, which involves a term that appears in the induction (in ℓ.support.card).

[Gareth Ma]

Do you have an example of how the induction would work? If I have

example {ι : Type*} [Fintype ι] : ∃ ℓ : ι →₀ ℕ, ℓ.support = Finset.univ := by
  sorry

I can't do induction \ell directly right

[Kyle Miller]

Maybe something like this:

import Mathlib

example {ι : Type*} [Fintype ι] : ∃ ℓ : ι →₀ ℕ, ℓ.support = Finset.univ := by
  suffices ∀ n ≤ Fintype.card ι, ∃ ℓ : ι →₀ ℕ, ℓ.support.card = n by
    obtain ⟨ℓ, h⟩ := this (Fintype.card ι) le_rfl
    use ℓ
    rwa [Finset.card_eq_iff_eq_univ] at h
  intro n hn
  induction n with
  | zero =>
    use 0
    simp
  | succ n ih =>
    specialize ih (Nat.le_of_succ_le hn)
    obtain ⟨ℓ, hℓ⟩ := ih
    /-
    ι : Type u_1
    inst✝ : Fintype ι
    n : ℕ
    hn : n + 1 ≤ Fintype.card ι
    ℓ : ι →₀ ℕ
    hℓ : ℓ.support.card = n
    ⊢ ∃ ℓ, ℓ.support.card = n + 1
    -/

[Gareth Ma]

got it! thanks so much

[Gareth Ma]

https://gist.github.com/grhkm21/1438e449e2c2f4cd3aed1773bb23a94f

[Gareth Ma]

Now I wonder how long it would take to explain the approach + all the minor details to my friend :3
I'll probably delete some of the proofs and let him play around + proof himself

[Gareth Ma]

Thanks once again!