induction on number of vertices

Stream: graph theory

[Robin Petit]

Hi everyone, Lean beginner here.

TLDR: how to write a proof by induction on the size of a graph?

I wanted to write a formal proof of Caro-Wei's theorem (providing a lower bound on the independence number of a graph, solely based on the degree distribution), and the typical proof is by induction on the number of vertices. Since SimpleGraph is not an inductive type in Lean, here is the way I managed to do it (full code on GitHub) :

theorem _CaroWei : ∀ {n : ℕ} {G : SimpleGraph V} (G' : G.Subgraph) {_ : Finset.card G'.vertsF = n}
    [DecidableRel G.Adj] [DecidableEq V], Nonempty (_CaroWeiSolution G') := by
  intro n
  induction n with
  | zero =>
      intro G G' h _ _
      exact @_CaroWei_on_empty_subgraph ...
  | succ n ih =>
      -- ...
      obtain ⟨v, _⟩ := -- ...
      let H := G'.induce (G'.verts \ {v})  -- H = G-v
      have Hcard : #H.verts.toFinset = n := by grind
      let sol_H := Nonempty.some <| @ih G H Hcard _ _  -- apply induction on H = G-v
      -- ...

Is this the right way to do or is there a better (or more correct) way to do?

Also I ended up formulating the result in terms of subgraphs to prevent type coersion: while $G$ has type SimpleGraph V, $G-v$ has type SimpleGraph ↑(@Set.univ V \ {v}), so the canonical injection w ↦ w.val must be explicit all the way through and this is really cumbersome. Yes this feels like a _hacky way_ to proceed, basically treating a graph on n vertices as a subgraph of a graph isomorphic to $K_n$ and this requires to write every theorem in terms of SimpleGraph.Subgraph in addition to having them written in terms of SimpleGraph. This feels like things would be easier if graphs were defined as a pair $(V, E)$ on a given type (i.e. SimpleGraph α would contain V : Set α and E : Set (Sym2 α) with a property ∀ {v, w}, s(v, w) ∈ E → v ∈ V ∧ w ∈ V), closer to the type Matroid. I guess you must already have had this discussion, and I would like to understand why this structure has been chosen.

Anyway, what is the _recommended_ way to write a proof by induction on the size of a graph?

[Vlad Tsyrklevich]

Does something like this work?

import Mathlib
theorem _CaroWei {V} {G : SimpleGraph V} [Finite V] : True := by
  have (eq := hcard) card := Nat.card V
  induction card

This doesn't match what you've done with Subgraphs, but I don't think n needs to be specified in the theorem statement, it can be derived from Finite V or Fintype V.

[Aaron Liu]

how about induction hcard : Nat.card V generalizing V

[Aaron Liu]

or docs#Fintype.induction_empty_option

[Robin Petit]

Oh right, this seems way cleaner to not have n be explicit. However this forces the induction to be performed on a graph over another vertex type, thus requiring casting from V \ v to V all the time in the proof. Is there a way to prevent that as well?

[Vlad Tsyrklevich]

Do the induction on Finset.card G'.vertsF then? It would be easier to understand your issue with an #mwe

[Shreyas Srinivas]

As an aside, if we had an explicit vertex set, we could use Finset.induction

[Jakub Nowak]

Maybe we could have a strong induction principle for docs#SimpleGraph.Subgraph ? By strong, I mean that you can use any strict subgraph in induction hypothesis. Would that be useful in your case @Robin Petit?

[Robin Petit]

The issue is not strong induction vs weak induction. I'm trying to write a short example to show what is bothering me with doing the induction induction on SimpleGraph, brb

[Robin Petit]

Oh actually, I remember now why I had n be explicit: When writing

theorem thm {V : Type*} [Fintype V] : True := by
  induction hcard : Fintype.card V with
  | zero => sorry
  | succ n ih =>
      -- here
      sorry

in the succ n case of the induction (see comment), ih is of the form Fintype.card V = n → [...]. But hcard is Fintype.card V = n + 1, therefore we can never apply the induction hypothesis.

[Jakub Nowak]

Something like that might work for you?

import Mathlib

open SimpleGraph

variable {G : SimpleGraph V} [Finite V]

example : False := by
  induction (⊤ : G.Subgraph) using WellFoundedLT.induction with
  | ind H ih =>
    by_cases H = ⊥
    · exact @_CaroWei_on_empty_subgraph ..
    · -- ...
      obtain ⟨v, _⟩ := -- ...
      let H' := H.deleteVerts {v}  -- H' = H-v
      let sol_H := Nonempty.some <| @ih H' Subgraph.deleteVerts_le  -- apply induction on H' = H-v
      -- ...

[Vlad Tsyrklevich]

Does generalizing V as Aaron mentioned solve this issue? (I had just forgotten to include it)

[Robin Petit]

Oh, it just clicked. I now understand what generalizing is used for... Ok I'll cook a mwe for the "issue" with Subgraphs vs SimpleGraph

[Kevin Buzzard]

I guess one way to proceed is simply by formally writing down the induction principle you want in Lean (i.e. Lean code for "if P is a property of graphs and these 5 conditions are true about P then P is true for all graphs") rather than just asking for induction principles and then saying that they don't quite fit the bill in your case. If you abstract out the principle you want then perhaps it's provable using another principle (like strong induction on naturals is proved using induction).

[Robin Petit]

Maybe you're right, I have no idea: I've only been using Lean for like 10 days. But I feel like this is equivalent to proving the inductive step independently, and thus it would need to be changed every time, right? Also the reason it "doesn't quite fit the bill" is not the induction per se. I guess
it'll be clearer when I'll have a mwe

[Eric Wieser]

Is refine Fintype.induction_empty_option ?_ ?_ ?_ V useful?

[Robin Petit]

Ok so here is what is still bothering me. I can do induction on graphs or on subgraphs.
Let's look at a simple example: every graph has an independent set, and let's prove it by induction (yes, this is silly, but at least it's short).

Let's do induction on graphs:

import Mathlib

theorem Theorem {V : Type*} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] [DecidableEq V] :
    ∃ s : Finset V, G.IsIndepSet s := by
  induction hcard : Fintype.card V generalizing V with
  | zero => sorry
  | succ n ih =>
      have nonemptyV : Nonempty V := by exact Fintype.card_pos_iff.mp <| Nat.lt_of_sub_eq_succ hcard
      let v : V := Classical.choice nonemptyV
      let V' : Set V := Set.univ \ {v}
      have _ : Fintype V' := by exact Fintype.ofFinite ↑V'
      let G' := G.induce (Set.univ \ {v})
      have G'_card : Fintype.card V' = n := sorry
      obtain ⟨s', s'_is_indep⟩ := ih G' G'_card
      -- here, the mapping is explicit
      let φ : V' → V := fun x' ↦ x'.val
      let s := Finset.image φ s'
      have φ_injective : Function.Injective φ := by
        intro x' y' image_eq
        grind
      use s
      intro x x_in_s y y_in_s x_ne_y
      -- explicit casts
      have in_s_implies_in_V' (x : V) : x ∈ s → x ∈ V' := by grind
      let x' : V' := ⟨x, Set.mem_diff_singleton.mpr (in_s_implies_in_V' x x_in_s)⟩
      let y' : V' := ⟨y, Set.mem_diff_singleton.mpr (in_s_implies_in_V' y y_in_s)⟩
      have x'_in_s' : x' ∈ s' := (Function.Injective.mem_finset_image φ_injective).mp x_in_s
      have y'_in_s' : y' ∈ s' := (Function.Injective.mem_finset_image φ_injective).mp y_in_s
      exact s'_is_indep x'_in_s' y'_in_s' (Subtype.coe_ne_coe.mp x_ne_y)

We need to have an explicit mapping x ↦ x.valto be able to use the solution obtained by applying the induction hypothesis, and this is rather cumbersome.

The other possibility is to do induction on subgraphs :

def IsIndepSet {V : Type*} {G : SimpleGraph V} (G' : G.Subgraph) [Fintype G'.verts]
    (s : Finset V) : Prop :=
  sorry  -- X

theorem Theorem' {V : Type*} [Fintype V] {G : SimpleGraph V} (H : G.Subgraph) [Fintype H.verts]
    [DecidableRel G.Adj] [DecidableEq V] : ∃ s : Finset V, IsIndepSet H s := by
  induction hcard : Finset.card H.verts.toFinset generalizing H with
  | zero => sorry
  | succ n ih =>
      have nonemptyV : Nonempty V :=
        Exists.nonempty <| Finset.card_pos.mp <| Nat.lt_of_sub_eq_succ hcard
      let v : V := Classical.choice nonemptyV
      let V' : Set V := Set.univ \ {v}
      have _ : Fintype V' := by exact Fintype.ofFinite ↑V'
      let G' := H.induce (Set.univ \ {v})
      have _ : Fintype G'.verts := Fintype.ofFinite G'.verts
      have G'_card : Finset.card G'.verts.toFinset = n := sorry
      obtain ⟨s', s'_is_indep⟩ := ih G' G'_card
      use s'
      sorry -- depends on how IsIndepSet is implemented

In this case, there is no need to convert vertices, they have the same type in H (the subgraph that we work on) and G' (the subgraph we apply induction on).
However we still have an "issue": while IsIndepSet is defined on SimpleGraph, it is not defined on SimpleGraph.Subgraph. And as I see it, we have two options: (1) rewrite the same definition as in SimpleGraph, which means code duplication, and that's not great; or (2) use the definition from SimpleGraph, hence forcing a coercion, and we're back to the annoyance from above.

[Robin Petit]

@Eric Wieser This is just another way (a less "tactic-y" one) of writing the induction part, right?

[Eric Wieser]

It's only "less tactic-y" because of lean4#4246, which makes it illegal to write induction V using Fintype.induction_empty_option. You can work around this with

/-- `Fintype.induction_empty_option` with a workaround for Lean4#4246.

The only difference is that `h_fintype` is explicit. -/
@[elab_as_elim]
theorem Fintype.induction_empty_option_lean_4246 {P : ∀ (α : Type u) [Fintype α], Prop}
    (of_equiv : ∀ (α β) [Fintype β] (e : α ≃ β), @P α (@Fintype.ofEquiv α β ‹_› e.symm) → @P β ‹_›)
    (h_empty : P PEmpty) (h_option : ∀ (α) [Fintype α], P α → P (Option α)) (α : Type u)
    (h_fintype : Fintype α) : P α :=
  Fintype.induction_empty_option (P := P) of_equiv h_empty h_option α

[Eric Wieser]

#34501 contains this workaround

[Vlad Tsyrklevich]

I have rewritten the original version as the following, perhaps I am missing the point of what you are doing with the maps and this is 'cheating'?

import Mathlib
theorem Theorem {V : Type*} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] [DecidableEq V] :
    ∃ s : Finset V, G.IsIndepSet s := by
  induction hcard : Fintype.card V generalizing V with
  | zero => exact ⟨∅, by simp⟩
  | succ n ih =>
      let v : V := Classical.choice <| Fintype.card_pos_iff.mp <| Nat.lt_of_sub_eq_succ hcard
      obtain ⟨s, hs⟩ := @ih (.univ \ {v} : Set V) (Set.univ.fintypeDiff _) (G.induce _) _ _
        (by simp [Fintype.card_ofFinset, Finset.card_sdiff, hcard])
      use s.image (·.val)
      simp
      exact Set.Pairwise.image hs

[Robin Petit]

Oh I guess this works in this case because there already is a theorem allowing to abstract the mapping (Set.Pairwise.image).

If I go back to Caro-Wei's theorem ,it states that
$\alpha(G) \ge \sum_{v \in V(G)}\frac{1}{d(v)+1}.$
The proof is as follows: pick a vertex v of degree Δ(G), apply induction on G' := G-v, and show that the bound on G' is at least that on G. For that second part, in Lean, I had to split the sum, and specifiy that neighbours of v have their degree diminished by exactly 1 in G' by comparing G.neighborSet w and G'.neighborSet w, but one has type Set V and the other has type Set V'.

But I guess what you mean is that using the \dot notation and the appropriate existing theorems might make the proof way shorter and less cumbersome. I still haven't found the best way to find the right theorems to use, and oftentimes using exact? or apply? doesn't really help (e.g. it never proposed Set.Pairwise.image to me).

[Eric Wieser]

Here's my version with the induction principle above:

theorem Theorem {V : Type*} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] [DecidableEq V] :
    ∃ s : Finset V, G.IsIndepSet s := by
  induction V, ‹Fintype V› using Fintype.induction_empty_option_lean_4246 with
  | of_equiv α β e ih =>
    classical
    obtain ⟨s, hs⟩ := ih (G.comap e)
    use s.map e
    simpa using hs.image
  | h_empty =>
    use ∅
    simp
  | h_option α ih =>
    obtain ⟨s, hs⟩ := ih (G.comap some)
    use s.map (.some)
    simpa using hs.image

[Vlad Tsyrklevich]

Closer to your original approach I could instead solve it as:

import Mathlib
theorem Theorem {V : Type*} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] [DecidableEq V] :
    ∃ s : Finset V, G.IsIndepSet s := by
  induction hcard : Fintype.card V generalizing V with
  | zero => exact ⟨∅, by simp⟩
  | succ n ih =>
      let v : V := Classical.choice <| Fintype.card_pos_iff.mp <| Nat.lt_of_sub_eq_succ hcard
      obtain ⟨s, hs⟩ := @ih (.univ \ {v} : Set V) (Set.univ.fintypeDiff _) (G.induce _) _ _
        (by simp [Finset.card_sdiff, hcard])
      use s.image (·.val)
      intro x hx y hy hxy
      simpa using @hs ⟨x, by grind⟩ (by grind) ⟨y, by grind⟩ (by grind) (by grind)

I found Set.Pairwise.image using exact?--it can be useful to develop with import Mathlib and then only #min_imports at the end, though it's hard on your RAM.

[Robin Petit]

Alright, thanks to you all, I think I see more clearly how to proceed. I'll come back after cleaning up the proof to see if this is relevant for mathlib.

[Mitchell Horner]

Robin Petit said:

Also I ended up formulating the result in terms of subgraphs to prevent type coersion: while $G$ has type SimpleGraph V, $G-v$ has type SimpleGraph ↑(@Set.univ V \ {v}), so the canonical injection w ↦ w.val must be explicit all the way through and this is really cumbersome.

I might be a little late, but you can use recursion and G.deleteIncidenceSet for this purpose! :grinning_face_with_smiling_eyes:

This gives you a SimpleGraph V with the incidence set of v deleted. You can then call your theorem recursively and add a proof like

termination_by card G.support
decreasing_by
  exact (G.card_support_deleteIncidenceSet v.prop).trans_lt (Nat.pred_lt_of_lt hcard_support_pos)

to the bottom of your theorem (where hcard_support_pos : 0 < card G.support).

Robin Petit said:

Ok so here is what is still bothering me. I can do induction on graphs or on subgraphs.

I needed to formalize a process similar to the one you are describing here for the Erdős-Stone theorem.

I used the approach I describe above.

I've found that pen-and-paper proofs that "repeatedly delete vertices" from a fixed graph (or similar repeated processes) are easy to formalize recursively where termination is guaranteed by a decreasing support on the fixed graph.

[Robin Petit]

I thought of using support for this, but in that case one cannot distinguish between a vertex not in the support because it was _removed_ in the induction or because it has degree 0 in the graph.

[Mitchell Horner]

Robin Petit said:

I thought of using support for this, but in that case one cannot distinguish between a vertex not in the support because it was _removed_ in the induction or because it has degree 0 in the graph.

If you do things recursively, you still retain the vertex you delete! It is slightly different to induction. You can distinguish the vertex you delete from the vertex not in the support because you have the vertex you delete. :grinning_face_with_smiling_eyes:

You only need the support to prove that the recursion terminates - since what you are really doing is not deleting the vertices of a graph but the edges incident to the vertices.

In my example from Erdős-Stone theorem above, I delete the incidence set of minimum degree vertex x in the support of G, get a bound on G-x recursively, then "add back" the number of edges in x's incidence set to prove the bound. I have x before and after the recursive call.

The pen-and-paper proof of Caro-Wei's theorem could be formalized in a similar fashion. If I remember how the proof goes. :sweat_smile:

1. Base case.
2. exists_minimal_degree_vertex gives you say v
3. Apply the theorem recursively to G.deleteIncidenceSet v to get the bound on the independent set.
4. Add the contribution from v and its neighbors back into the bound.
5. Celebrate!

The only drawback is that one often needs to provide an explicit proof that their recursion terminates (although it is sometimes inferred automatically). In this case, you'll have to add the thing I mention above.

[Robin Petit]

Sorry I haven't had much time to work on this lately.

Mitchell Horner said:

If you do things recursively, you still retain the vertex you delete! It is slightly different to induction. You can distinguish the vertex you delete from the vertex not in the support because you have the vertex you delete. :grinning_face_with_smiling_eyes:

I think I don't get it: there is a way for me to know what vertices have been removed if the "technical version" used for the induction also takes as a parameter the set of vertices removed until now (initialy \emptyset). Otherwise when applying the induction hypothesis, I have no information regarding the type of vertices.

[Mitchell Horner]

Robin Petit said:

I think I don't get it

Let me preface this by saying I hate when people just post code... :sweat_smile:

Take a look at the following code. The exact construction of G' is a little different then I first guessed above, but the recursive structure is identical.

You have x throughout the proof, no "technical version" required. The statement explicitly requires that your independent set be in the support of the graph.

open Classical in
theorem caro_wei' (G : SimpleGraph V) [DecidableRel G.Adj] :
    ∃ s : Finset V, ↑s ⊆ G.support ∧
      G.IsIndepSet s ∧ ∑ v ∈ G.support, (G.degree v + 1 : ℝ)⁻¹ ≤ #s := by
  rcases eq_zero_or_pos (card G.support) with h0 | hcard_sup
  -- base case of the *recursion*
  · sorry
  · have : Nonempty G.support := card_pos_iff.mp hcard_sup
    -- construct `G'` by deleting 'vertices' incident to a minimal degree vertex `x`
    have ⟨x, hδ_eq_degx⟩ := exists_minimal_degree_vertex (G.induce G.support)
    rw [degree_induce_support] at hδ_eq_degx
    let G' := G ⊓ ⨅ v ∈ G.neighborFinset ↑x, G.deleteIncidenceSet v
    -- ...
    -- `G'` subset of `G` deleting `x`
    have h_le' : G' ≤ G.deleteIncidenceSet ↑x := by sorry
    -- repeat the process
    have ⟨s', hs'_sub', hs'_ind, ihs'⟩ := caro_wei G'
    -- keep track of vertices that disappear in `G'`
    let t : Finset V := G.support.toFinset \ ({↑x} ∪ G.neighborFinset ↑x ∪ G'.support.toFinset)
    --- ...
    -- construct `s` by adding `x` to `s'` and `t`
    let s := cons ↑x (s' ∪ t) sorry
    -- `s` is a subset of `S(G)`
    have hs_sub : ↑s ⊆ G.support := by
      simp_rw [s, cons_eq_insert, coe_insert,
        Set.insert_subset_iff, coe_union, Set.union_subset_iff]
      exact ⟨x.prop, sorry, sorry⟩
    -- `s` is independent
    have hs_ind : G.IsIndepSet s := by
      sorry
    refine ⟨s, hs_sub, hs_ind, ?_⟩
    -- the contribution of `x` is the difference in the bound
    calc (#s : ℝ)
      -- recursion
      _ ≥ ∑ v ∈ G'.support, (G'.degree v + 1 : ℝ)⁻¹ + #t + 1 := by sorry
      _ ≥ ∑ v ∈ G'.support, (G.degree v + 1 : ℝ)⁻¹ + #t + 1 := by sorry
      -- bound plus `t` contribution and `x` contribution
      _ ≥ ∑ v ∈ G.support, (G.degree v + 1 : ℝ)⁻¹
        + (1 - ∑ v ∈ {↑x} ∪ G.neighborFinset ↑x, (G.degree v + 1 : ℝ)⁻¹)
        + (#t - ∑ v ∈ t, (G.degree v + 1 : ℝ)⁻¹) := by sorry
      -- celebrate!
      _ ≥ ∑ v ∈ G.support, (G.degree v + 1 : ℝ)⁻¹ := by sorry
termination_by card G.support
decreasing_by
  apply lt_of_le_of_lt ?_ <|
    (G.card_support_deleteIncidenceSet x.prop).trans_lt (Nat.pred_lt_of_lt hcard_sup)
  simp_rw [← Set.toFinset_card]
  apply card_le_card fun v hv ↦ ?_
  simp_rw [Set.mem_toFinset, mem_support] at hv ⊢
  exact ⟨hv.choose, h_le' hv.choose_spec⟩

The bit I've left at the bottom here following termination_by is the proof that the recursion terminates. :grinning_face_with_smiling_eyes:

Just in case there is any doubt. The complete proof is cobbled together here.

[Mitchell Horner]

I'd wager that any time you read "repeat this process until" in a similar proof, a recursive approach is often "true" to the original wording of the proof (up to implementation details).

[Robin Petit]

Oh I see you went for the min-degree approach. I'll need some time to read this carefully, and see if I'm ok with all of it, but thanks a lot!

[Robin Petit]

Thanks a lot @Mitchell Horner! I wanted a proof by max degree (to adapt it and write the proof of a strengthening of C-W), so I took inspiration from your solution and managed to prove it.
See here (on GH).

I'll come back when the strengthening is proven to see if anyone is interested (in another thread I guess)

[Robin Petit]

However I didn't want to use Simplegraph.support becase when removing a max-degree vertex, some of its neighbours could end up with degree 0 and thus require to be handled specifically. I ended up using the same idea and doing the induction on a subset $X \subseteq V$.

Here is the main theorem:

open Classical in
theorem CaroWei (G : SimpleGraph V) [DecidableRel G.Adj] :
    ∃ s : Finset V,
      G.IsIndepSet s ∧ ∑ v, (G.degree v + 1 : ℝ)⁻¹ ≤ #s := by
  obtain ⟨s, hs, hind, hcard⟩ := _CaroWei G univ (by simp)
  exact ⟨s, hind, hcard⟩

and the technical lemma used for it is thus:

open Classical in
private theorem _CaroWei (G : SimpleGraph V) [DecidableRel G.Adj] (X : Finset V)
    (hout : ∀ w ∈ (Finset.univ \ X), G.degree w = 0) :
    ∃ s : Finset V, s ⊆ X ∧ G.IsIndepSet s ∧ ∑ v ∈ X, (G.degree v + 1 : ℝ)⁻¹ ≤ #s := by
  -- ...

where X is the equivalent of the support: it starts out as Finset.univ and when the induction hypothesis is applied on G.deleteIncidenceSet v (i.e. G-v), the associated set X' is X \ {v}.

The induction is performed with:

    let ⟨s', ⟨hs', hs'_ind, hs'_card⟩⟩ := _CaroWei G' (X \ {v}) hout'
    use s'
    -- ...

[Mitchell Horner]

Tremendous.

[Mitchell Horner]

Robin Petit said:

I'll come back when the strengthening is proven to see if anyone is interested (in another thread I guess)

@ me if you do. :grinning_face_with_smiling_eyes: