feat(SimpleGraph): alternative characterizations of cycles/hamiltonian paths (leanprover-community#34766)

Give alternative characterizations of cycles, hamiltonian paths, and hamiltonian cycles in terms of the lengths of the underlying walks.

Author: vlad902

Mathlib/Combinatorics/SimpleGraph/Hamiltonian.lean

@@ -106,6 +106,16 @@ theorem IsHamiltonian.getVert_surjective (hp : p.IsHamiltonian) : p.getVert.Surj
   .of_comp <| p.getVert_comp_val_eq_get_support ▸
     isHamiltonian_iff_support_get_bijective.mp hp |>.surjective
 
+lemma isHamiltonian_iff_isPath_and_length_eq [Fintype α] :
+    p.IsHamiltonian ↔ p.IsPath ∧ p.length = Fintype.card α - 1 := by
+  by_cases! h : IsEmpty α
+  · exact h.elim' a
+  refine ⟨fun h ↦ ⟨h.isPath, h.length_eq⟩, fun ⟨hp, h⟩ ↦ ?_⟩
+  have := p.isPath_iff_injective_get_support.mp hp
+  refine isHamiltonian_iff_support_get_bijective.mpr ⟨this, this.surjective_of_finite ?_⟩
+  refine (Fintype.equivFinOfCardEq ?_).symm
+  simp_rw [length_support, h, Nat.sub_one_add_one Fintype.card_ne_zero]
+
 /-- A Hamiltonian cycle is a cycle that visits every vertex once. -/
 structure IsHamiltonianCycle (p : G.Walk a a) : Prop extends p.IsCycle where
   isHamiltonian_tail : p.tail.IsHamiltonian
@@ -158,6 +168,12 @@ lemma IsHamiltonianCycle.support_count_of_ne (hp : p.IsHamiltonianCycle) (h : a
     p.support.count b = 1 := by
   rw [← cons_support_tail p hp.1.not_nil, List.count_cons_of_ne h, hp.isHamiltonian_tail]
 
+lemma isHamiltonianCycle_iff_isCycle_and_length_eq [Fintype α] :
+    p.IsHamiltonianCycle ↔ p.IsCycle ∧ p.length = Fintype.card α := by
+  refine ⟨fun h ↦ ⟨h.isCycle, h.length_eq⟩, fun ⟨h₁, h₂⟩ ↦ ⟨h₁, ?_⟩⟩
+  refine isHamiltonian_iff_isPath_and_length_eq.mpr ⟨h₁.isPath_tail, ?_⟩
+  grind [length_tail_add_one, IsCycle.not_nil]
+
 end Walk
 
 variable [Fintype α]

Mathlib/Combinatorics/SimpleGraph/Paths.lean

@@ -323,6 +323,9 @@ lemma IsCycle.isPath_of_append_left {p : G.Walk u v} {q : G.Walk v u} (h : ¬ q.
     (hcyc : (p.append q).IsCycle) : p.IsPath :=
   p.isPath_reverse_iff.mp ((reverse_append _ _ ▸ hcyc.reverse).isPath_of_append_right (by simpa))
 
+theorem IsCycle.isPath_tail {p : G.Walk u u} (h : p.IsCycle) : p.tail.IsPath :=
+  IsPath.mk' <| p.support_tail_of_not_nil h.not_nil ▸ h.support_nodup
+
 lemma IsPath.tail {p : G.Walk u v} (hp : p.IsPath) : p.tail.IsPath := by
   cases p with
   | nil => simp
@@ -492,6 +495,19 @@ lemma IsCycle.getVert_sub_one_ne_getVert_add_one {i : ℕ} {p : G.Walk u u} (hpc
     (by simp only [Set.mem_setOf_eq]; lia) h'
   lia
 
+theorem isCycle_iff_isPath_tail_and_le_length {p : G.Walk u u} :
+    p.IsCycle ↔ p.tail.IsPath ∧ 3 ≤ p.length := by
+  refine ⟨fun h ↦ ⟨h.isPath_tail, h.three_le_length⟩, fun ⟨h₁, h₂⟩ ↦ ?_⟩
+  cases p with
+  | nil => simp_all
+  | cons h' p =>
+    simp only [getVert_cons_succ, tail_cons, isPath_copy, length_cons] at h₁ h₂
+    refine p.cons_isCycle_iff h' |>.mpr ⟨h₁, fun hh ↦ ?_⟩
+    have : p.support[0] = p.support[p.length - 1] := by
+      simp [← List.head_eq_getElem_zero, h₁.eq_penultimate_of_mem_edges hh]
+    have := p.isPath_iff_injective_get_support.mp h₁ this
+    lia
+
 /-! ### Walk decompositions -/
 
 section WalkDecomp