From 4d41532350b234fa99e3a210dcba78962f488ebe Mon Sep 17 00:00:00 2001 From: Kyle Miller Date: Tue, 1 Aug 2023 12:59:38 +0000 Subject: [PATCH] feat: Number of edges of a tree (#5918) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Port/review of [mathlib#18638](https://github.com/leanprover-community/mathlib/pull/18638) directly to Mathlib4. Co-authored-by: Yaël Dillies Co-authored-by: Bhavik Mehta --- .../Combinatorics/SimpleGraph/Acyclic.lean | 56 +++++++++++++ .../SimpleGraph/Connectivity.lean | 84 +++++++++++++++++++ 2 files changed, 140 insertions(+) diff --git a/Mathlib/Combinatorics/SimpleGraph/Acyclic.lean b/Mathlib/Combinatorics/SimpleGraph/Acyclic.lean index e0b27a8d086d1..5303baf15f210 100644 --- a/Mathlib/Combinatorics/SimpleGraph/Acyclic.lean +++ b/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 diff --git a/Mathlib/Combinatorics/SimpleGraph/Connectivity.lean b/Mathlib/Combinatorics/SimpleGraph/Connectivity.lean index 23d1b4a4bb872..a2e252f25aee9 100644 --- a/Mathlib/Combinatorics/SimpleGraph/Connectivity.lean +++ b/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 -/