feat(Combinatorics/SimpleGraph): basic Adj.toWalk API (leanprover-community#41797)

Author: SnirBroshi

Mathlib/Combinatorics/SimpleGraph/Connectivity/Subgraph.lean

@@ -215,6 +215,10 @@ theorem mem_edges_toSubgraph (p : G.Walk u v) {e : Sym2 V} :
 theorem edgeSet_toSubgraph (p : G.Walk u v) : p.toSubgraph.edgeSet = p.edgeSet :=
   Set.ext fun _ => p.mem_edges_toSubgraph
 
+theorem _root_.SimpleGraph.Adj.toSubgraph_toWalk (h : G.Adj u v) :
+    h.toWalk.toSubgraph = G.subgraphOfAdj h := by
+  ext <;> simp
+
 @[simp]
 theorem toSubgraph_append (p : G.Walk u v) (q : G.Walk v w) :
     (p.append q).toSubgraph = p.toSubgraph ⊔ q.toSubgraph := by induction p <;> simp [*, sup_assoc]

Mathlib/Combinatorics/SimpleGraph/Paths.lean

@@ -211,6 +211,9 @@ theorem IsPath.nil_iff_eq {u v : V} {p : G.Walk u v} (hp : p.IsPath) : p.Nil ↔
   rintro rfl
   exact isPath_iff_nil.mp hp
 
+theorem _root_.SimpleGraph.Adj.isPath_toWalk (h : G.Adj u v) : h.toWalk.IsPath := by
+  simp [h.ne]
+
 theorem IsPath.reverse {u v : V} {p : G.Walk u v} (h : p.IsPath) : p.reverse.IsPath := by
   simpa [isPath_def] using h
 

Mathlib/Combinatorics/SimpleGraph/Walk/Basic.lean

@@ -95,6 +95,9 @@ theorem length_nil {u : V} : (nil : G.Walk u u).length = 0 := rfl
 theorem length_cons {u v w : V} (h : G.Adj u v) (p : G.Walk v w) :
     (cons h p).length = p.length + 1 := rfl
 
+theorem _root_.SimpleGraph.Adj.length_toWalk (h : G.Adj u v) : h.toWalk.length = 1 := by
+  simp
+
 theorem eq_of_length_eq_zero {u v : V} : ∀ {p : G.Walk u v}, p.length = 0 → u = v
   | nil, _ => rfl
 
@@ -135,6 +138,9 @@ theorem support_nil {u : V} : (nil : G.Walk u u).support = [u] := rfl
 theorem support_cons {u v w : V} (h : G.Adj u v) (p : G.Walk v w) :
     (cons h p).support = u :: p.support := rfl
 
+theorem _root_.SimpleGraph.Adj.support_toWalk (h : G.Adj u v) : h.toWalk.support = [u, v] :=
+  rfl
+
 @[simp]
 theorem support_ne_nil {u v : V} (p : G.Walk u v) : p.support ≠ [] := by cases p <;> simp
 
@@ -225,6 +231,9 @@ theorem darts_nil {u : V} : (nil : G.Walk u u).darts = [] := rfl
 theorem darts_cons {u v w : V} (h : G.Adj u v) (p : G.Walk v w) :
     (cons h p).darts = ⟨(u, v), h⟩ :: p.darts := rfl
 
+theorem _root_.SimpleGraph.Adj.darts_toWalk (h : G.Adj u v) : h.toWalk.darts = [⟨(u, v), h⟩] :=
+  rfl
+
 theorem cons_map_snd_darts {u v : V} (p : G.Walk u v) : (u :: p.darts.map (·.snd)) = p.support := by
   induction p <;> simp [*]
 
@@ -245,6 +254,9 @@ theorem edges_nil {u : V} : (nil : G.Walk u u).edges = [] := rfl
 theorem edges_cons {u v w : V} (h : G.Adj u v) (p : G.Walk v w) :
     (cons h p).edges = s(u, v) :: p.edges := rfl
 
+theorem _root_.SimpleGraph.Adj.edges_toWalk (h : G.Adj u v) : h.toWalk.edges = [s(u, v)] :=
+  rfl
+
 @[simp, grind =]
 theorem length_support {u v : V} (p : G.Walk u v) : p.support.length = p.length + 1 := by
   induction p <;> simp [*]
@@ -499,10 +511,11 @@ def ofDarts (l : List G.Dart) (hne : l ≠ []) (hchain : l.IsChain G.DartAdj) :
   | d₁ :: d₂ :: l =>
     .cons (hchain.rel ▸ d₁.adj) <| ofDarts (d₂ :: l) (l.cons_ne_nil d₂) hchain.of_cons
 
-variable (G) in
 @[simp]
-theorem ofDarts_singleton (d : G.Dart) :
-    ofDarts [d] ([].cons_ne_nil d) (.singleton d) = .cons d.adj .nil :=
+theorem ofDarts_singleton (d : G.Dart) : ofDarts [d] (by simp) (by simp) = .cons d.adj .nil :=
+  rfl
+
+theorem ofDarts_singleton' (d : G.Dart) : ofDarts [d] (by simp) (by simp) = d.adj.toWalk :=
   rfl
 
 @[simp]

Mathlib/Combinatorics/SimpleGraph/Walk/Chord.lean

@@ -54,5 +54,8 @@ theorem IsChordless.mem_edges {p : G.Walk u v} (h : p.IsChordless) {u' v' : V}
     (hu' : u' ∈ p.support) (hv' : v' ∈ p.support) (hadj : G.Adj u' v') : s(u', v') ∈ p.edges :=
   isChordless_iff_forall_mem_edges.mp h hu' hv' hadj
 
+theorem _root_.SimpleGraph.Adj.isChordless_toWalk (h : G.Adj u v) : h.toWalk.IsChordless := by
+  grind [isChordless_iff_forall_mem_edges, h.support_toWalk, h.edges_toWalk, Adj.ne]
+
 end Walk
 end SimpleGraph