feat: turn a closed walk into a cycle (#31217)

From the ProofBench workshop

Closes #23637, which does the same thing under a stronger hypothesis on the starting closed walk.

Author: YaelDillies

Mathlib/Combinatorics/SimpleGraph/Acyclic.lean

@@ -157,7 +157,7 @@ theorem isAcyclic_of_path_unique (h : ∀ (v w : V) (p q : G.Path v w), p = q) :
   cases c with
   | nil => cases hc.2.1 rfl
   | cons ha c' =>
-    simp only [Walk.cons_isTrail_iff, Walk.support_cons, List.tail_cons] at hc
+    simp only [Walk.isTrail_cons, Walk.support_cons, List.tail_cons] at hc
     specialize h _ _ ⟨c', by simp only [Walk.isPath_def, hc.2]⟩ (Path.singleton ha.symm)
     rw [Path.singleton, Subtype.mk.injEq] at h
     simp [h] at hc

Mathlib/Combinatorics/SimpleGraph/Paths.lean

@@ -58,7 +58,7 @@ variable (G : SimpleGraph V) (G' : SimpleGraph V')
 
 namespace Walk
 
-variable {G} {u v w : V}
+variable {G} {u u' v w : V}
 
 /-! ### Trails, paths, circuits, cycles -/
 
@@ -136,9 +136,14 @@ theorem IsTrail.of_cons {u v w : V} {h : G.Adj u v} {p : G.Walk v w} :
     (cons h p).IsTrail → p.IsTrail := by simp [isTrail_def]
 
 @[simp]
-theorem cons_isTrail_iff {u v w : V} (h : G.Adj u v) (p : G.Walk v w) :
+theorem isTrail_cons {u v w : V} (h : G.Adj u v) (p : G.Walk v w) :
     (cons h p).IsTrail ↔ p.IsTrail ∧ s(u, v) ∉ p.edges := by simp [isTrail_def, and_comm]
 
+@[deprecated (since := "2025-11-03")] alias cons_isTrail_iff := isTrail_cons
+
+protected lemma IsTrail.cons {w : G.Walk u' v} (hw : w.IsTrail) (hu : G.Adj u u')
+    (hu' : s(u, u') ∉ w.edges) : (w.cons hu).IsTrail := by simp [*]
+
 theorem IsTrail.reverse {u v : V} (p : G.Walk u v) (h : p.IsTrail) : p.reverse.IsTrail := by
   simpa [isTrail_def] using h
 
@@ -581,7 +586,7 @@ theorem notMem_edges_of_loop {v : V} {e : Sym2 V} {p : G.Path v v} :
 
 theorem cons_isCycle {u v : V} (p : G.Path v u) (h : G.Adj u v)
     (he : s(u, v) ∉ (p : G.Walk v u).edges) : (Walk.cons h ↑p).IsCycle := by
-  simp [Walk.isCycle_def, Walk.cons_isTrail_iff, he]
+  simp [Walk.isCycle_def, Walk.isTrail_cons, he]
 
 end Path
 
@@ -590,7 +595,7 @@ end Path
 
 namespace Walk
 
-variable {G} [DecidableEq V]
+variable {G} [DecidableEq V] {u u' v v' : V}
 
 /-- Given a walk, produces a walk from it by bypassing subwalks between repeated vertices.
 The result is a path, as shown in `SimpleGraph.Walk.bypass_isPath`.
@@ -605,12 +610,12 @@ def bypass {u v : V} : G.Walk u v → G.Walk u v
       cons ha p'
 
 @[simp]
-theorem bypass_copy {u v u' v'} (p : G.Walk u v) (hu : u = u') (hv : v = v') :
+theorem bypass_copy (p : G.Walk u v) (hu : u = u') (hv : v = v') :
     (p.copy hu hv).bypass = p.bypass.copy hu hv := by
   subst_vars
   rfl
 
-theorem bypass_isPath {u v : V} (p : G.Walk u v) : p.bypass.IsPath := by
+theorem bypass_isPath (p : G.Walk u v) : p.bypass.IsPath := by
   induction p with
   | nil => simp!
   | cons _ p' ih =>
@@ -619,7 +624,7 @@ theorem bypass_isPath {u v : V} (p : G.Walk u v) : p.bypass.IsPath := by
     · exact ih.dropUntil hs
     · simp [*, cons_isPath_iff]
 
-theorem length_bypass_le {u v : V} (p : G.Walk u v) : p.bypass.length ≤ p.length := by
+theorem length_bypass_le (p : G.Walk u v) : p.bypass.length ≤ p.length := by
   induction p with
   | nil => rfl
   | cons _ _ ih =>
@@ -632,7 +637,7 @@ theorem length_bypass_le {u v : V} (p : G.Walk u v) : p.bypass.length ≤ p.leng
     · rw [length_cons, length_cons]
       exact Nat.add_le_add_right ih 1
 
-lemma bypass_eq_self_of_length_le {u v : V} (p : G.Walk u v) (h : p.length ≤ p.bypass.length) :
+lemma bypass_eq_self_of_length_le (p : G.Walk u v) (h : p.length ≤ p.bypass.length) :
     p.bypass = p := by
   induction p with
   | nil => rfl
@@ -651,10 +656,10 @@ lemma bypass_eq_self_of_length_le {u v : V} (p : G.Walk u v) (h : p.length ≤ p
       rw [ih h]
 
 /-- Given a walk, produces a path with the same endpoints using `SimpleGraph.Walk.bypass`. -/
-def toPath {u v : V} (p : G.Walk u v) : G.Path u v :=
+def toPath (p : G.Walk u v) : G.Path u v :=
   ⟨p.bypass, p.bypass_isPath⟩
 
-theorem support_bypass_subset {u v : V} (p : G.Walk u v) : p.bypass.support ⊆ p.support := by
+theorem support_bypass_subset (p : G.Walk u v) : p.bypass.support ⊆ p.support := by
   induction p with
   | nil => simp!
   | cons _ _ ih =>
@@ -667,11 +672,11 @@ theorem support_bypass_subset {u v : V} (p : G.Walk u v) : p.bypass.support ⊆
       apply List.cons_subset_cons
       assumption
 
-theorem support_toPath_subset {u v : V} (p : G.Walk u v) :
+theorem support_toPath_subset (p : G.Walk u v) :
     (p.toPath : G.Walk u v).support ⊆ p.support :=
   support_bypass_subset _
 
-theorem darts_bypass_subset {u v : V} (p : G.Walk u v) : p.bypass.darts ⊆ p.darts := by
+theorem darts_bypass_subset (p : G.Walk u v) : p.bypass.darts ⊆ p.darts := by
   induction p with
   | nil => simp!
   | cons _ _ ih =>
@@ -682,15 +687,41 @@ theorem darts_bypass_subset {u v : V} (p : G.Walk u v) : p.bypass.darts ⊆ p.da
     · rw [darts_cons]
       exact List.cons_subset_cons _ ih
 
-theorem edges_bypass_subset {u v : V} (p : G.Walk u v) : p.bypass.edges ⊆ p.edges :=
+theorem edges_bypass_subset (p : G.Walk u v) : p.bypass.edges ⊆ p.edges :=
   List.map_subset _ p.darts_bypass_subset
 
-theorem darts_toPath_subset {u v : V} (p : G.Walk u v) : (p.toPath : G.Walk u v).darts ⊆ p.darts :=
+theorem darts_toPath_subset (p : G.Walk u v) : (p.toPath : G.Walk u v).darts ⊆ p.darts :=
   darts_bypass_subset _
 
-theorem edges_toPath_subset {u v : V} (p : G.Walk u v) : (p.toPath : G.Walk u v).edges ⊆ p.edges :=
+theorem edges_toPath_subset (p : G.Walk u v) : (p.toPath : G.Walk u v).edges ⊆ p.edges :=
   edges_bypass_subset _
 
+/-- Bypass repeated vertices like `Walk.bypass`, except the starting vertex.
+
+This is intended to be used for closed walks, for which `Walk.bypass` unhelpfully returns the empty
+walk. -/
+def cycleBypass : G.Walk v v → G.Walk v v
+  | .nil => .nil
+  | .cons hvv' w => .cons hvv' w.bypass
+
+@[simp] lemma cycleBypass_nil : (.nil : G.Walk v v).cycleBypass = .nil := rfl
+
+lemma edges_cycleBypass_subset : ∀ {w : G.Walk v v}, w.cycleBypass.edges ⊆ w.edges
+  | .nil => by simp
+  | .cons (v := v') hvv' w => by
+    classical
+    dsimp only [cycleBypass, edges_cons]
+    gcongr
+    exact edges_bypass_subset _
+
+lemma IsTrail.isCycle_cycleBypass : ∀ {w : G.Walk v v}, w ≠ .nil → w.IsTrail → w.cycleBypass.IsCycle
+  | .cons (v := v') hvv' w, _, hw => by
+    dsimp [cycleBypass]
+    refine ⟨⟨(bypass_isPath _).isTrail.cons _ fun hvv' ↦ ?_, by simp⟩, ?_⟩
+    · simp only [isTrail_cons] at hw
+      exact hw.2 <| edges_bypass_subset _ hvv'
+    · simpa using (bypass_isPath _).support_nodup
+
 end Walk
 
 /-! ### Mapping paths -/
@@ -726,7 +757,7 @@ theorem map_isTrail_iff_of_injective (hinj : Function.Injective f) :
   induction p with
   | nil => simp
   | cons _ _ ih =>
-    rw [map_cons, cons_isTrail_iff, ih, cons_isTrail_iff]
+    rw [map_cons, isTrail_cons, ih, isTrail_cons]
     apply and_congr_right'
     rw [← Sym2.map_pair_eq, edges_map, ← List.mem_map_of_injective (Sym2.map.injective hinj)]
 

Mathlib/Combinatorics/SimpleGraph/Trails.lean

@@ -56,7 +56,7 @@ theorem IsTrail.even_countP_edges_iff {u v : V} {p : G.Walk u v} (ht : p.IsTrail
   induction p with
   | nil => simp
   | cons huv p ih =>
-    rw [cons_isTrail_iff] at ht
+    rw [isTrail_cons] at ht
     specialize ih ht.1
     simp only [List.countP_cons, Ne, edges_cons, Sym2.mem_iff]
     split_ifs with h

Mathlib/Tactic/GCongr/CoreAttrs.lean

@@ -36,6 +36,7 @@ attribute [gcongr] mt
   List.Sublist.append List.Sublist.append_left List.Sublist.append_right
   List.Sublist.reverse List.drop_sublist_drop_left List.Sublist.drop
   List.Perm.append_left List.Perm.append_right List.Perm.append List.Perm.map
+  List.cons_subset_cons
   Nat.sub_le_sub_left Nat.sub_le_sub_right Nat.sub_lt_sub_left Nat.sub_lt_sub_right
 
 end Mathlib.Tactic.GCongr