From d695bde18fd16fcb8fe63a5251bde01cdfd6a3f2 Mon Sep 17 00:00:00 2001
From: Samuel Schlesinger <samschlesinger@google.com>
Date: Sun, 25 Oct 2026 02:58:14 +0000
Subject: [PATCH] refactor(List,Ladner,PSPACE): move replicate delimiter idxOf
 lemmas to Foundations (#949)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Move `idxOf_false_replicate_append` and `eq_replicate_idxOf_false` from
`Complexity.Computability.Complexity.Classes.Ladner.Basic` and
`idxOf_true_replicate_false_append` from
`Complexity.Computability.Complexity.Classes.IP.PSPACE` to
`Complexity.Foundations.Data.List.Append` under namespace `List`.

Generalize to `List.idxOf_replicate_append_cons_of_ne` for arbitrary `α`
with `[DecidableEq α]` and `a ≠ b`. Add dual Boolean decomposition
`List.eq_replicate_idxOf_true`.

Delete domain duplicates and update call sites with no aliases needed.
Closes item D.7 on #949 (from #936).
---
 .../Complexity/Classes/IP/PSPACE.lean         | 24 ++-------
 .../Complexity/Classes/Ladner/Basic.lean      | 23 ++-------
 Complexity/Foundations/Data/List/Append.lean  | 49 +++++++++++++++++++
 3 files changed, 57 insertions(+), 39 deletions(-)

diff --git a/Complexity/Computability/Complexity/Classes/IP/PSPACE.lean b/Complexity/Computability/Complexity/Classes/IP/PSPACE.lean
index 7898a38874..169409f575 100644
--- a/Complexity/Computability/Complexity/Classes/IP/PSPACE.lean
+++ b/Complexity/Computability/Complexity/Classes/IP/PSPACE.lean
@@ -18,6 +18,7 @@ import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Na
 import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Option
 import Complexity.Computability.Machines.Turing.MultiTape.Encodings.NatPower
 import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolySpace.Plain
+import Complexity.Foundations.Data.List.Append
 
 /-!
 # `IP ⊆ PSPACE`
@@ -98,17 +99,10 @@ zeros, a one, then `w`. -/
 def encodeWord (L : ℕ) (w : List Bool) : List Bool :=
   List.replicate (L - w.length) false ++ true :: w
 
-theorem idxOf_true_replicate_false_append (n : ℕ) (w : List Bool) :
-    (List.replicate n false ++ true :: w).idxOf true = n := by
-  induction n with
-  | zero => simp
-  | succ n ih =>
-    rw [List.replicate_succ, List.cons_append, List.idxOf_cons_ne _ (by simp), ih]
-
 /-- Decoding inverts coding. -/
 private theorem decodeWord_encodeWord (L : ℕ) (w : List Bool) : decodeWord
     (encodeWord L w) = w := by
-  rw [decodeWord, encodeWord, idxOf_true_replicate_false_append, List.drop_append]
+  rw [decodeWord, encodeWord, List.idxOf_true_replicate_false_append, List.drop_append]
   simp
 
 private theorem length_encodeWord {L : ℕ} {w : List Bool} (hw : w.length ≤ L) :
@@ -125,17 +119,9 @@ private theorem length_decodeWord_le {L : ℕ} {u : List Bool} (hu : u.length =
   lia
 
 /-- A word with a `true` is its first `true` preceded by zeros and followed by its decoding. -/
-private theorem eq_replicate_append_decodeWord : ∀ {u : List Bool}, true ∈ u →
-    u = List.replicate (u.idxOf true) false ++ true :: decodeWord u
-  | b :: u, h => by
-    cases b
-    · have hu : true ∈ u := by simpa using h
-      rw [decodeWord, List.idxOf_cons_ne _ (by simp)]
-      have := eq_replicate_append_decodeWord hu
-      rw [decodeWord] at this
-      simp only [List.replicate_succ, List.cons_append, List.drop_succ_cons]
-      exact congrArg _ this
-    · simp [decodeWord]
+private theorem eq_replicate_append_decodeWord {u : List Bool} (ht : true ∈ u) :
+    u = List.replicate (u.idxOf true) false ++ true :: decodeWord u :=
+  List.eq_replicate_idxOf_true ht
 
 /-- Coding inverts decoding on the words of length `L + 1` with a `true`. -/
 private theorem encodeWord_decodeWord {L : ℕ} {u : List Bool} (hu : u.length = L + 1)
diff --git a/Complexity/Computability/Complexity/Classes/Ladner/Basic.lean b/Complexity/Computability/Complexity/Classes/Ladner/Basic.lean
index b2dae7d757..6a50113a4c 100644
--- a/Complexity/Computability/Complexity/Classes/Ladner/Basic.lean
+++ b/Complexity/Computability/Complexity/Classes/Ladner/Basic.lean
@@ -11,6 +11,7 @@ public import Complexity.Computability.Complexity.Problems.SAT
 public import Complexity.Computability.Machines.Turing.MultiTape.Universal.Machine
 public import Complexity.Computability.Machines.Turing.MultiTape.Universal.Compose
 public import Complexity.Computability.Machines.Turing.MultiTape.Universal.Decode
+public import Complexity.Foundations.Data.List.Append
 import Mathlib.Data.Nat.Size
 
 /-!
@@ -138,35 +139,17 @@ theorem length_pad (u : List Bool) (k : ℕ) : (pad u k).length = u.length + 1 +
   simp only [pad, List.length_append, List.length_cons, List.length_replicate]
   omega
 
-theorem idxOf_false_replicate_append (k : ℕ) (l : List Bool) :
-    (List.replicate k true ++ false :: l).idxOf false = k := by
-  induction k with
-  | zero => simp
-  | succ k ih =>
-    rw [List.replicate_succ, List.cons_append, List.idxOf_cons_ne _ (by decide), ih]
-
 /-- **Padding is undone.** -/
 @[simp]
 theorem unpad_pad (u : List Bool) (k : ℕ) : unpad (pad u k) = (u, k) := by
   have hrev : (pad u k).reverse = List.replicate k true ++ false :: u.reverse := by
     simp [pad]
-  rw [unpad, hrev, idxOf_false_replicate_append, length_pad,
+  rw [unpad, hrev, List.idxOf_false_replicate_append, length_pad,
     show u.length + 1 + k - (k + 1) = u.length by omega, pad, List.take_left' rfl]
 
 theorem pad_inj {u u' : List Bool} {k k' : ℕ} : pad u k = pad u' k' ↔ u = u' ∧ k = k' :=
   ⟨fun h => by simpa using congrArg unpad h, fun ⟨hu, hk⟩ => hu ▸ hk ▸ rfl⟩
 
-/-- A word with a `false` is a run of `true`s up to its first `false`, and what follows. -/
-theorem eq_replicate_idxOf_false {l : List Bool} (hl : false ∈ l) :
-    l = List.replicate (l.idxOf false) true ++ false :: l.drop (l.idxOf false + 1) := by
-  induction l with
-  | nil => simp at hl
-  | cons b l ih =>
-    cases b
-    · simp
-    · rw [List.idxOf_cons_ne _ (by decide), List.replicate_succ, List.cons_append,
-        List.drop_succ_cons, ← ih (by simpa using hl)]
-
 /-- **A word with a `false` is its padded split.** -/
 theorem pad_unpad {y : List Bool} (hy : (unpad y).2 < y.length) :
     pad (unpad y).1 (unpad y).2 = y := by
@@ -174,7 +157,7 @@ theorem pad_unpad {y : List Bool} (hy : (unpad y).2 < y.length) :
     List.idxOf_lt_length_iff.mp (by simpa [unpad] using hy)
   obtain ⟨v, k, rfl⟩ : ∃ v k, y = pad v k := by
     refine ⟨(y.reverse.drop (y.reverse.idxOf false + 1)).reverse, y.reverse.idxOf false, ?_⟩
-    conv_lhs => rw [← List.reverse_reverse y, eq_replicate_idxOf_false hmem]
+    conv_lhs => rw [← List.reverse_reverse y, List.eq_replicate_idxOf_false hmem]
     simp [pad]
   rw [unpad_pad]
 
diff --git a/Complexity/Foundations/Data/List/Append.lean b/Complexity/Foundations/Data/List/Append.lean
index 20f23fe373..3b7f0c1dc0 100644
--- a/Complexity/Foundations/Data/List/Append.lean
+++ b/Complexity/Foundations/Data/List/Append.lean
@@ -18,6 +18,10 @@ public import Mathlib.Data.List.Basic
 * `List.zip_tail_append_cons`: split adjacent pairs at a shared boundary element.
 * `List.replicate_not_append_cons_inj`, `List.replicate_true_append_false_inj`: a unary block
   followed by its delimiter determines both its length and the remaining suffix.
+* `List.idxOf_replicate_append_cons_of_ne`, `List.idxOf_false_replicate_append`,
+  `List.idxOf_true_replicate_false_append`: the index of a delimiter following a unary block.
+* `List.eq_replicate_idxOf_false`, `List.eq_replicate_idxOf_true`: canonical decomposition of a
+  word by its first delimiter.
 -/
 
 @[expose] public section
@@ -49,3 +53,48 @@ theorem List.replicate_true_append_false_inj {m m' : ℕ} {l l' : List Bool}
     (h : List.replicate m true ++ false :: l = List.replicate m' true ++ false :: l') :
     m = m' ∧ l = l' :=
   List.replicate_not_append_cons_inj (a := false) h
+
+/-- The first occurrence of `b` in `(replicate k a ++ b :: l)` is at index `k`, provided `a ≠ b`. -/
+theorem List.idxOf_replicate_append_cons_of_ne {α : Type*} [DecidableEq α] {a b : α}
+    (hab : a ≠ b) (k : ℕ) (l : List α) :
+    (List.replicate k a ++ b :: l).idxOf b = k := by
+  induction k with
+  | zero => simp
+  | succ k ih =>
+    rw [List.replicate_succ, List.cons_append, List.idxOf_cons_ne _ hab, ih]
+
+/-- The first occurrence of `false` in a list beginning with `k` `true`s is at index `k`. -/
+@[simp]
+theorem List.idxOf_false_replicate_append (k : ℕ) (l : List Bool) :
+    (List.replicate k true ++ false :: l).idxOf false = k :=
+  List.idxOf_replicate_append_cons_of_ne (by decide) k l
+
+/-- The first occurrence of `true` in a list beginning with `k` `false`s is at index `k`. -/
+@[simp]
+theorem List.idxOf_true_replicate_false_append (k : ℕ) (l : List Bool) :
+    (List.replicate k false ++ true :: l).idxOf true = k :=
+  List.idxOf_replicate_append_cons_of_ne (by decide) k l
+
+/-- A Boolean word containing `false` decomposes into a unary run of `true`s up to the first
+`false`, and the remaining suffix. -/
+theorem List.eq_replicate_idxOf_false {l : List Bool} (hl : false ∈ l) :
+    l = List.replicate (l.idxOf false) true ++ false :: l.drop (l.idxOf false + 1) := by
+  induction l with
+  | nil => simp at hl
+  | cons b l ih =>
+    cases b
+    · simp
+    · rw [List.idxOf_cons_ne _ (by decide), List.replicate_succ, List.cons_append,
+        List.drop_succ_cons, ← ih (by simpa using hl)]
+
+/-- A Boolean word containing `true` decomposes into a unary run of `false`s up to the first
+`true`, and the remaining suffix. -/
+theorem List.eq_replicate_idxOf_true {l : List Bool} (hl : true ∈ l) :
+    l = List.replicate (l.idxOf true) false ++ true :: l.drop (l.idxOf true + 1) := by
+  induction l with
+  | nil => simp at hl
+  | cons b l ih =>
+    cases b
+    · rw [List.idxOf_cons_ne _ (by decide), List.replicate_succ, List.cons_append,
+        List.drop_succ_cons, ← ih (by simpa using hl)]
+    · simp