From 483987cc02f9fbe34209cd3baa5059dbd4cba8d6 Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Fri, 23 Oct 2026 21:37:33 -0400 Subject: [PATCH 1/3] refactor(list): split Basic into topic modules and narrow free clients Preserve all sixteen declaration names, statements, proofs, attributes and source credit across Fold, Lookup, Counting and Append. Keep Basic as a public re-export. Narrow disjoint consumers and add the focused fixed-original-universe import comparison, reusing the existing native parser and quality-report closure. Refs #573 and #569. Three #656 consumer files and the Geography re-export/removal path remain held; this checkpoint is not completion of the consumer migration. AI assistance: OpenAI Codex worker codex-review-559 under coordinator-codex-01a16ab8. --- Complexity.lean | 4 + .../Circuit/Boolean/DepthTime.lean | 2 +- .../Circuit/Boolean/Encoding/Certificate.lean | 2 +- .../Circuit/Boolean/Layered/Compile.lean | 2 +- .../Circuit/Boolean/Tableau/Basic.lean | 2 +- .../Circuit/Boolean/Tableau/Correct.lean | 2 +- .../Circuit/Rational/EncodingBounds.lean | 2 +- .../Classes/LogSpace/FirstOrder.lean | 2 +- .../Classes/LogSpace/FirstOrder/Formula.lean | 2 +- .../Classes/LogSpace/FirstOrder/Output.lean | 2 +- .../LogSpace/FirstOrder/Transducer.lean | 2 +- .../GeneralizedGeography/Membership.lean | 1 + .../Problems/Hamiltonian/Sparse.lean | 2 +- .../Problems/IndependentSet/Sparse.lean | 2 +- .../Complexity/Problems/SharpSAT.lean | 2 +- .../Complexity/LogSpace/CounterProgram.lean | 1 - .../MultiTape/Complexity/PolyTime/Finite.lean | 2 +- .../MultiTape/Complexity/PolyTime/Fold.lean | 2 +- .../MultiTape/Complexity/Streaming.lean | 2 +- .../Computability/Probabilistic/Finite.lean | 2 +- .../Probabilistic/Oracle/Tidy.lean | 2 +- .../GSW/Serialized/Correctness.lean | 2 +- .../GSW/Serialized/Evaluation.lean | 2 +- .../Homomorphic/KeyChain/Hybrid.lean | 2 +- Complexity/Foundations/Data/List/Append.lean | 51 +++++ Complexity/Foundations/Data/List/Basic.lean | 182 +----------------- .../Foundations/Data/List/Counting.lean | 55 ++++++ Complexity/Foundations/Data/List/Fold.lean | 57 ++++++ Complexity/Foundations/Data/List/Lookup.lean | 81 ++++++++ .../Propositional/Resolution/Pigeonhole.lean | 2 +- .../Propositional/Resolution/SizeWidth.lean | 2 +- ComplexityTests/Reingold.lean | 2 +- scripts/list_split_fanout.py | 70 +++++++ scripts/test_list_split_fanout.py | 24 +++ 34 files changed, 374 insertions(+), 200 deletions(-) create mode 100644 Complexity/Foundations/Data/List/Append.lean create mode 100644 Complexity/Foundations/Data/List/Counting.lean create mode 100644 Complexity/Foundations/Data/List/Fold.lean create mode 100644 Complexity/Foundations/Data/List/Lookup.lean create mode 100644 scripts/list_split_fanout.py create mode 100644 scripts/test_list_split_fanout.py diff --git a/Complexity.lean b/Complexity.lean index 65da2a8312..f72624ac5d 100644 --- a/Complexity.lean +++ b/Complexity.lean @@ -1646,9 +1646,13 @@ public import Complexity.Foundations.Data.Finset.Sampling public import Complexity.Foundations.Data.Finset.SymmDiff public import Complexity.Foundations.Data.Hamming public import Complexity.Foundations.Data.HammingBound +public import Complexity.Foundations.Data.List.Append public import Complexity.Foundations.Data.List.BalancedFold public import Complexity.Foundations.Data.List.Basic +public import Complexity.Foundations.Data.List.Counting public import Complexity.Foundations.Data.List.Equiv +public import Complexity.Foundations.Data.List.Fold +public import Complexity.Foundations.Data.List.Lookup public import Complexity.Foundations.Data.List.OfFn public import Complexity.Foundations.Data.ListDecoding public import Complexity.Foundations.Data.Matrix.Binary diff --git a/Complexity/Computability/Circuit/Boolean/DepthTime.lean b/Complexity/Computability/Circuit/Boolean/DepthTime.lean index 9d6fa3489d..45a3b83724 100644 --- a/Complexity/Computability/Circuit/Boolean/DepthTime.lean +++ b/Complexity/Computability/Circuit/Boolean/DepthTime.lean @@ -10,7 +10,7 @@ module public import Complexity.Computability.Circuit.Boolean.EvaluationTime public import Complexity.Computability.Circuit.Depth -import Complexity.Foundations.Data.List.Basic +import Complexity.Foundations.Data.List.Lookup /-! # Computing the depths of a Boolean circuit diff --git a/Complexity/Computability/Circuit/Boolean/Encoding/Certificate.lean b/Complexity/Computability/Circuit/Boolean/Encoding/Certificate.lean index 4de039526c..dfdfb3a5ce 100644 --- a/Complexity/Computability/Circuit/Boolean/Encoding/Certificate.lean +++ b/Complexity/Computability/Circuit/Boolean/Encoding/Certificate.lean @@ -14,7 +14,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.Finite -import Complexity.Foundations.Data.List.Basic +import Complexity.Foundations.Data.List.Lookup import Mathlib.Data.List.GetD /-! diff --git a/Complexity/Computability/Circuit/Boolean/Layered/Compile.lean b/Complexity/Computability/Circuit/Boolean/Layered/Compile.lean index ea5a172cb4..2a987a7533 100644 --- a/Complexity/Computability/Circuit/Boolean/Layered/Compile.lean +++ b/Complexity/Computability/Circuit/Boolean/Layered/Compile.lean @@ -9,7 +9,7 @@ module public import Complexity.Computability.Circuit.Boolean.Layered public import Complexity.Computability.Circuit.Boolean.DepthTime -import Complexity.Foundations.Data.List.Basic +import Complexity.Foundations.Data.List.Lookup import Mathlib.Data.List.GetD /-! diff --git a/Complexity/Computability/Circuit/Boolean/Tableau/Basic.lean b/Complexity/Computability/Circuit/Boolean/Tableau/Basic.lean index cf376e92d4..86ec0eb176 100644 --- a/Complexity/Computability/Circuit/Boolean/Tableau/Basic.lean +++ b/Complexity/Computability/Circuit/Boolean/Tableau/Basic.lean @@ -9,7 +9,7 @@ module public import Complexity.Computability.Circuit.Boolean.Encoding public import Complexity.Computability.Circuit.Boolean.Tableau.Layout -import Complexity.Foundations.Data.List.Basic +import Complexity.Foundations.Data.List.Lookup /-! # The uniform tableau circuit of a multi-tape machine diff --git a/Complexity/Computability/Circuit/Boolean/Tableau/Correct.lean b/Complexity/Computability/Circuit/Boolean/Tableau/Correct.lean index 5359a0837d..3f4ce88172 100644 --- a/Complexity/Computability/Circuit/Boolean/Tableau/Correct.lean +++ b/Complexity/Computability/Circuit/Boolean/Tableau/Correct.lean @@ -9,7 +9,7 @@ module public import Complexity.Computability.Circuit.Boolean.Tableau.Basic public import Complexity.Computability.Circuit.Boolean.EvaluationTime -import Complexity.Foundations.Data.List.Basic +import Complexity.Foundations.Data.List.Lookup import Mathlib.Data.List.GetD /-! diff --git a/Complexity/Computability/Circuit/Rational/EncodingBounds.lean b/Complexity/Computability/Circuit/Rational/EncodingBounds.lean index 66694c71d3..802470bafb 100644 --- a/Complexity/Computability/Circuit/Rational/EncodingBounds.lean +++ b/Complexity/Computability/Circuit/Rational/EncodingBounds.lean @@ -9,7 +9,7 @@ module public import Complexity.Init public import Complexity.Computability.Circuit.Rational.IntegralLift -import Complexity.Foundations.Data.List.Basic +import Complexity.Foundations.Data.List.Counting import Mathlib.Data.Nat.Digits.Lemmas import Mathlib.LinearAlgebra.Matrix.AbsoluteValue diff --git a/Complexity/Computability/Complexity/Classes/LogSpace/FirstOrder.lean b/Complexity/Computability/Complexity/Classes/LogSpace/FirstOrder.lean index 85c617e998..8357678d43 100644 --- a/Complexity/Computability/Complexity/Classes/LogSpace/FirstOrder.lean +++ b/Complexity/Computability/Complexity/Classes/LogSpace/FirstOrder.lean @@ -11,7 +11,7 @@ public import Complexity.Computability.Complexity.Classes.LogSpace public import Complexity.Computability.Complexity.Classes.LogSpace.FirstOrder.Formula public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.LogSpace.CounterProgram public import Complexity.Logics.FirstOrder.Encoding.Layout -import Complexity.Foundations.Data.List.Basic +import Complexity.Foundations.Data.List.Lookup /-! # First-order model checking in logarithmic space diff --git a/Complexity/Computability/Complexity/Classes/LogSpace/FirstOrder/Formula.lean b/Complexity/Computability/Complexity/Classes/LogSpace/FirstOrder/Formula.lean index ed6205cc25..2b052da52d 100644 --- a/Complexity/Computability/Complexity/Classes/LogSpace/FirstOrder/Formula.lean +++ b/Complexity/Computability/Complexity/Classes/LogSpace/FirstOrder/Formula.lean @@ -9,7 +9,7 @@ module public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.LogSpace.CounterProgram public import Complexity.Logics.FirstOrder.Basic -import Complexity.Foundations.Data.List.Basic +import Complexity.Foundations.Data.List.Lookup /-! # Shared first-order counter-program control diff --git a/Complexity/Computability/Complexity/Classes/LogSpace/FirstOrder/Output.lean b/Complexity/Computability/Complexity/Classes/LogSpace/FirstOrder/Output.lean index a3b0b81bc2..35be4b9b5c 100644 --- a/Complexity/Computability/Complexity/Classes/LogSpace/FirstOrder/Output.lean +++ b/Complexity/Computability/Complexity/Classes/LogSpace/FirstOrder/Output.lean @@ -9,7 +9,7 @@ module public import Complexity.Computability.Complexity.Classes.LogSpace.FirstOrder public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.LogSpace.CounterProgram.Output -import Complexity.Foundations.Data.List.Basic +import Complexity.Foundations.Data.List.Lookup /-! # Shared output routines for first-order interpretation transducers diff --git a/Complexity/Computability/Complexity/Classes/LogSpace/FirstOrder/Transducer.lean b/Complexity/Computability/Complexity/Classes/LogSpace/FirstOrder/Transducer.lean index c302f2980b..c8e0d8c270 100644 --- a/Complexity/Computability/Complexity/Classes/LogSpace/FirstOrder/Transducer.lean +++ b/Complexity/Computability/Complexity/Classes/LogSpace/FirstOrder/Transducer.lean @@ -10,7 +10,7 @@ module public import Complexity.Computability.Complexity.Classes.LogSpace.FirstOrder.Output public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.LogSpace.CounterProgram.Output public import Complexity.Logics.FirstOrder.Interpretation.Rank -import Complexity.Foundations.Data.List.Basic +import Complexity.Foundations.Data.List.Lookup /-! # The domain-counting interpretation transducer diff --git a/Complexity/Computability/Complexity/Classes/Space/GeneralizedGeography/Membership.lean b/Complexity/Computability/Complexity/Classes/Space/GeneralizedGeography/Membership.lean index 29d66ef3f5..234561e146 100644 --- a/Complexity/Computability/Complexity/Classes/Space/GeneralizedGeography/Membership.lean +++ b/Complexity/Computability/Complexity/Classes/Space/GeneralizedGeography/Membership.lean @@ -14,6 +14,7 @@ import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Fo import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.List import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Option +import Complexity.Foundations.Data.List.Counting /-! # Generalized Geography is in `PSPACE` diff --git a/Complexity/Computability/Complexity/Problems/Hamiltonian/Sparse.lean b/Complexity/Computability/Complexity/Problems/Hamiltonian/Sparse.lean index de404df67e..eb72dd4d81 100644 --- a/Complexity/Computability/Complexity/Problems/Hamiltonian/Sparse.lean +++ b/Complexity/Computability/Complexity/Problems/Hamiltonian/Sparse.lean @@ -16,7 +16,7 @@ import Complexity.Computability.Complexity.Problems.Hamiltonian.Directed import Complexity.Computability.Complexity.Problems.SAT.PolyTime import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.List import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat -import Complexity.Foundations.Data.List.Basic +import Complexity.Foundations.Data.List.Lookup import Mathlib.Data.List.GetD /-! diff --git a/Complexity/Computability/Complexity/Problems/IndependentSet/Sparse.lean b/Complexity/Computability/Complexity/Problems/IndependentSet/Sparse.lean index a244d5d1c7..6c4b076821 100644 --- a/Complexity/Computability/Complexity/Problems/IndependentSet/Sparse.lean +++ b/Complexity/Computability/Complexity/Problems/IndependentSet/Sparse.lean @@ -10,7 +10,7 @@ module public import Complexity.Computability.Complexity.Problems.IndependentSet public import Complexity.Computability.Complexity.Problems.SubsetSum import Complexity.Computability.Complexity.FineGrained.Assignment -import Complexity.Foundations.Data.List.Basic +import Complexity.Foundations.Data.List.Counting import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.List import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat diff --git a/Complexity/Computability/Complexity/Problems/SharpSAT.lean b/Complexity/Computability/Complexity/Problems/SharpSAT.lean index 62354a801e..d9e25de6db 100644 --- a/Complexity/Computability/Complexity/Problems/SharpSAT.lean +++ b/Complexity/Computability/Complexity/Problems/SharpSAT.lean @@ -14,7 +14,7 @@ public import Complexity.Logics.Propositional.CNF.ModelCount import Complexity.Computability.Complexity.Problems.SAT.PolyTime import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.List import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat -import Complexity.Foundations.Data.List.Basic +import Complexity.Foundations.Data.List.Lookup import Mathlib.Data.List.GetD /-! diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/CounterProgram.lean b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/CounterProgram.lean index 542f744ab5..7323fa131e 100644 --- a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/CounterProgram.lean +++ b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/LogSpace/CounterProgram.lean @@ -10,7 +10,6 @@ module public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.LogSpace.QueryMachine import Complexity.Computability.Machines.Turing.MultiTape.Encodings.NatLength import Complexity.Computability.Machines.Turing.MultiTape.Complexity.InSpace.Bit -import Complexity.Foundations.Data.List.Basic import Mathlib.Data.List.GetD /-! diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/Finite.lean b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/Finite.lean index dacdb42dd7..a5ab5a25c5 100644 --- a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/Finite.lean +++ b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/Finite.lean @@ -8,7 +8,7 @@ module -- upstream: candidate public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Basic -import Complexity.Foundations.Data.List.Basic +import Complexity.Foundations.Data.List.Fold import Mathlib.Data.Fintype.Basic /-! diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/Fold.lean b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/Fold.lean index 80e742e703..4b56510e96 100644 --- a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/Fold.lean +++ b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/PolyTime/Fold.lean @@ -8,7 +8,7 @@ module -- upstream: candidate public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Basic -import Complexity.Foundations.Data.List.Basic +import Complexity.Foundations.Data.List.Fold /-! # Polynomial-time folds diff --git a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/Streaming.lean b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/Streaming.lean index f4fee0c03c..7f7f808585 100644 --- a/Complexity/Computability/Machines/Turing/MultiTape/Complexity/Streaming.lean +++ b/Complexity/Computability/Machines/Turing/MultiTape/Complexity/Streaming.lean @@ -9,7 +9,7 @@ module public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.BigO import Complexity.Computability.Machines.Turing.MultiTape.Combinators.Reverse -import Complexity.Foundations.Data.List.Basic +import Complexity.Foundations.Data.List.Fold public import Complexity.Computability.Machines.Turing.MultiTape.Encodings.StreamFold import Mathlib.Tactic.Linarith diff --git a/Complexity/Computability/Probabilistic/Finite.lean b/Complexity/Computability/Probabilistic/Finite.lean index b2db37fd9c..d0492c2799 100644 --- a/Complexity/Computability/Probabilistic/Finite.lean +++ b/Complexity/Computability/Probabilistic/Finite.lean @@ -8,7 +8,7 @@ module -- upstream: candidate public import Complexity.Computability.Probabilistic.PPT.Capture -import Complexity.Foundations.Data.List.Basic +import Complexity.Foundations.Data.List.Fold import Mathlib.Data.Fintype.Basic /-! diff --git a/Complexity/Computability/Probabilistic/Oracle/Tidy.lean b/Complexity/Computability/Probabilistic/Oracle/Tidy.lean index 08451aec43..873187a6f1 100644 --- a/Complexity/Computability/Probabilistic/Oracle/Tidy.lean +++ b/Complexity/Computability/Probabilistic/Oracle/Tidy.lean @@ -10,7 +10,7 @@ module public import Complexity.Computability.Probabilistic.Oracle public import Complexity.Computability.Machines.Turing.MultiTape.Probabilistic.Tidy public import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Basic -import Complexity.Foundations.Data.List.Basic +import Complexity.Foundations.Data.List.Fold import Mathlib.Data.Fintype.Basic /-! diff --git a/Complexity/Crypto/Computational/Homomorphic/GSW/Serialized/Correctness.lean b/Complexity/Crypto/Computational/Homomorphic/GSW/Serialized/Correctness.lean index 8209a58c58..eb64c9de82 100644 --- a/Complexity/Crypto/Computational/Homomorphic/GSW/Serialized/Correctness.lean +++ b/Complexity/Crypto/Computational/Homomorphic/GSW/Serialized/Correctness.lean @@ -9,7 +9,7 @@ module public import Complexity.Crypto.Computational.Homomorphic.GSW.Serialized import Mathlib.Algebra.BigOperators.Fin -import Complexity.Foundations.Data.List.Basic +import Complexity.Foundations.Data.List.Lookup /-! # Exact bridges for the serialized GSW algorithms diff --git a/Complexity/Crypto/Computational/Homomorphic/GSW/Serialized/Evaluation.lean b/Complexity/Crypto/Computational/Homomorphic/GSW/Serialized/Evaluation.lean index fa1cc895ef..8dfcaafa26 100644 --- a/Complexity/Crypto/Computational/Homomorphic/GSW/Serialized/Evaluation.lean +++ b/Complexity/Crypto/Computational/Homomorphic/GSW/Serialized/Evaluation.lean @@ -10,7 +10,7 @@ module public import Complexity.Crypto.Computational.Homomorphic.GSW.Serialized.Correctness public import Complexity.Crypto.Computational.Homomorphic.GSW.Decryption import Mathlib.Algebra.BigOperators.Fin -import Complexity.Foundations.Data.List.Basic +import Complexity.Foundations.Data.List.Lookup import Complexity.Foundations.Data.Nat.Bits /-! diff --git a/Complexity/Crypto/Computational/Homomorphic/KeyChain/Hybrid.lean b/Complexity/Crypto/Computational/Homomorphic/KeyChain/Hybrid.lean index b722004dda..c260a38dec 100644 --- a/Complexity/Crypto/Computational/Homomorphic/KeyChain/Hybrid.lean +++ b/Complexity/Crypto/Computational/Homomorphic/KeyChain/Hybrid.lean @@ -9,7 +9,7 @@ module public import Complexity.Crypto.Computational.Homomorphic.KeyChain public import Complexity.Crypto.Computational.Homomorphic.BitEncryption -import Complexity.Foundations.Data.List.Basic +import Complexity.Foundations.Data.List.Append import Complexity.Probability.PMF /-! diff --git a/Complexity/Foundations/Data/List/Append.lean b/Complexity/Foundations/Data/List/Append.lean new file mode 100644 index 0000000000..20f23fe373 --- /dev/null +++ b/Complexity/Foundations/Data/List/Append.lean @@ -0,0 +1,51 @@ +/- +Copyright (c) 2026 Christian Reitwiessner, Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Christian Reitwiessner, Samuel Schlesinger +-/ + +module +-- upstream: candidate + +public import Complexity.Init +public import Mathlib.Data.List.Basic + +/-! +# List append boundaries and unary delimiters + +## Main results + +* `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. +-/ + +@[expose] public section + +/-- Split consecutive pairs at a boundary element shared by the two list segments. -/ +theorem List.zip_tail_append_cons {α : Type*} (before : List α) (middle : α) + (after : List α) : + (before ++ middle :: after).zip (before ++ middle :: after).tail = + (before ++ [middle]).zip (before ++ [middle]).tail ++ (middle :: after).zip after := by + induction before with + | nil => simp + | cons first before ih => + cases before with + | nil => simp + | cons second before => + simpa only [List.cons_append, List.tail_cons, List.zip_cons_cons] using + congrArg (List.cons (first, second)) ih + +/-- A unary block of copies of `!a` followed by the delimiter `a` determines both its length and the +remaining suffix. -/ +theorem List.replicate_not_append_cons_inj {a : Bool} {m m' : ℕ} {l l' : List Bool} + (h : List.replicate m (!a) ++ a :: l = List.replicate m' (!a) ++ a :: l') : + m = m' ∧ l = l' := by + induction m generalizing m' <;> cases m' <;> simp_all [List.replicate_succ] + +/-- A unary block of `true` bits followed by `false` determines both its length and the remaining +suffix. -/ +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 diff --git a/Complexity/Foundations/Data/List/Basic.lean b/Complexity/Foundations/Data/List/Basic.lean index 070caae519..d0b195694e 100644 --- a/Complexity/Foundations/Data/List/Basic.lean +++ b/Complexity/Foundations/Data/List/Basic.lean @@ -7,182 +7,14 @@ Authors: Christian Reitwiessner, Samuel Schlesinger module -- upstream: candidate -public import Complexity.Init -public import Mathlib.Data.List.Basic -import Mathlib.Data.List.GetD -import Mathlib.Data.List.OfFn +public import Complexity.Foundations.Data.List.Append +public import Complexity.Foundations.Data.List.Counting +public import Complexity.Foundations.Data.List.Fold +public import Complexity.Foundations.Data.List.Lookup /-! -# List identities and fold invariants +# List identities -## Main results - -* `List.foldl_take_invariant`: an index-dependent invariant holds after every prefix of a fold. -* `List.foldr_ite_eq_of_mem`: a chain of equality tests selects the branch of a contained tag. - Used by deterministic and probabilistic finite-control certificates. -* `List.getD_mem_or`, `List.getD_idxOf`: a defaulted lookup returns a list member or the default - value, and returns a member at its first index. -* `List.getD_map_range`: look up a function tabulated over a bounded range. -* `List.map_range_eq_ofFn`: runtime tabulation agrees with the finite coordinate view. -* `List.countP_and_not_add_countP_and`: the members satisfying `p` split by whether they satisfy - `q`. -* `List.length_flatMap_le`: blocks of bounded length have bounded total length. -* `List.zip_tail_append_cons`: split adjacent pairs at a shared boundary element. -* `List.decide_mem_eq_any`: membership as a scan of the list. -* `List.getD_set_self`, `List.getD_set_ne`, `List.forall_mem_set_of_forall_mem`, - `List.getD_le_of_forall_le`: lists as register files, updated by `List.set` and read by - `List.getD`. -* `List.replicate_not_append_cons_inj`, `List.replicate_true_append_false_inj`: a unary block - followed by a delimiter bit determines both its length and the remaining suffix. - -## References - -Adapts the selection identity from `Computability/Probabilistic/Finite.lean` on the cslib -`crypto` branch at `5ff69ca93402e7c947208dc56396d6d86203ccd8`. +Re-export the fold, lookup, counting and append APIs. New consumers should import the topic +module they use; this module keeps the existing combined import available. -/ - -@[expose] public section - -/-- Split consecutive pairs at a boundary element shared by the two list segments. -/ -theorem List.zip_tail_append_cons {α : Type*} (before : List α) (middle : α) - (after : List α) : - (before ++ middle :: after).zip (before ++ middle :: after).tail = - (before ++ [middle]).zip (before ++ [middle]).tail ++ (middle :: after).zip after := by - induction before with - | nil => simp - | cons first before ih => - cases before with - | nil => simp - | cons second before => - simpa only [List.cons_append, List.tail_cons, List.zip_cons_cons] using - congrArg (List.cons (first, second)) ih - -/-- An invariant depending on the number of consumed elements holds after every bounded prefix -fold if it holds initially and is preserved by the next list element. Unlike `List.foldlRecOn`, -preservation may depend on the position. This is a semantic rule with no resource assumptions. -/ -theorem List.foldl_take_invariant {α β : Type*} (l : List α) (step : β → α → β) (init : β) - (P : ℕ → β → Prop) (hbase : P 0 init) - (hstep : ∀ i (hi : i < l.length) state, P i state → P (i + 1) (step state l[i])) : - ∀ i, i ≤ l.length → P i ((l.take i).foldl step init) := by - intro i - induction i with - | zero => intro _; simpa only [List.take_zero, List.foldl_nil] using hbase - | succ i ih => - intro hi - have hlt : i < l.length := Nat.lt_of_succ_le hi - simpa only [List.take_succ_eq_append_getElem hlt, List.foldl_append, - List.foldl_cons, List.foldl_nil] using hstep i hlt _ (ih (Nat.le_of_lt hlt)) - -/-- A chain of equality tests selects a contained tag, regardless of duplicates or fallback. -/ -theorem List.foldr_ite_eq_of_mem {Tag Value : Type*} [DecidableEq Tag] - (tags : List Tag) (tag : Tag) (branch : Tag → Value) (fallback : Value) (h : tag ∈ tags) : - tags.foldr (fun candidate rest => if tag = candidate then branch candidate else rest) - fallback = branch tag := by - induction tags with - | nil => simp at h - | cons candidate tags ih => - by_cases heq : tag = candidate - · simp [heq] - · simp only [List.foldr_cons, heq, ↓reduceIte] - exact ih (List.mem_cons.mp h |>.resolve_left heq) - -/-- Blocks of at most `k` elements each, one for each element of `l`, have at most `|l| k` -elements in total. -/ -theorem List.length_flatMap_le {α β : Type*} {l : List α} {f : α → List β} {k : ℕ} - (h : ∀ a ∈ l, (f a).length ≤ k) : (l.flatMap f).length ≤ l.length * k := by - induction l with - | nil => simp - | cons a l ih => - have ha := h a List.mem_cons_self - have hl := ih fun b hb => h b (List.mem_cons_of_mem _ hb) - rw [List.flatMap_cons, List.length_append, List.length_cons, Nat.succ_mul] - omega - -/-- Membership in a list as a scan of the list, the form in which polynomial-time membership tests -are certified. -/ -theorem List.decide_mem_eq_any {α : Type*} [DecidableEq α] (a : α) (l : List α) : - decide (a ∈ l) = l.any fun u => decide (u = a) := by - rw [Bool.eq_iff_iff, decide_eq_true_eq, List.any_eq_true] - simp - -/-! ### Lists as register files -/ - -/-- Reading the updated entry of a list. -/ -theorem List.getD_set_self {α : Type*} {l : List α} {i : ℕ} {x d : α} (h : i < l.length) : - (l.set i x).getD i d = x := by - rw [List.getD_eq_getElem _ _ (by simpa using h), List.getElem_set_self] - -/-- Reading another entry of an updated list. -/ -theorem List.getD_set_ne {α : Type*} {l : List α} {i j : ℕ} {x d : α} (h : i ≠ j) : - (l.set i x).getD j d = l.getD j d := by - simp only [List.getD_eq_getElem?_getD, List.getElem?_set_ne h] - -/-- A property of all the entries of a list holds of all the entries of an update by a value -having it. -/ -theorem List.forall_mem_set_of_forall_mem {α : Type*} {p : α → Prop} {l : List α} {i : ℕ} {x : α} - (h : ∀ a ∈ l, p a) (hx : p x) : ∀ a ∈ l.set i x, p a := fun a ha => by - rcases List.mem_or_eq_of_mem_set ha with ha | rfl - · exact h a ha - · exact hx - -/-- The entries of a list of numbers at most `B`, read with default `0`, are at most `B`. -/ -theorem List.getD_le_of_forall_le {l : List ℕ} {B : ℕ} (h : ∀ a ∈ l, a ≤ B) (j : ℕ) : - l.getD j 0 ≤ B := by - rw [List.getD_eq_getElem?_getD] - rcases hj : l[j]? with _ | a - · exact Nat.zero_le _ - · exact h a (List.mem_of_getElem? hj) - -/-- A defaulted lookup returns a member of the list or the default value. -/ -theorem List.getD_mem_or {α : Type*} (l : List α) (j : ℕ) (d : α) : - l.getD j d ∈ l ∨ l.getD j d = d := by - rw [List.getD_eq_getElem?_getD] - rcases h : l[j]? with _ | a - · exact Or.inr rfl - · exact Or.inl (List.mem_of_getElem? h) - -/-- Looking up the first index of a member of a list returns that member. -/ -theorem List.getD_idxOf {α : Type*} [BEq α] [LawfulBEq α] {l : List α} {x : α} (hx : x ∈ l) - (d : α) : l.getD (l.idxOf x) d = x := by - rw [List.getD_eq_getElem _ _ (List.idxOf_lt_length_iff.2 hx), List.getElem_idxOf] - -/-- Reading a mapped range at a valid index applies the map to that index. -/ -theorem List.getD_map_range {α : Type*} (f : ℕ → α) (d : α) {n i : ℕ} (hi : i < n) : - ((List.range n).map f).getD i d = f i := by - rw [List.getD_eq_getElem _ _ (by simpa using hi)] - simp - -/-- Tabulating a natural-indexed function over a range agrees with its finite coordinate view. -/ -theorem List.map_range_eq_ofFn {α : Type*} (n : ℕ) (f : ℕ → α) : - (List.range n).map f = List.ofFn (fun i : Fin n => f i.val) := by - apply List.ext_getElem (by simp) - intro i hi hi' - simp - -/-- Partitioning the elements of a list satisfying `p` by whether they satisfy `q`. -/ -theorem List.countP_and_not_add_countP_and {α : Type*} (p q : α → Prop) [DecidablePred p] - [DecidablePred q] (l : List α) : - l.countP (fun a => ¬ q a ∧ p a) + l.countP (fun a => p a ∧ q a) = l.countP (fun a => p a) := by - induction l with - | nil => rfl - | cons a l ih => - rw [List.countP_cons, List.countP_cons, List.countP_cons] - by_cases hp : p a <;> by_cases hq : q a <;> - simp only [hp, hq, not_true_eq_false, not_false_eq_true, and_true, and_false, - decide_true, decide_false, Bool.false_eq_true, ↓reduceIte] <;> omega - -/-! ### Unary headers -/ - -/-- A unary block of copies of `!a` followed by the delimiter `a` determines both its length and the -remaining suffix. -/ -theorem List.replicate_not_append_cons_inj {a : Bool} {m m' : ℕ} {l l' : List Bool} - (h : List.replicate m (!a) ++ a :: l = List.replicate m' (!a) ++ a :: l') : - m = m' ∧ l = l' := by - induction m generalizing m' <;> cases m' <;> simp_all [List.replicate_succ] - -/-- A unary block of `true` bits followed by `false` determines both its length and the remaining -suffix. -/ -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 diff --git a/Complexity/Foundations/Data/List/Counting.lean b/Complexity/Foundations/Data/List/Counting.lean new file mode 100644 index 0000000000..538186db1a --- /dev/null +++ b/Complexity/Foundations/Data/List/Counting.lean @@ -0,0 +1,55 @@ +/- +Copyright (c) 2026 Christian Reitwiessner, Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Christian Reitwiessner, Samuel Schlesinger +-/ + +module +-- upstream: candidate + +public import Complexity.Init +public import Mathlib.Data.List.Basic + +/-! +# List counts and scan bounds + +## Main results + +* `List.length_flatMap_le`: blocks of bounded length have bounded total length. +* `List.decide_mem_eq_any`: membership as a scan of the list. +* `List.countP_and_not_add_countP_and`: members satisfying one predicate split by whether + they satisfy another. +-/ + +@[expose] public section + +/-- Blocks of at most `k` elements each, one for each element of `l`, have at most `|l| k` +elements in total. -/ +theorem List.length_flatMap_le {α β : Type*} {l : List α} {f : α → List β} {k : ℕ} + (h : ∀ a ∈ l, (f a).length ≤ k) : (l.flatMap f).length ≤ l.length * k := by + induction l with + | nil => simp + | cons a l ih => + have ha := h a List.mem_cons_self + have hl := ih fun b hb => h b (List.mem_cons_of_mem _ hb) + rw [List.flatMap_cons, List.length_append, List.length_cons, Nat.succ_mul] + omega + +/-- Membership in a list as a scan of the list, the form in which polynomial-time membership tests +are certified. -/ +theorem List.decide_mem_eq_any {α : Type*} [DecidableEq α] (a : α) (l : List α) : + decide (a ∈ l) = l.any fun u => decide (u = a) := by + rw [Bool.eq_iff_iff, decide_eq_true_eq, List.any_eq_true] + simp + +/-- Partitioning the elements of a list satisfying `p` by whether they satisfy `q`. -/ +theorem List.countP_and_not_add_countP_and {α : Type*} (p q : α → Prop) [DecidablePred p] + [DecidablePred q] (l : List α) : + l.countP (fun a => ¬ q a ∧ p a) + l.countP (fun a => p a ∧ q a) = l.countP (fun a => p a) := by + induction l with + | nil => rfl + | cons a l ih => + rw [List.countP_cons, List.countP_cons, List.countP_cons] + by_cases hp : p a <;> by_cases hq : q a <;> + simp only [hp, hq, not_true_eq_false, not_false_eq_true, and_true, and_false, + decide_true, decide_false, Bool.false_eq_true, ↓reduceIte] <;> omega diff --git a/Complexity/Foundations/Data/List/Fold.lean b/Complexity/Foundations/Data/List/Fold.lean new file mode 100644 index 0000000000..d5b31b197d --- /dev/null +++ b/Complexity/Foundations/Data/List/Fold.lean @@ -0,0 +1,57 @@ +/- +Copyright (c) 2026 Christian Reitwiessner, Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Christian Reitwiessner, Samuel Schlesinger +-/ + +module +-- upstream: candidate + +public import Complexity.Init +public import Mathlib.Data.List.Basic + +/-! +# List fold invariants and selection + +## Main results + +* `List.foldl_take_invariant`: an index-dependent invariant holds after every prefix of a fold. +* `List.foldr_ite_eq_of_mem`: a chain of equality tests selects the branch of a contained tag, + regardless of duplicates or fallback. Used by finite-control certificates. + +## References + +Adapts the selection identity from `Computability/Probabilistic/Finite.lean` on the cslib +`crypto` branch at `5ff69ca93402e7c947208dc56396d6d86203ccd8`. +-/ + +@[expose] public section + +/-- An invariant depending on the number of consumed elements holds after every bounded prefix +fold if it holds initially and is preserved by the next list element. Unlike `List.foldlRecOn`, +preservation may depend on the position. This is a semantic rule with no resource assumptions. -/ +theorem List.foldl_take_invariant {α β : Type*} (l : List α) (step : β → α → β) (init : β) + (P : ℕ → β → Prop) (hbase : P 0 init) + (hstep : ∀ i (hi : i < l.length) state, P i state → P (i + 1) (step state l[i])) : + ∀ i, i ≤ l.length → P i ((l.take i).foldl step init) := by + intro i + induction i with + | zero => intro _; simpa only [List.take_zero, List.foldl_nil] using hbase + | succ i ih => + intro hi + have hlt : i < l.length := Nat.lt_of_succ_le hi + simpa only [List.take_succ_eq_append_getElem hlt, List.foldl_append, + List.foldl_cons, List.foldl_nil] using hstep i hlt _ (ih (Nat.le_of_lt hlt)) + +/-- A chain of equality tests selects a contained tag, regardless of duplicates or fallback. -/ +theorem List.foldr_ite_eq_of_mem {Tag Value : Type*} [DecidableEq Tag] + (tags : List Tag) (tag : Tag) (branch : Tag → Value) (fallback : Value) (h : tag ∈ tags) : + tags.foldr (fun candidate rest => if tag = candidate then branch candidate else rest) + fallback = branch tag := by + induction tags with + | nil => simp at h + | cons candidate tags ih => + by_cases heq : tag = candidate + · simp [heq] + · simp only [List.foldr_cons, heq, ↓reduceIte] + exact ih (List.mem_cons.mp h |>.resolve_left heq) diff --git a/Complexity/Foundations/Data/List/Lookup.lean b/Complexity/Foundations/Data/List/Lookup.lean new file mode 100644 index 0000000000..f617065553 --- /dev/null +++ b/Complexity/Foundations/Data/List/Lookup.lean @@ -0,0 +1,81 @@ +/- +Copyright (c) 2026 Christian Reitwiessner, Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Christian Reitwiessner, Samuel Schlesinger +-/ + +module +-- upstream: candidate + +public import Complexity.Init +public import Mathlib.Data.List.Basic +import Mathlib.Data.List.GetD +import Mathlib.Data.List.OfFn + +/-! +# Defaulted list lookup and updates + +## Main results + +* `List.getD_mem_or`, `List.getD_idxOf`: a defaulted lookup returns a member or the default, + and returns a member at its first index. +* `List.getD_set_self`, `List.getD_set_ne`: reading an updated entry or an unchanged entry. +* `List.forall_mem_set_of_forall_mem`, `List.getD_le_of_forall_le`: preserve invariants under + updates and bound defaulted reads of numeric register files. +* `List.getD_map_range`: read a function tabulated over a bounded range. +* `List.map_range_eq_ofFn`: runtime tabulation agrees with the finite coordinate view. +-/ + +@[expose] public section + +/-- Reading the updated entry of a list. -/ +theorem List.getD_set_self {α : Type*} {l : List α} {i : ℕ} {x d : α} (h : i < l.length) : + (l.set i x).getD i d = x := by + rw [List.getD_eq_getElem _ _ (by simpa using h), List.getElem_set_self] + +/-- Reading another entry of an updated list. -/ +theorem List.getD_set_ne {α : Type*} {l : List α} {i j : ℕ} {x d : α} (h : i ≠ j) : + (l.set i x).getD j d = l.getD j d := by + simp only [List.getD_eq_getElem?_getD, List.getElem?_set_ne h] + +/-- A property of all the entries of a list holds of all the entries of an update by a value +having it. -/ +theorem List.forall_mem_set_of_forall_mem {α : Type*} {p : α → Prop} {l : List α} {i : ℕ} {x : α} + (h : ∀ a ∈ l, p a) (hx : p x) : ∀ a ∈ l.set i x, p a := fun a ha => by + rcases List.mem_or_eq_of_mem_set ha with ha | rfl + · exact h a ha + · exact hx + +/-- The entries of a list of numbers at most `B`, read with default `0`, are at most `B`. -/ +theorem List.getD_le_of_forall_le {l : List ℕ} {B : ℕ} (h : ∀ a ∈ l, a ≤ B) (j : ℕ) : + l.getD j 0 ≤ B := by + rw [List.getD_eq_getElem?_getD] + rcases hj : l[j]? with _ | a + · exact Nat.zero_le _ + · exact h a (List.mem_of_getElem? hj) + +/-- A defaulted lookup returns a member of the list or the default value. -/ +theorem List.getD_mem_or {α : Type*} (l : List α) (j : ℕ) (d : α) : + l.getD j d ∈ l ∨ l.getD j d = d := by + rw [List.getD_eq_getElem?_getD] + rcases h : l[j]? with _ | a + · exact Or.inr rfl + · exact Or.inl (List.mem_of_getElem? h) + +/-- Looking up the first index of a member of a list returns that member. -/ +theorem List.getD_idxOf {α : Type*} [BEq α] [LawfulBEq α] {l : List α} {x : α} (hx : x ∈ l) + (d : α) : l.getD (l.idxOf x) d = x := by + rw [List.getD_eq_getElem _ _ (List.idxOf_lt_length_iff.2 hx), List.getElem_idxOf] + +/-- Reading a mapped range at a valid index applies the map to that index. -/ +theorem List.getD_map_range {α : Type*} (f : ℕ → α) (d : α) {n i : ℕ} (hi : i < n) : + ((List.range n).map f).getD i d = f i := by + rw [List.getD_eq_getElem _ _ (by simpa using hi)] + simp + +/-- Tabulating a natural-indexed function over a range agrees with its finite coordinate view. -/ +theorem List.map_range_eq_ofFn {α : Type*} (n : ℕ) (f : ℕ → α) : + (List.range n).map f = List.ofFn (fun i : Fin n => f i.val) := by + apply List.ext_getElem (by simp) + intro i hi hi' + simp diff --git a/Complexity/Logics/Propositional/Resolution/Pigeonhole.lean b/Complexity/Logics/Propositional/Resolution/Pigeonhole.lean index 93296568b0..6c4dea43b8 100644 --- a/Complexity/Logics/Propositional/Resolution/Pigeonhole.lean +++ b/Complexity/Logics/Propositional/Resolution/Pigeonhole.lean @@ -9,7 +9,7 @@ module public import Complexity.Logics.Propositional.Pigeonhole public import Complexity.Logics.Propositional.Resolution.TreeLike -import Complexity.Foundations.Data.List.Basic +import Complexity.Foundations.Data.List.Counting import Mathlib.Algebra.BigOperators.Group.Finset.Basic import Mathlib.Data.Finset.Sort import Mathlib.Tactic.Linarith diff --git a/Complexity/Logics/Propositional/Resolution/SizeWidth.lean b/Complexity/Logics/Propositional/Resolution/SizeWidth.lean index 705f32bb78..f31e0ab6ac 100644 --- a/Complexity/Logics/Propositional/Resolution/SizeWidth.lean +++ b/Complexity/Logics/Propositional/Resolution/SizeWidth.lean @@ -9,7 +9,7 @@ module public import Complexity.Logics.Propositional.Resolution.Proof public import Mathlib.Analysis.SpecialFunctions.Pow.Real -import Complexity.Foundations.Data.List.Basic +import Complexity.Foundations.Data.List.Counting import Mathlib.Algebra.BigOperators.Group.Finset.Basic /-! diff --git a/ComplexityTests/Reingold.lean b/ComplexityTests/Reingold.lean index b36a050bd1..fb2350e664 100644 --- a/ComplexityTests/Reingold.lean +++ b/ComplexityTests/Reingold.lean @@ -7,7 +7,7 @@ Authors: Samuel Schlesinger import Complexity.Algorithms.Reachability.Reingold import Complexity.Computability.Complexity.Classes.LogSpace.USTCON import Complexity.Foundations.Combinatorics.Expander.LowerBound -import Complexity.Foundations.Data.List.Basic +import Complexity.Foundations.Data.List.Append /-! # Reingold's transformation tests diff --git a/scripts/list_split_fanout.py b/scripts/list_split_fanout.py new file mode 100644 index 0000000000..5753b35b59 --- /dev/null +++ b/scripts/list_split_fanout.py @@ -0,0 +1,70 @@ +#!/usr/bin/env python3 +"""Compare #573's list-topic transitive importers over the base's fixed library universe. + +Uses the existing native Lean header parser and shared quality-report graph calculation. +Counts source-import reach, not actual rebuilds, cache hits or elapsed build time. +""" + +import argparse +import io +from pathlib import Path +import subprocess +import tarfile +import tempfile + +from quality_report import transitive_importers +from quick_check import imports_from_lean + +ROOT = Path(__file__).resolve().parents[1] +PREFIX = "Complexity.Foundations.Data.List." +TOPICS = ("Append", "Counting", "Fold", "Lookup") + + +def snapshot(ref: str, destination: Path) -> dict[str, list[tuple[str, bool]]]: + archive = subprocess.check_output(["git", "archive", ref, "Complexity"], cwd=ROOT) + sources = {} + with tarfile.open(fileobj=io.BytesIO(archive)) as files: + for entry in files: + if entry.isfile() and entry.name.endswith(".lean"): + path = destination / entry.name + path.parent.mkdir(parents=True, exist_ok=True) + path.write_bytes(files.extractfile(entry).read()) + sources[str(path)] = entry.name[:-5].replace("/", ".") + parsed = imports_from_lean(ROOT, list(sources)) + # Publicness does not affect transitive source-import reach. + return {sources[path]: [(module, False) for module in modules] + for path, modules in parsed.items()} + + +def fixed_scope_counts(base: dict, head: dict) -> tuple[int, dict[str, int]]: + """Walk all head edges, including new modules, then count only original library modules.""" + scope = set(base) + before, after = transitive_importers(base), transitive_importers(head) + return len(before[PREFIX + "Basic"] & scope), { + topic: len(after[PREFIX + topic] & scope) for topic in ("Basic", *TOPICS)} + + +def main() -> None: + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--base", required=True, help="original library revision") + parser.add_argument("--head", default="HEAD", help="committed split revision") + args = parser.parse_args() + refs = [subprocess.check_output(["git", "rev-parse", "--verify", ref + "^{commit}"], + cwd=ROOT, text=True).strip() + for ref in (args.base, args.head)] + with tempfile.TemporaryDirectory(prefix="list-split-fanout-") as temporary: + base = snapshot(refs[0], Path(temporary) / "base") + head = snapshot(refs[1], Path(temporary) / "head") + missing = {PREFIX + topic for topic in ("Basic", *TOPICS)} - head.keys() + if missing: + parser.error("head lacks split modules: " + ", ".join(sorted(missing))) + before, after = fixed_scope_counts(base, head) + print(f"Base {refs[0]}; head {refs[1]}") + print(f"Fixed original library scope: {len(base)} modules") + print(f"Before Basic: {before} transitive importers") + for topic, count in after.items(): + print(f"After {topic}: {count} transitive importers") + + +if __name__ == "__main__": + main() diff --git a/scripts/test_list_split_fanout.py b/scripts/test_list_split_fanout.py new file mode 100644 index 0000000000..e6c1cd47ce --- /dev/null +++ b/scripts/test_list_split_fanout.py @@ -0,0 +1,24 @@ +"""The split comparison must retain traversal through modules outside its counting universe.""" + +import unittest + +from list_split_fanout import PREFIX, TOPICS, fixed_scope_counts + + +class FixedScopeTests(unittest.TestCase): + def test_new_bridge_is_walked_but_not_counted(self): + basic, fold = PREFIX + "Basic", PREFIX + "Fold" + base = {basic: [], "Client": [(basic, False)], "Unrelated": []} + head = {basic: [(PREFIX + topic, True) for topic in TOPICS], + **{PREFIX + topic: [] for topic in TOPICS}, + "NewBridge": [(fold, False)], "Client": [("NewBridge", False)], + "Unrelated": []} + before, after = fixed_scope_counts(base, head) + self.assertEqual(before, 1) + self.assertEqual(after["Fold"], 2) # Original Basic and Client, not NewBridge. + self.assertEqual(after["Lookup"], 1) + self.assertEqual(after["Basic"], 0) + + +if __name__ == "__main__": + unittest.main() From 4fdda30d958736503ef06e82d0d97a2c7d27f1d5 Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Fri, 23 Oct 2026 21:55:09 -0400 Subject: [PATCH 2/3] refactor(list): finish consumer imports after the documentation merge Narrow the remaining Coloring, USTCON and TreeEval imports after #656 lands. Give both actual Geography clients explicit Counting imports and remove the unused broad public re-export. Preserve all merged documentation. Add old-Basic-only anonymous clients for all sixteen original theorem names. Refs #573. AI assistance: OpenAI Codex worker codex-review-559 under coordinator-codex-01a16ab8. --- .../Space/GeneralizedGeography/Reduction.lean | 1 + .../Complexity/Problems/Coloring.lean | 2 +- .../Problems/GeneralizedGeography.lean | 1 - .../Complexity/Problems/USTCON.lean | 2 +- .../Computability/TreeEval/Encoding.lean | 2 +- ComplexityTests.lean | 1 + ComplexityTests/ListBasicImports.lean | 33 +++++++++++++++++++ 7 files changed, 38 insertions(+), 4 deletions(-) create mode 100644 ComplexityTests/ListBasicImports.lean diff --git a/Complexity/Computability/Complexity/Classes/Space/GeneralizedGeography/Reduction.lean b/Complexity/Computability/Complexity/Classes/Space/GeneralizedGeography/Reduction.lean index fc0171ed22..1912061270 100644 --- a/Complexity/Computability/Complexity/Classes/Space/GeneralizedGeography/Reduction.lean +++ b/Complexity/Computability/Complexity/Classes/Space/GeneralizedGeography/Reduction.lean @@ -12,6 +12,7 @@ public import Complexity.Computability.Complexity.Classes.Space.TQBF.Prenex import Complexity.Computability.Complexity.Classes.Space.TQBF.PolyTime import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.List import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat +import Complexity.Foundations.Data.List.Counting /-! # Generalized Geography is `PSPACE`-hard diff --git a/Complexity/Computability/Complexity/Problems/Coloring.lean b/Complexity/Computability/Complexity/Problems/Coloring.lean index 27dc45189f..99defe25d9 100644 --- a/Complexity/Computability/Complexity/Problems/Coloring.lean +++ b/Complexity/Computability/Complexity/Problems/Coloring.lean @@ -14,7 +14,7 @@ import Complexity.Computability.Complexity.CookLevin.Completeness import Complexity.Computability.Complexity.Problems.SAT.PolyTime import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.List import Complexity.Computability.Machines.Turing.MultiTape.Complexity.PolyTime.Nat -import Complexity.Foundations.Data.List.Basic +import Complexity.Foundations.Data.List.Counting import Mathlib.Data.List.GetD /-! diff --git a/Complexity/Computability/Complexity/Problems/GeneralizedGeography.lean b/Complexity/Computability/Complexity/Problems/GeneralizedGeography.lean index 8198f4029d..871509a3c6 100644 --- a/Complexity/Computability/Complexity/Problems/GeneralizedGeography.lean +++ b/Complexity/Computability/Complexity/Problems/GeneralizedGeography.lean @@ -8,7 +8,6 @@ module -- upstream: candidate public import Complexity.Computability.Complexity.Problems.IndependentSet -public import Complexity.Foundations.Data.List.Basic /-! # Generalized Geography diff --git a/Complexity/Computability/Complexity/Problems/USTCON.lean b/Complexity/Computability/Complexity/Problems/USTCON.lean index a6f73b9c6e..ff48482184 100644 --- a/Complexity/Computability/Complexity/Problems/USTCON.lean +++ b/Complexity/Computability/Complexity/Problems/USTCON.lean @@ -12,7 +12,7 @@ public import Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected public import Mathlib.Data.List.OfFn public import Mathlib.Data.List.GetD public import Mathlib.Data.Nat.Size -import Complexity.Foundations.Data.List.Basic +import Complexity.Foundations.Data.List.Append /-! # Undirected s–t connectivity diff --git a/Complexity/Computability/TreeEval/Encoding.lean b/Complexity/Computability/TreeEval/Encoding.lean index ef64de169a..5ad02ff61f 100644 --- a/Complexity/Computability/TreeEval/Encoding.lean +++ b/Complexity/Computability/TreeEval/Encoding.lean @@ -9,7 +9,7 @@ module public import Complexity.Computability.TreeEval.Basic public import Mathlib.Data.List.OfFn -import Complexity.Foundations.Data.List.Basic +import Complexity.Foundations.Data.List.Append /-! # Bit encodings of Tree Evaluation instances diff --git a/ComplexityTests.lean b/ComplexityTests.lean index a0ca689226..de43a7caf1 100644 --- a/ComplexityTests.lean +++ b/ComplexityTests.lean @@ -214,6 +214,7 @@ import ComplexityTests.KeyedSort import ComplexityTests.KolmogorovCrypto import ComplexityTests.Ladner import ComplexityTests.LinearHash +import ComplexityTests.ListBasicImports import ComplexityTests.ListEnumeration import ComplexityTests.ListZipIdx import ComplexityTests.LogSpace diff --git a/ComplexityTests/ListBasicImports.lean b/ComplexityTests/ListBasicImports.lean new file mode 100644 index 0000000000..1f43676cad --- /dev/null +++ b/ComplexityTests/ListBasicImports.lean @@ -0,0 +1,33 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +-- upstream: local-only (list import regression tests) + +import Complexity.Foundations.Data.List.Basic + +/-! # The combined list import + +Every original theorem remains usable from the old `Basic` import alone. The anonymous clients +check elaborated references, so dropping a topic from the re-export fails without another topic +import masking it. Actual library consumers use the narrow topic modules. +-/ + +example := @List.zip_tail_append_cons +example := @List.foldl_take_invariant +example := @List.foldr_ite_eq_of_mem +example := @List.length_flatMap_le +example := @List.decide_mem_eq_any +example := @List.getD_set_self +example := @List.getD_set_ne +example := @List.forall_mem_set_of_forall_mem +example := @List.getD_le_of_forall_le +example := @List.getD_mem_or +example := @List.getD_idxOf +example := @List.getD_map_range +example := @List.map_range_eq_ofFn +example := @List.countP_and_not_add_countP_and +example := @List.replicate_not_append_cons_inj +example := @List.replicate_true_append_false_inj From 77b117661604ac32e6c261819571b7179b0ffee3 Mon Sep 17 00:00:00 2001 From: Samuel Giuseppe Schlesinger Date: Fri, 23 Oct 2026 22:03:49 -0400 Subject: [PATCH 3/3] doc(list): point roadmap and upstream notes to the topic homes Apply only the two coordinated location-reference updates for #573. All Lean, configuration and test source remains identical to the six-gate-validated 4fdda30d checkpoint. --- ROADMAP.md | 2 +- UPSTREAM.md | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/ROADMAP.md b/ROADMAP.md index 2955115401..538904d186 100644 --- a/ROADMAP.md +++ b/ROADMAP.md @@ -1426,7 +1426,7 @@ space bounds. Further class-level work needs resource certificates for the actua * Reingold's theorem: [USTCON ∈ L and SL = L](Complexity/Computability/Complexity/Classes/LogSpace/USTCON.lean) are proved for the adjacency-matrix encoding (with `SL` defined by logspace many-one reducibility to `USTCON`, completeness of `USTCON` for `SL` and `L`, and the unary-header injectivity lemma - shared with `TreeEval` in [List/Basic.lean](Complexity/Foundations/Data/List/Basic.lean)); a + shared with `TreeEval` in [List/Append.lean](Complexity/Foundations/Data/List/Append.lean)); a symmetric-Turing-machine model of `SL` and an edge-list variant of `USTCON` by a logspace reduction remain; * Native [NL = coNL](Complexity/Computability/Complexity/Classes/LogSpace/Complement.lean) is diff --git a/UPSTREAM.md b/UPSTREAM.md index b31b3bc127..ece6da48bf 100644 --- a/UPSTREAM.md +++ b/UPSTREAM.md @@ -195,7 +195,7 @@ agreement during upstream review. | `Computability/Circuit/{Unfolding,MapOp}`, `Computability/Circuit/Encoding/MapOp` | Consider integrating into `Circuit/Formula`, `Circuit/Program`, and `Circuit/Encoding`, respectively. | | `Computability/Circuit/Boolean/FirstOrder` | Consider a descriptive-complexity directory. | | `Foundations/Data/BitString/{Agree,Block,Hoeffding}` | Add to CSLib's `Foundations/Data/BitString`. | -| `Foundations/Data/List/Basic` | `List.getD_idxOf`, `List.countP_and_not_add_countP_and` and register-file/unary-header helpers; consider Mathlib's `Data/List/GetD` and `Data/List/Basic`. | +| `Foundations/Data/List/{Fold,Lookup,Counting,Append}` | Fold invariants, lookup and register-file bounds, predicate counts, and append identities including unary headers; `Basic` reexports these topics. Consider Mathlib's `Data/List/GetD` and `Data/List/Basic`. | | `Foundations/Relation/RelatesWithinSteps` | `Function.iterate_trans` and bounded reachability helpers; consider Mathlib's `Logic/Function/Iterate` and `Logic/Relation`. | | `Foundations/BooleanAnalysis/Fourier` | Consider Mathlib beside `Analysis/Fourier/FiniteAbelian`. | | `Foundations/BooleanAnalysis/{Bernoulli,CoordinateSampling,Fibers,HarmonicMean,LightPatterns,MirrorSets}`, `Foundations/Analysis/HarmonicMean` | Consider Mathlib probability APIs; generic finite-type `harmonicMean` is split into `Foundations/Analysis/HarmonicMean` (#317). |