Help me learn good style: IsTree

Stream: graph theory

[Ewan Davies]

I have been trying to learn how to work with graphs in mathlib. I tried to prove that a finite nontrivial tree (i.e. at least two vertices) has at least two leaves. My favorite proof of this is to consider a longest path, which by nontriviality has at least two vertices. Then by acyclicity and maximality of the length, the two endpoints are leaves. I struggled to express that proof, and instead relied on a few things already in mathlib about leaves and degree sums. Of course I'd love to write code suitable for inclusion in mathlib, so can I get some review on style from more experienced developers?

• Is it OK to use grind everywhere? Are explicit chains of rw and apply preferable?
• Are there some natural shortenings of my proofs that I don't know because I'm too inexperienced?
• How bad are my naming conventions?

Here's the code:

PastedText.txt

Edit: thanks Aaron.

twoleaves

import Mathlib.Combinatorics.SimpleGraph.Acyclic

universe u

namespace SimpleGraph

open Finset

/-- In a nontrivial tree, twice the order is at most the number of leaves plus the degree sum. --/
lemma IsTree.two_card_vert_le_card_leaves_plus_sum_degrees_of_nontrivial
  {V : Type u} {G : SimpleGraph V}
  [Fintype V] [Nontrivial V] [DecidableRel G.Adj]
  (h_tree : G.IsTree) : 2 * Fintype.card V ≤ #{ v | G.degree v = 1 } + ∑ v, G.degree v := by
    let is_leaf := fun x => G.degree x = 1
    let L := filter is_leaf univ
    let R := filter (fun x => ¬ is_leaf x) univ

    have h_disj : Disjoint L R := by apply disjoint_filter_filter_neg
    have h_disjUnion : univ = disjUnion L R h_disj := by grind
    have h_L_deg : ∀ v ∈ L, G.degree v = 1 := by grind

    have h_R_deg_lb : ∀ v ∈ R, G.degree v ≥ 2 := by
      intro v h_vinR
      have : 1 = G.minDegree := by simp only [h_tree, IsTree.minDegree_eq_one_of_nontrivial]
      have : 1 ≤ G.degree v := by simp only [this, minDegree_le_degree, le_of_eq_of_le]
      grind

    have h_n_l_r : Fintype.card V = #L + #R := by grind

    calc 2*Fintype.card V
      _ = 2*#L + 2*#R := by simp only [Nat.mul_add, h_n_l_r]
      _ ≤ 2*#L + ∑ v ∈ R, 2 := by
          gcongr; simp only [sum_const, smul_eq_mul, Nat.mul_comm, le_refl]
      _ ≤ 2*#L + ∑ v ∈ R, G.degree v := by gcongr with v hv; exact h_R_deg_lb v hv
      _ ≤ #L + ∑ v ∈ L, 1 + ∑ v ∈ R, G.degree v := by
          gcongr; simp only [Nat.two_mul, sum_const, smul_eq_mul, mul_one, le_refl]
      _ ≤ #L + ∑ v ∈ L, G.degree v + ∑ v ∈ R, G.degree v := by
          gcongr 2; gcongr with v hv
          exact ge_of_eq (h_L_deg v hv)
      _ ≤ #L + (∑ v ∈ L, G.degree v + ∑ v ∈ R, G.degree v) := by linarith
      _ ≤ #L + ∑ v, G.degree v := by
          gcongr; rw [h_disjUnion, sum_disjUnion]

/-- A nontrivial tree has two distinct vertices of degree one. --/
lemma IsTree.exists_two_verts_degree_one_of_nontrivial
  {V : Type u} (G : SimpleGraph V)
  [Fintype V] [Nontrivial V] [DecidableRel G.Adj]
  (h_tree : G.IsTree) : ∃ u v, G.degree u = 1 ∧ G.degree v = 1 ∧ u ≠ v := by
    let n := Fintype.card V
    let m := #G.edgeFinset
    let L : Finset V := { v | G.degree v = 1 }

    have hlem : 2*n ≤ #L + ∑ v, G.degree v := two_card_vert_le_card_leaves_plus_sum_degrees_of_nontrivial h_tree
    have : 1 < #L := by
      suffices 2*n + 2 ≤ #L + 2*n by grind
      calc 2*n + 2
        _ ≤ #L + ∑ v, G.degree v + 2 := by apply Nat.add_le_add_right hlem
        _ ≤ #L + 2*m + 2 := by rw [sum_degrees_eq_twice_card_edges]
        _ ≤ #L + 2*n := by
          have : m + 1 = n := IsTree.card_edgeFinset h_tree
          grind
    rw [one_lt_card_iff] at this
    rcases this with ⟨u, v, huL, hvL, hne⟩
    grind

end SimpleGraph

[Aaron Liu]

you can put long snippets of code inside a spoiler tag and it will be collapsed

like this

````spoiler foobar
```lean4
def foo := 1
def bar := foo

-- 3
#eval foo + bar + bar
```
````

and it shows up like this

foobar

def foo := 1
def bar := foo

-- 3
#eval foo + bar + bar

[Vlad Tsyrklevich]

Ewan Davies said:

• Is it OK to use grind everywhere? Are explicit chains of rw and apply preferable?
• Are there some natural shortenings of my proofs that I don't know because I'm too inexperienced?
• How bad are my naming conventions?

I think using grind is better than a long proof, if you could replace grind with a single theorem statement I would do that though.

In general, you don't need to squeeze simps (e.g. use simp? for terminal simps [e.g. simps that close the goal]), this makes it a bit easier to read IMO.
Instead of doing a proof by apply or by exact you can just use an explicit term.
I think the second calc proof is easier to read in the version I give below where it is replaced by rewrites instead. I unrolled the first one as well in the _ver2 proof but I think I actually prefer _ver1 with the calc left-in.

I have not given any thought as to whether there's a better way to write the proof in terms of what's in mathlib now, instead I just tried to golf down what you already wrote:

import Mathlib.Combinatorics.SimpleGraph.Acyclic

universe u

namespace SimpleGraph

open Finset

/-- In a nontrivial tree, twice the order is at most the number of leaves plus the degree sum. --/
lemma IsTree.two_card_vert_le_card_leaves_plus_sum_degrees_of_nontrivial_ver1
  {V : Type u} {G : SimpleGraph V}
  [Fintype V] [Nontrivial V] [DecidableRel G.Adj]
  (h_tree : G.IsTree) : 2 * Fintype.card V ≤ #{ v | G.degree v = 1 } + ∑ v, G.degree v := by
    let L : Finset V := { v : V | G.degree v = 1 } --filter is_leaf univ
    let R : Finset V := { v : V | G.degree v ≠ 1 } --filter (fun x => ¬ is_leaf x) univ

    have h_disjUnion : univ = disjUnion L R (disjoint_filter_filter_neg ..) := by grind
    have (v : V) : 1 ≤ G.degree v := by
      simp [← h_tree.minDegree_eq_one_of_nontrivial, minDegree_le_degree]
    have h_n_l_r : Fintype.card V = #L + #R := by grind

    rw [h_n_l_r, Nat.mul_add]
    calc 2*#L + 2*#R
      _ ≤ 2*#L + ∑ v ∈ R, 2 := by gcongr; simp [Nat.mul_comm]
      _ ≤ 2*#L + ∑ v ∈ R, G.degree v := by gcongr; grind
      _ ≤ #L + ∑ v ∈ L, 1 + ∑ v ∈ R, G.degree v := by gcongr; simp [Nat.two_mul]
      _ ≤ #L + ∑ v ∈ L, G.degree v + ∑ v ∈ R, G.degree v := by gcongr; grind
      _ ≤ #L + ∑ v, G.degree v := by rw [Nat.add_assoc, h_disjUnion, sum_disjUnion]

lemma IsTree.two_card_vert_le_card_leaves_plus_sum_degrees_of_nontrivial_ver2
  {V : Type u} {G : SimpleGraph V}
  [Fintype V] [Nontrivial V] [DecidableRel G.Adj]
  (h_tree : G.IsTree) : 2 * Fintype.card V ≤ #{ v | G.degree v = 1 } + ∑ v, G.degree v := by
    let L : Finset V := { v : V | G.degree v = 1 } --filter is_leaf univ
    let R : Finset V := { v : V | G.degree v ≠ 1 } --filter (fun x => ¬ is_leaf x) univ

    have h_disjUnion : univ = disjUnion L R (disjoint_filter_filter_neg ..) := by grind
    have h₁ : ∑ v ∈ R, 2 ≤ ∑ v ∈ R, G.degree v := by
      have (v : V) : 1 ≤ G.degree v := by
        simp [← h_tree.minDegree_eq_one_of_nontrivial, minDegree_le_degree]
      gcongr
      grind
    have h₂ : ∑ v ∈ L, 1 ≤ ∑ v ∈ L, G.degree v := by gcongr; grind

    grw [show Fintype.card V = #L + #R by grind, Nat.mul_add, Nat.mul_comm _ #R,
      ← smul_eq_mul #R, ← sum_const, h₁, Nat.two_mul]
    nth_rw 2 [← mul_one #L]
    grw [← smul_eq_mul, ← sum_const, h₂, Nat.add_assoc]
    nth_rw 2 [h_disjUnion]
    rw [sum_disjUnion]

/-- A nontrivial tree has two distinct vertices of degree one. --/
lemma IsTree.exists_two_verts_degree_one_of_nontrivial
  {V : Type u} (G : SimpleGraph V)
  [Fintype V] [Nontrivial V] [DecidableRel G.Adj]
  (h_tree : G.IsTree) : ∃ u v, G.degree u = 1 ∧ G.degree v = 1 ∧ u ≠ v := by
    let L : Finset V := { v | G.degree v = 1 }
    have : 1 < #L := by
      suffices 2*Fintype.card V + 2 ≤ #L + 2*Fintype.card V by grind
      grw [Nat.add_le_add_right (two_card_vert_le_card_leaves_plus_sum_degrees_of_nontrivial_ver1 h_tree) ..,
        sum_degrees_eq_twice_card_edges]
      grind [IsTree.card_edgeFinset]
    grind [one_lt_card_iff]

end SimpleGraph

[Vlad Tsyrklevich]

It does seem to be an oversight that we don't have an easy way to conjure a longest path in a finite graph. I've written the following though it needs further cleaning-up before being PRed. Hopefully it unblocks from you experimenting with the original approach you wanted to try.

import Mathlib.Combinatorics.SimpleGraph.Acyclic

namespace SimpleGraph

variable {V : Type*} {G : SimpleGraph V}

theorem eq_of_eq_bot_walk (hG : G = ⊥) {u v : V} (p : G.Walk u v) : u = v := by
  cases p <;> simp_all

theorem nil_of_eq_bot_isPath (hG : G = ⊥) {u v : V} (p : G.Walk u v) (hp : p.IsPath) : p.Nil := by
  have := eq_of_eq_bot_walk hG p
  subst this
  simp [p.isPath_iff_eq_nil.mp hp]

theorem exists_adj_of_ne_bot (h : G ≠ ⊥) : ∃ a b : V, G.Adj a b := by
  contrapose! h
  exact le_bot_iff.mp h

lemma exists_isPath_forall_isPath_length_le_length [N : Nonempty V] [Fintype V] :
  ∃ (u v : V) (p : G.Walk u v) (_ : p.IsPath),
    ∀ (u' v' : V) (p' : G.Walk u' v') (_ : p'.IsPath), p'.length ≤ p.length := by
  classical
  let maxPathLen :=
    Nat.findGreatest (fun n ↦ ∃ (u v : V) (p : G.Walk u v), p.IsPath ∧ p.length = n) (Fintype.card V - 1)
  by_cases h' : G = ⊥
  · obtain ⟨x⟩ := N
    refine ⟨x, x, Walk.nil, by simp, fun u v p hp ↦ ?_⟩
    simpa [Walk.nil_iff_length_eq] using nil_of_eq_bot_isPath h' p hp
  · have : 0 < maxPathLen := by
      simp only [Nat.findGreatest_pos, maxPathLen]
      obtain ⟨u, v, hadj⟩ := exists_adj_of_ne_bot h'
      have : 2 ≤ Fintype.card V := @Fintype.one_lt_card V _ ⟨u, v, hadj.ne⟩
      exact ⟨1, by simp, by grind, ⟨u, v, hadj.toWalk, by simp [hadj.ne], by simp⟩⟩
    obtain ⟨h₁, h₂, h₃⟩ := Nat.findGreatest_eq_iff.mp (by gcongr : Nat.findGreatest _ _ = maxPathLen)
    obtain ⟨u, v, p, hp₁, hp₂⟩ := h₂ (by grind)
    refine ⟨u, v, p, hp₁, fun u' v' p' hp' ↦ ?_⟩
    by_contra! hh
    have := hp'.length_lt
    grind

[Ewan Davies]

Thanks for the comments on the county proofs, I am happy to learn more tactics and good style. At the moment I seem to create endless have statements and I suspect that is poor form. But grind plays nicely with careful haves.

I'll take a while to digest your suggestion for conjuring a longest path. But someone (Rida Hamadani) plumbed in diameter, so I was hoping that this stub would be a good place to start:

/-- A nontrivial tree has two distinct vertices of degree one. --/
lemma IsTree.exists_two_verts_degree_one_of_nontrivial_via_path
  [DecidableEq V] [Fintype V] [Nontrivial V] [DecidableRel G.Adj]
  (h_tree : G.IsTree) : ∃ u v, G.degree u = 1 ∧ G.degree v = 1 ∧ u ≠ v := by

  have : Nonempty V := Nontrivial.to_nonempty
  have : ∃ (u : V) (v : V), G.dist u v = G.diam := SimpleGraph.exists_dist_eq_diam

  match this with
  | ⟨u, v, hdiam⟩ =>
    -- u and v are endpoints of a maximum path in G
    have hne : u ≠ v := by
      -- follows from Nontrival V and h_tree
      sorry
    have : G.degree u = 1 ∧ G.degree v = 1 := by
      -- the same argument should work for both
      sorry
    sorry

[Vlad Tsyrklevich]

Vlad Tsyrklevich said:

it needs further cleaning-up before being PRed

Just FYI, the PR is #30293