feat: Define Hamiltonian paths and cycles (#7102)

Co-authored-by: Bhavik Mehta <bhavikmehta8@gmail.com>
Co-authored-by: Linus Sommer
Co-authored-by: Lode Vermeulen



Co-authored-by: Lode <lode685@gmail.com>
Co-authored-by: Linus <95619282+linus-md@users.noreply.github.com>
Co-authored-by: Bhavik Mehta <bhavikmehta8@gmail.com>
Co-authored-by: Doga Can Sertbas <dogacan.sertbas@gmail.com>
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>

Author: 5 people

Mathlib.lean

@@ -1735,6 +1735,7 @@ import Mathlib.Combinatorics.SimpleGraph.Ends.Properties
 import Mathlib.Combinatorics.SimpleGraph.Finite
 import Mathlib.Combinatorics.SimpleGraph.Finsubgraph
 import Mathlib.Combinatorics.SimpleGraph.Girth
+import Mathlib.Combinatorics.SimpleGraph.Hamiltonian
 import Mathlib.Combinatorics.SimpleGraph.Hasse
 import Mathlib.Combinatorics.SimpleGraph.IncMatrix
 import Mathlib.Combinatorics.SimpleGraph.Init

Mathlib/Algebra/BigOperators/Group/Finset.lean

@@ -2407,6 +2407,11 @@ theorem prod_toFinset {M : Type*} [DecidableEq α] [CommMonoid M] (f : α → M)
 #align list.prod_to_finset List.prod_toFinset
 #align list.sum_to_finset List.sum_toFinset
 
+@[simp]
+theorem sum_toFinset_count_eq_length [DecidableEq α] (l : List α) :
+    ∑ a in l.toFinset, l.count a = l.length :=
+  by simpa using (Finset.sum_list_map_count l fun _ => (1 : ℕ)).symm
+
 end List
 
 namespace Multiset
@@ -2450,11 +2455,8 @@ theorem disjoint_finset_sum_right {β : Type*} {i : Finset β} {f : β → Multi
 variable [DecidableEq α]
 
 @[simp]
-theorem toFinset_sum_count_eq (s : Multiset α) : ∑ a ∈ s.toFinset, s.count a = card s :=
-  calc
-    ∑ a ∈ s.toFinset, s.count a = ∑ a ∈ s.toFinset, s.count a • 1 := by simp
-    _ = (s.map fun _ => 1).sum := (Finset.sum_multiset_map_count _ _).symm
-    _ = card s := by simp
+theorem toFinset_sum_count_eq (s : Multiset α) : ∑ a in s.toFinset, s.count a = card s :=
+  by simpa using (Finset.sum_multiset_map_count s (fun _ => (1 : ℕ))).symm
 #align multiset.to_finset_sum_count_eq Multiset.toFinset_sum_count_eq
 
 @[simp]

Mathlib/Combinatorics/SimpleGraph/Connectivity.lean

@@ -877,6 +877,12 @@ 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 [*]
 
+/-- A walk with its endpoints defeq is `Nil` if and only if it is equal to `nil`. -/
+lemma nil_iff_eq_nil : ∀ {p : G.Walk v v}, p.Nil ↔ p = nil
+  | .nil | .cons _ _ => by simp
+
+alias ⟨Nil.eq_nil, _⟩ := nil_iff_eq_nil
+
 @[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)
@@ -913,7 +919,7 @@ variable {x y : V} -- TODO: rename to u, v, w instead?
     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) :
+@[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]
 
@@ -925,6 +931,10 @@ variable {x y : V} -- TODO: rename to u, v, w instead?
     (p.copy hx hy).Nil = p.Nil := by
   subst_vars; rfl
 
+@[simp] lemma support_tail (p : G.Walk v v) (hp) :
+    (p.tail hp).support = p.support.tail := by
+  rw [← cons_support_tail p hp, List.tail_cons]
+
 /-! ### Trails, paths, circuits, cycles -/
 
 /-- A *trail* is a walk with no repeating edges. -/
@@ -994,6 +1004,8 @@ theorem isCircuit_copy {u u'} (p : G.Walk u u) (hu : u = u') :
   rfl
 #align simple_graph.walk.is_circuit_copy SimpleGraph.Walk.isCircuit_copy
 
+lemma IsCircuit.not_nil {p : G.Walk v v} (hp : IsCircuit p) : ¬ p.Nil := (hp.ne_nil ·.eq_nil)
+
 theorem isCycle_def {u : V} (p : G.Walk u u) :
     p.IsCycle ↔ p.IsTrail ∧ p ≠ nil ∧ p.support.tail.Nodup :=
   Iff.intro (fun h => ⟨h.1.1, h.1.2, h.2⟩) fun h => ⟨⟨h.1, h.2.1⟩, h.2.2⟩
@@ -1006,6 +1018,8 @@ theorem isCycle_copy {u u'} (p : G.Walk u u) (hu : u = u') :
   rfl
 #align simple_graph.walk.is_cycle_copy SimpleGraph.Walk.isCycle_copy
 
+lemma IsCycle.not_nil {p : G.Walk v v} (hp : IsCycle p) : ¬ p.Nil := (hp.ne_nil ·.eq_nil)
+
 @[simp]
 theorem IsTrail.nil {u : V} : (nil : G.Walk u u).IsTrail :=
   ⟨by simp [edges]⟩
@@ -1710,8 +1724,8 @@ theorem map_isCycle_iff_of_injective {p : G.Walk u u} (hinj : Function.Injective
     support_map, ← List.map_tail, List.nodup_map_iff hinj]
 #align simple_graph.walk.map_is_cycle_iff_of_injective SimpleGraph.Walk.map_isCycle_iff_of_injective
 
-alias ⟨_, map_isCycle_of_injective⟩ := map_isCycle_iff_of_injective
-#align simple_graph.walk.map_is_cycle_of_injective SimpleGraph.Walk.map_isCycle_of_injective
+alias ⟨_, IsCycle.map⟩ := map_isCycle_iff_of_injective
+#align simple_graph.walk.map_is_cycle_of_injective SimpleGraph.Walk.IsCycle.map
 
 variable (p f)
 

Mathlib/Combinatorics/SimpleGraph/Hamiltonian.lean

@@ -0,0 +1,136 @@
+/-
+Copyright (c) 2023 Bhavik Mehta, Rishi Mehta, Linus Sommer. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Bhavik Mehta, Rishi Mehta, Linus Sommer
+-/
+import Mathlib.Algebra.Order.Ring.Nat
+import Mathlib.Combinatorics.SimpleGraph.Connectivity
+
+/-!
+# Hamiltonian Graphs
+
+In this file we introduce hamiltonian paths, cycles and graphs.
+
+## Main definitions
+
+- `SimpleGraph.Walk.IsHamiltonian`: Predicate for a walk to be hamiltonian.
+- `SimpleGraph.Walk.IsHamiltonianCycle`: Predicate for a walk to be a hamiltonian cycle.
+- `SimpleGraph.IsHamiltonian`: Predicate for a graph to be hamiltonian.
+-/
+
+open Finset Function
+open scoped BigOperators
+
+namespace SimpleGraph
+variable {α β : Type*} [Fintype α] [Fintype β] [DecidableEq α] [DecidableEq β] {G : SimpleGraph α}
+  {a b : α} {p : G.Walk a b}
+
+namespace Walk
+
+/-- A hamiltonian path is a walk `p` that visits every vertex exactly once. Note that while
+this definition doesn't contain that `p` is a path, `p.isPath` gives that. -/
+def IsHamiltonian (p : G.Walk a b) : Prop := ∀ a, p.support.count a = 1
+
+lemma IsHamiltonian.map {H : SimpleGraph β} (f : G →g H) (hf : Bijective f) (hp : p.IsHamiltonian) :
+    (p.map f).IsHamiltonian := by
+  simp [IsHamiltonian, hf.surjective.forall, hf.injective, hp _]
+
+/-- A hamiltonian path visits every vertex. -/
+@[simp] lemma IsHamiltonian.mem_support (hp : p.IsHamiltonian) (c : α) : c ∈ p.support := by
+  simp only [← List.count_pos_iff_mem, hp _, Nat.zero_lt_one]
+
+/-- The support of a hamiltonian walk is the entire vertex set. -/
+lemma IsHamiltonian.support_toFinset (hp : p.IsHamiltonian) : p.support.toFinset = Finset.univ := by
+  simp [eq_univ_iff_forall, hp]
+
+/-- The length of a hamiltonian path is one less than the number of vertices of the graph. -/
+lemma IsHamiltonian.length_eq (hp : p.IsHamiltonian) : p.length = Fintype.card α - 1 :=
+  eq_tsub_of_add_eq $ by
+    rw [← length_support, ← List.sum_toFinset_count_eq_length, Finset.sum_congr rfl fun _ _ ↦ hp _,
+      ← card_eq_sum_ones, hp.support_toFinset, card_univ]
+
+/-- Hamiltonian paths are paths. -/
+lemma IsHamiltonian.isPath (hp : p.IsHamiltonian) : p.IsPath :=
+  IsPath.mk' <| List.nodup_iff_count_le_one.2 <| (le_of_eq <| hp ·)
+
+/-- A path whose support contains every vertex is hamiltonian. -/
+lemma IsPath.isHamiltonian_of_mem (hp : p.IsPath) (hp' : ∀ w, w ∈ p.support) :
+    p.IsHamiltonian := fun _ ↦
+  le_antisymm (List.nodup_iff_count_le_one.1 hp.support_nodup _) (List.count_pos_iff_mem.2 (hp' _))
+
+lemma IsPath.isHamiltonian_iff (hp : p.IsPath) : p.IsHamiltonian ↔ ∀ w, w ∈ p.support :=
+  ⟨(·.mem_support), hp.isHamiltonian_of_mem⟩
+
+/-- A hamiltonian cycle is a cycle that visits every vertex once. -/
+structure IsHamiltonianCycle (p : G.Walk a a) extends p.IsCycle : Prop :=
+  isHamiltonian_tail : (p.tail toIsCycle.not_nil).IsHamiltonian
+
+variable {p : G.Walk a a}
+
+lemma IsHamiltonianCycle.isCycle (hp : p.IsHamiltonianCycle) : p.IsCycle :=
+  hp.toIsCycle
+
+lemma IsHamiltonianCycle.map {H : SimpleGraph β} (f : G →g H) (hf : Bijective f)
+    (hp : p.IsHamiltonianCycle) : (p.map f).IsHamiltonianCycle where
+  toIsCycle := hp.isCycle.map hf.injective
+  isHamiltonian_tail := by
+    simp [IsHamiltonian, support_tail, hf.surjective.forall, List.count_tail, hf.injective]
+    intro x
+    rcases p with (_ | ⟨y, p⟩)
+    · cases hp.ne_nil rfl
+    simp only [support_cons, List.count_cons, List.map_cons, List.head_cons, hf.injective.eq_iff,
+      add_tsub_cancel_right]
+    exact hp.isHamiltonian_tail _
+
+lemma isHamiltonianCycle_isCycle_and_isHamiltonian_tail  :
+    p.IsHamiltonianCycle ↔ ∃ h : p.IsCycle, (p.tail h.not_nil).IsHamiltonian :=
+  ⟨fun ⟨h, h'⟩ ↦ ⟨h, h'⟩, fun ⟨h, h'⟩ ↦ ⟨h, h'⟩⟩
+
+lemma isHamiltonianCycle_iff_isCycle_and_support_count_tail_eq_one :
+    p.IsHamiltonianCycle ↔ p.IsCycle ∧ ∀ a, (support p).tail.count a = 1 := by
+  simp only [isHamiltonianCycle_isCycle_and_isHamiltonian_tail , IsHamiltonian, support_tail,
+   exists_prop]
+
+/-- A hamiltonian cycle visits every vertex. -/
+lemma IsHamiltonianCycle.mem_support (hp : p.IsHamiltonianCycle) (b : α) :
+    b ∈ p.support := List.mem_of_mem_tail <| support_tail p _ ▸ hp.isHamiltonian_tail.mem_support _
+
+/-- The length of a hamiltonian cycle is the number of vertices. -/
+lemma IsHamiltonianCycle.length_eq (hp : p.IsHamiltonianCycle) :
+    p.length = Fintype.card α := by
+  rw [← length_tail_add_one hp.not_nil, hp.isHamiltonian_tail.length_eq, Nat.sub_add_cancel]
+  rw [Nat.succ_le, Fintype.card_pos_iff]
+  exact ⟨a⟩
+
+lemma IsHamiltonianCycle.count_support_self (hp : p.IsHamiltonianCycle) :
+    p.support.count a = 2 := by
+  rw [support_eq_cons, List.count_cons_self, ← support_tail, hp.isHamiltonian_tail]
+
+lemma IsHamiltonianCycle.support_count_of_ne (hp : p.IsHamiltonianCycle) (h : a ≠ b) :
+    p.support.count b = 1 := by
+  rw [← cons_support_tail p, List.count_cons_of_ne h.symm, hp.isHamiltonian_tail]
+
+end Walk
+
+/-- A hamiltonian graph is a graph that contains a hamiltonian cycle.
+
+By convention, the singleton graph is considered to be hamiltonian. -/
+def IsHamiltonian (G : SimpleGraph α) : Prop :=
+  Fintype.card α ≠ 1 → ∃ a, ∃ p : G.Walk a a, p.IsHamiltonianCycle
+
+lemma IsHamiltonian.mono {H : SimpleGraph α} (hGH : G ≤ H) (hG : G.IsHamiltonian) :
+    H.IsHamiltonian :=
+  fun hα ↦ let ⟨_, p, hp⟩ := hG hα; ⟨_, p.map $ .ofLE hGH, hp.map _ bijective_id⟩
+
+lemma IsHamiltonian.connected (hG : G.IsHamiltonian) : G.Connected where
+  preconnected a b := by
+    obtain rfl | hab := eq_or_ne a b
+    · rfl
+    have : Nontrivial α := ⟨a, b, hab⟩
+    obtain ⟨_, p, hp⟩ := hG Fintype.one_lt_card.ne'
+    have a_mem := hp.mem_support a
+    have b_mem := hp.mem_support b
+    exact ((p.takeUntil a a_mem).reverse.append $ p.takeUntil b b_mem).reachable
+  nonempty := not_isEmpty_iff.1 fun _ ↦ by simpa using hG $ by simp [@Fintype.card_eq_zero]
+
+end SimpleGraph