feat(bitstring): add numeral bridges and remove duplicate private lemmas (#614)

Complexity.lean

@@ -1617,6 +1617,7 @@ public import Complexity.Foundations.Data.BiTape
 public import Complexity.Foundations.Data.BitString.AffineDisperser
 public import Complexity.Foundations.Data.BitString.Agree
 public import Complexity.Foundations.Data.BitString.Basic
+public import Complexity.Foundations.Data.BitString.Binary
 public import Complexity.Foundations.Data.BitString.Block
 public import Complexity.Foundations.Data.BitString.Broadcast
 public import Complexity.Foundations.Data.BitString.Counter

Complexity/Computability/Complexity/Classes/Counting/Space.lean

@@ -63,14 +63,6 @@ theorem PP_subset_PSPACE : PP enc ⊆ PSPACE enc := by
           (SharpP.computableTidilyInPolySpace hf)))
   exact mem_PSPACE_of_computableTidilyInPolySpace htest fun a => by simpa using hA a
 
-private theorem ofBits_eq_lsbValue (w : List Bool) : ofBits w = BitString.lsbValue w := by
-  induction w with
-  | nil => rfl
-  | cons b w ih =>
-    change Nat.bit b (ofBits w) = b.toNat + 2 * BitString.lsbValue w
-    rw [ih]
-    cases b <;> simp [Nat.bit, Nat.add_comm]
-
 /-- Testing whether a fixed modulus divides a #P count is in polynomial space. A quotient has
 at most one more bit than the verifier's certificate length, even for moduli zero and one. -/
 theorem coModP_subset_PSPACE (k : ℕ) : coModP k enc ⊆ PSPACE enc := by
@@ -110,7 +102,7 @@ theorem coModP_subset_PSPACE (k : ℕ) : coModP k enc ⊆ PSPACE enc := by
         (Nat.pow_lt_pow_right (by norm_num) (by lia)))
     obtain ⟨hv, hl⟩ := BitString.iterate_increment _ _ hlt
     refine ⟨_, hl, ?_⟩
-    rw [ofBits_eq_lsbValue, hv]
+    rw [ofBits, ← BitString.lsbValue_eq_foldr_bit, hv]
     exact (Nat.mul_div_cancel' (Nat.dvd_of_mod_eq_zero hdiv)).symm
   · rintro ⟨w, _, hw⟩
     exact Nat.mod_eq_zero_of_dvd ⟨ofBits w, hw⟩

Complexity/Computability/MCSP/NP.lean

@@ -18,6 +18,7 @@ import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Li
 import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat
 import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat.Binary
 import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat.Log
+import Complexity.Foundations.Data.BitString.Binary
 import Mathlib.Data.List.GetD
 
 /-!
@@ -98,25 +99,13 @@ def verifier (p : Instance × List Bool) : Bool :=
 
 /-! ### Correctness -/
 
-/-- Reading the bits of an input, least significant first, gives its number in the order of
-`BitString.equivFin`. -/
-private theorem binaryValue_reverse_ofFn {n : ℕ} (y : BitString n) :
-    BitString.binaryValue (List.ofFn y).reverse = BitString.equivFin n y := by
-  induction n with
-  | zero => rfl
-  | succ n ih =>
-    rw [List.ofFn_succ, List.reverse_cons, BitString.binaryValue_snoc, ih fun i => y i.succ]
-    have h := BitString.val_equivFin_cons (y 0) (Fin.tail y)
-    rw [Fin.cons_self_tail] at h
-    rw [h, Nat.add_comm]
-    rfl
-
 /-- The verifier reads the function of an instance from its truth table. -/
 theorem tableValue_ofFn (x : Instance) (y : BitString x.arity) :
     tableValue (List.ofFn x.table) (List.ofFn y) = x.function y := by
   have hlt := (BitString.equivFin x.arity y).isLt
-  rw [tableValue, BitString.boundedBinaryValue_eq, binaryValue_reverse_ofFn, List.length_ofFn,
-    Nat.min_eq_right hlt.le, List.getD_eq_getElem _ _ (by simp), List.getElem_ofFn]
+  rw [tableValue, BitString.boundedBinaryValue_eq, BitString.binaryValue_reverse_ofFn,
+    List.length_ofFn, Nat.min_eq_right hlt.le, List.getD_eq_getElem _ _ (by simp),
+    List.getElem_ofFn]
   rfl
 
 /-- The polynomial bounding the length of certificates. -/

Complexity/Crypto/Computational/SchnorrIdentification.lean

@@ -132,21 +132,12 @@ noncomputable def SchnorrImpersonator.rewind (k : ℕ → ℕ) (A : F.SchnorrImp
 
 /-! ### The exact bound -/
 
-/-- Binary digits, least significant first, read as a number (a private copy of the bridge in
-`Complexity/Computability/Complexity/Classes/Counting/Space.lean`). -/
-private theorem ofBits_eq_lsbValue (w : List Bool) : ofBits w = BitString.lsbValue w := by
-  induction w with
-  | nil => rfl
-  | cons b w ih =>
-    change Nat.bit b (ofBits w) = b.toNat + 2 * BitString.lsbValue w
-    rw [ih]
-    cases b <;> simp [Nat.bit, Nat.add_comm]
-
 /-- Distinct `k`-bit challenges are distinct modulo `q` when `2 ^ k ≤ q`. -/
 private theorem challenge_ne {q k : ℕ} (hkq : 2 ^ k ≤ q) {c c' : BitString k} (hc : c ≠ c') :
     (ofBits (List.ofFn c) : ZMod q) ≠ ofBits (List.ofFn c') := by
   intro h
-  rw [ZMod.natCast_eq_natCast_iff', ofBits_eq_lsbValue, ofBits_eq_lsbValue,
+  rw [ZMod.natCast_eq_natCast_iff', ofBits, ofBits, ← BitString.lsbValue_eq_foldr_bit,
+    ← BitString.lsbValue_eq_foldr_bit,
     Nat.mod_eq_of_lt ((BitString.lsbValue_lt _).trans_le (by simpa using hkq)),
     Nat.mod_eq_of_lt ((BitString.lsbValue_lt _).trans_le (by simpa using hkq))] at h
   exact hc (List.ofFn_injective (BitString.lsbValue_injective (by simp) h))

Complexity/Foundations/Data/BitString/Binary.lean

@@ -0,0 +1,85 @@
+/-
+Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Samuel Schlesinger
+-/
+
+module
+-- upstream: candidate
+
+public import Batteries.Data.Nat.Basic
+public import Complexity.Foundations.Data.BitString.Basic
+public import Complexity.Foundations.Data.BitString.Counter
+public import Complexity.Foundations.Data.BitString.List.Binary
+public import Complexity.Init
+public import Mathlib.Data.List.OfFn
+
+/-!
+# Bridges between `BitString.equivFin` and binary numeral views
+
+`Cslib.BitString.equivFin n` numbers `n`-bit strings `Fin n → Bool` with `0` as the least
+significant coordinate. This module connects `equivFin n` to the list-based numeral views
+`Cslib.BitString.lsbValue` (least significant bit first) and `Cslib.BitString.binaryValue` (most
+significant bit first), as well as `Nat.ofBits` and `Nat.testBit`, without adding a
+`BitString.Basic` dependency to the list-level modules `BitString.Counter` or
+`BitString.List.Binary`.
+
+## Main results
+
+* `Cslib.BitString.val_equivFin_eq_ofBits`: `equivFin` agrees with `Nat.ofBits`.
+* `Cslib.BitString.equivFin_symm_apply`: the `i`-th bit of `(equivFin n).symm k` is
+  `(k : ℕ).testBit i`.
+* `Cslib.BitString.lsbValue_ofFn`: reading the bits of an `n`-bit word in order gives its number in
+  `equivFin n`.
+* `Cslib.BitString.binaryValue_reverse_ofFn`: reading the reversed list of bits of an `n`-bit word
+  gives its number in `equivFin n`.
+-/
+
+@[expose] public section
+
+namespace Cslib.BitString
+
+/-- `equivFin` agrees with `Nat.ofBits` on `n`-bit words. -/
+theorem val_equivFin_eq_ofBits {n : ℕ} (x : BitString n) : (equivFin n x : ℕ) = Nat.ofBits x := by
+  induction n with
+  | zero => rfl
+  | succ n ih =>
+    have h := val_equivFin_cons (x 0) (Fin.tail x)
+    rw [Fin.cons_self_tail] at h
+    rw [h, Nat.ofBits, Fin.foldr_succ, ← Nat.ofBits, ih (Fin.tail x), Nat.add_comm]
+    rfl
+
+/-- The `i`-th bit of `(equivFin n).symm k` is the `i`-th binary digit of `k`. -/
+@[simp] theorem equivFin_symm_apply {n : ℕ} (k : Fin (2 ^ n)) (i : Fin n) :
+    (equivFin n).symm k i = (k : ℕ).testBit i := by
+  have hfin (x : Fin 2) : finTwoEquiv x = decide ((x : ℕ) = 1) := by
+    rcases x with ⟨_ | _ | _, h⟩ <;> rfl
+  rw [Nat.testBit_eq_decide_div_mod_eq]
+  simp only [equivFin, Equiv.symm_trans_apply, Equiv.arrowCongr_symm, Equiv.refl_symm,
+    Equiv.symm_symm, Equiv.arrowCongr_apply, Function.comp_apply, Equiv.refl_apply, hfin]
+  rfl
+
+/-- Reading the bits of an `n`-bit word in order gives its number in `equivFin n`. -/
+theorem lsbValue_ofFn {n : ℕ} (x : BitString n) : lsbValue (List.ofFn x) = equivFin n x := by
+  induction n with
+  | zero => rfl
+  | succ n ih =>
+    rw [List.ofFn_succ, lsbValue, ih]
+    have h := val_equivFin_cons (x 0) (Fin.tail x)
+    rw [Fin.cons_self_tail] at h
+    exact h.symm
+
+/-- Reading the bits of an input, least significant first, gives its number in the order of
+`BitString.equivFin`. -/
+theorem binaryValue_reverse_ofFn {n : ℕ} (y : BitString n) :
+    binaryValue (List.ofFn y).reverse = equivFin n y := by
+  induction n with
+  | zero => rfl
+  | succ n ih =>
+    rw [List.ofFn_succ, List.reverse_cons, binaryValue_snoc, ih fun i => y i.succ]
+    have h := val_equivFin_cons (y 0) (Fin.tail y)
+    rw [Fin.cons_self_tail] at h
+    rw [h, Nat.add_comm]
+    rfl
+
+end Cslib.BitString

Complexity/Foundations/Data/BitString/Counter.lean

@@ -10,6 +10,7 @@ module
 public import Complexity.Init
 public import Mathlib.Algebra.Order.Monoid.Unbundled.Pow
 public import Mathlib.Data.Nat.Basic
+public import Mathlib.Data.Nat.Bits
 
 /-!
 # A binary counter
@@ -33,6 +34,7 @@ their candidates in this way, storing only the current one.
 * `Cslib.BitString.lsbValue_injective`: words of the same length are determined by their values.
 * `Cslib.BitString.iterate_increment`, `Cslib.BitString.iterate_increment_lsbValue`: counting from
   zero enumerates the words of a length.
+* `Cslib.BitString.lsbValue_eq_foldr_bit`: `lsbValue` is a right fold of `Nat.bit`.
 -/
 
 @[expose] public section
@@ -146,4 +148,10 @@ theorem iterate_increment_lsbValue (u : List Bool) :
   let h := iterate_increment u.length (lsbValue u) (lsbValue_lt u)
   lsbValue_injective h.2 h.1
 
+/-- `lsbValue` is a right fold of `Nat.bit`. -/
+theorem lsbValue_eq_foldr_bit (w : List Bool) : lsbValue w = w.foldr Nat.bit 0 := by
+  induction w with
+  | nil => rfl
+  | cons b w ih => rw [lsbValue, List.foldr_cons, ← ih, Nat.bit_val, Nat.add_comm]
+
 end Cslib.BitString

Complexity/Foundations/Data/ListDecoding.lean

@@ -7,6 +7,7 @@ Authors: Samuel Schlesinger
 module
 -- upstream: candidate
 
+public import Complexity.Foundations.Data.BitString.Basic
 public import Complexity.Init
 public import Cslib.Foundations.Data.BitString
 public import Mathlib.Basic.Real.Basic
@@ -93,19 +94,16 @@ theorem card_candidates_le [DecidableEq α] (w : ι → β) : #(C.candidates w)
 /-- The candidate named by the binary index `b` of `Nat.clog 2 L` bits, read least significant bit
 first: the `k`-th candidate for `w` if `b` spells a number `k < L`, and nothing otherwise. -/
 def decodeBits (w : ι → β) (b : BitString (Nat.clog 2 L)) : Option α :=
-  let k : Fin (2 ^ Nat.clog 2 L) := finFunctionFinEquiv (finTwoEquiv.symm ∘ b)
+  let k : Fin (2 ^ Nat.clog 2 L) := BitString.equivFin (Nat.clog 2 L) b
   if h : (k : ℕ) < L then some (C.decode w ⟨k, h⟩) else none
 
 /-- **Short index.** Every candidate is named by an index of `Nat.clog 2 L` bits. -/
 theorem exists_decodeBits_eq_some {w : ι → β} {x : α} (h : ∃ k, C.decode w k = x) :
     ∃ b : BitString (Nat.clog 2 L), C.decodeBits w b = some x := by
   obtain ⟨k, rfl⟩ := h
-  let k' : Fin (2 ^ Nat.clog 2 L) := Fin.castLE (Nat.le_pow_clog one_lt_two L) k
-  refine ⟨finTwoEquiv ∘ finFunctionFinEquiv.symm k', ?_⟩
-  have hk : finFunctionFinEquiv (finTwoEquiv.symm ∘ finTwoEquiv ∘ finFunctionFinEquiv.symm k') =
-      k' := by
-    rw [← Function.comp_assoc, Equiv.symm_comp_self, Function.id_comp, Equiv.apply_symm_apply]
-  simp only [decodeBits, hk, k', Fin.val_castLE, k.isLt, ↓reduceDIte]
+  refine ⟨BitString.indexBits k, ?_⟩
+  simp only [decodeBits, BitString.indexBits, Equiv.apply_symm_apply, Fin.val_castLE, k.isLt,
+    ↓reduceDIte]
 
 variable [Fintype ι] [DecidableEq β] {C}
 

ComplexityTests/BitString.lean

@@ -5,6 +5,7 @@ Authors: Samuel Schlesinger
 -/
 
 import Complexity.Foundations.Data.BitString.Basic
+import Complexity.Foundations.Data.BitString.Binary
 import Complexity.Foundations.Data.BitString.Block
 import Complexity.Foundations.Data.BitString.Counter
 import Complexity.Foundations.Data.BitString.Enumeration
@@ -42,6 +43,22 @@ example : binaryValue [true, true, false] = 6 := by decide
 -- `lowBits` writes a value least significant bit first, padded to the requested width.
 example : lowBits 4 6 = [false, true, true, false] := by decide
 
+-- Numeral bridges between `equivFin`, `lsbValue`, `binaryValue`, `Nat.ofBits` and `Nat.testBit`.
+example : lsbValue [true, false, true] = [true, false, true].foldr Nat.bit 0 :=
+  lsbValue_eq_foldr_bit [true, false, true]
+
+example : lsbValue (List.ofFn ![true, false, true]) = equivFin 3 ![true, false, true] :=
+  lsbValue_ofFn ![true, false, true]
+
+example : (equivFin 3 ![true, false, true] : ℕ) = Nat.ofBits ![true, false, true] :=
+  val_equivFin_eq_ofBits ![true, false, true]
+
+example : (equivFin 3).symm 5 2 = (5 : ℕ).testBit 2 :=
+  equivFin_symm_apply 5 2
+
+example : binaryValue (List.ofFn ![true, false, true]).reverse = equivFin 3 ![true, false, true] :=
+  binaryValue_reverse_ofFn ![true, false, true]
+
 -- There are `2 ^ n` words of `n` bits.
 example : Fintype.card (BitString 5) = 32 := by rw [BitString.card]; rfl