feat: Number of edges of a tree (#5918)

Port/review of [mathlib#18638](leanprover-community/mathlib3#18638) directly to Mathlib4.

Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
Co-authored-by: Bhavik Mehta <bhavikmehta8@gmail.com>

Author: kmill

Mathlib/Combinatorics/SimpleGraph/Acyclic.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kyle Miller
 -/
 import Mathlib.Combinatorics.SimpleGraph.Connectivity
+import Mathlib.Tactic.Linarith
 
 #align_import combinatorics.simple_graph.acyclic from "leanprover-community/mathlib"@"b07688016d62f81d14508ff339ea3415558d6353"
 
@@ -43,6 +44,8 @@ universe u v
 
 namespace SimpleGraph
 
+open Walk
+
 variable {V : Type u} (G : SimpleGraph V)
 
 /-- A graph is *acyclic* (or a *forest*) if it has no cycles. -/
@@ -149,4 +152,57 @@ theorem isTree_iff_existsUnique_path :
       simp only [ExistsUnique.unique (h v w) hp hq]
 #align simple_graph.is_tree_iff_exists_unique_path SimpleGraph.isTree_iff_existsUnique_path
 
+lemma IsTree.existsUnique_path (hG : G.IsTree) : ∀ v w, ∃! p : G.Walk v w, p.IsPath :=
+  (isTree_iff_existsUnique_path.1 hG).2
+
+lemma IsTree.card_edgeFinset [Fintype V] [Fintype G.edgeSet] (hG : G.IsTree) :
+    Finset.card G.edgeFinset + 1 = Fintype.card V := by
+  have := hG.isConnected.nonempty
+  inhabit V
+  classical
+  have : Finset.card ({default} : Finset V)ᶜ + 1 = Fintype.card V := by
+    rw [Finset.card_compl, Finset.card_singleton, Nat.sub_add_cancel Fintype.card_pos]
+  rw [← this, add_left_inj]
+  choose f hf hf' using (hG.existsUnique_path · default)
+  refine Eq.symm <| Finset.card_congr
+          (fun w hw => ((f w).firstDart <| ?notNil).edge)
+          (fun a ha => ?memEdges) ?inj ?surj
+  case notNil => exact not_nil_of_ne (by simpa using hw)
+  case memEdges => simp
+  case inj =>
+    intros a b ha hb h
+    wlog h' : (f a).length ≤ (f b).length generalizing a b
+    · exact Eq.symm (this _ _ hb ha h.symm (le_of_not_le h'))
+    rw [dart_edge_eq_iff] at h
+    obtain (h | h) := h
+    · exact (congrArg (·.fst) h)
+    · have h1 : ((f a).firstDart <| not_nil_of_ne (by simpa using ha)).snd = b :=
+        congrArg (·.snd) h
+      have h3 := congrArg length (hf' _ (((f _).tail _).copy h1 rfl) ?_)
+      rw [length_copy, ← add_left_inj 1, length_tail_add_one] at h3
+      · exfalso
+        linarith
+      · simp only [ne_eq, eq_mp_eq_cast, id_eq, isPath_copy]
+        exact (hf _).tail _
+  case surj =>
+    simp only [mem_edgeFinset, Finset.mem_compl, Finset.mem_singleton, Sym2.forall, mem_edgeSet]
+    intros x y h
+    wlog h' : (f x).length ≤ (f y).length generalizing x y
+    · rw [Sym2.eq_swap]
+      exact this y x h.symm (le_of_not_le h')
+    refine ⟨y, ?_, dart_edge_eq_mk'_iff.2 <| Or.inr ?_⟩
+    · rintro rfl
+      rw [← hf' _ nil IsPath.nil, length_nil,
+          ← hf' _ (.cons h .nil) (IsPath.nil.cons <| by simpa using h.ne),
+          length_cons, length_nil] at h'
+      simp [le_zero_iff, Nat.one_ne_zero] at h'
+    rw [← hf' _ (.cons h.symm (f x)) ((cons_isPath_iff _ _).2 ⟨hf _, fun hy => ?contra⟩)]
+    rfl
+    case contra =>
+      suffices : (f x).takeUntil y hy = .cons h .nil
+      · rw [← take_spec _ hy] at h'
+        simp [this, hf' _ _ ((hf _).dropUntil hy)] at h'
+      refine (hG.existsUnique_path _ _).unique ((hf _).takeUntil _) ?_
+      simp [h.ne]
+
 end SimpleGraph

Mathlib/Combinatorics/SimpleGraph/Connectivity.lean

@@ -556,6 +556,7 @@ theorem support_reverse {u v : V} (p : G.Walk u v) : p.reverse.support = p.suppo
   induction p <;> simp [support_append, *]
 #align simple_graph.walk.support_reverse SimpleGraph.Walk.support_reverse
 
+@[simp]
 theorem support_ne_nil {u v : V} (p : G.Walk u v) : p.support ≠ [] := by cases p <;> simp
 #align simple_graph.walk.support_ne_nil SimpleGraph.Walk.support_ne_nil
 
@@ -825,6 +826,81 @@ theorem edges_nodup_of_support_nodup {u v : V} {p : G.Walk u v} (h : p.support.N
     exact ⟨fun h' => h.1 (fst_mem_support_of_mem_edges p' h'), ih h.2⟩
 #align simple_graph.walk.edges_nodup_of_support_nodup SimpleGraph.Walk.edges_nodup_of_support_nodup
 
+/-- Predicate for the empty walk.
+
+Solves the dependent type problem where `p = G.Walk.nil` typechecks
+only if `p` has defeq endpoints. -/
+inductive Nil : {v w : V} → G.Walk v w → Prop
+  | nil {u : V} : Nil (nil : G.Walk u u)
+
+@[simp] lemma nil_nil : (nil : G.Walk u u).Nil := Nil.nil
+
+@[simp] lemma not_nil_cons {h : G.Adj u v} {p : G.Walk v w} : ¬ (cons h p).Nil := fun.
+
+instance (p : G.Walk v w) : Decidable p.Nil :=
+  match p with
+  | nil => isTrue .nil
+  | cons _ _ => isFalse fun.
+
+protected lemma Nil.eq {p : G.Walk v w} : p.Nil → v = w | .nil => rfl
+
+lemma not_nil_of_ne {p : G.Walk v w} : v ≠ w → ¬ p.Nil := mt Nil.eq
+
+lemma nil_iff_support_eq {p : G.Walk v w} : p.Nil ↔ p.support = [v] := by
+  cases p <;> simp
+
+lemma nil_iff_length_eq {p : G.Walk v w} : p.Nil ↔ p.length = 0 := by
+  cases p <;> simp
+
+lemma not_nil_iff {p : G.Walk v w} :
+    ¬ p.Nil ↔ ∃ (u : V) (h : G.Adj v u) (q : G.Walk u w), p = cons h q := by
+  cases p <;> simp [*]
+
+@[elab_as_elim]
+def notNilRec {motive : {u w : V} → (p : G.Walk u w) → (h : ¬ p.Nil) → Sort _}
+    (cons : {u v w : V} → (h : G.Adj u v) → (q : G.Walk v w) → motive (cons h q) not_nil_cons)
+    (p : G.Walk u w) : (hp : ¬ p.Nil) → motive p hp :=
+  match p with
+  | nil => fun hp => absurd .nil hp
+  | .cons h q => fun _ => cons h q
+
+/-- The second vertex along a non-nil walk. -/
+def sndOfNotNil (p : G.Walk v w) (hp : ¬ p.Nil) : V :=
+  p.notNilRec (@fun _ u _ _ _ => u) hp
+
+@[simp] lemma adj_sndOfNotNil {p : G.Walk v w} (hp : ¬ p.Nil) :
+    G.Adj v (p.sndOfNotNil hp) :=
+  p.notNilRec (fun h _ => h) hp
+
+/-- The walk obtained by removing the first dart of a non-nil walk. -/
+def tail (p : G.Walk x y) (hp : ¬ p.Nil) : G.Walk (p.sndOfNotNil hp) y :=
+  p.notNilRec (fun _ q => q) hp
+
+/-- The first dart of a walk. -/
+@[simps]
+def firstDart (p : G.Walk v w) (hp : ¬ p.Nil) : G.Dart where
+  fst := v
+  snd := p.sndOfNotNil hp
+  is_adj := p.adj_sndOfNotNil hp
+
+lemma edge_firstDart (p : G.Walk v w) (hp : ¬ p.Nil) :
+    (p.firstDart hp).edge = ⟦(v, p.sndOfNotNil hp)⟧ := rfl
+
+@[simp] lemma cons_tail_eq (p : G.Walk x y) (hp : ¬ p.Nil) :
+    cons (p.adj_sndOfNotNil hp) (p.tail hp) = p :=
+  p.notNilRec (fun _ _ => rfl) hp
+
+@[simp] lemma cons_support_tail (p : G.Walk x y) (hp : ¬ p.Nil) :
+    x :: (p.tail hp).support = p.support := by
+  rw [← support_cons, cons_tail_eq]
+
+@[simp] lemma length_tail_add_one {p : G.Walk x y} (hp : ¬ p.Nil) :
+    (p.tail hp).length + 1 = p.length := by
+  rw [← length_cons, cons_tail_eq]
+
+@[simp] lemma nil_copy {p : G.Walk x y} (hx : x = x') (hy : y = y') :
+    (p.copy hx hy).Nil = p.Nil := by
+  subst_vars; rfl
 
 /-! ### Trails, paths, circuits, cycles -/
 
@@ -972,6 +1048,10 @@ theorem cons_isPath_iff {u v w : V} (h : G.Adj u v) (p : G.Walk v w) :
   constructor <;> simp (config := { contextual := true }) [isPath_def]
 #align simple_graph.walk.cons_is_path_iff SimpleGraph.Walk.cons_isPath_iff
 
+protected lemma IsPath.cons (hp : p.IsPath) (hu : u ∉ p.support) {h : G.Adj u v} :
+    (cons h p).IsPath :=
+  (cons_isPath_iff _ _).2 ⟨hp, hu⟩
+
 @[simp]
 theorem isPath_iff_eq_nil {u : V} (p : G.Walk u u) : p.IsPath ↔ p = nil := by
   cases p <;> simp [IsPath.nil]
@@ -1011,6 +1091,10 @@ theorem cons_isCycle_iff {u v : V} (p : G.Walk v u) (h : G.Adj u v) :
   tauto
 #align simple_graph.walk.cons_is_cycle_iff SimpleGraph.Walk.cons_isCycle_iff
 
+lemma IsPath.tail {p : G.Walk u v} (hp : p.IsPath) (hp' : ¬ p.Nil) : (p.tail hp').IsPath := by
+  rw [Walk.isPath_def] at hp ⊢
+  rw [← cons_support_tail _ hp', List.nodup_cons] at hp
+  exact hp.2
 
 /-! ### About paths -/