From 5b021d48fb9fde3363a7b09e89bbc6ac0a3787d5 Mon Sep 17 00:00:00 2001
From: Basil Rohner <basil.rohner@outlook.de>
Date: Sat, 18 Apr 2026 18:41:20 +0200
Subject: [PATCH 01/10] feat: define notions of graphs,  walks, cycles and
 paths

---
 Cslib/Algorithms/Lean/Graph/Graph.lean | 181 ++++++++++
 Cslib/Algorithms/Lean/Graph/Walk.lean  | 442 +++++++++++++++++++++++++
 2 files changed, 623 insertions(+)
 create mode 100644 Cslib/Algorithms/Lean/Graph/Graph.lean
 create mode 100644 Cslib/Algorithms/Lean/Graph/Walk.lean

diff --git a/Cslib/Algorithms/Lean/Graph/Graph.lean b/Cslib/Algorithms/Lean/Graph/Graph.lean
new file mode 100644
index 000000000..89b77ae01
--- /dev/null
+++ b/Cslib/Algorithms/Lean/Graph/Graph.lean
@@ -0,0 +1,181 @@
+/-
+Copyright (c) 2026 Basil Rohner. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Basil Rohner, Sorrachai Yingchareonthawornchai, Weixuan Yuan
+-/
+
+module
+public import Cslib.Init
+public import Mathlib.Data.Sym.Sym2
+
+@[expose] public section
+
+/-!
+# Graph structures
+
+This file introduces a small hierarchy of graph-like combinatorial structures on a vertex
+type `α`. Each structure carries its vertex and edge sets explicitly.
+
+## Main definitions
+
+* `Hypergraph α ε`: a hypergraph with abstract edge index type `ε`; each edge carries an
+  arbitrary `Set α` of endpoints. Parallel edges and loops are permitted, and the vertex
+  and edge sets may be infinite.
+* `Graph α ε`: a general graph with abstract edge index type `ε`; each edge carries an
+  unordered pair of endpoints as a `Sym2 α`. Parallel edges and loops are permitted.
+* `SimpleGraph α`: a finite simple graph, with edges indexed by `Sym2 α` itself, `Finset`
+  vertex and edge sets, and no loops.
+* `DiGraph α ε`: a directed graph with abstract edge index type `ε`; each edge carries an
+  ordered pair `α × α` of endpoints.
+* `SimpleDiGraph α`: a finite simple directed graph with edges as ordered pairs and no
+  loops.
+
+## Main forgetful maps
+
+* `Graph.toHypergraph`: reinterpret a graph as a hypergraph by viewing each `Sym2 α`
+  endpoint pair as a two-element set.
+* `SimpleGraph.toGraph`: forget the finiteness and looplessness axioms of a simple graph.
+* `SimpleDiGraph.toDiGraph`: forget the finiteness and looplessness axioms of a simple
+  directed graph.
+
+The corresponding `Coe` instances are registered.
+-/
+
+namespace Cslib.Algorithms.Lean
+variable {α ε : Type*}
+
+/-- A hypergraph on vertex type `α` with edges indexed by `ε`. The edge set is abstract;
+endpoints are carried by a separate map. Parallel edges and loops are permitted, and both
+the vertex and edge sets may be infinite. -/
+structure Hypergraph (α ε : Type*) where
+  /-- The set of vertices. -/
+  vertexSet : Set α
+  /-- The set of edges. -/
+  edgeSet : Set ε
+  /-- The endpoint map, assigning to each edge its set of incident vertices. -/
+  endpoints : ε → Set α
+  /-- Every endpoint of an edge is a vertex. -/
+  incidence : ∀ e ∈ edgeSet, ∀ v ∈ endpoints e, v ∈ vertexSet
+
+/-- A general graph on vertex type `α` with edges indexed by `ε`. The edge set is abstract;
+endpoints are carried by a separate map. Parallel edges and loops are permitted, and both
+the vertex and edge sets may be infinite. -/
+structure Graph (α ε : Type*) where
+  /-- The set of vertices. -/
+  vertexSet : Set α
+  /-- The set of edges. -/
+  edgeSet : Set ε
+  /-- The endpoint map, sending each edge to its unordered pair of endpoints. -/
+  endpoints : ε → Sym2 α
+  /-- Every endpoint of an edge is a vertex. -/
+  incidence : ∀ e ∈ edgeSet, ∀ v ∈ endpoints e, v ∈ vertexSet
+
+/-- A finite simple graph on `α`: finite vertex and edge sets, edges as unordered pairs of
+distinct vertices. -/
+@[grind]
+structure SimpleGraph (α : Type*) where
+  /-- The finite set of vertices. -/
+  vertexSet : Finset α
+  /-- The finite set of edges, each an unordered pair of vertices. -/
+  edgeSet : Finset (Sym2 α)
+  /-- Both endpoints of every edge are vertices. -/
+  incidence : ∀ e ∈ edgeSet, ∀ v ∈ e, v ∈ vertexSet
+  /-- No edge is a loop. -/
+  loopless : ∀ e ∈ edgeSet, ¬ e.IsDiag
+
+/-- A directed graph on vertex type `α` with edges indexed by `ε`. The edge set is abstract;
+ordered endpoints are carried by a separate map. Parallel edges and loops are permitted,
+and both the vertex and edge sets may be infinite. -/
+structure DiGraph (α ε : Type*) where
+  /-- The set of vertices. -/
+  vertexSet : Set α
+  /-- The set of edges. -/
+  edgeSet : Set ε
+  /-- The endpoint map, sending each edge to its ordered pair `(source, target)`. -/
+  endpoints : ε → α × α
+  /-- Both endpoints of every edge are vertices. -/
+  incidence : ∀ e ∈ edgeSet, (endpoints e).1 ∈ vertexSet ∧ (endpoints e).2 ∈ vertexSet
+
+/-- A finite simple directed graph on `α`: finite vertex and edge sets, edges as ordered
+pairs of distinct vertices. -/
+structure SimpleDiGraph (α : Type*) where
+  /-- The finite set of vertices. -/
+  vertexSet : Finset α
+  /-- The finite set of directed edges. -/
+  edgeSet : Finset (α × α)
+  /-- Both endpoints of every directed edge are vertices. -/
+  incidence : ∀ e ∈ edgeSet, e.1 ∈ vertexSet ∧ e.2 ∈ vertexSet
+  /-- No directed edge is a loop. -/
+  loopless : ∀ e ∈ edgeSet, e.1 ≠ e.2
+
+/-- Reinterpret a `Graph` as a `Hypergraph` by replacing each `Sym2 α` endpoint pair by
+the corresponding two-element set. -/
+def Graph.toHypergraph (G : Graph α ε) : Hypergraph α ε where
+  vertexSet := G.vertexSet
+  edgeSet := G.edgeSet
+  endpoints e := {v | v ∈ G.endpoints e}
+  incidence e he v hv := G.incidence e he v hv
+
+/-- Forget the finiteness and looplessness axioms of a `SimpleGraph`, viewing it as a
+`Graph` with edges indexed by `Sym2 α` itself and identity endpoint map. -/
+def SimpleGraph.toGraph (G : SimpleGraph α) : Graph α (Sym2 α) where
+  vertexSet := G.vertexSet
+  edgeSet := G.edgeSet
+  endpoints := id
+  incidence e he v hv := by simpa using G.incidence e (by simpa using he) v hv
+
+/-- Forget the finiteness and looplessness axioms of a `SimpleDiGraph`, viewing it as a
+`DiGraph` with edges indexed by `α × α` itself and identity endpoint map. -/
+def SimpleDiGraph.toDiGraph (G : SimpleDiGraph α) : DiGraph α (α × α) where
+  vertexSet := G.vertexSet
+  edgeSet := G.edgeSet
+  endpoints := id
+  incidence e he := by simpa using G.incidence e (by simpa using he)
+
+instance : Coe (Graph α ε) (Hypergraph α ε) := ⟨Graph.toHypergraph⟩
+
+instance : Coe (SimpleGraph α) (Graph α (Sym2 α)) := ⟨SimpleGraph.toGraph⟩
+
+instance : Coe (SimpleDiGraph α) (DiGraph α (α × α)) := ⟨SimpleDiGraph.toDiGraph⟩
+
+
+class HasVertexSet (G : Type*) (V : outParam Type*) where
+  vertexSet : G → V
+
+class HasEdgeSet (G : Type*) (E : outParam Type*) where
+  edgeSet : G → E
+
+@[simp] instance {α ε : Type*} : HasVertexSet (Hypergraph α ε) (Set α) :=
+  ⟨Hypergraph.vertexSet⟩
+
+@[simp] instance {α ε : Type*} : HasVertexSet (Graph α ε) (Set α) :=
+  ⟨Graph.vertexSet⟩
+
+@[simp] instance {α : Type*} : HasVertexSet (SimpleGraph α) (Finset α) :=
+  ⟨SimpleGraph.vertexSet⟩
+
+@[simp] instance {α ε : Type*} : HasVertexSet (DiGraph α ε) (Set α) :=
+  ⟨DiGraph.vertexSet⟩
+
+@[simp] instance {α : Type*} : HasVertexSet (SimpleDiGraph α) (Finset α) :=
+  ⟨SimpleDiGraph.vertexSet⟩
+
+@[simp] instance {α ε : Type*} : HasEdgeSet (Hypergraph α ε) (Set (Set α)) :=
+  ⟨fun G => G.edgeSet.image G.endpoints⟩
+
+@[simp] instance {α ε : Type*} : HasEdgeSet (Graph α ε) (Set (Sym2 α)) :=
+  ⟨fun G => G.edgeSet.image G.endpoints⟩
+
+@[simp] instance {α : Type*} : HasEdgeSet (SimpleGraph α) (Finset (Sym2 α)) :=
+  ⟨SimpleGraph.edgeSet⟩
+
+@[simp] instance {α ε : Type*} : HasEdgeSet (DiGraph α ε) (Set (α × α)) :=
+  ⟨fun G => G.edgeSet.image G.endpoints⟩
+
+@[simp] instance {α : Type*} : HasEdgeSet (SimpleDiGraph α) (Finset (α × α)) :=
+  ⟨SimpleDiGraph.edgeSet⟩
+
+scoped notation "V(" G ")" => HasVertexSet.vertexSet G
+scoped notation "E(" G ")" => HasEdgeSet.edgeSet G
+
+end Cslib.Algorithms.Lean
diff --git a/Cslib/Algorithms/Lean/Graph/Walk.lean b/Cslib/Algorithms/Lean/Graph/Walk.lean
new file mode 100644
index 000000000..79f162f0a
--- /dev/null
+++ b/Cslib/Algorithms/Lean/Graph/Walk.lean
@@ -0,0 +1,442 @@
+-- Authors: Sorrachai Yingchareonthawornchai and Weixuan Yuan
+-- This definition of walk are well-defined for both directed and undirected simple graphs.
+
+import Mathlib.Data.Sym.Sym2
+set_option tactic.hygienic false
+variable {α : Type*}
+
+
+/- VertexSeq as a non-empty seq -/
+@[grind] inductive VertexSeq (α : Type*)
+  | singleton (v : α) : VertexSeq α
+  | cons (w : VertexSeq α) (v : α) : VertexSeq α
+
+namespace VertexSeq
+
+/-! ## Basic accessors -/
+
+/- The list of vertices visited by the walk, in order. -/
+@[grind] def toList : VertexSeq α → List α
+  | .singleton v => [v]
+  | .cons p v => p.toList.cons v
+
+/-- The first node does not count in the sequence. -/
+@[grind] def length : VertexSeq α → ℕ
+  | .singleton _ => 0
+  | .cons w _ => 1 + w.length
+
+@[grind] def head : VertexSeq α → α
+  | .singleton v => v
+  | .cons w _ => head w
+
+@[grind] def tail : VertexSeq α → α
+  | .singleton v => v
+  | .cons _ v => v
+
+@[simp, grind =] lemma singleton_head_eq (u : α) :
+  (VertexSeq.singleton u).head = u := by simp [head]
+@[simp, grind =] lemma singleton_tail_eq (u : α) :
+  (VertexSeq.singleton u).tail = u := by simp [tail]
+
+@[simp, grind =] lemma con_head_eq (w : VertexSeq α) (u : α) :
+    (w.cons u).head = w.head := rfl
+
+@[simp, grind =] lemma con_tail_eq (w : VertexSeq α) (u : α) :
+    (w.cons u).tail = u := rfl
+
+@[simp, grind ←] lemma head_mem_toList (w : VertexSeq α) : w.head ∈ w.toList := by
+  induction w <;> grind [VertexSeq.head, VertexSeq.toList]
+
+/-! ## dropHead, dropTail -/
+
+@[grind] def dropHead : VertexSeq α → VertexSeq α
+  | .singleton v => .singleton v
+  | .cons (.singleton _) v => .singleton v
+  | .cons w v => .cons (dropHead w) v
+
+@[grind] def dropTail : VertexSeq α → VertexSeq α
+  | .singleton v => .singleton v
+  | .cons w _ => w
+
+/-! ## append, reverse, and their laws -/
+
+@[grind] def append : VertexSeq α → VertexSeq α → VertexSeq α
+  | w, .singleton v => .cons w v
+  | w, .cons w2 v => .cons (append w w2) v
+
+@[grind] def reverse : VertexSeq α → VertexSeq α
+  | .singleton v => .singleton v
+  | .cons w v => append (.singleton v) (reverse w)
+
+@[simp, grind =] lemma length_append (p q : VertexSeq α) :
+  (p.append q).length = p.length + q.length + 1 := by
+  fun_induction append p q <;> grind
+
+@[simp, grind =] lemma singleton_reverse_eq (v : α) :
+  (VertexSeq.singleton v).reverse = .singleton v := rfl
+
+@[simp, grind =] lemma tail_on_tail (p q : VertexSeq α) : (p.append q).tail = q.tail := by
+  fun_induction append <;> simp_all [tail]
+
+@[simp, grind =] lemma head_on_head (p q : VertexSeq α) : (p.append q).head = p.head := by
+  fun_induction append <;> simp_all
+
+@[simp, grind =] lemma tail_on_tail_singleton (p : VertexSeq α) (x : α) :
+    (p.append (.singleton x)).tail = x := by
+  unfold append
+  unfold tail
+  split <;> aesop
+
+@[simp, grind =] lemma head_on_head_singleton (p : VertexSeq α) (x : α) :
+  ((VertexSeq.singleton x).append p).head = x := by
+  unfold append
+  unfold head
+  split <;> aesop
+
+@[simp, grind =] lemma append_assoc (p q r : VertexSeq α) :
+    (p.append q).append r = p.append (q.append r) := by
+  fun_induction append q r <;> simp_all [append]
+
+@[simp, grind =] lemma reverse_append (p q : VertexSeq α) :
+    (p.append q).reverse = q.reverse.append p.reverse := by
+  fun_induction append <;> simp_all [reverse]
+
+
+@[simp, grind =] lemma reverse_reverse (p : VertexSeq α) : (p.reverse).reverse = p := by
+  fun_induction reverse p <;> aesop
+
+
+@[simp, grind =] lemma head_reverse (p : VertexSeq α) : (p.reverse).head = p.tail := by
+  fun_induction reverse p <;> aesop
+
+
+@[simp, grind =] lemma tail_reverse (p : VertexSeq α) : (p.reverse).tail = p.head := by
+  fun_induction reverse p <;> aesop
+
+@[simp, grind =] lemma dropTail_head (p : VertexSeq α) : p.dropTail.head = p.head := by
+  fun_induction reverse p <;> aesop
+
+/-! ## takeUntil, dropUntil, loopErase -/
+
+/-- Take vertices until the first occurrence of `v` (including `v`). -/
+@[simp, grind] def takeUntil [DecidableEq α] (w : VertexSeq α) (v : α)
+  (h : v ∈ w.toList) : VertexSeq α :=
+  match w with
+  | .singleton x => .singleton x
+  | .cons w2 x =>
+    if h2 : v ∈ w2.toList then takeUntil w2 v h2
+    else .cons w2 x
+
+/-- Drop vertices until the last occurrence of `v` (not including `v`). -/
+@[simp, grind] def dropUntil [DecidableEq α] (w : VertexSeq α) (v : α)
+  (h : v ∈ w.toList) : VertexSeq α :=
+  match w with
+  | .singleton x => .singleton x
+  | .cons w2 x =>
+    if h2 : v ∈ w2.toList then .cons (dropUntil w2 v h2) x
+    else .singleton x
+
+@[simp] lemma takeUntil_length_le [DecidableEq α] (w : VertexSeq α) (v : α)
+    (h : v ∈ w.toList) : (w.takeUntil v h).length ≤ w.length := by
+  fun_induction takeUntil w v h <;> grind
+
+@[simp] lemma dropUntil_length_le [DecidableEq α] (w : VertexSeq α) (v : α)
+    (h : v ∈ w.toList) : (w.dropUntil v h).length ≤ w.length := by
+  fun_induction dropUntil w v h <;> grind
+
+@[simp, grind =] lemma head_takeUntil [DecidableEq α] (w : VertexSeq α) (v : α) (h : v ∈ w.toList) :
+    (takeUntil w v h).head = w.head := by
+  induction w <;> grind
+
+@[simp, grind =] lemma tail_takeUntil [DecidableEq α] (w : VertexSeq α) (v : α) (h : v ∈ w.toList) :
+    (takeUntil w v h).tail = v := by
+  induction w <;> grind
+
+@[simp, grind →] lemma mem_takeUntil [DecidableEq α] (w : VertexSeq α)
+  (v x : α) (h : v ∈ w.toList) : x ∈ (takeUntil w v h).toList → x ∈ w.toList := by
+  induction w generalizing v <;> grind
+
+@[simp, grind =] lemma head_dropUntil [DecidableEq α] (w : VertexSeq α) (v : α)
+    (h : v ∈ w.toList) :
+    (w.dropUntil v h).head = v := by
+  induction w <;> grind
+
+@[simp, grind =] lemma tail_dropUntil [DecidableEq α] (w : VertexSeq α) (v : α)
+    (h : v ∈ w.toList) :
+    (w.dropUntil v h).tail = w.tail := by
+  fun_induction VertexSeq.dropUntil w v h <;> simp [VertexSeq.tail]
+
+
+
+@[simp, grind →] lemma mem_dropUntil [DecidableEq α] (w : VertexSeq α) (v x : α)
+    (h : v ∈ w.toList) : x ∈ (w.dropUntil v h).toList → x ∈ w.toList := by
+  induction w generalizing v <;> grind
+
+@[grind] def loopErase [DecidableEq α] : VertexSeq α → VertexSeq α
+  | .singleton v => .singleton v
+  | .cons w v =>
+      if h : v ∈ w.toList then
+        loopErase (takeUntil w v h)
+      else
+        .cons (loopErase w) v
+  termination_by p => p.length
+  decreasing_by
+  · simp [length]; grind [takeUntil_length_le]
+  · simp [length]
+
+lemma mem_loopErase [DecidableEq α] (w : VertexSeq α) :
+    ∀ {x : α}, x ∈ w.loopErase.toList → x ∈ w.toList := by
+  fun_induction loopErase w <;> grind [toList, mem_takeUntil]
+
+theorem loopErase_nodup [DecidableEq α] (w : VertexSeq α) : w.loopErase.toList.Nodup := by
+  fun_induction VertexSeq.loopErase w <;> grind [toList, mem_loopErase]
+
+@[simp] lemma head_loopErase [DecidableEq α] (w : VertexSeq α) : w.loopErase.head = w.head := by
+  fun_induction loopErase w <;> simp_all
+
+@[simp] lemma tail_loopErase [DecidableEq α] (w : VertexSeq α) : w.loopErase.tail = w.tail := by
+  fun_induction loopErase w <;> simp_all
+
+end VertexSeq
+
+/-! ## IsWalk, Walk core data -/
+
+@[grind] inductive IsWalk : VertexSeq α → Prop
+  | singleton (v : α) : IsWalk (.singleton v)
+  | cons (w : VertexSeq α) (u : α)
+      (hw : IsWalk w)
+      (hneq : w.tail ≠ u)
+    : IsWalk (.cons w u)
+
+grind_pattern IsWalk.singleton => IsWalk (.singleton v)
+grind_pattern IsWalk.cons => IsWalk (.cons w u)
+
+structure Walk (α : Type*) where
+  seq : VertexSeq α
+  valid : IsWalk seq
+
+namespace Walk
+open VertexSeq
+
+@[ext] lemma ext {w1 w2 : Walk α} (hseq : w1.seq = w2.seq) : w1 = w2 := by
+  cases w1
+  cases w2
+  cases hseq
+  rfl
+
+/-! ## Basic IsWalk helper lemmas -/
+
+@[simp, grind =>] lemma iswalk_prefix (w2 : VertexSeq α) (v : α)
+    (valid : IsWalk (w2.cons v)) : IsWalk w2 := by
+  cases valid
+  grind
+
+@[simp, grind <=] lemma tail_neq_of_iswalk (w2 : VertexSeq α) (v : α)
+    (valid : IsWalk (w2.cons v)) : w2.tail ≠ v := by
+  cases valid
+  grind
+
+@[grind ←]
+lemma is_walk_two_seqs_append_of (w1 w2 : VertexSeq α)
+  (h1 : IsWalk w1) (h2 : IsWalk w2) (hneq : w1.tail ≠ w2.head) :
+    IsWalk (w1.append w2) := by
+  fun_induction w1.append w2 <;> grind
+
+@[grind ←]
+theorem prepend_iswalk (p : VertexSeq α) (v : α) (h : IsWalk p) (h2 : p.head ≠ v) :
+  IsWalk ((VertexSeq.singleton v).append p) := by grind
+
+@[grind →, grind ←]
+lemma isWalk_rev_if (w : VertexSeq α) : IsWalk w → IsWalk w.reverse := by
+  intro h
+  induction h <;> grind
+
+@[grind →]
+theorem is_walk_neq_of_append (p q : VertexSeq α) (h : IsWalk (p.append q))
+  : IsWalk p ∧ IsWalk q ∧ p.tail ≠ q.head := by fun_induction append <;> grind
+
+@[grind →]
+lemma isWalk_rev_imp (w : VertexSeq α) : IsWalk w.reverse → IsWalk w := by
+  fun_induction reverse <;> grind
+
+@[simp, grind =]
+lemma isWalk_rev_iff (w : VertexSeq α) : IsWalk w.reverse ↔ IsWalk w := by grind
+
+lemma nodup_iswalk (w : VertexSeq α) (h : w.toList.Nodup) : IsWalk w := by
+  induction w <;> grind
+
+-- @[grind ←]
+-- lemma prepend_iswalk' (w2 : VertexSeq α) (v : α)
+--     (valid : IsWalk w2) (hneq : v ≠ w2.head) :
+--   IsWalk ((VertexSeq.singleton v).append w2) := by
+--   induction valid generalizing v with
+--   | singleton x => grind [head, tail, append, IsWalk.singleton, IsWalk.cons]
+--   | cons w u hw htail ih => grind [head, append, IsWalk.cons, tail_on_tail]
+
+
+@[grind →]
+lemma takeUntil_iswalk [DecidableEq α] (w : VertexSeq α) (v : α) (h : v ∈ w.toList)
+  (hw : IsWalk w) :
+    IsWalk (w.takeUntil v h) := by
+  induction hw generalizing v <;> grind
+
+@[grind →]
+lemma dropUntil_iswalk [DecidableEq α] (w : VertexSeq α) (v : α)
+    (h : v ∈ w.toList) (hw : IsWalk w) :
+    IsWalk (w.dropUntil v h) := by
+  induction hw generalizing v <;> grind
+
+lemma loopErase_iswalk [DecidableEq α] (w : VertexSeq α) : IsWalk w.loopErase := by
+  grind [nodup_iswalk, loopErase_nodup]
+
+/-! ## support, head, tail, length, dropTail for Walk -/
+
+/-- The list of vertices visited by the walk, in order. -/
+@[simp, grind] def support (w : Walk α) : List α := w.seq.toList
+
+abbrev head (w : Walk α) : α := w.seq.head
+abbrev tail (w : Walk α) : α := w.seq.tail
+abbrev length (w : Walk α) : ℕ := w.seq.length
+
+abbrev dropTail (w : Walk α) : Walk α :=
+  { seq := w.seq.dropTail
+    valid := by grind [Walk]}
+
+def append_single (w : Walk α) (u : α) (h : u ≠ w.tail) : Walk α :=
+  ⟨w.seq.cons u, .cons w.seq u w.valid (by aesop)⟩
+
+@[simp, grind =]
+lemma dropTail_head (w : Walk α) : w.dropTail.head = w.head := by
+  cases w; induction valid <;> grind
+
+@[simp, grind .]
+lemma len_zero_of_drop_tail_eq_tail (w : Walk α) (h : w.dropTail.tail = w.tail) :
+    w.length = 0 := by
+  cases w; induction valid <;> grind
+
+@[simp, grind ←]
+lemma head_eq_tail_of_length_zero (w : Walk α) (h : w.length = 0)
+  : w.head = w.tail := by
+  cases w; induction valid <;> grind
+
+
+/-! ## Walk append, reverse and related lemmas -/
+
+@[grind ←]
+lemma two_seqs_append_of (w1 w2 : Walk α) (hneq : w1.tail ≠ w2.head) :
+    IsWalk (w1.seq.append w2.seq) := by
+  cases w1; cases w2; grind
+
+@[grind =]
+def append (w1 w2 : Walk α) (h : w1.tail = w2.head) : Walk α :=
+  if h1 : w1.length = 0 then w2
+  else
+    { seq := w1.dropTail.seq.append w2.seq
+      valid := by grind [Walk]}
+
+@[grind =]
+def reverse (w : Walk α) : Walk α :=
+  { seq := w.seq.reverse
+    valid := by grind [Walk]}
+
+@[simp, grind =] lemma head_reverse (w : Walk α) : (w.reverse).head = w.tail := by grind
+@[simp, grind =] lemma tail_reverse (w : Walk α) : (w.reverse).tail = w.head := by grind
+@[simp, grind =] lemma head_on_head (w1 w2 : Walk α) (h : w1.tail = w2.head) :
+    (Walk.append w1 w2 h).head = w1.head := by
+  cases w1; induction valid <;> grind
+@[simp, grind =] lemma tail_on_tail (w1 w2 : Walk α) (h : w1.tail = w2.head) :
+    (Walk.append w1 w2 h).tail = w2.tail := by grind
+
+@[simp, grind =] lemma length_append (w1 w2 : Walk α) (h : w1.tail = w2.head) :
+    (Walk.append w1 w2 h).length = w1.length + w2.length := by
+  unfold Walk.append
+  by_cases h1 : w1.length = 0
+  · grind
+  · have hdrop : w1.dropTail.length + 1 = w1.length := by
+      cases w1; induction valid <;> grind
+    grind
+
+/-! ## Path, cycle -/
+
+@[grind] def IsPath (w : Walk α) : Prop := w.support.Nodup
+
+abbrev toPath [DecidableEq α] (w : Walk α) : Walk α :=
+  { seq := w.seq.loopErase
+    valid := loopErase_iswalk w.seq }
+
+theorem toPath_isPath [DecidableEq α] (w : Walk α) : IsPath (toPath w) := by
+  unfold IsPath toPath support
+  simpa using loopErase_nodup w.seq
+
+lemma tail_toPath [DecidableEq α] (w : Walk α) : (toPath w).tail = w.tail := by
+  grind [tail_loopErase]
+
+lemma head_toPath [DecidableEq α] (w : Walk α) : (toPath w).head = w.head := by
+  grind [head_loopErase]
+
+def IsCycle (w : Walk α) : Prop :=
+  3 ≤ w.length ∧ w.head = w.tail ∧ IsPath w.dropTail
+
+
+
+/-! ## Some more helper lemmas -/
+@[simp, grind .] lemma takeUntil_head_eq_singleton [DecidableEq α] (w : VertexSeq α)
+  (h : w.head ∈ w.toList) :
+  w.takeUntil w.head h = VertexSeq.singleton w.head := by
+  induction w <;> grind
+
+@[simp, grind .] lemma dropUntil_head_eq_self [DecidableEq α] (w : VertexSeq α)
+  (h : w.head ∈ w.toList) :
+  w.dropUntil w.head h = w := by
+  induction w <;> grind
+
+@[simp, grind →] lemma vertex_seq_split [DecidableEq α]
+    (w : VertexSeq α) (v : α) (h : v ∈ w.toList) (hne : v ≠ w.head) :
+  (w.takeUntil v h).dropTail.append (w.dropUntil v h) = w := by
+  induction w generalizing v <;> grind
+
+@[simp, grind →] lemma walk_split [DecidableEq α]
+  (w : Walk α) (u : α) (hu : u ∈ w.support) :
+    w = Walk.append
+      ⟨w.seq.takeUntil u hu, takeUntil_iswalk w.seq u hu w.valid⟩
+      ⟨w.seq.dropUntil u hu, dropUntil_iswalk w.seq u hu w.valid⟩
+      (by grind) := by
+  by_cases h : u = w.head
+  · ext; grind
+  · ext; grind
+
+
+/-! ## Re-rooting a cycle -/
+/-- Re-root a cycle at any chosen vertex in its support. -/
+@[simp, grind] def rerootCycle [DecidableEq α] (w : Walk α) (hcyc : IsCycle w)
+    (u : α) (hu : u ∈ w.support) : Walk α :=
+  Walk.append
+    ⟨w.seq.dropUntil u hu, dropUntil_iswalk w.seq u hu w.valid⟩
+    ⟨w.seq.takeUntil u hu, takeUntil_iswalk w.seq u hu w.valid⟩
+    (by rcases hcyc with ⟨_, hht, _⟩; grind)
+
+@[simp, grind =] lemma toList_append (p q : VertexSeq α) :
+    (p.append q).toList = q.toList ++ p.toList := by
+  induction q generalizing p <;> grind
+
+lemma append_dropTail_eq_dropTail_append (w1 w2 : Walk α) (h : w1.tail = w2.head)
+  (hlen : w2.head ≠ w2.tail) :
+  (Walk.append w1 w2 h).dropTail = Walk.append w1 w2.dropTail (by grind) := by
+  by_cases h1 : w1.length = 0
+  · grind
+  · ext; cases w2; induction valid <;> grind
+
+lemma isCycle_rerootCycle [DecidableEq α] (w : Walk α) (hcyc : IsCycle w)
+  (u : α) (hu : u ∈ w.support) :
+  IsCycle (rerootCycle w hcyc u hu):= by
+  have h2 : w.length = (w.rerootCycle hcyc u hu).length := by grind
+  rcases hcyc with ⟨hlen, hht, hpath⟩
+  refine ⟨?_, ?_, ?_⟩
+  · grind
+  · grind
+  · by_cases h : u = w.head
+    · have hz : w.length ≠ 0 := by omega
+      grind
+    · grind [append_dropTail_eq_dropTail_append]
+
+end Walk

From a4e131228530d6349ae4c3dde8bd22e408a617bc Mon Sep 17 00:00:00 2001
From: Basil Rohner <basil.rohner@outlook.de>
Date: Sat, 18 Apr 2026 18:48:28 +0200
Subject: [PATCH 02/10] updates

---
 Cslib.lean                                    |   3 +
 Cslib/Algorithms/Lean/Graph/Walk.lean         | 417 +++++++++++++-----
 .../Data/FenwickTree/FenwickTree.lean         |  15 +
 3 files changed, 324 insertions(+), 111 deletions(-)
 create mode 100644 Cslib/Foundations/Data/FenwickTree/FenwickTree.lean

diff --git a/Cslib.lean b/Cslib.lean
index ef09e6f16..e30e8a559 100644
--- a/Cslib.lean
+++ b/Cslib.lean
@@ -1,5 +1,7 @@
 module  -- shake: keep-all
 
+public import Cslib.Algorithms.Lean.Graph.Graph
+public import Cslib.Algorithms.Lean.Graph.Walk
 public import Cslib.Algorithms.Lean.MergeSort.MergeSort
 public import Cslib.Algorithms.Lean.TimeM
 public import Cslib.Computability.Automata.Acceptors.Acceptor
@@ -48,6 +50,7 @@ public import Cslib.Foundations.Control.Monad.Free
 public import Cslib.Foundations.Control.Monad.Free.Effects
 public import Cslib.Foundations.Control.Monad.Free.Fold
 public import Cslib.Foundations.Data.BiTape
+public import Cslib.Foundations.Data.FenwickTree.FenwickTree
 public import Cslib.Foundations.Data.FinFun
 public import Cslib.Foundations.Data.HasFresh
 public import Cslib.Foundations.Data.Nat.Segment
diff --git a/Cslib/Algorithms/Lean/Graph/Walk.lean b/Cslib/Algorithms/Lean/Graph/Walk.lean
index 79f162f0a..8c783a5a6 100644
--- a/Cslib/Algorithms/Lean/Graph/Walk.lean
+++ b/Cslib/Algorithms/Lean/Graph/Walk.lean
@@ -1,13 +1,58 @@
--- Authors: Sorrachai Yingchareonthawornchai and Weixuan Yuan
--- This definition of walk are well-defined for both directed and undirected simple graphs.
+/-
+Copyright (c) 2026 Basil Rohner. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Basil Rohner, Sorrachai Yingchareonthawornchai, Weixuan Yuan
+-/
+
+module
+public import Cslib.Init
+public import Cslib.Algorithms.Lean.Graph.Graph
+public import Mathlib.Data.Sym.Sym2
+
+@[expose] public section
 
-import Mathlib.Data.Sym.Sym2
 set_option tactic.hygienic false
 variable {α : Type*}
 
-
-/- VertexSeq as a non-empty seq -/
-@[grind] inductive VertexSeq (α : Type*)
+/-!
+# Vertex sequences and walks
+
+This file defines vertex sequences (`VertexSeq`) and walks (`Walk`) for simple graphs.
+The definitions are well-defined for both directed and undirected simple graphs.
+
+A `VertexSeq` is a nonempty sequence of vertices, and a `Walk` is a vertex sequence
+satisfying the `IsWalk` predicate, which requires that consecutive vertices are distinct.
+
+## Main definitions
+
+* `VertexSeq`: a nonempty sequence of vertices, defined inductively as either a singleton
+  or a cons extension.
+* `VertexSeq.takeUntil`: truncate a vertex sequence at the first occurrence of a given vertex.
+* `VertexSeq.dropUntil`: drop the prefix up to the last occurrence of a given vertex.
+* `VertexSeq.loopErase`: erase loops from a vertex sequence, producing a sequence with no
+  repeated vertices.
+* `IsWalk`: a predicate asserting that consecutive vertices in a `VertexSeq` are distinct.
+* `Walk`: a bundled vertex sequence together with a proof of `IsWalk`.
+* `Walk.IsPath`: a walk whose support has no duplicate vertices.
+* `Walk.IsCycle`: a walk of length at least 3 whose head equals its tail and whose interior
+  is a path.
+* `Walk.toPath`: loop-erase a walk to obtain a path.
+* `Walk.rerootCycle`: re-root a cycle at any vertex in its support.
+
+## Main statements
+
+* `VertexSeq.loopErase_nodup`: loop erasure produces a duplicate-free vertex list.
+* `Walk.loopErase_iswalk`: loop erasure of any vertex sequence yields a valid walk.
+* `Walk.toPath_isPath`: `Walk.toPath` produces a path.
+* `Walk.isCycle_rerootCycle`: re-rooting a cycle at any vertex in its support yields a cycle.
+-/
+
+namespace Cslib.Algorithms.Lean
+
+/-- A nonempty sequence of vertices, used as the underlying data for walks.
+`singleton v` is the trivial sequence containing only `v`, and `cons w v` extends the
+sequence `w` by appending vertex `v` at the end. -/
+@[scoped grind] inductive VertexSeq (α : Type*)
   | singleton (v : α) : VertexSeq α
   | cons (w : VertexSeq α) (v : α) : VertexSeq α
 
@@ -15,111 +60,134 @@ namespace VertexSeq
 
 /-! ## Basic accessors -/
 
-/- The list of vertices visited by the walk, in order. -/
-@[grind] def toList : VertexSeq α → List α
+/-- The list of vertices in the sequence, in order. -/
+@[scoped grind] def toList : VertexSeq α → List α
   | .singleton v => [v]
   | .cons p v => p.toList.cons v
 
-/-- The first node does not count in the sequence. -/
-@[grind] def length : VertexSeq α → ℕ
+/-- The number of edges in the sequence, i.e., one less than the number of vertices.
+A singleton has length 0. -/
+@[scoped grind] def length : VertexSeq α → ℕ
   | .singleton _ => 0
   | .cons w _ => 1 + w.length
 
-@[grind] def head : VertexSeq α → α
+/-- The first vertex of the sequence. -/
+@[scoped grind] def head : VertexSeq α → α
   | .singleton v => v
   | .cons w _ => head w
 
-@[grind] def tail : VertexSeq α → α
+/-- The last vertex of the sequence. -/
+@[scoped grind] def tail : VertexSeq α → α
   | .singleton v => v
   | .cons _ v => v
 
-@[simp, grind =] lemma singleton_head_eq (u : α) :
+/-- The head of a singleton sequence is the vertex itself. -/
+@[simp, scoped grind =] lemma singleton_head_eq (u : α) :
   (VertexSeq.singleton u).head = u := by simp [head]
-@[simp, grind =] lemma singleton_tail_eq (u : α) :
+
+/-- The tail of a singleton sequence is the vertex itself. -/
+@[simp, scoped grind =] lemma singleton_tail_eq (u : α) :
   (VertexSeq.singleton u).tail = u := by simp [tail]
 
-@[simp, grind =] lemma con_head_eq (w : VertexSeq α) (u : α) :
+/-- The head of `w.cons u` is the head of `w`. -/
+@[simp, scoped grind =] lemma con_head_eq (w : VertexSeq α) (u : α) :
     (w.cons u).head = w.head := rfl
 
-@[simp, grind =] lemma con_tail_eq (w : VertexSeq α) (u : α) :
+/-- The tail of `w.cons u` is `u`. -/
+@[simp, scoped grind =] lemma con_tail_eq (w : VertexSeq α) (u : α) :
     (w.cons u).tail = u := rfl
 
-@[simp, grind ←] lemma head_mem_toList (w : VertexSeq α) : w.head ∈ w.toList := by
+/-- The head of a vertex sequence belongs to its vertex list. -/
+@[simp, scoped grind ←] lemma head_mem_toList (w : VertexSeq α) : w.head ∈ w.toList := by
   induction w <;> grind [VertexSeq.head, VertexSeq.toList]
 
 /-! ## dropHead, dropTail -/
 
-@[grind] def dropHead : VertexSeq α → VertexSeq α
+/-- Remove the first vertex from the sequence. A singleton is left unchanged. -/
+@[scoped grind] def dropHead : VertexSeq α → VertexSeq α
   | .singleton v => .singleton v
   | .cons (.singleton _) v => .singleton v
   | .cons w v => .cons (dropHead w) v
 
-@[grind] def dropTail : VertexSeq α → VertexSeq α
+/-- Remove the last vertex from the sequence. A singleton is left unchanged. -/
+@[scoped grind] def dropTail : VertexSeq α → VertexSeq α
   | .singleton v => .singleton v
   | .cons w _ => w
 
 /-! ## append, reverse, and their laws -/
 
-@[grind] def append : VertexSeq α → VertexSeq α → VertexSeq α
+/-- Concatenate two vertex sequences by appending all vertices of the second sequence
+after the first. -/
+@[scoped grind] def append : VertexSeq α → VertexSeq α → VertexSeq α
   | w, .singleton v => .cons w v
   | w, .cons w2 v => .cons (append w w2) v
 
-@[grind] def reverse : VertexSeq α → VertexSeq α
+/-- Reverse the order of vertices in the sequence. -/
+@[scoped grind] def reverse : VertexSeq α → VertexSeq α
   | .singleton v => .singleton v
   | .cons w v => append (.singleton v) (reverse w)
 
-@[simp, grind =] lemma length_append (p q : VertexSeq α) :
+/-- The length of the concatenation equals the sum of the lengths plus one. -/
+@[simp, scoped grind =] lemma length_append (p q : VertexSeq α) :
   (p.append q).length = p.length + q.length + 1 := by
   fun_induction append p q <;> grind
 
-@[simp, grind =] lemma singleton_reverse_eq (v : α) :
+/-- Reversing a singleton is a no-op. -/
+@[simp, scoped grind =] lemma singleton_reverse_eq (v : α) :
   (VertexSeq.singleton v).reverse = .singleton v := rfl
 
-@[simp, grind =] lemma tail_on_tail (p q : VertexSeq α) : (p.append q).tail = q.tail := by
+/-- The tail of an appended sequence is the tail of the second sequence. -/
+@[simp, scoped grind =] lemma tail_on_tail (p q : VertexSeq α) : (p.append q).tail = q.tail := by
   fun_induction append <;> simp_all [tail]
 
-@[simp, grind =] lemma head_on_head (p q : VertexSeq α) : (p.append q).head = p.head := by
+/-- The head of an appended sequence is the head of the first sequence. -/
+@[simp, scoped grind =] lemma head_on_head (p q : VertexSeq α) : (p.append q).head = p.head := by
   fun_induction append <;> simp_all
 
-@[simp, grind =] lemma tail_on_tail_singleton (p : VertexSeq α) (x : α) :
+/-- The tail of a sequence appended with a singleton is the singleton's vertex. -/
+@[simp, scoped grind =] lemma tail_on_tail_singleton (p : VertexSeq α) (x : α) :
     (p.append (.singleton x)).tail = x := by
   unfold append
   unfold tail
   split <;> aesop
 
-@[simp, grind =] lemma head_on_head_singleton (p : VertexSeq α) (x : α) :
+/-- The head of a singleton appended with a sequence is the singleton's vertex. -/
+@[simp, scoped grind =] lemma head_on_head_singleton (p : VertexSeq α) (x : α) :
   ((VertexSeq.singleton x).append p).head = x := by
   unfold append
   unfold head
   split <;> aesop
 
-@[simp, grind =] lemma append_assoc (p q r : VertexSeq α) :
+/-- Append is associative. -/
+@[simp, scoped grind =] lemma append_assoc (p q r : VertexSeq α) :
     (p.append q).append r = p.append (q.append r) := by
   fun_induction append q r <;> simp_all [append]
 
-@[simp, grind =] lemma reverse_append (p q : VertexSeq α) :
+/-- Reversing a concatenation distributes as `q.reverse.append p.reverse`. -/
+@[simp, scoped grind =] lemma reverse_append (p q : VertexSeq α) :
     (p.append q).reverse = q.reverse.append p.reverse := by
   fun_induction append <;> simp_all [reverse]
 
-
-@[simp, grind =] lemma reverse_reverse (p : VertexSeq α) : (p.reverse).reverse = p := by
+/-- Reversing a vertex sequence twice yields the original sequence. -/
+@[simp, scoped grind =] lemma reverse_reverse (p : VertexSeq α) : (p.reverse).reverse = p := by
   fun_induction reverse p <;> aesop
 
-
-@[simp, grind =] lemma head_reverse (p : VertexSeq α) : (p.reverse).head = p.tail := by
+/-- The head of a reversed sequence is the tail of the original. -/
+@[simp, scoped grind =] lemma head_reverse (p : VertexSeq α) : (p.reverse).head = p.tail := by
   fun_induction reverse p <;> aesop
 
-
-@[simp, grind =] lemma tail_reverse (p : VertexSeq α) : (p.reverse).tail = p.head := by
+/-- The tail of a reversed sequence is the head of the original. -/
+@[simp, scoped grind =] lemma tail_reverse (p : VertexSeq α) : (p.reverse).tail = p.head := by
   fun_induction reverse p <;> aesop
 
-@[simp, grind =] lemma dropTail_head (p : VertexSeq α) : p.dropTail.head = p.head := by
+/-- Dropping the tail preserves the head. -/
+@[simp, scoped grind =] lemma dropTail_head (p : VertexSeq α) : p.dropTail.head = p.head := by
   fun_induction reverse p <;> aesop
 
 /-! ## takeUntil, dropUntil, loopErase -/
 
-/-- Take vertices until the first occurrence of `v` (including `v`). -/
-@[simp, grind] def takeUntil [DecidableEq α] (w : VertexSeq α) (v : α)
+/-- Truncate the sequence at the first occurrence of `v`, retaining `v` as the new tail. -/
+@[simp, scoped grind] def takeUntil [DecidableEq α] (w : VertexSeq α) (v : α)
   (h : v ∈ w.toList) : VertexSeq α :=
   match w with
   | .singleton x => .singleton x
@@ -127,8 +195,8 @@ namespace VertexSeq
     if h2 : v ∈ w2.toList then takeUntil w2 v h2
     else .cons w2 x
 
-/-- Drop vertices until the last occurrence of `v` (not including `v`). -/
-@[simp, grind] def dropUntil [DecidableEq α] (w : VertexSeq α) (v : α)
+/-- Drop the prefix up to the last occurrence of `v`, retaining `v` as the new head. -/
+@[simp, scoped grind] def dropUntil [DecidableEq α] (w : VertexSeq α) (v : α)
   (h : v ∈ w.toList) : VertexSeq α :=
   match w with
   | .singleton x => .singleton x
@@ -136,43 +204,51 @@ namespace VertexSeq
     if h2 : v ∈ w2.toList then .cons (dropUntil w2 v h2) x
     else .singleton x
 
+/-- `takeUntil` does not increase the length of the sequence. -/
 @[simp] lemma takeUntil_length_le [DecidableEq α] (w : VertexSeq α) (v : α)
     (h : v ∈ w.toList) : (w.takeUntil v h).length ≤ w.length := by
   fun_induction takeUntil w v h <;> grind
 
+/-- `dropUntil` does not increase the length of the sequence. -/
 @[simp] lemma dropUntil_length_le [DecidableEq α] (w : VertexSeq α) (v : α)
     (h : v ∈ w.toList) : (w.dropUntil v h).length ≤ w.length := by
   fun_induction dropUntil w v h <;> grind
 
-@[simp, grind =] lemma head_takeUntil [DecidableEq α] (w : VertexSeq α) (v : α) (h : v ∈ w.toList) :
-    (takeUntil w v h).head = w.head := by
+/-- The head of `takeUntil w v h` is the head of `w`. -/
+@[simp, scoped grind =] lemma head_takeUntil [DecidableEq α] (w : VertexSeq α) (v : α)
+    (h : v ∈ w.toList) : (takeUntil w v h).head = w.head := by
   induction w <;> grind
 
-@[simp, grind =] lemma tail_takeUntil [DecidableEq α] (w : VertexSeq α) (v : α) (h : v ∈ w.toList) :
-    (takeUntil w v h).tail = v := by
+/-- The tail of `takeUntil w v h` is `v`. -/
+@[simp, scoped grind =] lemma tail_takeUntil [DecidableEq α] (w : VertexSeq α) (v : α)
+    (h : v ∈ w.toList) : (takeUntil w v h).tail = v := by
   induction w <;> grind
 
-@[simp, grind →] lemma mem_takeUntil [DecidableEq α] (w : VertexSeq α)
+/-- Membership in `takeUntil` implies membership in the original sequence. -/
+@[simp, scoped grind →] lemma mem_takeUntil [DecidableEq α] (w : VertexSeq α)
   (v x : α) (h : v ∈ w.toList) : x ∈ (takeUntil w v h).toList → x ∈ w.toList := by
   induction w generalizing v <;> grind
 
-@[simp, grind =] lemma head_dropUntil [DecidableEq α] (w : VertexSeq α) (v : α)
+/-- The head of `dropUntil w v h` is `v`. -/
+@[simp, scoped grind =] lemma head_dropUntil [DecidableEq α] (w : VertexSeq α) (v : α)
     (h : v ∈ w.toList) :
     (w.dropUntil v h).head = v := by
   induction w <;> grind
 
-@[simp, grind =] lemma tail_dropUntil [DecidableEq α] (w : VertexSeq α) (v : α)
+/-- The tail of `dropUntil w v h` is the tail of `w`. -/
+@[simp, scoped grind =] lemma tail_dropUntil [DecidableEq α] (w : VertexSeq α) (v : α)
     (h : v ∈ w.toList) :
     (w.dropUntil v h).tail = w.tail := by
   fun_induction VertexSeq.dropUntil w v h <;> simp [VertexSeq.tail]
 
-
-
-@[simp, grind →] lemma mem_dropUntil [DecidableEq α] (w : VertexSeq α) (v x : α)
+/-- Membership in `dropUntil` implies membership in the original sequence. -/
+@[simp, scoped grind →] lemma mem_dropUntil [DecidableEq α] (w : VertexSeq α) (v x : α)
     (h : v ∈ w.toList) : x ∈ (w.dropUntil v h).toList → x ∈ w.toList := by
   induction w generalizing v <;> grind
 
-@[grind] def loopErase [DecidableEq α] : VertexSeq α → VertexSeq α
+/-- Erase all loops from a vertex sequence by repeatedly truncating at the first repeated
+vertex. The result has no duplicate vertices. -/
+@[scoped grind] def loopErase [DecidableEq α] : VertexSeq α → VertexSeq α
   | .singleton v => .singleton v
   | .cons w v =>
       if h : v ∈ w.toList then
@@ -184,40 +260,53 @@ namespace VertexSeq
   · simp [length]; grind [takeUntil_length_le]
   · simp [length]
 
+/-- Every vertex in the loop-erased sequence was present in the original. -/
 lemma mem_loopErase [DecidableEq α] (w : VertexSeq α) :
     ∀ {x : α}, x ∈ w.loopErase.toList → x ∈ w.toList := by
   fun_induction loopErase w <;> grind [toList, mem_takeUntil]
 
+/-- The vertex list of a loop-erased sequence has no duplicates. -/
 theorem loopErase_nodup [DecidableEq α] (w : VertexSeq α) : w.loopErase.toList.Nodup := by
   fun_induction VertexSeq.loopErase w <;> grind [toList, mem_loopErase]
 
-@[simp] lemma head_loopErase [DecidableEq α] (w : VertexSeq α) : w.loopErase.head = w.head := by
+/-- Loop erasure preserves the head of the sequence. -/
+@[simp] lemma head_loopErase [DecidableEq α] (w : VertexSeq α) :
+    w.loopErase.head = w.head := by
   fun_induction loopErase w <;> simp_all
 
-@[simp] lemma tail_loopErase [DecidableEq α] (w : VertexSeq α) : w.loopErase.tail = w.tail := by
+/-- Loop erasure preserves the tail of the sequence. -/
+@[simp] lemma tail_loopErase [DecidableEq α] (w : VertexSeq α) :
+    w.loopErase.tail = w.tail := by
   fun_induction loopErase w <;> simp_all
 
 end VertexSeq
 
 /-! ## IsWalk, Walk core data -/
 
-@[grind] inductive IsWalk : VertexSeq α → Prop
+/-- `IsWalk w` asserts that the vertex sequence `w` is a valid walk: every pair of
+consecutive vertices is distinct. -/
+@[scoped grind] inductive IsWalk : VertexSeq α → Prop
   | singleton (v : α) : IsWalk (.singleton v)
   | cons (w : VertexSeq α) (u : α)
       (hw : IsWalk w)
       (hneq : w.tail ≠ u)
     : IsWalk (.cons w u)
 
-grind_pattern IsWalk.singleton => IsWalk (.singleton v)
-grind_pattern IsWalk.cons => IsWalk (.cons w u)
+scoped grind_pattern IsWalk.singleton => IsWalk (.singleton v)
+scoped grind_pattern IsWalk.cons => IsWalk (.cons w u)
 
+/-- A walk in a graph, consisting of a nonempty vertex sequence together with a proof that
+consecutive vertices are distinct. -/
 structure Walk (α : Type*) where
+  /-- The underlying vertex sequence. -/
   seq : VertexSeq α
-  valid : IsWalk seq
+  /-- Proof that the vertex sequence is a valid walk. -/
+  isWalk : IsWalk seq
 
 namespace Walk
 open VertexSeq
 
+/-- Two walks are equal if and only if their underlying vertex sequences are equal. -/
 @[ext] lemma ext {w1 w2 : Walk α} (hseq : w1.seq = w2.seq) : w1 = w2 := by
   cases w1
   cases w2
@@ -226,180 +315,222 @@ open VertexSeq
 
 /-! ## Basic IsWalk helper lemmas -/
 
-@[simp, grind =>] lemma iswalk_prefix (w2 : VertexSeq α) (v : α)
+/-- The prefix of a valid walk is itself a valid walk. -/
+@[simp, scoped grind =>] lemma iswalk_prefix (w2 : VertexSeq α) (v : α)
     (valid : IsWalk (w2.cons v)) : IsWalk w2 := by
   cases valid
   grind
 
-@[simp, grind <=] lemma tail_neq_of_iswalk (w2 : VertexSeq α) (v : α)
+/-- In a valid walk `w2.cons v`, the tail of `w2` differs from `v`. -/
+@[simp, scoped grind <=] lemma tail_neq_of_iswalk (w2 : VertexSeq α) (v : α)
     (valid : IsWalk (w2.cons v)) : w2.tail ≠ v := by
   cases valid
   grind
 
-@[grind ←]
+/-- Appending two valid walks whose junction vertices are distinct yields a valid walk. -/
+@[scoped grind ←]
 lemma is_walk_two_seqs_append_of (w1 w2 : VertexSeq α)
   (h1 : IsWalk w1) (h2 : IsWalk w2) (hneq : w1.tail ≠ w2.head) :
     IsWalk (w1.append w2) := by
   fun_induction w1.append w2 <;> grind
 
-@[grind ←]
+/-- Prepending a singleton vertex to a valid walk yields a valid walk, provided the vertex
+is distinct from the walk's head. -/
+@[scoped grind ←]
 theorem prepend_iswalk (p : VertexSeq α) (v : α) (h : IsWalk p) (h2 : p.head ≠ v) :
   IsWalk ((VertexSeq.singleton v).append p) := by grind
 
-@[grind →, grind ←]
+/-- Reversing a valid walk yields a valid walk. -/
+@[scoped grind →, scoped grind ←]
 lemma isWalk_rev_if (w : VertexSeq α) : IsWalk w → IsWalk w.reverse := by
   intro h
   induction h <;> grind
 
-@[grind →]
+/-- Appending two sequences that form a valid walk implies each piece is a valid walk and
+the junction vertices are distinct. -/
+@[scoped grind →]
 theorem is_walk_neq_of_append (p q : VertexSeq α) (h : IsWalk (p.append q))
   : IsWalk p ∧ IsWalk q ∧ p.tail ≠ q.head := by fun_induction append <;> grind
 
-@[grind →]
+/-- If the reverse of a vertex sequence is a valid walk, then so is the original. -/
+@[scoped grind →]
 lemma isWalk_rev_imp (w : VertexSeq α) : IsWalk w.reverse → IsWalk w := by
   fun_induction reverse <;> grind
 
-@[simp, grind =]
+/-- A vertex sequence is a valid walk if and only if its reverse is. -/
+@[simp, scoped grind =]
 lemma isWalk_rev_iff (w : VertexSeq α) : IsWalk w.reverse ↔ IsWalk w := by grind
 
+/-- A vertex sequence with no duplicate vertices is a valid walk. -/
 lemma nodup_iswalk (w : VertexSeq α) (h : w.toList.Nodup) : IsWalk w := by
   induction w <;> grind
 
--- @[grind ←]
--- lemma prepend_iswalk' (w2 : VertexSeq α) (v : α)
---     (valid : IsWalk w2) (hneq : v ≠ w2.head) :
---   IsWalk ((VertexSeq.singleton v).append w2) := by
---   induction valid generalizing v with
---   | singleton x => grind [head, tail, append, IsWalk.singleton, IsWalk.cons]
---   | cons w u hw htail ih => grind [head, append, IsWalk.cons, tail_on_tail]
-
-
-@[grind →]
+/-- Truncating a valid walk at a vertex in its list yields a valid walk. -/
+@[scoped grind →]
 lemma takeUntil_iswalk [DecidableEq α] (w : VertexSeq α) (v : α) (h : v ∈ w.toList)
   (hw : IsWalk w) :
     IsWalk (w.takeUntil v h) := by
   induction hw generalizing v <;> grind
 
-@[grind →]
+/-- The suffix of a valid walk obtained by `dropUntil` is a valid walk. -/
+@[scoped grind →]
 lemma dropUntil_iswalk [DecidableEq α] (w : VertexSeq α) (v : α)
     (h : v ∈ w.toList) (hw : IsWalk w) :
     IsWalk (w.dropUntil v h) := by
   induction hw generalizing v <;> grind
 
+/-- The loop erasure of any vertex sequence is a valid walk. -/
 lemma loopErase_iswalk [DecidableEq α] (w : VertexSeq α) : IsWalk w.loopErase := by
   grind [nodup_iswalk, loopErase_nodup]
 
 /-! ## support, head, tail, length, dropTail for Walk -/
 
 /-- The list of vertices visited by the walk, in order. -/
-@[simp, grind] def support (w : Walk α) : List α := w.seq.toList
+@[simp, scoped grind] def support (w : Walk α) : List α := w.seq.toList
 
+/-- The first vertex of the walk. -/
 abbrev head (w : Walk α) : α := w.seq.head
+
+/-- The last vertex of the walk. -/
 abbrev tail (w : Walk α) : α := w.seq.tail
+
+/-- The number of edges in the walk. -/
 abbrev length (w : Walk α) : ℕ := w.seq.length
 
+/-- The walk obtained by removing the last vertex. -/
 abbrev dropTail (w : Walk α) : Walk α :=
   { seq := w.seq.dropTail
-    valid := by grind [Walk]}
+    isWalk := by grind [Walk]}
 
+/-- Extend a walk by appending a single vertex, given a proof that it differs from the
+current tail. -/
 def append_single (w : Walk α) (u : α) (h : u ≠ w.tail) : Walk α :=
-  ⟨w.seq.cons u, .cons w.seq u w.valid (by aesop)⟩
+  ⟨w.seq.cons u, .cons w.seq u w.isWalk (by aesop)⟩
 
-@[simp, grind =]
+/-- Dropping the tail of a walk preserves its head. -/
+@[simp, scoped grind =]
 lemma dropTail_head (w : Walk α) : w.dropTail.head = w.head := by
-  cases w; induction valid <;> grind
+  cases w; induction isWalk <;> grind
 
-@[simp, grind .]
+/-- If the tail of `w.dropTail` equals `w.tail`, then `w` has length 0. -/
+@[simp, scoped grind .]
 lemma len_zero_of_drop_tail_eq_tail (w : Walk α) (h : w.dropTail.tail = w.tail) :
     w.length = 0 := by
-  cases w; induction valid <;> grind
+  cases w; induction isWalk <;> grind
 
-@[simp, grind ←]
+/-- A walk of length 0 has equal head and tail. -/
+@[simp, scoped grind ←]
 lemma head_eq_tail_of_length_zero (w : Walk α) (h : w.length = 0)
   : w.head = w.tail := by
-  cases w; induction valid <;> grind
+  cases w; induction isWalk <;> grind
 
 
 /-! ## Walk append, reverse and related lemmas -/
 
-@[grind ←]
+/-- Appending the underlying sequences of two walks yields a valid walk when their junction
+vertices are distinct. -/
+@[scoped grind ←]
 lemma two_seqs_append_of (w1 w2 : Walk α) (hneq : w1.tail ≠ w2.head) :
     IsWalk (w1.seq.append w2.seq) := by
   cases w1; cases w2; grind
 
-@[grind =]
+/-- Concatenate two walks whose tail and head agree. The shared vertex appears only once
+in the result. -/
+@[scoped grind =]
 def append (w1 w2 : Walk α) (h : w1.tail = w2.head) : Walk α :=
   if h1 : w1.length = 0 then w2
   else
     { seq := w1.dropTail.seq.append w2.seq
-      valid := by grind [Walk]}
+      isWalk := by grind [Walk]}
 
-@[grind =]
+/-- Reverse a walk, swapping its head and tail. -/
+@[scoped grind =]
 def reverse (w : Walk α) : Walk α :=
   { seq := w.seq.reverse
-    valid := by grind [Walk]}
+    isWalk := by grind [Walk]}
 
-@[simp, grind =] lemma head_reverse (w : Walk α) : (w.reverse).head = w.tail := by grind
-@[simp, grind =] lemma tail_reverse (w : Walk α) : (w.reverse).tail = w.head := by grind
-@[simp, grind =] lemma head_on_head (w1 w2 : Walk α) (h : w1.tail = w2.head) :
+/-- The head of a reversed walk is the tail of the original. -/
+@[simp, scoped grind =] lemma head_reverse (w : Walk α) : (w.reverse).head = w.tail := by grind
+
+/-- The tail of a reversed walk is the head of the original. -/
+@[simp, scoped grind =] lemma tail_reverse (w : Walk α) : (w.reverse).tail = w.head := by grind
+
+/-- The head of an appended walk is the head of the first walk. -/
+@[simp, scoped grind =] lemma head_on_head (w1 w2 : Walk α) (h : w1.tail = w2.head) :
     (Walk.append w1 w2 h).head = w1.head := by
-  cases w1; induction valid <;> grind
-@[simp, grind =] lemma tail_on_tail (w1 w2 : Walk α) (h : w1.tail = w2.head) :
+  cases w1; induction isWalk <;> grind
+
+/-- The tail of an appended walk is the tail of the second walk. -/
+@[simp, scoped grind =] lemma tail_on_tail (w1 w2 : Walk α) (h : w1.tail = w2.head) :
     (Walk.append w1 w2 h).tail = w2.tail := by grind
 
-@[simp, grind =] lemma length_append (w1 w2 : Walk α) (h : w1.tail = w2.head) :
+/-- The length of an appended walk is the sum of the lengths of its parts. -/
+@[simp, scoped grind =] lemma length_append (w1 w2 : Walk α) (h : w1.tail = w2.head) :
     (Walk.append w1 w2 h).length = w1.length + w2.length := by
   unfold Walk.append
   by_cases h1 : w1.length = 0
   · grind
   · have hdrop : w1.dropTail.length + 1 = w1.length := by
-      cases w1; induction valid <;> grind
+      cases w1; induction isWalk <;> grind
     grind
 
 /-! ## Path, cycle -/
 
-@[grind] def IsPath (w : Walk α) : Prop := w.support.Nodup
+/-- A walk is a *path* if its support has no duplicate vertices. -/
+@[scoped grind] def IsPath (w : Walk α) : Prop := w.support.Nodup
 
+/-- Loop-erase a walk to obtain a walk with no repeated vertices. -/
 abbrev toPath [DecidableEq α] (w : Walk α) : Walk α :=
   { seq := w.seq.loopErase
-    valid := loopErase_iswalk w.seq }
+    isWalk := loopErase_iswalk w.seq }
 
+/-- The walk produced by `toPath` is a path. -/
 theorem toPath_isPath [DecidableEq α] (w : Walk α) : IsPath (toPath w) := by
   unfold IsPath toPath support
   simpa using loopErase_nodup w.seq
 
+/-- Loop erasure preserves the tail of a walk. -/
 lemma tail_toPath [DecidableEq α] (w : Walk α) : (toPath w).tail = w.tail := by
   grind [tail_loopErase]
 
+/-- Loop erasure preserves the head of a walk. -/
 lemma head_toPath [DecidableEq α] (w : Walk α) : (toPath w).head = w.head := by
   grind [head_loopErase]
 
+/-- A walk is a *cycle* if it has length at least 3, its head equals its tail, and the walk
+with its tail dropped is a path. -/
 def IsCycle (w : Walk α) : Prop :=
   3 ≤ w.length ∧ w.head = w.tail ∧ IsPath w.dropTail
 
 
-
 /-! ## Some more helper lemmas -/
-@[simp, grind .] lemma takeUntil_head_eq_singleton [DecidableEq α] (w : VertexSeq α)
+
+/-- Taking until the head of a sequence yields just the singleton of that head. -/
+@[simp, scoped grind .] lemma takeUntil_head_eq_singleton [DecidableEq α] (w : VertexSeq α)
   (h : w.head ∈ w.toList) :
   w.takeUntil w.head h = VertexSeq.singleton w.head := by
   induction w <;> grind
 
-@[simp, grind .] lemma dropUntil_head_eq_self [DecidableEq α] (w : VertexSeq α)
+/-- Dropping until the head of a sequence returns the original sequence. -/
+@[simp, scoped grind .] lemma dropUntil_head_eq_self [DecidableEq α] (w : VertexSeq α)
   (h : w.head ∈ w.toList) :
   w.dropUntil w.head h = w := by
   induction w <;> grind
 
-@[simp, grind →] lemma vertex_seq_split [DecidableEq α]
+/-- A vertex sequence can be split at any interior vertex into a prefix (with tail dropped)
+appended to a suffix. -/
+@[simp, scoped grind →] lemma vertex_seq_split [DecidableEq α]
     (w : VertexSeq α) (v : α) (h : v ∈ w.toList) (hne : v ≠ w.head) :
   (w.takeUntil v h).dropTail.append (w.dropUntil v h) = w := by
   induction w generalizing v <;> grind
 
-@[simp, grind →] lemma walk_split [DecidableEq α]
+/-- Any walk can be split at a vertex in its support into two sub-walks joined at that
+vertex. -/
+@[simp, scoped grind →] lemma walk_split [DecidableEq α]
   (w : Walk α) (u : α) (hu : u ∈ w.support) :
     w = Walk.append
-      ⟨w.seq.takeUntil u hu, takeUntil_iswalk w.seq u hu w.valid⟩
-      ⟨w.seq.dropUntil u hu, dropUntil_iswalk w.seq u hu w.valid⟩
+      ⟨w.seq.takeUntil u hu, takeUntil_iswalk w.seq u hu w.isWalk⟩
+      ⟨w.seq.dropUntil u hu, dropUntil_iswalk w.seq u hu w.isWalk⟩
       (by grind) := by
   by_cases h : u = w.head
   · ext; grind
@@ -407,25 +538,30 @@ def IsCycle (w : Walk α) : Prop :=
 
 
 /-! ## Re-rooting a cycle -/
+
 /-- Re-root a cycle at any chosen vertex in its support. -/
-@[simp, grind] def rerootCycle [DecidableEq α] (w : Walk α) (hcyc : IsCycle w)
+@[simp, scoped grind] def rerootCycle [DecidableEq α] (w : Walk α) (hcyc : IsCycle w)
     (u : α) (hu : u ∈ w.support) : Walk α :=
   Walk.append
-    ⟨w.seq.dropUntil u hu, dropUntil_iswalk w.seq u hu w.valid⟩
-    ⟨w.seq.takeUntil u hu, takeUntil_iswalk w.seq u hu w.valid⟩
+    ⟨w.seq.dropUntil u hu, dropUntil_iswalk w.seq u hu w.isWalk⟩
+    ⟨w.seq.takeUntil u hu, takeUntil_iswalk w.seq u hu w.isWalk⟩
     (by rcases hcyc with ⟨_, hht, _⟩; grind)
 
-@[simp, grind =] lemma toList_append (p q : VertexSeq α) :
+/-- The vertex list of an appended vertex sequence is the concatenation in reverse order. -/
+@[simp, scoped grind =] lemma toList_append (p q : VertexSeq α) :
     (p.append q).toList = q.toList ++ p.toList := by
   induction q generalizing p <;> grind
 
+/-- Dropping the tail of an appended walk commutes with append when the second walk is
+non-trivial. -/
 lemma append_dropTail_eq_dropTail_append (w1 w2 : Walk α) (h : w1.tail = w2.head)
   (hlen : w2.head ≠ w2.tail) :
   (Walk.append w1 w2 h).dropTail = Walk.append w1 w2.dropTail (by grind) := by
   by_cases h1 : w1.length = 0
   · grind
-  · ext; cases w2; induction valid <;> grind
+  · ext; cases w2; induction isWalk <;> grind
 
+/-- Re-rooting a cycle at any vertex in its support yields a cycle. -/
 lemma isCycle_rerootCycle [DecidableEq α] (w : Walk α) (hcyc : IsCycle w)
   (u : α) (hu : u ∈ w.support) :
   IsCycle (rerootCycle w hcyc u hu):= by
@@ -440,3 +576,62 @@ lemma isCycle_rerootCycle [DecidableEq α] (w : Walk α) (hcyc : IsCycle w)
     · grind [append_dropTail_eq_dropTail_append]
 
 end Walk
+
+/-! ## Walks in a SimpleGraph -/
+
+section WalksInGraphs
+
+variable [DecidableEq α]
+
+namespace VertexSeq
+
+/-- `IsVertexSeqIn G w` asserts that the vertex sequence `w` is a walk in the simple
+graph `G`: the first vertex belongs to `G` and every consecutive pair is an edge of `G`. -/
+@[scoped grind] inductive IsVertexSeqIn (G : SimpleGraph α) : VertexSeq α → Prop
+  | singleton (v : α) (hv : v ∈ V(G)) : IsVertexSeqIn G (.singleton v)
+  | cons (w : VertexSeq α) (u : α)
+      (hw : IsVertexSeqIn G w)
+      (he : s(w.tail, u) ∈ E(G)) :
+      IsVertexSeqIn G (.cons w u)
+
+/-- Abbreviation: `w` is a vertex sequence in `G`. -/
+abbrev vertex_seq_in (w : VertexSeq α) (G : SimpleGraph α) := IsVertexSeqIn G w
+
+/-- The set of edges traversed by the vertex sequence, as a `Finset` of unordered pairs. -/
+abbrev edgeSet (w : VertexSeq α) : Finset (Sym2 α) :=
+  match w with
+  | .singleton _ => ∅
+  | .cons w u => w.edgeSet ∪ {s(w.tail, u)}
+
+/-- A vertex sequence is in `G` if and only if its head is a vertex of `G` and every edge
+it traverses belongs to `G`. -/
+@[simp] lemma is_vertex_seq_in_iff (G : SimpleGraph α) (p : VertexSeq α) :
+  IsVertexSeqIn G p ↔ p.head ∈ V(G) ∧ p.edgeSet ⊆ E(G) := by
+  induction p <;> grind
+
+/-- The edge set of `takeUntil` is a subset of the original edge set. -/
+lemma takeUntil_edgeSet (w : VertexSeq α) (v : α)
+    (h : v ∈ w.toList) :
+    (w.takeUntil v h).edgeSet ⊆ w.edgeSet := by
+  induction w generalizing v
+  · intro a ha; simp [takeUntil] at ha
+  · by_cases h2 : v ∈ w_1.toList
+    · grind
+    · simp [takeUntil, h2]
+
+/-- The edge set of a loop-erased sequence is a subset of the original edge set. -/
+lemma loopErase_edgeSet (w : VertexSeq α) :
+    w.loopErase.edgeSet ⊆ w.edgeSet := by
+  suffices h : ∀ n : ℕ, ∀ w : VertexSeq α,
+      w.length = n → w.loopErase.edgeSet ⊆ w.edgeSet by grind
+  intro n; refine Nat.strong_induction_on n ?_
+  intro n ih w hlen; cases w
+  · intro a ha; simp [loopErase, edgeSet] at ha
+  · by_cases hmem : v ∈ w_1.toList
+    · grind [takeUntil_edgeSet, takeUntil_length_le]
+    · intro a ha
+      have ha' : a = s(w_1.loopErase.tail, v) ∨ a ∈ w_1.loopErase.edgeSet := by
+        simpa [loopErase, hmem] using ha
+      grind [tail_loopErase]
+
+end VertexSeq
diff --git a/Cslib/Foundations/Data/FenwickTree/FenwickTree.lean b/Cslib/Foundations/Data/FenwickTree/FenwickTree.lean
new file mode 100644
index 000000000..54c081732
--- /dev/null
+++ b/Cslib/Foundations/Data/FenwickTree/FenwickTree.lean
@@ -0,0 +1,15 @@
+/-
+Copyright (c) 2026 Basil Rohner. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Basil Rohner
+-/
+
+module
+
+public import Cslib.Init
+
+@[expose] public section
+
+namespace FenwickTree
+
+end FenwickTree

From e7d08db8fb8a71e1d95440b4340b930b1dc205ad Mon Sep 17 00:00:00 2001
From: Basil Rohner <basil.rohner@outlook.de>
Date: Sat, 18 Apr 2026 18:51:07 +0200
Subject: [PATCH 03/10] only graph

---
 Cslib/Algorithms/Lean/Graph/Walk.lean | 637 --------------------------
 1 file changed, 637 deletions(-)
 delete mode 100644 Cslib/Algorithms/Lean/Graph/Walk.lean

diff --git a/Cslib/Algorithms/Lean/Graph/Walk.lean b/Cslib/Algorithms/Lean/Graph/Walk.lean
deleted file mode 100644
index 8c783a5a6..000000000
--- a/Cslib/Algorithms/Lean/Graph/Walk.lean
+++ /dev/null
@@ -1,637 +0,0 @@
-/-
-Copyright (c) 2026 Basil Rohner. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Basil Rohner, Sorrachai Yingchareonthawornchai, Weixuan Yuan
--/
-
-module
-public import Cslib.Init
-public import Cslib.Algorithms.Lean.Graph.Graph
-public import Mathlib.Data.Sym.Sym2
-
-@[expose] public section
-
-set_option tactic.hygienic false
-variable {α : Type*}
-
-/-!
-# Vertex sequences and walks
-
-This file defines vertex sequences (`VertexSeq`) and walks (`Walk`) for simple graphs.
-The definitions are well-defined for both directed and undirected simple graphs.
-
-A `VertexSeq` is a nonempty sequence of vertices, and a `Walk` is a vertex sequence
-satisfying the `IsWalk` predicate, which requires that consecutive vertices are distinct.
-
-## Main definitions
-
-* `VertexSeq`: a nonempty sequence of vertices, defined inductively as either a singleton
-  or a cons extension.
-* `VertexSeq.takeUntil`: truncate a vertex sequence at the first occurrence of a given vertex.
-* `VertexSeq.dropUntil`: drop the prefix up to the last occurrence of a given vertex.
-* `VertexSeq.loopErase`: erase loops from a vertex sequence, producing a sequence with no
-  repeated vertices.
-* `IsWalk`: a predicate asserting that consecutive vertices in a `VertexSeq` are distinct.
-* `Walk`: a bundled vertex sequence together with a proof of `IsWalk`.
-* `Walk.IsPath`: a walk whose support has no duplicate vertices.
-* `Walk.IsCycle`: a walk of length at least 3 whose head equals its tail and whose interior
-  is a path.
-* `Walk.toPath`: loop-erase a walk to obtain a path.
-* `Walk.rerootCycle`: re-root a cycle at any vertex in its support.
-
-## Main statements
-
-* `VertexSeq.loopErase_nodup`: loop erasure produces a duplicate-free vertex list.
-* `Walk.loopErase_iswalk`: loop erasure of any vertex sequence yields a valid walk.
-* `Walk.toPath_isPath`: `Walk.toPath` produces a path.
-* `Walk.isCycle_rerootCycle`: re-rooting a cycle at any vertex in its support yields a cycle.
--/
-
-namespace Cslib.Algorithms.Lean
-
-/-- A nonempty sequence of vertices, used as the underlying data for walks.
-`singleton v` is the trivial sequence containing only `v`, and `cons w v` extends the
-sequence `w` by appending vertex `v` at the end. -/
-@[scoped grind] inductive VertexSeq (α : Type*)
-  | singleton (v : α) : VertexSeq α
-  | cons (w : VertexSeq α) (v : α) : VertexSeq α
-
-namespace VertexSeq
-
-/-! ## Basic accessors -/
-
-/-- The list of vertices in the sequence, in order. -/
-@[scoped grind] def toList : VertexSeq α → List α
-  | .singleton v => [v]
-  | .cons p v => p.toList.cons v
-
-/-- The number of edges in the sequence, i.e., one less than the number of vertices.
-A singleton has length 0. -/
-@[scoped grind] def length : VertexSeq α → ℕ
-  | .singleton _ => 0
-  | .cons w _ => 1 + w.length
-
-/-- The first vertex of the sequence. -/
-@[scoped grind] def head : VertexSeq α → α
-  | .singleton v => v
-  | .cons w _ => head w
-
-/-- The last vertex of the sequence. -/
-@[scoped grind] def tail : VertexSeq α → α
-  | .singleton v => v
-  | .cons _ v => v
-
-/-- The head of a singleton sequence is the vertex itself. -/
-@[simp, scoped grind =] lemma singleton_head_eq (u : α) :
-  (VertexSeq.singleton u).head = u := by simp [head]
-
-/-- The tail of a singleton sequence is the vertex itself. -/
-@[simp, scoped grind =] lemma singleton_tail_eq (u : α) :
-  (VertexSeq.singleton u).tail = u := by simp [tail]
-
-/-- The head of `w.cons u` is the head of `w`. -/
-@[simp, scoped grind =] lemma con_head_eq (w : VertexSeq α) (u : α) :
-    (w.cons u).head = w.head := rfl
-
-/-- The tail of `w.cons u` is `u`. -/
-@[simp, scoped grind =] lemma con_tail_eq (w : VertexSeq α) (u : α) :
-    (w.cons u).tail = u := rfl
-
-/-- The head of a vertex sequence belongs to its vertex list. -/
-@[simp, scoped grind ←] lemma head_mem_toList (w : VertexSeq α) : w.head ∈ w.toList := by
-  induction w <;> grind [VertexSeq.head, VertexSeq.toList]
-
-/-! ## dropHead, dropTail -/
-
-/-- Remove the first vertex from the sequence. A singleton is left unchanged. -/
-@[scoped grind] def dropHead : VertexSeq α → VertexSeq α
-  | .singleton v => .singleton v
-  | .cons (.singleton _) v => .singleton v
-  | .cons w v => .cons (dropHead w) v
-
-/-- Remove the last vertex from the sequence. A singleton is left unchanged. -/
-@[scoped grind] def dropTail : VertexSeq α → VertexSeq α
-  | .singleton v => .singleton v
-  | .cons w _ => w
-
-/-! ## append, reverse, and their laws -/
-
-/-- Concatenate two vertex sequences by appending all vertices of the second sequence
-after the first. -/
-@[scoped grind] def append : VertexSeq α → VertexSeq α → VertexSeq α
-  | w, .singleton v => .cons w v
-  | w, .cons w2 v => .cons (append w w2) v
-
-/-- Reverse the order of vertices in the sequence. -/
-@[scoped grind] def reverse : VertexSeq α → VertexSeq α
-  | .singleton v => .singleton v
-  | .cons w v => append (.singleton v) (reverse w)
-
-/-- The length of the concatenation equals the sum of the lengths plus one. -/
-@[simp, scoped grind =] lemma length_append (p q : VertexSeq α) :
-  (p.append q).length = p.length + q.length + 1 := by
-  fun_induction append p q <;> grind
-
-/-- Reversing a singleton is a no-op. -/
-@[simp, scoped grind =] lemma singleton_reverse_eq (v : α) :
-  (VertexSeq.singleton v).reverse = .singleton v := rfl
-
-/-- The tail of an appended sequence is the tail of the second sequence. -/
-@[simp, scoped grind =] lemma tail_on_tail (p q : VertexSeq α) : (p.append q).tail = q.tail := by
-  fun_induction append <;> simp_all [tail]
-
-/-- The head of an appended sequence is the head of the first sequence. -/
-@[simp, scoped grind =] lemma head_on_head (p q : VertexSeq α) : (p.append q).head = p.head := by
-  fun_induction append <;> simp_all
-
-/-- The tail of a sequence appended with a singleton is the singleton's vertex. -/
-@[simp, scoped grind =] lemma tail_on_tail_singleton (p : VertexSeq α) (x : α) :
-    (p.append (.singleton x)).tail = x := by
-  unfold append
-  unfold tail
-  split <;> aesop
-
-/-- The head of a singleton appended with a sequence is the singleton's vertex. -/
-@[simp, scoped grind =] lemma head_on_head_singleton (p : VertexSeq α) (x : α) :
-  ((VertexSeq.singleton x).append p).head = x := by
-  unfold append
-  unfold head
-  split <;> aesop
-
-/-- Append is associative. -/
-@[simp, scoped grind =] lemma append_assoc (p q r : VertexSeq α) :
-    (p.append q).append r = p.append (q.append r) := by
-  fun_induction append q r <;> simp_all [append]
-
-/-- Reversing a concatenation distributes as `q.reverse.append p.reverse`. -/
-@[simp, scoped grind =] lemma reverse_append (p q : VertexSeq α) :
-    (p.append q).reverse = q.reverse.append p.reverse := by
-  fun_induction append <;> simp_all [reverse]
-
-/-- Reversing a vertex sequence twice yields the original sequence. -/
-@[simp, scoped grind =] lemma reverse_reverse (p : VertexSeq α) : (p.reverse).reverse = p := by
-  fun_induction reverse p <;> aesop
-
-/-- The head of a reversed sequence is the tail of the original. -/
-@[simp, scoped grind =] lemma head_reverse (p : VertexSeq α) : (p.reverse).head = p.tail := by
-  fun_induction reverse p <;> aesop
-
-/-- The tail of a reversed sequence is the head of the original. -/
-@[simp, scoped grind =] lemma tail_reverse (p : VertexSeq α) : (p.reverse).tail = p.head := by
-  fun_induction reverse p <;> aesop
-
-/-- Dropping the tail preserves the head. -/
-@[simp, scoped grind =] lemma dropTail_head (p : VertexSeq α) : p.dropTail.head = p.head := by
-  fun_induction reverse p <;> aesop
-
-/-! ## takeUntil, dropUntil, loopErase -/
-
-/-- Truncate the sequence at the first occurrence of `v`, retaining `v` as the new tail. -/
-@[simp, scoped grind] def takeUntil [DecidableEq α] (w : VertexSeq α) (v : α)
-  (h : v ∈ w.toList) : VertexSeq α :=
-  match w with
-  | .singleton x => .singleton x
-  | .cons w2 x =>
-    if h2 : v ∈ w2.toList then takeUntil w2 v h2
-    else .cons w2 x
-
-/-- Drop the prefix up to the last occurrence of `v`, retaining `v` as the new head. -/
-@[simp, scoped grind] def dropUntil [DecidableEq α] (w : VertexSeq α) (v : α)
-  (h : v ∈ w.toList) : VertexSeq α :=
-  match w with
-  | .singleton x => .singleton x
-  | .cons w2 x =>
-    if h2 : v ∈ w2.toList then .cons (dropUntil w2 v h2) x
-    else .singleton x
-
-/-- `takeUntil` does not increase the length of the sequence. -/
-@[simp] lemma takeUntil_length_le [DecidableEq α] (w : VertexSeq α) (v : α)
-    (h : v ∈ w.toList) : (w.takeUntil v h).length ≤ w.length := by
-  fun_induction takeUntil w v h <;> grind
-
-/-- `dropUntil` does not increase the length of the sequence. -/
-@[simp] lemma dropUntil_length_le [DecidableEq α] (w : VertexSeq α) (v : α)
-    (h : v ∈ w.toList) : (w.dropUntil v h).length ≤ w.length := by
-  fun_induction dropUntil w v h <;> grind
-
-/-- The head of `takeUntil w v h` is the head of `w`. -/
-@[simp, scoped grind =] lemma head_takeUntil [DecidableEq α] (w : VertexSeq α) (v : α)
-    (h : v ∈ w.toList) : (takeUntil w v h).head = w.head := by
-  induction w <;> grind
-
-/-- The tail of `takeUntil w v h` is `v`. -/
-@[simp, scoped grind =] lemma tail_takeUntil [DecidableEq α] (w : VertexSeq α) (v : α)
-    (h : v ∈ w.toList) : (takeUntil w v h).tail = v := by
-  induction w <;> grind
-
-/-- Membership in `takeUntil` implies membership in the original sequence. -/
-@[simp, scoped grind →] lemma mem_takeUntil [DecidableEq α] (w : VertexSeq α)
-  (v x : α) (h : v ∈ w.toList) : x ∈ (takeUntil w v h).toList → x ∈ w.toList := by
-  induction w generalizing v <;> grind
-
-/-- The head of `dropUntil w v h` is `v`. -/
-@[simp, scoped grind =] lemma head_dropUntil [DecidableEq α] (w : VertexSeq α) (v : α)
-    (h : v ∈ w.toList) :
-    (w.dropUntil v h).head = v := by
-  induction w <;> grind
-
-/-- The tail of `dropUntil w v h` is the tail of `w`. -/
-@[simp, scoped grind =] lemma tail_dropUntil [DecidableEq α] (w : VertexSeq α) (v : α)
-    (h : v ∈ w.toList) :
-    (w.dropUntil v h).tail = w.tail := by
-  fun_induction VertexSeq.dropUntil w v h <;> simp [VertexSeq.tail]
-
-/-- Membership in `dropUntil` implies membership in the original sequence. -/
-@[simp, scoped grind →] lemma mem_dropUntil [DecidableEq α] (w : VertexSeq α) (v x : α)
-    (h : v ∈ w.toList) : x ∈ (w.dropUntil v h).toList → x ∈ w.toList := by
-  induction w generalizing v <;> grind
-
-/-- Erase all loops from a vertex sequence by repeatedly truncating at the first repeated
-vertex. The result has no duplicate vertices. -/
-@[scoped grind] def loopErase [DecidableEq α] : VertexSeq α → VertexSeq α
-  | .singleton v => .singleton v
-  | .cons w v =>
-      if h : v ∈ w.toList then
-        loopErase (takeUntil w v h)
-      else
-        .cons (loopErase w) v
-  termination_by p => p.length
-  decreasing_by
-  · simp [length]; grind [takeUntil_length_le]
-  · simp [length]
-
-/-- Every vertex in the loop-erased sequence was present in the original. -/
-lemma mem_loopErase [DecidableEq α] (w : VertexSeq α) :
-    ∀ {x : α}, x ∈ w.loopErase.toList → x ∈ w.toList := by
-  fun_induction loopErase w <;> grind [toList, mem_takeUntil]
-
-/-- The vertex list of a loop-erased sequence has no duplicates. -/
-theorem loopErase_nodup [DecidableEq α] (w : VertexSeq α) : w.loopErase.toList.Nodup := by
-  fun_induction VertexSeq.loopErase w <;> grind [toList, mem_loopErase]
-
-/-- Loop erasure preserves the head of the sequence. -/
-@[simp] lemma head_loopErase [DecidableEq α] (w : VertexSeq α) :
-    w.loopErase.head = w.head := by
-  fun_induction loopErase w <;> simp_all
-
-/-- Loop erasure preserves the tail of the sequence. -/
-@[simp] lemma tail_loopErase [DecidableEq α] (w : VertexSeq α) :
-    w.loopErase.tail = w.tail := by
-  fun_induction loopErase w <;> simp_all
-
-end VertexSeq
-
-/-! ## IsWalk, Walk core data -/
-
-/-- `IsWalk w` asserts that the vertex sequence `w` is a valid walk: every pair of
-consecutive vertices is distinct. -/
-@[scoped grind] inductive IsWalk : VertexSeq α → Prop
-  | singleton (v : α) : IsWalk (.singleton v)
-  | cons (w : VertexSeq α) (u : α)
-      (hw : IsWalk w)
-      (hneq : w.tail ≠ u)
-    : IsWalk (.cons w u)
-
-scoped grind_pattern IsWalk.singleton => IsWalk (.singleton v)
-scoped grind_pattern IsWalk.cons => IsWalk (.cons w u)
-
-/-- A walk in a graph, consisting of a nonempty vertex sequence together with a proof that
-consecutive vertices are distinct. -/
-structure Walk (α : Type*) where
-  /-- The underlying vertex sequence. -/
-  seq : VertexSeq α
-  /-- Proof that the vertex sequence is a valid walk. -/
-  isWalk : IsWalk seq
-
-namespace Walk
-open VertexSeq
-
-/-- Two walks are equal if and only if their underlying vertex sequences are equal. -/
-@[ext] lemma ext {w1 w2 : Walk α} (hseq : w1.seq = w2.seq) : w1 = w2 := by
-  cases w1
-  cases w2
-  cases hseq
-  rfl
-
-/-! ## Basic IsWalk helper lemmas -/
-
-/-- The prefix of a valid walk is itself a valid walk. -/
-@[simp, scoped grind =>] lemma iswalk_prefix (w2 : VertexSeq α) (v : α)
-    (valid : IsWalk (w2.cons v)) : IsWalk w2 := by
-  cases valid
-  grind
-
-/-- In a valid walk `w2.cons v`, the tail of `w2` differs from `v`. -/
-@[simp, scoped grind <=] lemma tail_neq_of_iswalk (w2 : VertexSeq α) (v : α)
-    (valid : IsWalk (w2.cons v)) : w2.tail ≠ v := by
-  cases valid
-  grind
-
-/-- Appending two valid walks whose junction vertices are distinct yields a valid walk. -/
-@[scoped grind ←]
-lemma is_walk_two_seqs_append_of (w1 w2 : VertexSeq α)
-  (h1 : IsWalk w1) (h2 : IsWalk w2) (hneq : w1.tail ≠ w2.head) :
-    IsWalk (w1.append w2) := by
-  fun_induction w1.append w2 <;> grind
-
-/-- Prepending a singleton vertex to a valid walk yields a valid walk, provided the vertex
-is distinct from the walk's head. -/
-@[scoped grind ←]
-theorem prepend_iswalk (p : VertexSeq α) (v : α) (h : IsWalk p) (h2 : p.head ≠ v) :
-  IsWalk ((VertexSeq.singleton v).append p) := by grind
-
-/-- Reversing a valid walk yields a valid walk. -/
-@[scoped grind →, scoped grind ←]
-lemma isWalk_rev_if (w : VertexSeq α) : IsWalk w → IsWalk w.reverse := by
-  intro h
-  induction h <;> grind
-
-/-- Appending two sequences that form a valid walk implies each piece is a valid walk and
-the junction vertices are distinct. -/
-@[scoped grind →]
-theorem is_walk_neq_of_append (p q : VertexSeq α) (h : IsWalk (p.append q))
-  : IsWalk p ∧ IsWalk q ∧ p.tail ≠ q.head := by fun_induction append <;> grind
-
-/-- If the reverse of a vertex sequence is a valid walk, then so is the original. -/
-@[scoped grind →]
-lemma isWalk_rev_imp (w : VertexSeq α) : IsWalk w.reverse → IsWalk w := by
-  fun_induction reverse <;> grind
-
-/-- A vertex sequence is a valid walk if and only if its reverse is. -/
-@[simp, scoped grind =]
-lemma isWalk_rev_iff (w : VertexSeq α) : IsWalk w.reverse ↔ IsWalk w := by grind
-
-/-- A vertex sequence with no duplicate vertices is a valid walk. -/
-lemma nodup_iswalk (w : VertexSeq α) (h : w.toList.Nodup) : IsWalk w := by
-  induction w <;> grind
-
-/-- Truncating a valid walk at a vertex in its list yields a valid walk. -/
-@[scoped grind →]
-lemma takeUntil_iswalk [DecidableEq α] (w : VertexSeq α) (v : α) (h : v ∈ w.toList)
-  (hw : IsWalk w) :
-    IsWalk (w.takeUntil v h) := by
-  induction hw generalizing v <;> grind
-
-/-- The suffix of a valid walk obtained by `dropUntil` is a valid walk. -/
-@[scoped grind →]
-lemma dropUntil_iswalk [DecidableEq α] (w : VertexSeq α) (v : α)
-    (h : v ∈ w.toList) (hw : IsWalk w) :
-    IsWalk (w.dropUntil v h) := by
-  induction hw generalizing v <;> grind
-
-/-- The loop erasure of any vertex sequence is a valid walk. -/
-lemma loopErase_iswalk [DecidableEq α] (w : VertexSeq α) : IsWalk w.loopErase := by
-  grind [nodup_iswalk, loopErase_nodup]
-
-/-! ## support, head, tail, length, dropTail for Walk -/
-
-/-- The list of vertices visited by the walk, in order. -/
-@[simp, scoped grind] def support (w : Walk α) : List α := w.seq.toList
-
-/-- The first vertex of the walk. -/
-abbrev head (w : Walk α) : α := w.seq.head
-
-/-- The last vertex of the walk. -/
-abbrev tail (w : Walk α) : α := w.seq.tail
-
-/-- The number of edges in the walk. -/
-abbrev length (w : Walk α) : ℕ := w.seq.length
-
-/-- The walk obtained by removing the last vertex. -/
-abbrev dropTail (w : Walk α) : Walk α :=
-  { seq := w.seq.dropTail
-    isWalk := by grind [Walk]}
-
-/-- Extend a walk by appending a single vertex, given a proof that it differs from the
-current tail. -/
-def append_single (w : Walk α) (u : α) (h : u ≠ w.tail) : Walk α :=
-  ⟨w.seq.cons u, .cons w.seq u w.isWalk (by aesop)⟩
-
-/-- Dropping the tail of a walk preserves its head. -/
-@[simp, scoped grind =]
-lemma dropTail_head (w : Walk α) : w.dropTail.head = w.head := by
-  cases w; induction isWalk <;> grind
-
-/-- If the tail of `w.dropTail` equals `w.tail`, then `w` has length 0. -/
-@[simp, scoped grind .]
-lemma len_zero_of_drop_tail_eq_tail (w : Walk α) (h : w.dropTail.tail = w.tail) :
-    w.length = 0 := by
-  cases w; induction isWalk <;> grind
-
-/-- A walk of length 0 has equal head and tail. -/
-@[simp, scoped grind ←]
-lemma head_eq_tail_of_length_zero (w : Walk α) (h : w.length = 0)
-  : w.head = w.tail := by
-  cases w; induction isWalk <;> grind
-
-
-/-! ## Walk append, reverse and related lemmas -/
-
-/-- Appending the underlying sequences of two walks yields a valid walk when their junction
-vertices are distinct. -/
-@[scoped grind ←]
-lemma two_seqs_append_of (w1 w2 : Walk α) (hneq : w1.tail ≠ w2.head) :
-    IsWalk (w1.seq.append w2.seq) := by
-  cases w1; cases w2; grind
-
-/-- Concatenate two walks whose tail and head agree. The shared vertex appears only once
-in the result. -/
-@[scoped grind =]
-def append (w1 w2 : Walk α) (h : w1.tail = w2.head) : Walk α :=
-  if h1 : w1.length = 0 then w2
-  else
-    { seq := w1.dropTail.seq.append w2.seq
-      isWalk := by grind [Walk]}
-
-/-- Reverse a walk, swapping its head and tail. -/
-@[scoped grind =]
-def reverse (w : Walk α) : Walk α :=
-  { seq := w.seq.reverse
-    isWalk := by grind [Walk]}
-
-/-- The head of a reversed walk is the tail of the original. -/
-@[simp, scoped grind =] lemma head_reverse (w : Walk α) : (w.reverse).head = w.tail := by grind
-
-/-- The tail of a reversed walk is the head of the original. -/
-@[simp, scoped grind =] lemma tail_reverse (w : Walk α) : (w.reverse).tail = w.head := by grind
-
-/-- The head of an appended walk is the head of the first walk. -/
-@[simp, scoped grind =] lemma head_on_head (w1 w2 : Walk α) (h : w1.tail = w2.head) :
-    (Walk.append w1 w2 h).head = w1.head := by
-  cases w1; induction isWalk <;> grind
-
-/-- The tail of an appended walk is the tail of the second walk. -/
-@[simp, scoped grind =] lemma tail_on_tail (w1 w2 : Walk α) (h : w1.tail = w2.head) :
-    (Walk.append w1 w2 h).tail = w2.tail := by grind
-
-/-- The length of an appended walk is the sum of the lengths of its parts. -/
-@[simp, scoped grind =] lemma length_append (w1 w2 : Walk α) (h : w1.tail = w2.head) :
-    (Walk.append w1 w2 h).length = w1.length + w2.length := by
-  unfold Walk.append
-  by_cases h1 : w1.length = 0
-  · grind
-  · have hdrop : w1.dropTail.length + 1 = w1.length := by
-      cases w1; induction isWalk <;> grind
-    grind
-
-/-! ## Path, cycle -/
-
-/-- A walk is a *path* if its support has no duplicate vertices. -/
-@[scoped grind] def IsPath (w : Walk α) : Prop := w.support.Nodup
-
-/-- Loop-erase a walk to obtain a walk with no repeated vertices. -/
-abbrev toPath [DecidableEq α] (w : Walk α) : Walk α :=
-  { seq := w.seq.loopErase
-    isWalk := loopErase_iswalk w.seq }
-
-/-- The walk produced by `toPath` is a path. -/
-theorem toPath_isPath [DecidableEq α] (w : Walk α) : IsPath (toPath w) := by
-  unfold IsPath toPath support
-  simpa using loopErase_nodup w.seq
-
-/-- Loop erasure preserves the tail of a walk. -/
-lemma tail_toPath [DecidableEq α] (w : Walk α) : (toPath w).tail = w.tail := by
-  grind [tail_loopErase]
-
-/-- Loop erasure preserves the head of a walk. -/
-lemma head_toPath [DecidableEq α] (w : Walk α) : (toPath w).head = w.head := by
-  grind [head_loopErase]
-
-/-- A walk is a *cycle* if it has length at least 3, its head equals its tail, and the walk
-with its tail dropped is a path. -/
-def IsCycle (w : Walk α) : Prop :=
-  3 ≤ w.length ∧ w.head = w.tail ∧ IsPath w.dropTail
-
-
-/-! ## Some more helper lemmas -/
-
-/-- Taking until the head of a sequence yields just the singleton of that head. -/
-@[simp, scoped grind .] lemma takeUntil_head_eq_singleton [DecidableEq α] (w : VertexSeq α)
-  (h : w.head ∈ w.toList) :
-  w.takeUntil w.head h = VertexSeq.singleton w.head := by
-  induction w <;> grind
-
-/-- Dropping until the head of a sequence returns the original sequence. -/
-@[simp, scoped grind .] lemma dropUntil_head_eq_self [DecidableEq α] (w : VertexSeq α)
-  (h : w.head ∈ w.toList) :
-  w.dropUntil w.head h = w := by
-  induction w <;> grind
-
-/-- A vertex sequence can be split at any interior vertex into a prefix (with tail dropped)
-appended to a suffix. -/
-@[simp, scoped grind →] lemma vertex_seq_split [DecidableEq α]
-    (w : VertexSeq α) (v : α) (h : v ∈ w.toList) (hne : v ≠ w.head) :
-  (w.takeUntil v h).dropTail.append (w.dropUntil v h) = w := by
-  induction w generalizing v <;> grind
-
-/-- Any walk can be split at a vertex in its support into two sub-walks joined at that
-vertex. -/
-@[simp, scoped grind →] lemma walk_split [DecidableEq α]
-  (w : Walk α) (u : α) (hu : u ∈ w.support) :
-    w = Walk.append
-      ⟨w.seq.takeUntil u hu, takeUntil_iswalk w.seq u hu w.isWalk⟩
-      ⟨w.seq.dropUntil u hu, dropUntil_iswalk w.seq u hu w.isWalk⟩
-      (by grind) := by
-  by_cases h : u = w.head
-  · ext; grind
-  · ext; grind
-
-
-/-! ## Re-rooting a cycle -/
-
-/-- Re-root a cycle at any chosen vertex in its support. -/
-@[simp, scoped grind] def rerootCycle [DecidableEq α] (w : Walk α) (hcyc : IsCycle w)
-    (u : α) (hu : u ∈ w.support) : Walk α :=
-  Walk.append
-    ⟨w.seq.dropUntil u hu, dropUntil_iswalk w.seq u hu w.isWalk⟩
-    ⟨w.seq.takeUntil u hu, takeUntil_iswalk w.seq u hu w.isWalk⟩
-    (by rcases hcyc with ⟨_, hht, _⟩; grind)
-
-/-- The vertex list of an appended vertex sequence is the concatenation in reverse order. -/
-@[simp, scoped grind =] lemma toList_append (p q : VertexSeq α) :
-    (p.append q).toList = q.toList ++ p.toList := by
-  induction q generalizing p <;> grind
-
-/-- Dropping the tail of an appended walk commutes with append when the second walk is
-non-trivial. -/
-lemma append_dropTail_eq_dropTail_append (w1 w2 : Walk α) (h : w1.tail = w2.head)
-  (hlen : w2.head ≠ w2.tail) :
-  (Walk.append w1 w2 h).dropTail = Walk.append w1 w2.dropTail (by grind) := by
-  by_cases h1 : w1.length = 0
-  · grind
-  · ext; cases w2; induction isWalk <;> grind
-
-/-- Re-rooting a cycle at any vertex in its support yields a cycle. -/
-lemma isCycle_rerootCycle [DecidableEq α] (w : Walk α) (hcyc : IsCycle w)
-  (u : α) (hu : u ∈ w.support) :
-  IsCycle (rerootCycle w hcyc u hu):= by
-  have h2 : w.length = (w.rerootCycle hcyc u hu).length := by grind
-  rcases hcyc with ⟨hlen, hht, hpath⟩
-  refine ⟨?_, ?_, ?_⟩
-  · grind
-  · grind
-  · by_cases h : u = w.head
-    · have hz : w.length ≠ 0 := by omega
-      grind
-    · grind [append_dropTail_eq_dropTail_append]
-
-end Walk
-
-/-! ## Walks in a SimpleGraph -/
-
-section WalksInGraphs
-
-variable [DecidableEq α]
-
-namespace VertexSeq
-
-/-- `IsVertexSeqIn G w` asserts that the vertex sequence `w` is a walk in the simple
-graph `G`: the first vertex belongs to `G` and every consecutive pair is an edge of `G`. -/
-@[scoped grind] inductive IsVertexSeqIn (G : SimpleGraph α) : VertexSeq α → Prop
-  | singleton (v : α) (hv : v ∈ V(G)) : IsVertexSeqIn G (.singleton v)
-  | cons (w : VertexSeq α) (u : α)
-      (hw : IsVertexSeqIn G w)
-      (he : s(w.tail, u) ∈ E(G)) :
-      IsVertexSeqIn G (.cons w u)
-
-/-- Abbreviation: `w` is a vertex sequence in `G`. -/
-abbrev vertex_seq_in (w : VertexSeq α) (G : SimpleGraph α) := IsVertexSeqIn G w
-
-/-- The set of edges traversed by the vertex sequence, as a `Finset` of unordered pairs. -/
-abbrev edgeSet (w : VertexSeq α) : Finset (Sym2 α) :=
-  match w with
-  | .singleton _ => ∅
-  | .cons w u => w.edgeSet ∪ {s(w.tail, u)}
-
-/-- A vertex sequence is in `G` if and only if its head is a vertex of `G` and every edge
-it traverses belongs to `G`. -/
-@[simp] lemma is_vertex_seq_in_iff (G : SimpleGraph α) (p : VertexSeq α) :
-  IsVertexSeqIn G p ↔ p.head ∈ V(G) ∧ p.edgeSet ⊆ E(G) := by
-  induction p <;> grind
-
-/-- The edge set of `takeUntil` is a subset of the original edge set. -/
-lemma takeUntil_edgeSet (w : VertexSeq α) (v : α)
-    (h : v ∈ w.toList) :
-    (w.takeUntil v h).edgeSet ⊆ w.edgeSet := by
-  induction w generalizing v
-  · intro a ha; simp [takeUntil] at ha
-  · by_cases h2 : v ∈ w_1.toList
-    · grind
-    · simp [takeUntil, h2]
-
-/-- The edge set of a loop-erased sequence is a subset of the original edge set. -/
-lemma loopErase_edgeSet (w : VertexSeq α) :
-    w.loopErase.edgeSet ⊆ w.edgeSet := by
-  suffices h : ∀ n : ℕ, ∀ w : VertexSeq α,
-      w.length = n → w.loopErase.edgeSet ⊆ w.edgeSet by grind
-  intro n; refine Nat.strong_induction_on n ?_
-  intro n ih w hlen; cases w
-  · intro a ha; simp [loopErase, edgeSet] at ha
-  · by_cases hmem : v ∈ w_1.toList
-    · grind [takeUntil_edgeSet, takeUntil_length_le]
-    · intro a ha
-      have ha' : a = s(w_1.loopErase.tail, v) ∨ a ∈ w_1.loopErase.edgeSet := by
-        simpa [loopErase, hmem] using ha
-      grind [tail_loopErase]
-
-end VertexSeq

From d12c198870555e399ddfde1656952b4553711622 Mon Sep 17 00:00:00 2001
From: Basil Rohner <basil.rohner@outlook.de>
Date: Sat, 18 Apr 2026 22:29:39 +0200
Subject: [PATCH 04/10] fixed

---
 Cslib.lean | 1 -
 1 file changed, 1 deletion(-)

diff --git a/Cslib.lean b/Cslib.lean
index e30e8a559..4bff61d53 100644
--- a/Cslib.lean
+++ b/Cslib.lean
@@ -1,7 +1,6 @@
 module  -- shake: keep-all
 
 public import Cslib.Algorithms.Lean.Graph.Graph
-public import Cslib.Algorithms.Lean.Graph.Walk
 public import Cslib.Algorithms.Lean.MergeSort.MergeSort
 public import Cslib.Algorithms.Lean.TimeM
 public import Cslib.Computability.Automata.Acceptors.Acceptor

From 892dae83a3c5eb30143fdf2ecbd700990778f05f Mon Sep 17 00:00:00 2001
From: Basil Rohner <basil.rohner@outlook.de>
Date: Sat, 18 Apr 2026 22:34:07 +0200
Subject: [PATCH 05/10] changes

---
 Cslib/Algorithms/Lean/Graph/Graph.lean | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/Cslib/Algorithms/Lean/Graph/Graph.lean b/Cslib/Algorithms/Lean/Graph/Graph.lean
index 89b77ae01..7ad954a46 100644
--- a/Cslib/Algorithms/Lean/Graph/Graph.lean
+++ b/Cslib/Algorithms/Lean/Graph/Graph.lean
@@ -139,10 +139,14 @@ instance : Coe (SimpleGraph α) (Graph α (Sym2 α)) := ⟨SimpleGraph.toGraph
 instance : Coe (SimpleDiGraph α) (DiGraph α (α × α)) := ⟨SimpleDiGraph.toDiGraph⟩
 
 
+/-- Typeclass for graph-like structures that have a vertex set. -/
 class HasVertexSet (G : Type*) (V : outParam Type*) where
+  /-- The vertex set of the graph. -/
   vertexSet : G → V
 
+/-- Typeclass for graph-like structures that have an edge set. -/
 class HasEdgeSet (G : Type*) (E : outParam Type*) where
+  /-- The edge set of the graph. -/
   edgeSet : G → E
 
 @[simp] instance {α ε : Type*} : HasVertexSet (Hypergraph α ε) (Set α) :=
@@ -175,7 +179,9 @@ class HasEdgeSet (G : Type*) (E : outParam Type*) where
 @[simp] instance {α : Type*} : HasEdgeSet (SimpleDiGraph α) (Finset (α × α)) :=
   ⟨SimpleDiGraph.edgeSet⟩
 
+/-- Notation for the vertex set of a graph. -/
 scoped notation "V(" G ")" => HasVertexSet.vertexSet G
+/-- Notation for the edge set of a graph. -/
 scoped notation "E(" G ")" => HasEdgeSet.edgeSet G
 
 end Cslib.Algorithms.Lean

From 48ac00d72d5f62899efb4d5101d07bee8ec4a24c Mon Sep 17 00:00:00 2001
From: Basil Rohner <basil.rohner@outlook.de>
Date: Sat, 18 Apr 2026 22:40:35 +0200
Subject: [PATCH 06/10] removed unfinished code

---
 Cslib.lean                                    |  1 -
 .../Data/FenwickTree/FenwickTree.lean         | 15 -----------
 flake.lock                                    | 27 +++++++++++++++++++
 flake.nix                                     | 22 +++++++++++++++
 4 files changed, 49 insertions(+), 16 deletions(-)
 delete mode 100644 Cslib/Foundations/Data/FenwickTree/FenwickTree.lean
 create mode 100644 flake.lock
 create mode 100644 flake.nix

diff --git a/Cslib.lean b/Cslib.lean
index 4bff61d53..f79085022 100644
--- a/Cslib.lean
+++ b/Cslib.lean
@@ -49,7 +49,6 @@ public import Cslib.Foundations.Control.Monad.Free
 public import Cslib.Foundations.Control.Monad.Free.Effects
 public import Cslib.Foundations.Control.Monad.Free.Fold
 public import Cslib.Foundations.Data.BiTape
-public import Cslib.Foundations.Data.FenwickTree.FenwickTree
 public import Cslib.Foundations.Data.FinFun
 public import Cslib.Foundations.Data.HasFresh
 public import Cslib.Foundations.Data.Nat.Segment
diff --git a/Cslib/Foundations/Data/FenwickTree/FenwickTree.lean b/Cslib/Foundations/Data/FenwickTree/FenwickTree.lean
deleted file mode 100644
index 54c081732..000000000
--- a/Cslib/Foundations/Data/FenwickTree/FenwickTree.lean
+++ /dev/null
@@ -1,15 +0,0 @@
-/-
-Copyright (c) 2026 Basil Rohner. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Basil Rohner
--/
-
-module
-
-public import Cslib.Init
-
-@[expose] public section
-
-namespace FenwickTree
-
-end FenwickTree
diff --git a/flake.lock b/flake.lock
new file mode 100644
index 000000000..682004de6
--- /dev/null
+++ b/flake.lock
@@ -0,0 +1,27 @@
+{
+  "nodes": {
+    "nixpkgs": {
+      "locked": {
+        "lastModified": 1776169885,
+        "narHash": "sha256-l/iNYDZ4bGOAFQY2q8y5OAfBBtrDAaPuRQqWaFHVRXM=",
+        "owner": "NixOS",
+        "repo": "nixpkgs",
+        "rev": "4bd9165a9165d7b5e33ae57f3eecbcb28fb231c9",
+        "type": "github"
+      },
+      "original": {
+        "owner": "NixOS",
+        "ref": "nixos-unstable",
+        "repo": "nixpkgs",
+        "type": "github"
+      }
+    },
+    "root": {
+      "inputs": {
+        "nixpkgs": "nixpkgs"
+      }
+    }
+  },
+  "root": "root",
+  "version": 7
+}
diff --git a/flake.nix b/flake.nix
new file mode 100644
index 000000000..69a62e185
--- /dev/null
+++ b/flake.nix
@@ -0,0 +1,22 @@
+{
+  description = "Claude in a dev shell";
+
+  inputs = {
+    nixpkgs.url = "github:NixOS/nixpkgs/nixos-unstable";
+  };
+
+  outputs = { self, nixpkgs }:
+    let
+      system = "x86_64-linux";
+      pkgs = import nixpkgs {
+        inherit system;
+        config.allowUnfree = true;
+      };
+    in {
+      devShells.${system}.default = pkgs.mkShell {
+        packages = [
+          pkgs.claude-code
+        ];
+      };
+    };
+}

From 48e7aea366ec583c20b2c03aed0279e099a606a0 Mon Sep 17 00:00:00 2001
From: Basil <103287590+BasilRohner@users.noreply.github.com>
Date: Sat, 18 Apr 2026 23:57:49 +0200
Subject: [PATCH 07/10] Delete flake.lock

---
 flake.lock | 27 ---------------------------
 1 file changed, 27 deletions(-)
 delete mode 100644 flake.lock

diff --git a/flake.lock b/flake.lock
deleted file mode 100644
index 682004de6..000000000
--- a/flake.lock
+++ /dev/null
@@ -1,27 +0,0 @@
-{
-  "nodes": {
-    "nixpkgs": {
-      "locked": {
-        "lastModified": 1776169885,
-        "narHash": "sha256-l/iNYDZ4bGOAFQY2q8y5OAfBBtrDAaPuRQqWaFHVRXM=",
-        "owner": "NixOS",
-        "repo": "nixpkgs",
-        "rev": "4bd9165a9165d7b5e33ae57f3eecbcb28fb231c9",
-        "type": "github"
-      },
-      "original": {
-        "owner": "NixOS",
-        "ref": "nixos-unstable",
-        "repo": "nixpkgs",
-        "type": "github"
-      }
-    },
-    "root": {
-      "inputs": {
-        "nixpkgs": "nixpkgs"
-      }
-    }
-  },
-  "root": "root",
-  "version": 7
-}

From 9449cafd057588ef76234717fd150d3f164bac48 Mon Sep 17 00:00:00 2001
From: Basil <103287590+BasilRohner@users.noreply.github.com>
Date: Sat, 18 Apr 2026 23:58:04 +0200
Subject: [PATCH 08/10] Delete flake.nix

---
 flake.nix | 22 ----------------------
 1 file changed, 22 deletions(-)
 delete mode 100644 flake.nix

diff --git a/flake.nix b/flake.nix
deleted file mode 100644
index 69a62e185..000000000
--- a/flake.nix
+++ /dev/null
@@ -1,22 +0,0 @@
-{
-  description = "Claude in a dev shell";
-
-  inputs = {
-    nixpkgs.url = "github:NixOS/nixpkgs/nixos-unstable";
-  };
-
-  outputs = { self, nixpkgs }:
-    let
-      system = "x86_64-linux";
-      pkgs = import nixpkgs {
-        inherit system;
-        config.allowUnfree = true;
-      };
-    in {
-      devShells.${system}.default = pkgs.mkShell {
-        packages = [
-          pkgs.claude-code
-        ];
-      };
-    };
-}

From dafe8b4df8e0d039747d0fba874628174b3786b3 Mon Sep 17 00:00:00 2001
From: Basil Rohner <basil.rohner@outlook.de>
Date: Sun, 19 Apr 2026 11:09:44 +0200
Subject: [PATCH 09/10] removed hypergraphs

---
 Cslib/Algorithms/Lean/Graph/Graph.lean | 26 --------------------------
 1 file changed, 26 deletions(-)

diff --git a/Cslib/Algorithms/Lean/Graph/Graph.lean b/Cslib/Algorithms/Lean/Graph/Graph.lean
index 7ad954a46..0ed64a7dc 100644
--- a/Cslib/Algorithms/Lean/Graph/Graph.lean
+++ b/Cslib/Algorithms/Lean/Graph/Graph.lean
@@ -18,9 +18,6 @@ type `α`. Each structure carries its vertex and edge sets explicitly.
 
 ## Main definitions
 
-* `Hypergraph α ε`: a hypergraph with abstract edge index type `ε`; each edge carries an
-  arbitrary `Set α` of endpoints. Parallel edges and loops are permitted, and the vertex
-  and edge sets may be infinite.
 * `Graph α ε`: a general graph with abstract edge index type `ε`; each edge carries an
   unordered pair of endpoints as a `Sym2 α`. Parallel edges and loops are permitted.
 * `SimpleGraph α`: a finite simple graph, with edges indexed by `Sym2 α` itself, `Finset`
@@ -32,8 +29,6 @@ type `α`. Each structure carries its vertex and edge sets explicitly.
 
 ## Main forgetful maps
 
-* `Graph.toHypergraph`: reinterpret a graph as a hypergraph by viewing each `Sym2 α`
-  endpoint pair as a two-element set.
 * `SimpleGraph.toGraph`: forget the finiteness and looplessness axioms of a simple graph.
 * `SimpleDiGraph.toDiGraph`: forget the finiteness and looplessness axioms of a simple
   directed graph.
@@ -44,19 +39,6 @@ The corresponding `Coe` instances are registered.
 namespace Cslib.Algorithms.Lean
 variable {α ε : Type*}
 
-/-- A hypergraph on vertex type `α` with edges indexed by `ε`. The edge set is abstract;
-endpoints are carried by a separate map. Parallel edges and loops are permitted, and both
-the vertex and edge sets may be infinite. -/
-structure Hypergraph (α ε : Type*) where
-  /-- The set of vertices. -/
-  vertexSet : Set α
-  /-- The set of edges. -/
-  edgeSet : Set ε
-  /-- The endpoint map, assigning to each edge its set of incident vertices. -/
-  endpoints : ε → Set α
-  /-- Every endpoint of an edge is a vertex. -/
-  incidence : ∀ e ∈ edgeSet, ∀ v ∈ endpoints e, v ∈ vertexSet
-
 /-- A general graph on vertex type `α` with edges indexed by `ε`. The edge set is abstract;
 endpoints are carried by a separate map. Parallel edges and loops are permitted, and both
 the vertex and edge sets may be infinite. -/
@@ -132,8 +114,6 @@ def SimpleDiGraph.toDiGraph (G : SimpleDiGraph α) : DiGraph α (α × α) where
   endpoints := id
   incidence e he := by simpa using G.incidence e (by simpa using he)
 
-instance : Coe (Graph α ε) (Hypergraph α ε) := ⟨Graph.toHypergraph⟩
-
 instance : Coe (SimpleGraph α) (Graph α (Sym2 α)) := ⟨SimpleGraph.toGraph⟩
 
 instance : Coe (SimpleDiGraph α) (DiGraph α (α × α)) := ⟨SimpleDiGraph.toDiGraph⟩
@@ -149,9 +129,6 @@ class HasEdgeSet (G : Type*) (E : outParam Type*) where
   /-- The edge set of the graph. -/
   edgeSet : G → E
 
-@[simp] instance {α ε : Type*} : HasVertexSet (Hypergraph α ε) (Set α) :=
-  ⟨Hypergraph.vertexSet⟩
-
 @[simp] instance {α ε : Type*} : HasVertexSet (Graph α ε) (Set α) :=
   ⟨Graph.vertexSet⟩
 
@@ -164,9 +141,6 @@ class HasEdgeSet (G : Type*) (E : outParam Type*) where
 @[simp] instance {α : Type*} : HasVertexSet (SimpleDiGraph α) (Finset α) :=
   ⟨SimpleDiGraph.vertexSet⟩
 
-@[simp] instance {α ε : Type*} : HasEdgeSet (Hypergraph α ε) (Set (Set α)) :=
-  ⟨fun G => G.edgeSet.image G.endpoints⟩
-
 @[simp] instance {α ε : Type*} : HasEdgeSet (Graph α ε) (Set (Sym2 α)) :=
   ⟨fun G => G.edgeSet.image G.endpoints⟩
 

From ba8b1b2de829dfbd3bab08bc1fd229f1f3ba4009 Mon Sep 17 00:00:00 2001
From: Basil Rohner <basil.rohner@outlook.de>
Date: Sun, 19 Apr 2026 11:14:42 +0200
Subject: [PATCH 10/10] fixes

---
 Cslib/Algorithms/Lean/Graph/Graph.lean | 8 --------
 1 file changed, 8 deletions(-)

diff --git a/Cslib/Algorithms/Lean/Graph/Graph.lean b/Cslib/Algorithms/Lean/Graph/Graph.lean
index 0ed64a7dc..8887d3cf6 100644
--- a/Cslib/Algorithms/Lean/Graph/Graph.lean
+++ b/Cslib/Algorithms/Lean/Graph/Graph.lean
@@ -90,14 +90,6 @@ structure SimpleDiGraph (α : Type*) where
   /-- No directed edge is a loop. -/
   loopless : ∀ e ∈ edgeSet, e.1 ≠ e.2
 
-/-- Reinterpret a `Graph` as a `Hypergraph` by replacing each `Sym2 α` endpoint pair by
-the corresponding two-element set. -/
-def Graph.toHypergraph (G : Graph α ε) : Hypergraph α ε where
-  vertexSet := G.vertexSet
-  edgeSet := G.edgeSet
-  endpoints e := {v | v ∈ G.endpoints e}
-  incidence e he v hv := G.incidence e he v hv
-
 /-- Forget the finiteness and looplessness axioms of a `SimpleGraph`, viewing it as a
 `Graph` with edges indexed by `Sym2 α` itself and identity endpoint map. -/
 def SimpleGraph.toGraph (G : SimpleGraph α) : Graph α (Sym2 α) where