feat(SimpleGraph/Trails): define Eulerian graphs

Mathlib/Combinatorics/SimpleGraph/Trails.lean

@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2022 Kyle Miller. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Kyle Miller
+Authors: Kyle Miller, Snir Broshi
 -/
 module
 
@@ -38,24 +38,22 @@ Eulerian trails
 
 namespace SimpleGraph
 
-variable {V : Type*} {G : SimpleGraph V} {u v w : V} {p : G.Walk u v}
+variable {V : Type*} [DecidableEq V] {G : SimpleGraph V} {u v w : V} {p : G.Walk u v}
 
 namespace Walk
 
 /-- The edges of a trail as a finset, since each edge in a trail appears exactly once. -/
 abbrev IsTrail.edgesFinset (h : p.IsTrail) : Finset (Sym2 V) :=
   ⟨p.edges, Multiset.coe_nodup.mpr h.edges_nodup⟩
 
-variable [DecidableEq V]
-
 theorem IsTrail.even_countP_edges_iff (ht : p.IsTrail) (x : V) :
     Even (p.edges.countP fun e ↦ x ∈ e) ↔ u ≠ v → x ≠ u ∧ x ≠ v := by
   induction p with
   | nil => simp
   | cons huv p ih => grind [isTrail_cons, edges_cons, G.irrefl]
 
 /-- An *Eulerian trail* (also known as an "Eulerian path") is a walk
-`p` that visits every edge exactly once.  The lemma `SimpleGraph.Walk.IsEulerian.IsTrail` shows
+`p` that visits every edge exactly once.  The lemma `IsEulerian.isTrail` shows
 that these are trails.
 
 Combine with `p.IsCircuit` to get an Eulerian circuit (also known as an "Eulerian cycle"). -/
@@ -100,28 +98,44 @@ theorem IsEulerian.mem_support_of_not_isIsolated (hp : p.IsEulerian) (hw : ¬G.I
   have ⟨_, hadj⟩ := exists_adj_iff_not_isIsolated.mpr hw
   p.fst_mem_support_of_mem_edges <| hp.mem_edges_iff.mpr hadj
 
+theorem IsEulerian.mem_support_of_preconnected (hp : p.IsEulerian) (h : G.Preconnected) :
+    w ∈ p.support := by
+  nontriviality V using Subsingleton.elim w u
+  exact hp.mem_support_of_not_isIsolated <| h.not_isIsolated w
+
 theorem IsEulerian.nil_iff (hp : p.IsEulerian) : p.Nil ↔ G = ⊥ := by
   simp [← edgeSet_eq_empty, hp.edgeSet_eq]
 
-theorem isEulerian_of_bot (p : Walk ⊥ u v) : p.IsEulerian := by
+theorem IsEulerian.of_bot (p : Walk ⊥ u v) : p.IsEulerian := by
   intro e h
   simp at h
 
+@[deprecated (since := "2026-10-25")] alias isEulerian_of_bot := IsEulerian.of_bot
+
+theorem IsEulerian.isCircuit_iff {p : G.Walk v v} (h : p.IsEulerian) : p.IsCircuit ↔ G ≠ ⊥ := by
+  simp [isCircuit_def, h.isTrail, h.nil_iff]
+
+@[simp]
+theorem isEulerian_rotate {p : G.Walk u u} (hv : v ∈ p.support) :
+    (p.rotate v hv).IsEulerian ↔ p.IsEulerian := by
+  simp_rw [IsEulerian, p.rotate_edges v hv |>.perm.count_eq]
+
+protected alias ⟨_, IsEulerian.rotate⟩ := isEulerian_rotate
+
 /-- The support of a non-nil Eulerian trail equals the support of the graph. -/
 theorem IsEulerian.mem_support_iff (hp : p.IsEulerian) (hnil : ¬p.Nil) :
     w ∈ p.support ↔ ¬G.IsIsolated w :=
   ⟨fun hwp hw ↦ hnil <| p.nil_of_isIsolated_of_mem_support hw hwp, hp.mem_support_of_not_isIsolated⟩
 
 theorem IsEulerian.connected_of_forall_not_isIsolated (hp : p.IsEulerian)
     (hG : ∀ v, ¬G.IsIsolated v) : G.Connected where
-  preconnected a b :=
-    have ha : a ∈ p.support := hp.mem_support_of_not_isIsolated <| hG a
-    have hb : b ∈ p.support := hp.mem_support_of_not_isIsolated <| hG b
-    ⟨p.takeUntil a ha |>.reverse.append <| p.takeUntil b hb⟩
+  preconnected a b := by
+    apply reachable_of_mem_support <;> apply hp.mem_support_of_not_isIsolated <;> apply hG
   nonempty := ⟨u⟩
 
-theorem IsEulerian.even_degree_iff (ht : p.IsEulerian) [Fintype V] [DecidableRel G.Adj] :
+theorem IsEulerian.even_degree_iff (ht : p.IsEulerian) [Fintype (G.neighborSet w)] :
     Even (G.degree w) ↔ u ≠ v → w ≠ u ∧ w ≠ v := by
+  have := ht.fintypeEdgeSet
   rw [← ht.isTrail.even_countP_edges_iff, ← Multiset.coe_countP, Multiset.countP_eq_card_filter,
     ← card_incidenceFinset_eq_degree, incidenceFinset_eq_filter, ← ht.edgesFinset_eq]
   simp [Finset.card_def]
@@ -142,4 +156,49 @@ theorem IsEulerian.card_odd_degree [Fintype V] [DecidableRel G.Adj] (ht : p.IsEu
 
 end Walk
 
+variable (G) in
+/-- A graph is Eulerian if it contains a closed Eulerian trail. -/
+@[mk_iff]
+structure IsEulerian where
+  exists_isEulerian : ∃ (v : V) (p : G.Walk v v), p.IsEulerian
+
+protected theorem IsEulerian.nonempty (h : G.IsEulerian) : Nonempty V :=
+  h.exists_isEulerian.nonempty
+
+/-- A graph is Eulerian and nontrivial iff it contains an Eulerian circuit. -/
+theorem isEulerian_and_ne_bot_iff :
+    G.IsEulerian ∧ G ≠ ⊥ ↔ ∃ (v : V) (p : G.Walk v v), p.IsEulerian ∧ p.IsCircuit := by
+  grind [isEulerian_iff, Walk.IsEulerian.isCircuit_iff]
+
+variable (V) in
+@[simp]
+protected theorem IsEulerian.bot [Nonempty V] : (⊥ : SimpleGraph V).IsEulerian :=
+  ⟨Classical.arbitrary V, .nil, .of_bot .nil⟩
+
+/-- In an Eulerian graph there exists an Eulerian circuit from any non-isolated vertex. -/
+theorem IsEulerian.exists_isEulerian_of_not_isIsolated (hG : G.IsEulerian) (hv : ¬G.IsIsolated v) :
+    ∃ p : G.Walk v v, p.IsEulerian :=
+  have ⟨_, _, hp⟩ := hG.exists_isEulerian
+  ⟨_, hp.rotate <| hp.mem_support_of_not_isIsolated hv⟩
+
+variable (v) in
+/-- In a connected Eulerian graph there exists a closed Eulerian trail from any vertex.
+Since Eulerian graphs are nonempty, it suffices to require preconnected. -/
+theorem IsEulerian.exists_isEulerian_of_preconnected (h : G.IsEulerian) (h' : G.Preconnected) :
+    ∃ p : G.Walk v v, p.IsEulerian := by
+  cases subsingleton_or_nontrivial V
+  · exact ⟨.nil, Subsingleton.elim G ⊥ ▸ .of_bot .nil⟩
+  exact h.exists_isEulerian_of_not_isIsolated <| h'.not_isIsolated v
+
+theorem IsEulerian.connected_of_forall_not_isIsolated (h : G.IsEulerian)
+    (h' : ∀ v, ¬G.IsIsolated v) : G.Connected :=
+  have ⟨_, _, hp⟩ := h.exists_isEulerian
+  hp.connected_of_forall_not_isIsolated h'
+
+variable (v) in
+theorem IsEulerian.even_degree (h : G.IsEulerian) [Fintype (G.neighborSet v)] :
+    Even (G.degree v) := by
+  have ⟨u, p, hp⟩ := h.exists_isEulerian
+  simp [hp.even_degree_iff]
+
 end SimpleGraph