From cce51a62435c697dc35338a6576274cc15a68f7d Mon Sep 17 00:00:00 2001
From: crei <crei.github@gmail.com>
Date: Thu, 6 Aug 2026 18:18:18 +0200
Subject: [PATCH 01/10] Results about reachability with repeated visits.

---
 .../Turing/SingleTape/Deterministic.lean      |   2 +-
 Cslib/Foundations/Data/RelatesInSteps.lean    | 126 +++++++++++++++++-
 2 files changed, 120 insertions(+), 8 deletions(-)

diff --git a/Cslib/Computability/Machines/Turing/SingleTape/Deterministic.lean b/Cslib/Computability/Machines/Turing/SingleTape/Deterministic.lean
index 29f379d5a..77ce68176 100644
--- a/Cslib/Computability/Machines/Turing/SingleTape/Deterministic.lean
+++ b/Cslib/Computability/Machines/Turing/SingleTape/Deterministic.lean
@@ -445,7 +445,7 @@ def TimeComputable.comp {f g : List Symbol → List Symbol}
         (hg.timeBound (f a).length) hg_outputsFun
     -- Therefore, the computer reduces a to g (f a) in the sum of those times.
     have h_a_reducesTo_g_f_a := RelatesWithinSteps.trans h_a_reducesTo_f_a h_f_a_reducesTo_g_f_a
-    apply RelatesWithinSteps.of_le h_a_reducesTo_g_f_a
+    refine RelatesWithinSteps.mono ?_ h_a_reducesTo_g_f_a
     refine Nat.add_le_add_left ?_ (hf.timeBound a.length)
     · apply h_mono
       -- Use the lemma about output length being bounded by input length + time
diff --git a/Cslib/Foundations/Data/RelatesInSteps.lean b/Cslib/Foundations/Data/RelatesInSteps.lean
index 052e52c98..33288889a 100644
--- a/Cslib/Foundations/Data/RelatesInSteps.lean
+++ b/Cslib/Foundations/Data/RelatesInSteps.lean
@@ -7,6 +7,7 @@ Authors: Bolton Bailey
 module
 
 public import Cslib.Init
+public import Mathlib.Data.Set.Card
 public import Mathlib.Logic.Relation
 
 /-! # Relations Across Steps
@@ -14,6 +15,13 @@ public import Mathlib.Logic.Relation
 This file defines `Relation.RelatesInSteps` (and `Relation.RelatesWithinSteps`).
 These are inductively defines propositions that communicate whether a relation forms a
 chain of length `n` (or at most `n`) between two elements.
+
+The theorem `RelatesInSteps.exists_isPath` allows to obtain a path along the relation of
+transitively related elements and `IsPath.relatesInSteps` is the converse direction.
+
+Another result is `Relation.reflTransGen_iff_relatesWithinSteps_of_finite`, which states that if
+only `n` elements are reachable from `a`, then any element reachable from `a` is reachable in at
+most `n - 1` steps.
 -/
 
 @[expose] public section
@@ -147,6 +155,81 @@ lemma RelatesInSteps.map {α α' : Type*}
   | tail t' t'' m _ hstep ih =>
     exact .tail (g _) (g t') (g t'') m ih (hg t' t'' hstep)
 
+/-! ## Definition of and results about paths along a relation -/
+
+/--
+`IsPath r f n` means that the first `n` steps of the sequence `f : ℕ → α` form a path along `r`,
+i.e. `r (f i) (f (i + 1))` holds for every `i < n`. The values of `f` beyond index `n` are
+irrelevant.
+-/
+def IsPath (r : α → α → Prop) (f : ℕ → α) (n : ℕ) : Prop := ∀ i < n, r (f i) (f (i + 1))
+
+/-- A path of length `n` is in particular a path of any smaller length. -/
+lemma IsPath.mono {f : ℕ → α} : Antitone (IsPath r f) := by
+  intro m n hle h_path i hi
+  exact h_path i (by omega)
+
+/-- If `a` and `b` are related in `n` steps, then there is a path of length `n` from `a` to `b`. -/
+theorem RelatesInSteps.exists_isPath {a b : α} {n : ℕ} (h : RelatesInSteps r a b n) :
+    ∃ f : ℕ → α, f 0 = a ∧ f n = b ∧ IsPath r f n := by
+  induction h with
+  | refl => exact ⟨fun _ => a, rfl, rfl, by simp [IsPath]⟩
+  | tail t' t'' m _ hstep ih =>
+    obtain ⟨f, hf0, hfm, hfstep⟩ := ih
+    refine ⟨fun i => if i ≤ m then f i else t'', by simpa using hf0, by simp, fun i hi => ?_⟩
+    rcases Nat.lt_or_ge i m with h' | h'
+    · simpa [h'.le, h'] using hfstep i h'
+    · have : i = m := by lia
+      subst this
+      simpa [hfm] using hstep
+
+/-- Any two positions along a path are related in as many steps as their distance. -/
+theorem IsPath.relatesInSteps {f : ℕ → α} {n : ℕ} (hf : IsPath r f n) (p k : ℕ) (hpk : p + k ≤ n) :
+    RelatesInSteps r (f p) (f (p + k)) k := by
+  induction k with
+  | zero => exact .refl _
+  | succ k ih =>
+    refine .tail _ (f (p + k)) _ k (ih (by lia)) ?_
+    have := hf (p + k) (by lia)
+    rwa [← Nat.add_assoc]
+
+/-- A path that visits the same element at two different positions can be shortened by splicing
+out the loop in between. -/
+theorem IsPath.relatesInSteps_of_eq {f : ℕ → α} {n i j : ℕ}
+    (hf : IsPath r f n)
+    (hij : i < j)
+    (hjn : j ≤ n)
+    (heq : f i = f j) :
+    RelatesInSteps r (f 0) (f n) (i + (n - j)) := by
+  have h₁ : RelatesInSteps r (f 0) (f j) i := by grind [hf.relatesInSteps 0 i (by lia)]
+  have h₂ : RelatesInSteps r (f j) (f n) (n - j) := by grind [hf.relatesInSteps j (n - j) (by lia)]
+  exact h₁.trans h₂
+
+/-- Every element visited by a path is reachable from its starting point. -/
+theorem IsPath.reflTransGen {f : ℕ → α} {n : ℕ} (hf : IsPath r f n) {i : ℕ} (hi : i ≤ n) :
+    ReflTransGen r (f 0) (f i) := by
+  have := (hf.relatesInSteps 0 i (by lia)).reflTransGen
+  rwa [Nat.zero_add] at this
+
+/-- A path visiting more positions than there are elements reachable from its starting point must
+visit some element twice. -/
+theorem IsPath.exists_eq_of_ncard_le {f : ℕ → α} {n : ℕ}
+    (hf : IsPath r f n)
+    (hfin : Set.Finite (ReflTransGen r (f 0)))
+    (hn : Set.ncard (ReflTransGen r (f 0)) ≤ n) :
+    ∃ i j, i < j ∧ j ≤ n ∧ f i = f j := by
+  have hmaps : ∀ i ∈ Finset.range (n + 1), f i ∈ hfin.toFinset := fun i hi =>
+    hfin.mem_toFinset.mpr (hf.reflTransGen (by simpa [Nat.lt_succ_iff] using hi))
+  have hcard : hfin.toFinset.card < (Finset.range (n + 1)).card := by
+    grind [Set.ncard_eq_toFinset_card _ hfin]
+  obtain ⟨i, hi, j, hj, hij, hfij⟩ := Finset.exists_ne_map_eq_of_card_lt_of_maps_to hcard hmaps
+  simp only [Finset.mem_range, Nat.lt_succ_iff] at hi hj
+  rcases Nat.lt_or_ge i j with hlt | hge
+  · exact ⟨i, j, hlt, hj, hfij⟩
+  · exact ⟨j, i, by lia, hi, hfij.symm⟩
+
+/-! ## RelatesWithinSteps - only requires an upper bound on the number of steps -/
+
 /--
 `RelatesWithinSteps` is a variant of `RelatesInSteps` that allows for a loose bound.
 It states that `a` relates to `b` in *at most* `n` steps.
@@ -191,17 +274,18 @@ lemma RelatesWithinSteps.trans {a b c : α} {n₁ n₂ : ℕ}
   · lia
   · exact RelatesInSteps.trans hevals₁ hevals₂
 
-lemma RelatesWithinSteps.of_le {a b : α} {n₁ n₂ : ℕ}
-    (h : RelatesWithinSteps r a b n₁) (hn : n₁ ≤ n₂) :
-    RelatesWithinSteps r a b n₂ := by
-  obtain ⟨m, hm, hevals⟩ := h
+/-- If two elements `a` and `b` are related in at most `n₁` steps in the relation `r` and
+`n₁ ≤ n₂`, then they are also related in at most `n₂` steps. -/
+lemma RelatesWithinSteps.mono {a b : α} : Monotone (RelatesWithinSteps r a b ·) := by
+  intro n₁ n₂ hn ⟨m, hm, hevals⟩
   exact ⟨m, Nat.le_trans hm hn, hevals⟩
 
 /-- If `h : α → ℕ` increases by at most 1 on each step of `r`,
 then the value of `h` at the output is at most `h` at the input plus the step bound. -/
-lemma RelatesWithinSteps.apply_le_apply_add {a b : α} {m : ℕ} (hevals : RelatesWithinSteps r a b m)
-    (h : α → ℕ) (h_step : ∀ a b, r a b → h b ≤ h a + 1)
-    :
+lemma RelatesWithinSteps.apply_le_apply_add {a b : α} {m : ℕ}
+    (hevals : RelatesWithinSteps r a b m)
+    (h : α → ℕ)
+    (h_step : ∀ a b, r a b → h b ≤ h a + 1) :
     h b ≤ h a + m := by
   obtain ⟨m, hm, hevals_m⟩ := hevals
   have := RelatesInSteps.apply_le_apply_add hevals_m h h_step
@@ -218,4 +302,32 @@ lemma RelatesWithinSteps.map {α α' : Type*} {r : α → α → Prop} {r' : α'
   obtain ⟨m, hm, hevals⟩ := h
   exact ⟨m, hm, RelatesInSteps.map g hg hevals⟩
 
+/-! ### Reachability under a bound on the number of reachable elements -/
+
+/-- An `r`-chain from `a` to `b` visiting at least as many positions as there are elements
+(transitively) related to `a` must visit some element twice, and can therefore be shortened. -/
+theorem RelatesInSteps.exists_lt_of_ncard_le {b : α} {n : ℕ}
+    (hfin : Set.Finite (ReflTransGen r a))
+    (h : RelatesInSteps r a b n)
+    (hn : Set.ncard (ReflTransGen r a) ≤ n) :
+    ∃ m < n, RelatesInSteps r a b m := by
+  obtain ⟨f, rfl, rfl, hpath⟩ := h.exists_isPath
+  obtain ⟨i, j, hij, hjn, heq⟩ := hpath.exists_eq_of_ncard_le hfin hn
+  exact ⟨i + (n - j), by lia, hpath.relatesInSteps_of_eq hij hjn heq⟩
+
+/-- If only a finite number of elements are (transitively) related to `a`, then any such element
+is related to `a` in at most `k - 1` steps, where `k` is the cardinality of that set. -/
+theorem reflTransGen_iff_relatesWithinSteps_of_finite {b : α}
+    (hfin : Set.Finite (ReflTransGen r a)) :
+    ReflTransGen r a b ↔ RelatesWithinSteps r a b (Set.ncard (ReflTransGen r a) - 1) := by
+  classical
+  simp only [RelatesWithinSteps]
+  constructor
+  · intro h_reach
+    have hex : ∃ n, RelatesInSteps r a b n := ReflTransGen.relatesInSteps h_reach
+    -- A chain of minimal length cannot be shortened, so it is short enough.
+    have hmin : ∀ m < Nat.find hex, ¬ RelatesInSteps r a b m := fun m hm => Nat.find_min hex hm
+    grind [RelatesInSteps.exists_lt_of_ncard_le]
+  · grind [RelatesInSteps.reflTransGen]
+
 end Relation

From c462faa6c5934b1a6455cd6c4d3c2e60ae86648d Mon Sep 17 00:00:00 2001
From: crei <crei.github@gmail.com>
Date: Wed, 12 Aug 2026 17:05:02 +0200
Subject: [PATCH 02/10] Use isChain.

---
 Cslib/Foundations/Data/RelatesInSteps.lean | 236 +++++++++------------
 1 file changed, 99 insertions(+), 137 deletions(-)

diff --git a/Cslib/Foundations/Data/RelatesInSteps.lean b/Cslib/Foundations/Data/RelatesInSteps.lean
index 33288889a..14c58fa58 100644
--- a/Cslib/Foundations/Data/RelatesInSteps.lean
+++ b/Cslib/Foundations/Data/RelatesInSteps.lean
@@ -13,20 +13,19 @@ public import Mathlib.Logic.Relation
 /-! # Relations Across Steps
 
 This file defines `Relation.RelatesInSteps` (and `Relation.RelatesWithinSteps`).
-These are inductively defines propositions that communicate whether a relation forms a
+These are inductively defined propositions that communicate whether a relation forms a
 chain of length `n` (or at most `n`) between two elements.
 
-The theorem `RelatesInSteps.exists_isPath` allows to obtain a path along the relation of
-transitively related elements and `IsPath.relatesInSteps` is the converse direction.
+The theorem `RelatesInSteps.exists_isChain` allows to obtain a chain (`List.IsChain`) along the
+relation of transitively related elements and `RelatesInSteps.of_isChain` is the converse direction.
 
-Another result is `Relation.reflTransGen_iff_relatesWithinSteps_of_finite`, which states that if
-only `n` elements are reachable from `a`, then any element reachable from `a` is reachable in at
-most `n - 1` steps.
+Another result is `Relation.ReflTransGen.relatesInSteps_lt_encard`, which states that any element
+reachable from `a` is reachable in fewer steps than there are elements reachable from `a`.
 -/
 
 @[expose] public section
 
-variable {α : Type*} {r : α → α → Prop} {a b c : α}
+variable {α : Type*} {r : α → α → Prop} {a b c : α} {n m : ℕ}
 
 namespace Relation
 
@@ -45,6 +44,9 @@ theorem RelatesInSteps.reflTransGen (h : RelatesInSteps r a b n) : ReflTransGen
   | refl => rfl
   | tail _ _ _ _ h ih => exact .tail ih h
 
+/-- If `b` is reachable from `a` via `r`, then they relate to each other for some number
+of steps.
+See `ReflTransGen.relatesInSteps_lt_encard` for a bound on the number of steps. -/
 theorem ReflTransGen.relatesInSteps (h : ReflTransGen r a b) : ∃ n, RelatesInSteps r a b n := by
   induction h with
   | refl => exact ⟨0, .refl a⟩
@@ -81,11 +83,8 @@ lemma RelatesInSteps.zero {a b : α} (h : RelatesInSteps r a b 0) : a = b := by
   rfl
 
 @[simp]
-lemma RelatesInSteps.zero_iff {a b : α} : RelatesInSteps r a b 0 ↔ a = b := by
-  constructor
-  · exact RelatesInSteps.zero
-  · intro rfl
-    exact RelatesInSteps.refl a
+lemma RelatesInSteps.zero_iff {a b : α} : RelatesInSteps r a b 0 ↔ a = b :=
+  ⟨RelatesInSteps.zero, fun h => h ▸ .refl a⟩
 
 lemma RelatesInSteps.trans {a b c : α} {n m : ℕ}
     (h₁ : RelatesInSteps r a b n) (h₂ : RelatesInSteps r b c m) :
@@ -102,31 +101,23 @@ lemma RelatesInSteps.succ {n : ℕ} (h : RelatesInSteps r a b (n + 1)) :
   | tail t' _ _ hsteps hstep => exact ⟨t', hsteps, hstep⟩
 
 lemma RelatesInSteps.succ_iff {a b : α} {n : ℕ} :
-    RelatesInSteps r a b (n + 1) ↔ ∃ t', RelatesInSteps r a t' n ∧ r t' b := by
-  constructor
-  · exact RelatesInSteps.succ
-  · rintro ⟨t', h_steps, h_red⟩
-    exact .tail _ t' b n h_steps h_red
+    RelatesInSteps r a b (n + 1) ↔ ∃ t', RelatesInSteps r a t' n ∧ r t' b :=
+  ⟨RelatesInSteps.succ, fun ⟨t', h_steps, h_red⟩ => .tail _ t' b n h_steps h_red⟩
 
-lemma RelatesInSteps.succ' {a b : α} : ∀ {n : ℕ}, RelatesInSteps r a b (n + 1) →
+lemma RelatesInSteps.succ' {a b : α} {n : ℕ} (h : RelatesInSteps r a b (n + 1)) :
     ∃ t', r a t' ∧ RelatesInSteps r t' b n := by
-  intro n h
-  obtain ⟨t', hsteps, hstep⟩ := succ h
-  cases n with
+  induction n generalizing b with
   | zero =>
-    rw [zero_iff] at hsteps
-    subst hsteps
-    exact ⟨b, hstep, .refl _⟩
-  | succ k' =>
-    obtain ⟨t''', h_red''', h_steps'''⟩ := succ' hsteps
-    exact ⟨t''', h_red''', .tail _ _ b k' h_steps''' hstep⟩
+    obtain ⟨t', hsteps, hstep⟩ := succ h
+    exact ⟨b, hsteps.zero ▸ hstep, .refl _⟩
+  | succ k ih =>
+    obtain ⟨t', hsteps, hstep⟩ := succ h
+    obtain ⟨t'', h_red, h_steps⟩ := ih hsteps
+    exact ⟨t'', h_red, .tail _ t' b k h_steps hstep⟩
 
 lemma RelatesInSteps.succ'_iff {a b : α} {n : ℕ} :
-    RelatesInSteps r a b (n + 1) ↔ ∃ t', r a t' ∧ RelatesInSteps r t' b n := by
-  constructor
-  · exact succ'
-  · rintro ⟨t', h_red, h_steps⟩
-    exact h_steps.head a t' b n h_red
+    RelatesInSteps r a b (n + 1) ↔ ∃ t', r a t' ∧ RelatesInSteps r t' b n :=
+  ⟨succ', fun ⟨t', h_red, h_steps⟩ => h_steps.head a t' b n h_red⟩
 
 /--
 If `h : α → ℕ` increases by at most 1 on each step of `r`,
@@ -155,78 +146,49 @@ lemma RelatesInSteps.map {α α' : Type*}
   | tail t' t'' m _ hstep ih =>
     exact .tail (g _) (g t') (g t'') m ih (hg t' t'' hstep)
 
-/-! ## Definition of and results about paths along a relation -/
-
-/--
-`IsPath r f n` means that the first `n` steps of the sequence `f : ℕ → α` form a path along `r`,
-i.e. `r (f i) (f (i + 1))` holds for every `i < n`. The values of `f` beyond index `n` are
-irrelevant.
--/
-def IsPath (r : α → α → Prop) (f : ℕ → α) (n : ℕ) : Prop := ∀ i < n, r (f i) (f (i + 1))
-
-/-- A path of length `n` is in particular a path of any smaller length. -/
-lemma IsPath.mono {f : ℕ → α} : Antitone (IsPath r f) := by
-  intro m n hle h_path i hi
-  exact h_path i (by omega)
+/-! ## Lemmas to translate between RelatesInSteps and the existence of a chain (`List.IsChain`) -/
 
-/-- If `a` and `b` are related in `n` steps, then there is a path of length `n` from `a` to `b`. -/
-theorem RelatesInSteps.exists_isPath {a b : α} {n : ℕ} (h : RelatesInSteps r a b n) :
-    ∃ f : ℕ → α, f 0 = a ∧ f n = b ∧ IsPath r f n := by
+/-- If `a` and `b` are related in `n` steps, then there is an `r`-chain of `n + 1` elements
+starting at `a` and ending at `b`.
+This is similar to `List.exists_isChain_ne_nil_of_relationReflTransGen`, but also provides
+a length guarantee. -/
+lemma RelatesInSteps.exists_isChain {a b : α} {n : ℕ} (h : RelatesInSteps r a b n) :
+    ∃ chain : List α,
+      chain.IsChain r ∧ ∃ h_len : chain.length = n + 1, chain[0] = a ∧ chain[n] = b := by
   induction h with
-  | refl => exact ⟨fun _ => a, rfl, rfl, by simp [IsPath]⟩
+  | refl => use [a]; simp
   | tail t' t'' m _ hstep ih =>
-    obtain ⟨f, hf0, hfm, hfstep⟩ := ih
-    refine ⟨fun i => if i ≤ m then f i else t'', by simpa using hf0, by simp, fun i hi => ?_⟩
-    rcases Nat.lt_or_ge i m with h' | h'
-    · simpa [h'.le, h'] using hfstep i h'
-    · have : i = m := by lia
-      subst this
-      simpa [hfm] using hstep
-
-/-- Any two positions along a path are related in as many steps as their distance. -/
-theorem IsPath.relatesInSteps {f : ℕ → α} {n : ℕ} (hf : IsPath r f n) (p k : ℕ) (hpk : p + k ≤ n) :
-    RelatesInSteps r (f p) (f (p + k)) k := by
+    obtain ⟨l, hchain, _, _, _⟩ := ih
+    use l ++ [t'']
+    constructor
+    · apply hchain.append (by simp) (by grind)
+    · grind
+
+/-- Any two elements along an `r`-chain are related in as many steps as their distance in the
+chain. -/
+lemma RelatesInSteps.of_isChain {chain : List α}
+    (hc : chain.IsChain r)
+    (p k : ℕ)
+    (hpk : p + k < chain.length) :
+    RelatesInSteps r chain[p] chain[p + k] k := by
   induction k with
   | zero => exact .refl _
   | succ k ih =>
-    refine .tail _ (f (p + k)) _ k (ih (by lia)) ?_
-    have := hf (p + k) (by lia)
-    rwa [← Nat.add_assoc]
-
-/-- A path that visits the same element at two different positions can be shortened by splicing
-out the loop in between. -/
-theorem IsPath.relatesInSteps_of_eq {f : ℕ → α} {n i j : ℕ}
-    (hf : IsPath r f n)
+    refine .tail _ (chain[p + k]) _ k (ih (by lia)) ?_
+    apply List.IsChain.getElem hc
+
+/-- A chain that visits the same element at two different positions can be shortened by splicing
+out the loop in between, i.e. the first and last elements are also related to each other
+by fewer steps. -/
+lemma RelatesInSteps.of_isChain_eq {chain : List α} {i j : ℕ}
+    (hc : chain.IsChain r)
     (hij : i < j)
-    (hjn : j ≤ n)
-    (heq : f i = f j) :
-    RelatesInSteps r (f 0) (f n) (i + (n - j)) := by
-  have h₁ : RelatesInSteps r (f 0) (f j) i := by grind [hf.relatesInSteps 0 i (by lia)]
-  have h₂ : RelatesInSteps r (f j) (f n) (n - j) := by grind [hf.relatesInSteps j (n - j) (by lia)]
-  exact h₁.trans h₂
-
-/-- Every element visited by a path is reachable from its starting point. -/
-theorem IsPath.reflTransGen {f : ℕ → α} {n : ℕ} (hf : IsPath r f n) {i : ℕ} (hi : i ≤ n) :
-    ReflTransGen r (f 0) (f i) := by
-  have := (hf.relatesInSteps 0 i (by lia)).reflTransGen
-  rwa [Nat.zero_add] at this
-
-/-- A path visiting more positions than there are elements reachable from its starting point must
-visit some element twice. -/
-theorem IsPath.exists_eq_of_ncard_le {f : ℕ → α} {n : ℕ}
-    (hf : IsPath r f n)
-    (hfin : Set.Finite (ReflTransGen r (f 0)))
-    (hn : Set.ncard (ReflTransGen r (f 0)) ≤ n) :
-    ∃ i j, i < j ∧ j ≤ n ∧ f i = f j := by
-  have hmaps : ∀ i ∈ Finset.range (n + 1), f i ∈ hfin.toFinset := fun i hi =>
-    hfin.mem_toFinset.mpr (hf.reflTransGen (by simpa [Nat.lt_succ_iff] using hi))
-  have hcard : hfin.toFinset.card < (Finset.range (n + 1)).card := by
-    grind [Set.ncard_eq_toFinset_card _ hfin]
-  obtain ⟨i, hi, j, hj, hij, hfij⟩ := Finset.exists_ne_map_eq_of_card_lt_of_maps_to hcard hmaps
-  simp only [Finset.mem_range, Nat.lt_succ_iff] at hi hj
-  rcases Nat.lt_or_ge i j with hlt | hge
-  · exact ⟨i, j, hlt, hj, hfij⟩
-  · exact ⟨j, i, by lia, hi, hfij.symm⟩
+    (hjn : j < chain.length)
+    (heq : chain[i] = chain[j]) :
+    RelatesInSteps r chain[0] chain[chain.length - 1] (i + (chain.length - 1 - j)) := by
+  have h₁ := RelatesInSteps.of_isChain hc 0 i (by omega)
+  have h₂ := RelatesInSteps.of_isChain hc j (chain.length - 1 - j) (by omega)
+  grind [RelatesInSteps.trans]
 
 /-! ## RelatesWithinSteps - only requires an upper bound on the number of steps -/
 
@@ -249,18 +211,12 @@ lemma RelatesWithinSteps.single {a b : α} (h : r a b) : RelatesWithinSteps r a
   RelatesWithinSteps.of_relatesInSteps (RelatesInSteps.single h)
 
 lemma RelatesWithinSteps.zero {a b : α} (h : RelatesWithinSteps r a b 0) : a = b := by
-  obtain ⟨m, hm, hevals⟩ := h
-  have : m = 0 := Nat.le_zero.mp hm
-  subst this
-  exact RelatesInSteps.zero hevals
+  obtain ⟨_, hm, hevals⟩ := h
+  simp_all
 
 @[simp]
-lemma RelatesWithinSteps.zero_iff {a b : α} : RelatesWithinSteps r a b 0 ↔ a = b := by
-  constructor
-  · exact RelatesWithinSteps.zero
-  · intro h
-    subst h
-    exact RelatesWithinSteps.refl a
+lemma RelatesWithinSteps.zero_iff {a b : α} : RelatesWithinSteps r a b 0 ↔ a = b :=
+  ⟨RelatesWithinSteps.zero, fun h => h ▸ .refl a⟩
 
 /-- Transitivity of `RelatesWithinSteps` in the sum of the step bounds. -/
 @[trans]
@@ -269,10 +225,7 @@ lemma RelatesWithinSteps.trans {a b c : α} {n₁ n₂ : ℕ}
     RelatesWithinSteps r a c (n₁ + n₂) := by
   obtain ⟨m₁, hm₁, hevals₁⟩ := h₁
   obtain ⟨m₂, hm₂, hevals₂⟩ := h₂
-  use m₁ + m₂
-  constructor
-  · lia
-  · exact RelatesInSteps.trans hevals₁ hevals₂
+  exact ⟨m₁ + m₂, by lia, hevals₁.trans hevals₂⟩
 
 /-- If two elements `a` and `b` are related in at most `n₁` steps in the relation `r` and
 `n₁ ≤ n₂`, then they are also related in at most `n₂` steps. -/
@@ -287,8 +240,8 @@ lemma RelatesWithinSteps.apply_le_apply_add {a b : α} {m : ℕ}
     (h : α → ℕ)
     (h_step : ∀ a b, r a b → h b ≤ h a + 1) :
     h b ≤ h a + m := by
-  obtain ⟨m, hm, hevals_m⟩ := hevals
-  have := RelatesInSteps.apply_le_apply_add hevals_m h h_step
+  obtain ⟨_, hm, hevals_m⟩ := hevals
+  have := hevals_m.apply_le_apply_add h h_step
   lia
 
 /--
@@ -304,30 +257,39 @@ lemma RelatesWithinSteps.map {α α' : Type*} {r : α → α → Prop} {r' : α'
 
 /-! ### Reachability under a bound on the number of reachable elements -/
 
-/-- An `r`-chain from `a` to `b` visiting at least as many positions as there are elements
-(transitively) related to `a` must visit some element twice, and can therefore be shortened. -/
-theorem RelatesInSteps.exists_lt_of_ncard_le {b : α} {n : ℕ}
-    (hfin : Set.Finite (ReflTransGen r a))
-    (h : RelatesInSteps r a b n)
-    (hn : Set.ncard (ReflTransGen r a) ≤ n) :
-    ∃ m < n, RelatesInSteps r a b m := by
-  obtain ⟨f, rfl, rfl, hpath⟩ := h.exists_isPath
-  obtain ⟨i, j, hij, hjn, heq⟩ := hpath.exists_eq_of_ncard_le hfin hn
-  exact ⟨i + (n - j), by lia, hpath.relatesInSteps_of_eq hij hjn heq⟩
-
-/-- If only a finite number of elements are (transitively) related to `a`, then any such element
-is related to `a` in at most `k - 1` steps, where `k` is the cardinality of that set. -/
-theorem reflTransGen_iff_relatesWithinSteps_of_finite {b : α}
-    (hfin : Set.Finite (ReflTransGen r a)) :
-    ReflTransGen r a b ↔ RelatesWithinSteps r a b (Set.ncard (ReflTransGen r a) - 1) := by
+/-- A more precise version of `ReflTransGen.relatesInSteps`: if `b` is reachable from `a`, then it
+is related to `a` in fewer steps than there are elements reachable from `a`.
+Note that this cardinality is an `ℕ∞`, and if it is infinite, no bound on the number of steps
+is stated. -/
+theorem ReflTransGen.relatesInSteps_lt_encard {b : α} (h : ReflTransGen r a b) :
+    ∃ n, RelatesInSteps r a b n ∧ (n : ℕ∞) < {x | ReflTransGen r a x}.encard := by
   classical
-  simp only [RelatesWithinSteps]
-  constructor
-  · intro h_reach
-    have hex : ∃ n, RelatesInSteps r a b n := ReflTransGen.relatesInSteps h_reach
-    -- A chain of minimal length cannot be shortened, so it is short enough.
-    have hmin : ∀ m < Nat.find hex, ¬ RelatesInSteps r a b m := fun m hm => Nat.find_min hex hm
-    grind [RelatesInSteps.exists_lt_of_ncard_le]
-  · grind [RelatesInSteps.reflTransGen]
+  -- Let us use the shortest chain from `a` to `b`.
+  have hex : ∃ n, RelatesInSteps r a b n := h.relatesInSteps
+  refine ⟨Nat.find hex, Nat.find_spec hex, ?_⟩
+  obtain ⟨chain, hc, hlen, h0, hb⟩ := (Nat.find_spec hex).exists_isChain
+  -- All elements in the chain are reachable from `a`.
+  have hsub : {x | x ∈ chain} ⊆ {x | ReflTransGen r a x} := by
+    simp only [Set.subset_def, Set.mem_ofPred_eq]
+    intro y hy
+    obtain ⟨i, hi, rfl⟩ := List.getElem_of_mem hy
+    simpa [h0] using (RelatesInSteps.of_isChain hc 0 i (by omega)).reflTransGen
+  -- Now assume, for the sake of contradiction, that the minimal chain has at least as many
+  -- elements as there are reachable elements.
+  by_contra hcard
+  push Not at hcard
+  -- Then there is at least one duplicate element.
+  have h_dup : ¬chain.Nodup := by
+    intro h_nodup
+    have hle := (Set.encard_le_encard hsub).trans hcard
+    rw [← List.coe_toFinset, Set.encard_coe_eq_coe_finsetCard] at hle
+    grind [List.toFinset_card_of_nodup, Nat.cast_le]
+  -- But then we can shorten the chain which contradicts the fact that it is minimal.
+  rw [List.nodup_iff_getElem?_ne_getElem?] at h_dup
+  push Not at h_dup
+  obtain ⟨i, j, hij, hjn, heq⟩ := h_dup
+  have heq' : chain[i] = chain[j] := by grind [List.getElem?_eq_getElem]
+  have hshort := RelatesInSteps.of_isChain_eq hc hij hjn heq'
+  exact Nat.find_min hex (m := i + (chain.length - 1 - j)) (by omega) (by grind)
 
 end Relation

From 877f6d5533d9fbd6ddea2553408ec780d3e5b6cc Mon Sep 17 00:00:00 2001
From: crei <crei.github@gmail.com>
Date: Wed, 12 Aug 2026 17:26:47 +0200
Subject: [PATCH 03/10] Extract a lemma and clean up.

---
 Cslib/Foundations/Data/RelatesInSteps.lean | 31 +++++++++++++++-------
 1 file changed, 22 insertions(+), 9 deletions(-)

diff --git a/Cslib/Foundations/Data/RelatesInSteps.lean b/Cslib/Foundations/Data/RelatesInSteps.lean
index 14c58fa58..7e3f2dd25 100644
--- a/Cslib/Foundations/Data/RelatesInSteps.lean
+++ b/Cslib/Foundations/Data/RelatesInSteps.lean
@@ -16,9 +16,12 @@ This file defines `Relation.RelatesInSteps` (and `Relation.RelatesWithinSteps`).
 These are inductively defined propositions that communicate whether a relation forms a
 chain of length `n` (or at most `n`) between two elements.
 
-The theorem `RelatesInSteps.exists_isChain` allows to obtain a chain (`List.IsChain`) along the
+The lemma `RelatesInSteps.exists_isChain` allows to obtain a chain (`List.IsChain`) along the
 relation of transitively related elements and `RelatesInSteps.of_isChain` is the converse direction.
 
+If a chain has duplicates, the lemmas `RelatesInSteps.of_isChain_eq` and `RelatesInSteps.of_dup`
+show that the start and end point are reachable in fewer steps by removing the "loop".
+
 Another result is `Relation.ReflTransGen.relatesInSteps_lt_encard`, which states that any element
 reachable from `a` is reachable in fewer steps than there are elements reachable from `a`.
 -/
@@ -185,11 +188,25 @@ lemma RelatesInSteps.of_isChain_eq {chain : List α} {i j : ℕ}
     (hij : i < j)
     (hjn : j < chain.length)
     (heq : chain[i] = chain[j]) :
-    RelatesInSteps r chain[0] chain[chain.length - 1] (i + (chain.length - 1 - j)) := by
+    RelatesInSteps r (chain.head (by grind)) (chain.getLast (by grind))
+      (i + (chain.length - 1 - j)) := by
+  rw [List.head_eq_getElem, List.getLast_eq_getElem]
   have h₁ := RelatesInSteps.of_isChain hc 0 i (by omega)
   have h₂ := RelatesInSteps.of_isChain hc j (chain.length - 1 - j) (by omega)
   grind [RelatesInSteps.trans]
 
+/-- If a chain has duplicates, there is a shorter version with the same start and end point.
+This is a less explicit version of `RelatesInSteps.of_isChain_eq`. -/
+lemma RelatesInSteps.of_isChain_neg_nodup {chain : List α}
+    (hc : chain.IsChain r)
+    (hne : chain ≠ [])
+    (hdup : ¬ chain.Nodup) :
+    ∃ n < chain.length - 1, RelatesInSteps r (chain.head hne) (chain.getLast hne) n := by
+  rw [List.nodup_iff_getElem?_ne_getElem?] at hdup
+  push Not at hdup
+  obtain ⟨i, j, hij, hjn, heq⟩ := hdup
+  exact ⟨_, by omega, RelatesInSteps.of_isChain_eq hc hij hjn (by grind)⟩
+
 /-! ## RelatesWithinSteps - only requires an upper bound on the number of steps -/
 
 /--
@@ -255,7 +272,7 @@ lemma RelatesWithinSteps.map {α α' : Type*} {r : α → α → Prop} {r' : α'
   obtain ⟨m, hm, hevals⟩ := h
   exact ⟨m, hm, RelatesInSteps.map g hg hevals⟩
 
-/-! ### Reachability under a bound on the number of reachable elements -/
+/-! ## Reachability under a bound on the number of reachable elements -/
 
 /-- A more precise version of `ReflTransGen.relatesInSteps`: if `b` is reachable from `a`, then it
 is related to `a` in fewer steps than there are elements reachable from `a`.
@@ -285,11 +302,7 @@ theorem ReflTransGen.relatesInSteps_lt_encard {b : α} (h : ReflTransGen r a b)
     rw [← List.coe_toFinset, Set.encard_coe_eq_coe_finsetCard] at hle
     grind [List.toFinset_card_of_nodup, Nat.cast_le]
   -- But then we can shorten the chain which contradicts the fact that it is minimal.
-  rw [List.nodup_iff_getElem?_ne_getElem?] at h_dup
-  push Not at h_dup
-  obtain ⟨i, j, hij, hjn, heq⟩ := h_dup
-  have heq' : chain[i] = chain[j] := by grind [List.getElem?_eq_getElem]
-  have hshort := RelatesInSteps.of_isChain_eq hc hij hjn heq'
-  exact Nat.find_min hex (m := i + (chain.length - 1 - j)) (by omega) (by grind)
+  obtain ⟨n, hn, hshort⟩ := RelatesInSteps.of_isChain_neg_nodup hc (by grind) h_dup
+  exact Nat.find_min hex (m := n) (by omega) (by grind)
 
 end Relation

From ba0c2b5be69c206cdf116364fb32c71f3afb08db Mon Sep 17 00:00:00 2001
From: crei <crei.github@gmail.com>
Date: Wed, 12 Aug 2026 17:29:45 +0200
Subject: [PATCH 04/10] Undo some golfing.

---
 Cslib/Foundations/Data/RelatesInSteps.lean | 22 +++++++++++++++-------
 1 file changed, 15 insertions(+), 7 deletions(-)

diff --git a/Cslib/Foundations/Data/RelatesInSteps.lean b/Cslib/Foundations/Data/RelatesInSteps.lean
index 7e3f2dd25..8445bae5a 100644
--- a/Cslib/Foundations/Data/RelatesInSteps.lean
+++ b/Cslib/Foundations/Data/RelatesInSteps.lean
@@ -86,8 +86,11 @@ lemma RelatesInSteps.zero {a b : α} (h : RelatesInSteps r a b 0) : a = b := by
   rfl
 
 @[simp]
-lemma RelatesInSteps.zero_iff {a b : α} : RelatesInSteps r a b 0 ↔ a = b :=
-  ⟨RelatesInSteps.zero, fun h => h ▸ .refl a⟩
+lemma RelatesInSteps.zero_iff {a b : α} : RelatesInSteps r a b 0 ↔ a = b := by
+  constructor
+  · exact RelatesInSteps.zero
+  · intro rfl
+    exact RelatesInSteps.refl a
 
 lemma RelatesInSteps.trans {a b c : α} {n m : ℕ}
     (h₁ : RelatesInSteps r a b n) (h₂ : RelatesInSteps r b c m) :
@@ -104,8 +107,11 @@ lemma RelatesInSteps.succ {n : ℕ} (h : RelatesInSteps r a b (n + 1)) :
   | tail t' _ _ hsteps hstep => exact ⟨t', hsteps, hstep⟩
 
 lemma RelatesInSteps.succ_iff {a b : α} {n : ℕ} :
-    RelatesInSteps r a b (n + 1) ↔ ∃ t', RelatesInSteps r a t' n ∧ r t' b :=
-  ⟨RelatesInSteps.succ, fun ⟨t', h_steps, h_red⟩ => .tail _ t' b n h_steps h_red⟩
+    RelatesInSteps r a b (n + 1) ↔ ∃ t', RelatesInSteps r a t' n ∧ r t' b := by
+  constructor
+  · exact RelatesInSteps.succ
+  · rintro ⟨t', h_steps, h_red⟩
+    exact .tail _ t' b n h_steps h_red
 
 lemma RelatesInSteps.succ' {a b : α} {n : ℕ} (h : RelatesInSteps r a b (n + 1)) :
     ∃ t', r a t' ∧ RelatesInSteps r t' b n := by
@@ -119,9 +125,11 @@ lemma RelatesInSteps.succ' {a b : α} {n : ℕ} (h : RelatesInSteps r a b (n + 1
     exact ⟨t'', h_red, .tail _ t' b k h_steps hstep⟩
 
 lemma RelatesInSteps.succ'_iff {a b : α} {n : ℕ} :
-    RelatesInSteps r a b (n + 1) ↔ ∃ t', r a t' ∧ RelatesInSteps r t' b n :=
-  ⟨succ', fun ⟨t', h_red, h_steps⟩ => h_steps.head a t' b n h_red⟩
-
+    RelatesInSteps r a b (n + 1) ↔ ∃ t', r a t' ∧ RelatesInSteps r t' b n := by
+  constructor
+  · exact succ'
+  · rintro ⟨t', h_red, h_steps⟩
+    exact h_steps.head a t' b n h_red
 /--
 If `h : α → ℕ` increases by at most 1 on each step of `r`,
 then the value of `h` at the output is at most `h` at the input plus the number of steps.

From cd5c63f5a1eca67d5934fe267b2d88f5371cca9a Mon Sep 17 00:00:00 2001
From: crei <crei.github@gmail.com>
Date: Wed, 12 Aug 2026 17:32:43 +0200
Subject: [PATCH 05/10] Undo some more golfing.

---
 Cslib/Foundations/Data/RelatesInSteps.lean | 28 +++++++++++++---------
 1 file changed, 17 insertions(+), 11 deletions(-)

diff --git a/Cslib/Foundations/Data/RelatesInSteps.lean b/Cslib/Foundations/Data/RelatesInSteps.lean
index 8445bae5a..f4020165a 100644
--- a/Cslib/Foundations/Data/RelatesInSteps.lean
+++ b/Cslib/Foundations/Data/RelatesInSteps.lean
@@ -115,14 +115,15 @@ lemma RelatesInSteps.succ_iff {a b : α} {n : ℕ} :
 
 lemma RelatesInSteps.succ' {a b : α} {n : ℕ} (h : RelatesInSteps r a b (n + 1)) :
     ∃ t', r a t' ∧ RelatesInSteps r t' b n := by
-  induction n generalizing b with
+  obtain ⟨t', hsteps, hstep⟩ := succ h
+  cases n with
   | zero =>
-    obtain ⟨t', hsteps, hstep⟩ := succ h
-    exact ⟨b, hsteps.zero ▸ hstep, .refl _⟩
-  | succ k ih =>
-    obtain ⟨t', hsteps, hstep⟩ := succ h
-    obtain ⟨t'', h_red, h_steps⟩ := ih hsteps
-    exact ⟨t'', h_red, .tail _ t' b k h_steps hstep⟩
+    rw [zero_iff] at hsteps
+    subst hsteps
+    exact ⟨b, hstep, .refl _⟩
+  | succ k' =>
+    obtain ⟨t''', h_red''', h_steps'''⟩ := succ' hsteps
+    exact ⟨t''', h_red''', .tail _ _ b k' h_steps''' hstep⟩
 
 lemma RelatesInSteps.succ'_iff {a b : α} {n : ℕ} :
     RelatesInSteps r a b (n + 1) ↔ ∃ t', r a t' ∧ RelatesInSteps r t' b n := by
@@ -130,6 +131,7 @@ lemma RelatesInSteps.succ'_iff {a b : α} {n : ℕ} :
   · exact succ'
   · rintro ⟨t', h_red, h_steps⟩
     exact h_steps.head a t' b n h_red
+
 /--
 If `h : α → ℕ` increases by at most 1 on each step of `r`,
 then the value of `h` at the output is at most `h` at the input plus the number of steps.
@@ -240,8 +242,12 @@ lemma RelatesWithinSteps.zero {a b : α} (h : RelatesWithinSteps r a b 0) : a =
   simp_all
 
 @[simp]
-lemma RelatesWithinSteps.zero_iff {a b : α} : RelatesWithinSteps r a b 0 ↔ a = b :=
-  ⟨RelatesWithinSteps.zero, fun h => h ▸ .refl a⟩
+lemma RelatesWithinSteps.zero_iff {a b : α} : RelatesWithinSteps r a b 0 ↔ a = b := by
+  constructor
+  · exact RelatesWithinSteps.zero
+  · intro h
+    subst h
+    exact RelatesWithinSteps.refl a
 
 /-- Transitivity of `RelatesWithinSteps` in the sum of the step bounds. -/
 @[trans]
@@ -265,8 +271,8 @@ lemma RelatesWithinSteps.apply_le_apply_add {a b : α} {m : ℕ}
     (h : α → ℕ)
     (h_step : ∀ a b, r a b → h b ≤ h a + 1) :
     h b ≤ h a + m := by
-  obtain ⟨_, hm, hevals_m⟩ := hevals
-  have := hevals_m.apply_le_apply_add h h_step
+  obtain ⟨m, hm, hevals_m⟩ := hevals
+  have := RelatesInSteps.apply_le_apply_add hevals_m h h_step
   lia
 
 /--

From c4c92c1ae8f91cf7915b5fa8d954823708171561 Mon Sep 17 00:00:00 2001
From: crei <crei.github@gmail.com>
Date: Mon, 17 Aug 2026 15:28:22 +0200
Subject: [PATCH 06/10] Extract results related to List.isChain into their own
 file.

---
 Cslib.lean                                 |  1 +
 Cslib/Foundations/Data/List.lean           | 65 ++++++++++++++++++++++
 Cslib/Foundations/Data/RelatesInSteps.lean | 63 +++++++++------------
 3 files changed, 91 insertions(+), 38 deletions(-)
 create mode 100644 Cslib/Foundations/Data/List.lean

diff --git a/Cslib.lean b/Cslib.lean
index a4da6b124..648f8453a 100644
--- a/Cslib.lean
+++ b/Cslib.lean
@@ -71,6 +71,7 @@ public import Cslib.Foundations.Data.DecidableEqZero
 public import Cslib.Foundations.Data.FinFun.Basic
 public import Cslib.Foundations.Data.FinFun.Update
 public import Cslib.Foundations.Data.HasFresh
+public import Cslib.Foundations.Data.List
 public import Cslib.Foundations.Data.Nat.Segment
 public import Cslib.Foundations.Data.OmegaSequence.Defs
 public import Cslib.Foundations.Data.OmegaSequence.Flatten
diff --git a/Cslib/Foundations/Data/List.lean b/Cslib/Foundations/Data/List.lean
new file mode 100644
index 000000000..b725f1d18
--- /dev/null
+++ b/Cslib/Foundations/Data/List.lean
@@ -0,0 +1,65 @@
+/-
+Copyright (c) 2026 Christian Reitwiessner. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Christian Reitwiessner
+-/
+
+module
+
+public import Cslib.Init
+public import Mathlib.Data.List.Chain
+public import Mathlib.Data.List.Nodup
+
+/-! # Results related to List.IsChain
+
+This file defines `List.IsChainFromTo`, a variant of `List.IsChain` that also fixes the first and
+last element of the chain.
+
+The lemma `List.IsChainFromTo.exists_length_lt_of_not_nodup` shows that a chain with duplicates can
+always be shortened.
+-/
+
+@[expose] public section
+
+variable {α : Type*} {r : α → α → Prop} {a b : α}
+
+/-- A "chain from to" is a list of elements where adjacent elements relate to each other
+(cf. `List.IsChain`) and start and end with specific elements. -/
+structure List.IsChainFromTo {α : Type*} (r : α → α → Prop) (chain : List α) (a b : α) : Prop where
+  isChain : chain.IsChain r
+  ne_nil : chain ≠ []
+  head_eq : chain.head ne_nil = a
+  getLast_eq : chain.getLast ne_nil = b
+
+@[simp, grind →]
+lemma List.IsChainFromTo_head_eq {chain : List α} (hc : chain.IsChainFromTo r a b) :
+    chain.head hc.ne_nil = a :=
+  hc.head_eq
+
+@[simp, grind →]
+lemma List.IsChainFromTo_getLast_eq {chain : List α} (hc : chain.IsChainFromTo r a b) :
+    chain.getLast hc.ne_nil = b :=
+  hc.getLast_eq
+
+@[simp, grind ←]
+lemma List.IsChainFromTo_singleton {a : α} : List.IsChainFromTo r [a] a a :=
+  ⟨List.IsChain.singleton a, by simp, rfl, rfl⟩
+
+/-- If there is an `r`-chain from `a` to `b` with duplicates, then there is a shorter `r`-chain
+from `a` to `b` (the one that skips the part between the duplicates).
+Note that applying this method iteratively does not necessarily lead to the shortest `r`-chain
+from `a` to `b`, since we always keep the initial and final segment. -/
+lemma List.IsChainFromTo.exists_length_lt_of_not_nodup {chain : List α}
+    (hc : chain.IsChainFromTo r a b)
+    (h_dup : ¬ chain.Nodup) :
+    ∃ chain' : List α, chain'.IsChainFromTo r a b ∧ chain'.length < chain.length := by
+  rw [nodup_iff_getElem?_ne_getElem?] at h_dup
+  push Not at h_dup
+  obtain ⟨i, j, h_ij, h_lt, h_eq⟩ := h_dup
+  use chain.take i ++ chain.drop j
+  refine ⟨⟨?_, by simp; omega, by grind, by grind⟩, by grind⟩
+  · refine (hc.isChain.take _).append (hc.isChain.drop _) ?_
+    intro x hx y hy
+    rw [List.head?_drop] at hy
+    have := hc.isChain.getElem (i := i - 1) (by omega)
+    grind
diff --git a/Cslib/Foundations/Data/RelatesInSteps.lean b/Cslib/Foundations/Data/RelatesInSteps.lean
index f4020165a..6ae91b73b 100644
--- a/Cslib/Foundations/Data/RelatesInSteps.lean
+++ b/Cslib/Foundations/Data/RelatesInSteps.lean
@@ -7,6 +7,7 @@ Authors: Bolton Bailey
 module
 
 public import Cslib.Init
+public import Cslib.Foundations.Data.List
 public import Mathlib.Data.Set.Card
 public import Mathlib.Logic.Relation
 
@@ -161,20 +162,19 @@ lemma RelatesInSteps.map {α α' : Type*}
 
 /-! ## Lemmas to translate between RelatesInSteps and the existence of a chain (`List.IsChain`) -/
 
-/-- If `a` and `b` are related in `n` steps, then there is an `r`-chain of `n + 1` elements
+/-- If `b` is related to `a` via `r` in `n` steps, then there is an `r`-chain of `n + 1` elements
 starting at `a` and ending at `b`.
 This is similar to `List.exists_isChain_ne_nil_of_relationReflTransGen`, but also provides
 a length guarantee. -/
-lemma RelatesInSteps.exists_isChain {a b : α} {n : ℕ} (h : RelatesInSteps r a b n) :
-    ∃ chain : List α,
-      chain.IsChain r ∧ ∃ h_len : chain.length = n + 1, chain[0] = a ∧ chain[n] = b := by
+lemma RelatesInSteps.exists_isChainFromTo {a b : α} {n : ℕ} (h : RelatesInSteps r a b n) :
+    ∃ chain : List α, chain.IsChainFromTo r a b ∧ chain.length = n + 1 := by
   induction h with
-  | refl => use [a]; simp
+  | refl => exact ⟨[a], by simp, rfl⟩
   | tail t' t'' m _ hstep ih =>
-    obtain ⟨l, hchain, _, _, _⟩ := ih
+    obtain ⟨l, hchain, hlen⟩ := ih
     use l ++ [t'']
-    constructor
-    · apply hchain.append (by simp) (by grind)
+    refine ⟨⟨?_, by simp, ?_, by simp⟩, by grind⟩
+    · exact hchain.isChain.append (by simp) (by grind)
     · grind
 
 /-- Any two elements along an `r`-chain are related in as many steps as their distance in the
@@ -190,32 +190,17 @@ lemma RelatesInSteps.of_isChain {chain : List α}
     refine .tail _ (chain[p + k]) _ k (ih (by lia)) ?_
     apply List.IsChain.getElem hc
 
-/-- A chain that visits the same element at two different positions can be shortened by splicing
-out the loop in between, i.e. the first and last elements are also related to each other
-by fewer steps. -/
-lemma RelatesInSteps.of_isChain_eq {chain : List α} {i j : ℕ}
-    (hc : chain.IsChain r)
-    (hij : i < j)
-    (hjn : j < chain.length)
-    (heq : chain[i] = chain[j]) :
-    RelatesInSteps r (chain.head (by grind)) (chain.getLast (by grind))
-      (i + (chain.length - 1 - j)) := by
-  rw [List.head_eq_getElem, List.getLast_eq_getElem]
-  have h₁ := RelatesInSteps.of_isChain hc 0 i (by omega)
-  have h₂ := RelatesInSteps.of_isChain hc j (chain.length - 1 - j) (by omega)
-  grind [RelatesInSteps.trans]
-
-/-- If a chain has duplicates, there is a shorter version with the same start and end point.
-This is a less explicit version of `RelatesInSteps.of_isChain_eq`. -/
-lemma RelatesInSteps.of_isChain_neg_nodup {chain : List α}
-    (hc : chain.IsChain r)
-    (hne : chain ≠ [])
-    (hdup : ¬ chain.Nodup) :
-    ∃ n < chain.length - 1, RelatesInSteps r (chain.head hne) (chain.getLast hne) n := by
-  rw [List.nodup_iff_getElem?_ne_getElem?] at hdup
-  push Not at hdup
-  obtain ⟨i, j, hij, hjn, heq⟩ := hdup
-  exact ⟨_, by omega, RelatesInSteps.of_isChain_eq hc hij hjn (by grind)⟩
+
+/-- If there is an `r`-chain from `a` to `b`, then `a` and `b` are related to each other with
+a number of steps equal to the length of the chain minus one. -/
+lemma RelatesInSteps.of_isChainFromTo {chain : List α} (hc : chain.IsChainFromTo r a b) :
+    RelatesInSteps r a b (chain.length - 1) := by
+  have h_ne : chain.length > 0 := by grind
+  have hrel := RelatesInSteps.of_isChain hc.isChain 0 (chain.length - 1) (by omega)
+  have h0 : chain[0] = a := by grind
+  have hl : chain[chain.length - 1] = b := by grind
+  simpa [h0, hl] using hrel
+
 
 /-! ## RelatesWithinSteps - only requires an upper bound on the number of steps -/
 
@@ -298,13 +283,14 @@ theorem ReflTransGen.relatesInSteps_lt_encard {b : α} (h : ReflTransGen r a b)
   -- Let us use the shortest chain from `a` to `b`.
   have hex : ∃ n, RelatesInSteps r a b n := h.relatesInSteps
   refine ⟨Nat.find hex, Nat.find_spec hex, ?_⟩
-  obtain ⟨chain, hc, hlen, h0, hb⟩ := (Nat.find_spec hex).exists_isChain
+  obtain ⟨chain, hc, hlen⟩ := (Nat.find_spec hex).exists_isChainFromTo
   -- All elements in the chain are reachable from `a`.
   have hsub : {x | x ∈ chain} ⊆ {x | ReflTransGen r a x} := by
     simp only [Set.subset_def, Set.mem_ofPred_eq]
     intro y hy
     obtain ⟨i, hi, rfl⟩ := List.getElem_of_mem hy
-    simpa [h0] using (RelatesInSteps.of_isChain hc 0 i (by omega)).reflTransGen
+    have := RelatesInSteps.of_isChain hc.isChain 0 i (by omega)
+    grind [RelatesInSteps.reflTransGen]
   -- Now assume, for the sake of contradiction, that the minimal chain has at least as many
   -- elements as there are reachable elements.
   by_contra hcard
@@ -316,7 +302,8 @@ theorem ReflTransGen.relatesInSteps_lt_encard {b : α} (h : ReflTransGen r a b)
     rw [← List.coe_toFinset, Set.encard_coe_eq_coe_finsetCard] at hle
     grind [List.toFinset_card_of_nodup, Nat.cast_le]
   -- But then we can shorten the chain which contradicts the fact that it is minimal.
-  obtain ⟨n, hn, hshort⟩ := RelatesInSteps.of_isChain_neg_nodup hc (by grind) h_dup
-  exact Nat.find_min hex (m := n) (by omega) (by grind)
+  obtain ⟨chain', hc', hlt⟩ := hc.exists_length_lt_of_not_nodup h_dup
+  have := List.length_pos_iff.mpr hc'.ne_nil
+  exact Nat.find_min hex (m := chain'.length - 1) (by omega) (RelatesInSteps.of_isChainFromTo hc')
 
 end Relation

From af70d3bdc90e12bf14fc8bc5f6151e4dd49159e9 Mon Sep 17 00:00:00 2001
From: crei <crei.github@gmail.com>
Date: Mon, 17 Aug 2026 15:40:48 +0200
Subject: [PATCH 07/10] Minor tweaks.

---
 Cslib/Foundations/Data/List.lean           | 14 ++++++++------
 Cslib/Foundations/Data/RelatesInSteps.lean | 10 +++-------
 2 files changed, 11 insertions(+), 13 deletions(-)

diff --git a/Cslib/Foundations/Data/List.lean b/Cslib/Foundations/Data/List.lean
index b725f1d18..559d97141 100644
--- a/Cslib/Foundations/Data/List.lean
+++ b/Cslib/Foundations/Data/List.lean
@@ -10,7 +10,7 @@ public import Cslib.Init
 public import Mathlib.Data.List.Chain
 public import Mathlib.Data.List.Nodup
 
-/-! # Results related to List.IsChain
+/-! # Chains with a designated start and end
 
 This file defines `List.IsChainFromTo`, a variant of `List.IsChain` that also fixes the first and
 last element of the chain.
@@ -21,7 +21,7 @@ always be shortened.
 
 @[expose] public section
 
-variable {α : Type*} {r : α → α → Prop} {a b : α}
+variable {α : Type*} {r : α → α → Prop} {chain : List α} {a b : α}
 
 /-- A "chain from to" is a list of elements where adjacent elements relate to each other
 (cf. `List.IsChain`) and start and end with specific elements. -/
@@ -31,25 +31,27 @@ structure List.IsChainFromTo {α : Type*} (r : α → α → Prop) (chain : List
   head_eq : chain.head ne_nil = a
   getLast_eq : chain.getLast ne_nil = b
 
+/-- Restatement of `head_eq`, but tagged with simp and grind. -/
 @[simp, grind →]
-lemma List.IsChainFromTo_head_eq {chain : List α} (hc : chain.IsChainFromTo r a b) :
+lemma List.IsChainFromTo_head_eq (hc : chain.IsChainFromTo r a b) :
     chain.head hc.ne_nil = a :=
   hc.head_eq
 
+/-- Restatement of `getLast_eq`, but tagged with simp and grind. -/
 @[simp, grind →]
-lemma List.IsChainFromTo_getLast_eq {chain : List α} (hc : chain.IsChainFromTo r a b) :
+lemma List.IsChainFromTo_getLast_eq (hc : chain.IsChainFromTo r a b) :
     chain.getLast hc.ne_nil = b :=
   hc.getLast_eq
 
 @[simp, grind ←]
-lemma List.IsChainFromTo_singleton {a : α} : List.IsChainFromTo r [a] a a :=
+lemma List.IsChainFromTo.singleton {a : α} : List.IsChainFromTo r [a] a a :=
   ⟨List.IsChain.singleton a, by simp, rfl, rfl⟩
 
 /-- If there is an `r`-chain from `a` to `b` with duplicates, then there is a shorter `r`-chain
 from `a` to `b` (the one that skips the part between the duplicates).
 Note that applying this method iteratively does not necessarily lead to the shortest `r`-chain
 from `a` to `b`, since we always keep the initial and final segment. -/
-lemma List.IsChainFromTo.exists_length_lt_of_not_nodup {chain : List α}
+lemma List.IsChainFromTo.exists_length_lt_of_not_nodup
     (hc : chain.IsChainFromTo r a b)
     (h_dup : ¬ chain.Nodup) :
     ∃ chain' : List α, chain'.IsChainFromTo r a b ∧ chain'.length < chain.length := by
diff --git a/Cslib/Foundations/Data/RelatesInSteps.lean b/Cslib/Foundations/Data/RelatesInSteps.lean
index 6ae91b73b..7c0bc1c01 100644
--- a/Cslib/Foundations/Data/RelatesInSteps.lean
+++ b/Cslib/Foundations/Data/RelatesInSteps.lean
@@ -17,11 +17,9 @@ This file defines `Relation.RelatesInSteps` (and `Relation.RelatesWithinSteps`).
 These are inductively defined propositions that communicate whether a relation forms a
 chain of length `n` (or at most `n`) between two elements.
 
-The lemma `RelatesInSteps.exists_isChain` allows to obtain a chain (`List.IsChain`) along the
-relation of transitively related elements and `RelatesInSteps.of_isChain` is the converse direction.
-
-If a chain has duplicates, the lemmas `RelatesInSteps.of_isChain_eq` and `RelatesInSteps.of_dup`
-show that the start and end point are reachable in fewer steps by removing the "loop".
+The lemma `RelatesInSteps.exists_isChainFromTo` allows to obtain a chain
+(`List.IsChainFromTo`) of related elements that witness the reachability, and
+`RelatesInSteps.of_isChainFromTo` is the converse direction.
 
 Another result is `Relation.ReflTransGen.relatesInSteps_lt_encard`, which states that any element
 reachable from `a` is reachable in fewer steps than there are elements reachable from `a`.
@@ -190,7 +188,6 @@ lemma RelatesInSteps.of_isChain {chain : List α}
     refine .tail _ (chain[p + k]) _ k (ih (by lia)) ?_
     apply List.IsChain.getElem hc
 
-
 /-- If there is an `r`-chain from `a` to `b`, then `a` and `b` are related to each other with
 a number of steps equal to the length of the chain minus one. -/
 lemma RelatesInSteps.of_isChainFromTo {chain : List α} (hc : chain.IsChainFromTo r a b) :
@@ -201,7 +198,6 @@ lemma RelatesInSteps.of_isChainFromTo {chain : List α} (hc : chain.IsChainFromT
   have hl : chain[chain.length - 1] = b := by grind
   simpa [h0, hl] using hrel
 
-
 /-! ## RelatesWithinSteps - only requires an upper bound on the number of steps -/
 
 /--

From f03aca6139fb3a94e2e9b358a9ea6d487ef018a5 Mon Sep 17 00:00:00 2001
From: crei <crei.github@gmail.com>
Date: Mon, 17 Aug 2026 18:25:33 +0200
Subject: [PATCH 08/10] Remove simp.

---
 Cslib/Foundations/Data/List.lean | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/Cslib/Foundations/Data/List.lean b/Cslib/Foundations/Data/List.lean
index 559d97141..b2e247d94 100644
--- a/Cslib/Foundations/Data/List.lean
+++ b/Cslib/Foundations/Data/List.lean
@@ -31,14 +31,14 @@ structure List.IsChainFromTo {α : Type*} (r : α → α → Prop) (chain : List
   head_eq : chain.head ne_nil = a
   getLast_eq : chain.getLast ne_nil = b
 
-/-- Restatement of `head_eq`, but tagged with simp and grind. -/
-@[simp, grind →]
+/-- Restatement of `head_eq`, but tagged with grind. -/
+@[grind →]
 lemma List.IsChainFromTo_head_eq (hc : chain.IsChainFromTo r a b) :
     chain.head hc.ne_nil = a :=
   hc.head_eq
 
-/-- Restatement of `getLast_eq`, but tagged with simp and grind. -/
-@[simp, grind →]
+/-- Restatement of `getLast_eq`, but tagged with grind. -/
+@[grind →]
 lemma List.IsChainFromTo_getLast_eq (hc : chain.IsChainFromTo r a b) :
     chain.getLast hc.ne_nil = b :=
   hc.getLast_eq

From f85d8ed268ffc51c2e9e597fb7f6d946b6a76d78 Mon Sep 17 00:00:00 2001
From: crei <crei.github@gmail.com>
Date: Thu, 20 Aug 2026 10:50:23 +0200
Subject: [PATCH 09/10] Move file.

---
 Cslib/Foundations/Data/{List.lean => IsChainFromTo.lean} | 0
 1 file changed, 0 insertions(+), 0 deletions(-)
 rename Cslib/Foundations/Data/{List.lean => IsChainFromTo.lean} (100%)

diff --git a/Cslib/Foundations/Data/List.lean b/Cslib/Foundations/Data/IsChainFromTo.lean
similarity index 100%
rename from Cslib/Foundations/Data/List.lean
rename to Cslib/Foundations/Data/IsChainFromTo.lean

From bd393f3c463f3c266da7d41e0d68048db227f216 Mon Sep 17 00:00:00 2001
From: crei <crei.github@gmail.com>
Date: Thu, 20 Aug 2026 11:15:08 +0200
Subject: [PATCH 10/10] Review comments.

---
 Cslib.lean                                    |  2 +-
 .../Data/{ => List}/IsChainFromTo.lean        | 26 ++++++++++++-------
 Cslib/Foundations/Data/RelatesInSteps.lean    | 23 +++++++---------
 3 files changed, 28 insertions(+), 23 deletions(-)
 rename Cslib/Foundations/Data/{ => List}/IsChainFromTo.lean (74%)

diff --git a/Cslib.lean b/Cslib.lean
index 5cb58db9d..2482c4312 100644
--- a/Cslib.lean
+++ b/Cslib.lean
@@ -74,7 +74,7 @@ public import Cslib.Foundations.Data.DecidableEqZero
 public import Cslib.Foundations.Data.FinFun.Basic
 public import Cslib.Foundations.Data.FinFun.Update
 public import Cslib.Foundations.Data.HasFresh
-public import Cslib.Foundations.Data.List
+public import Cslib.Foundations.Data.List.IsChainFromTo
 public import Cslib.Foundations.Data.Nat.Segment
 public import Cslib.Foundations.Data.OmegaSequence.Defs
 public import Cslib.Foundations.Data.OmegaSequence.Flatten
diff --git a/Cslib/Foundations/Data/IsChainFromTo.lean b/Cslib/Foundations/Data/List/IsChainFromTo.lean
similarity index 74%
rename from Cslib/Foundations/Data/IsChainFromTo.lean
rename to Cslib/Foundations/Data/List/IsChainFromTo.lean
index b2e247d94..35a44fea7 100644
--- a/Cslib/Foundations/Data/IsChainFromTo.lean
+++ b/Cslib/Foundations/Data/List/IsChainFromTo.lean
@@ -28,20 +28,26 @@ variable {α : Type*} {r : α → α → Prop} {chain : List α} {a b : α}
 structure List.IsChainFromTo {α : Type*} (r : α → α → Prop) (chain : List α) (a b : α) : Prop where
   isChain : chain.IsChain r
   ne_nil : chain ≠ []
-  head_eq : chain.head ne_nil = a
-  getLast_eq : chain.getLast ne_nil = b
+  head : chain.head ne_nil = a
+  last : chain.getLast ne_nil = b
+
+/-- Create a `List.IsChainFromTo` from a non-empty `List.IsChain`. -/
+theorem List.IsChainFromTo.of_isChain_ne_nil
+    (chain : List α) (hc : chain.IsChain r) (h_ne_nil : chain ≠ []) :
+    List.IsChainFromTo r chain (chain.head h_ne_nil) (chain.getLast h_ne_nil) :=
+  ⟨hc, h_ne_nil, rfl, rfl⟩
 
 /-- Restatement of `head_eq`, but tagged with grind. -/
 @[grind →]
-lemma List.IsChainFromTo_head_eq (hc : chain.IsChainFromTo r a b) :
+lemma List.IsChainFromTo.head_eq (hc : chain.IsChainFromTo r a b) :
     chain.head hc.ne_nil = a :=
-  hc.head_eq
+  hc.head
 
 /-- Restatement of `getLast_eq`, but tagged with grind. -/
 @[grind →]
-lemma List.IsChainFromTo_getLast_eq (hc : chain.IsChainFromTo r a b) :
+lemma List.IsChainFromTo.last_eq (hc : chain.IsChainFromTo r a b) :
     chain.getLast hc.ne_nil = b :=
-  hc.getLast_eq
+  hc.last
 
 @[simp, grind ←]
 lemma List.IsChainFromTo.singleton {a : α} : List.IsChainFromTo r [a] a a :=
@@ -59,9 +65,11 @@ lemma List.IsChainFromTo.exists_length_lt_of_not_nodup
   push Not at h_dup
   obtain ⟨i, j, h_ij, h_lt, h_eq⟩ := h_dup
   use chain.take i ++ chain.drop j
-  refine ⟨⟨?_, by simp; omega, by grind, by grind⟩, by grind⟩
-  · refine (hc.isChain.take _).append (hc.isChain.drop _) ?_
+  constructor
+  · apply IsChainFromTo.mk ((hc.isChain.take _).append (hc.isChain.drop _) ?_)
+      (by simp; omega) (by grind) (by grind)
     intro x hx y hy
     rw [List.head?_drop] at hy
-    have := hc.isChain.getElem (i := i - 1) (by omega)
+    have := hc.isChain.getElem (i := i - 1)
     grind
+  · grind
diff --git a/Cslib/Foundations/Data/RelatesInSteps.lean b/Cslib/Foundations/Data/RelatesInSteps.lean
index 7c0bc1c01..efbc79d85 100644
--- a/Cslib/Foundations/Data/RelatesInSteps.lean
+++ b/Cslib/Foundations/Data/RelatesInSteps.lean
@@ -7,7 +7,7 @@ Authors: Bolton Bailey
 module
 
 public import Cslib.Init
-public import Cslib.Foundations.Data.List
+public import Cslib.Foundations.Data.List.IsChainFromTo
 public import Mathlib.Data.Set.Card
 public import Mathlib.Logic.Relation
 
@@ -171,9 +171,10 @@ lemma RelatesInSteps.exists_isChainFromTo {a b : α} {n : ℕ} (h : RelatesInSte
   | tail t' t'' m _ hstep ih =>
     obtain ⟨l, hchain, hlen⟩ := ih
     use l ++ [t'']
-    refine ⟨⟨?_, by simp, ?_, by simp⟩, by grind⟩
-    · exact hchain.isChain.append (by simp) (by grind)
-    · grind
+    constructor
+    · apply List.IsChainFromTo.mk (hchain.isChain.append (by simp) (by grind))
+        (by simp) (by grind) (by simp)
+    · simp [hlen]
 
 /-- Any two elements along an `r`-chain are related in as many steps as their distance in the
 chain. -/
@@ -185,7 +186,7 @@ lemma RelatesInSteps.of_isChain {chain : List α}
   induction k with
   | zero => exact .refl _
   | succ k ih =>
-    refine .tail _ (chain[p + k]) _ k (ih (by lia)) ?_
+    apply RelatesInSteps.tail _ (chain[p + k]) _ k (ih (by lia))
     apply List.IsChain.getElem hc
 
 /-- If there is an `r`-chain from `a` to `b`, then `a` and `b` are related to each other with
@@ -278,28 +279,24 @@ theorem ReflTransGen.relatesInSteps_lt_encard {b : α} (h : ReflTransGen r a b)
   classical
   -- Let us use the shortest chain from `a` to `b`.
   have hex : ∃ n, RelatesInSteps r a b n := h.relatesInSteps
-  refine ⟨Nat.find hex, Nat.find_spec hex, ?_⟩
+  use Nat.find hex, Nat.find_spec hex
   obtain ⟨chain, hc, hlen⟩ := (Nat.find_spec hex).exists_isChainFromTo
   -- All elements in the chain are reachable from `a`.
   have hsub : {x | x ∈ chain} ⊆ {x | ReflTransGen r a x} := by
-    simp only [Set.subset_def, Set.mem_ofPred_eq]
     intro y hy
     obtain ⟨i, hi, rfl⟩ := List.getElem_of_mem hy
-    have := RelatesInSteps.of_isChain hc.isChain 0 i (by omega)
+    have := RelatesInSteps.of_isChain hc.isChain 0 i
     grind [RelatesInSteps.reflTransGen]
   -- Now assume, for the sake of contradiction, that the minimal chain has at least as many
   -- elements as there are reachable elements.
-  by_contra hcard
-  push Not at hcard
+  by_contra! hcard
   -- Then there is at least one duplicate element.
   have h_dup : ¬chain.Nodup := by
-    intro h_nodup
     have hle := (Set.encard_le_encard hsub).trans hcard
     rw [← List.coe_toFinset, Set.encard_coe_eq_coe_finsetCard] at hle
     grind [List.toFinset_card_of_nodup, Nat.cast_le]
   -- But then we can shorten the chain which contradicts the fact that it is minimal.
   obtain ⟨chain', hc', hlt⟩ := hc.exists_length_lt_of_not_nodup h_dup
-  have := List.length_pos_iff.mpr hc'.ne_nil
-  exact Nat.find_min hex (m := chain'.length - 1) (by omega) (RelatesInSteps.of_isChainFromTo hc')
+  grind [Nat.find_min hex (m := chain'.length - 1), RelatesInSteps.of_isChainFromTo hc']
 
 end Relation