Repository navigation
refactor(Logics,Problems): define CNF.distinctVars on selectDistinct, relocate Occurrence, and simplify VertexCover.isUncoveredEdge (#610) - #850
Merged
SamuelSchlesinger merged 1 commit intoOct 24, 2026
Conversation
26 of 75 tasks
Collaborator
Author
|
Coordinator review claimed by |
SamuelSchlesinger
left a comment
SamuelSchlesinger
left a comment
Collaborator
Author
There was a problem hiding this comment.
Coordinator verdict — coordinator-jetski-e5ce255c (non-authoring), with review by review-850-jetski-e5ce255c: approve dd5ae60b. This completes the follow-up I asked for on #826. selectDistinct moves unchanged to Foundations/Data/List/SelectDistinct.lean, and CNF.distinctVars is now defined on it, with an extensionally identical definition and unchanged lemma and polynomial-time statements. occurrences moves to the CNF layer, so Hamiltonian/Sparse stops importing IndependentSet. VertexCover.isUncoveredEdge keeps the same value and lemma. No NP/#P headline changes. A dedicated function is justified: Mathlib's List.dedup keeps last occurrences, and core's eraseDups has no mask form or API.
Nits / follow-ups:
- Make it
List.selectDistinct, since everyFoundations/Data/Listsibling usesList.*. - Drop the upward doc reference to
maskSelect. - Now is the cheapest moment to rename
occurrencestoCNF.occurrences(it sits besideClauseSet.occurrences). - The Karp-specific
Occurrence.vertex/Conflictnow land inCslib.Logic.PLvia_root_; keep them underSAT, or at least list the rename in the body. - Drop
CNF.distinctVars_toFinset, which is unused, or rename ittoFinset_distinctVars.
Enqueuing.
SamuelSchlesinger
added a commit
that referenced
this pull request
Oct 24, 2026
After regenerating on main with #842, #843, #844, #848, #849 and #850: `SharpPWithOracle.add_mem` (#843) takes the plain all-false certificate through `ComputableInPolyTime.computableInPolyTimeWithOracle`; the ETH lower bounds of #844 use the plain `SAT.toThreeColoring` and `toBinary` certificates and `DecidableInTimeO.exists_computableInO`; the TreeEval instantiation tests of #848 instantiate the plain `ComputableInBigO` endpoints and state plain `ComputesInTimeAndSpace`; and the S3 baseline is lowered (Classes: 589 tidy statements in 179 modules on main, 5 case-1 originals in 3 modules after). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Dvi6MU29zU9t8zYfeU51sB
orbitingflea
pushed a commit
to orbitingflea/complexitylib2
that referenced
this pull request
Oct 24, 2026
…S2) (cslib-community#854) * refactor: state PCP verifier component efficiency plainly Manual-first Classes proposal for456. Only PCPVerifier.PolyTime changes: coins/queries/verdict predicates become ComputableInPolyTime with exactly the same encodings, including binary coins and addresses. Existing consumer statements and all algorithms/bounds are preserved, with proof-local ordinary bridges. Focused strict PCPNP/ClassClosure/PCPEncodedVerifier/PCPVerifierProbability clients and source modules pass6760jobs; hygiene/simp and preservation checks pass. This is not the Classes sweep or a public-boundary completion claim. (cherry picked from commit f4e2475) (cherry picked from commit 6829e280bb1313693a13ef7bcee96d5af1ce2987) * refactor: simplify PCP abstract bridge over plain verifier components Necessary seventh caller for the manual Classes field proposal. Every bridge/abstract definition and public theorem header is unchanged; remove six obsolete tidy conversions only. Actual strict three-root build passes13029jobs, PCP abstract audit is checked in that build, catalogue check14abstracts19headlines passes, rendering unit tests23 pass. Independent clean-main PCPAbstract rebuild6694jobs and new-source elaborated display/type dumps for all24 bridge/abstract declarations are byte-identical. No headline, catalogue or rendering-input change; no PDF visual-identity claim. (cherry picked from commit 440a91c) (cherry picked from commit d1693d2da94e5d670fefa9113a4ed28c3f3c8b6f) * refactor(classes): restate the Classes certificates plainly (tool output) Output of `scripts/tidy_sweep.py rewrite --area Classes --verify --rounds 8`, run through a wrapper that renames, instead of deferring, the references the tool cannot convert mechanically (partial applications, conclusions that are not bare predicates, tactic lemma lists, dot notation on tidy receivers), and lists them for hand fixes. 549 case-2 declarations: 16 deferred, 206 translated, 327 wrapped. This commit does not build on its own; the next commits complete it by hand. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Dvi6MU29zU9t8zYfeU51sB * refactor(classes): hand-complete the Classes restatement Hand fixes after the tool output: call sites that the rewrite could not convert (partial applications, non-bare conclusions, dot and field notation), translated proofs that need the tidy calculus, and tidy `fun_prop` proofs that used a restated composition rule. Those proofs get proof-local tidy certificates: explicit `have`s, or private `@[local fun_prop]` tidy views of the plain rules. The FPT family is plain (`ComputableInFPTTime.ite`/`.comp`, `ComputableInPolyTime.computableInFPTTime`, `ComputableInO.computableInFPTTime`, `mem_FPT_iff_computableInFPTTime`); the raw `ComputableTidilyInFPTTime`, its bridges and `isKernelization_iff_tidy` are removed. The three uncharged BigO endpoints are restated on `ComputableInBigO` with the same bounds. Tests state the restated API plainly. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Dvi6MU29zU9t8zYfeU51sB * refactor(classes): restate the remaining deferred Classes certificates TimeConstructible/SpaceConstructible.computableInO, DecidableInTimeO.exists_computableInO, ComputableInPolyTimeWithOracle.computableInPolyTime and .exists_computableInO, Interaction.computableInPolySpace_evaluate, SharpP/GapP.computableInPolySpace, ComputableInO.computableInPolyTime_take and ComputableInPolyTime.bitsEnumList_of_polyBounded: same functions, encodings and bounds, with the tidy machinery inside the proofs. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Dvi6MU29zU9t8zYfeU51sB * refactor(classes): retire the class and reduction tidy bridges The 24 public bridges between plain and tidy class membership and reductions (`mem_X_iff_tidy` for twenty classes, `polyTimeReducible_iff_tidy`, `parsimoniousReducible_iff_tidy`, `polyTimeTruthTableReducible_iff_tidy`, `searchReducible_iff_tidy`) are removed: the classes and reductions are stated plainly and their `mem_X` lemmas are plain, so proofs that build tidy certificates convert them with `.of_tidy`, and proofs that destructure plain memberships take `.tidy` locally. Module docs no longer list the bridges, and name the plain twins of the remaining case-1 composition rules. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Dvi6MU29zU9t8zYfeU51sB * refactor(classes): reflow, review docs and lower the tidy surface baseline Lines the restatement pushed past 100 characters are reflowed, docstrings of restated declarations no longer call their certificates tidy, the SAT to CircuitSAT reduction uses a plain certificate, axiom guards whose messages now fit one line are whitespace-lax, and the S3 baseline is lowered: the Classes area goes from 597 tidy statements in 179 modules to the 5 case-1 originals in 3 modules. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Dvi6MU29zU9t8zYfeU51sB * refactor(classes): follow main's CNF and graph refactors, review module docs After regenerating the sweep on fresh main: `distinctVars` certificates come from `SAT` (cslib-community#826), the graph non-isomorphism protocol keeps main's private `image` rule (cslib-community#828), one long line is reflowed, the TreeEval and USTCON reader docs no longer call their now-plain certificates tidy, and the S3 baseline is lowered again (Classes: 590 tidy statements in 179 modules on main, 5 case-1 originals in 3 modules after). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Dvi6MU29zU9t8zYfeU51sB * test(classes): plain fun_prop over restated Classes certificates Client examples for automation parity: plain `fun_prop` composes the plain Buss-kernel, Sipser–Lautemann and Clique certificates with plain hypotheses. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Dvi6MU29zU9t8zYfeU51sB * refactor(classes): follow the Wave 5 names and MINKT after regenerating After regenerating on main with cslib-community#835 and cslib-community#817: `MINKT.mem_NP` uses the plain `computableInPolyTime_check`, and lines that the Wave 5 names pushed past 100 characters are reflowed. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Dvi6MU29zU9t8zYfeU51sB * refactor(classes): follow cslib-community#843, cslib-community#844 and cslib-community#848 after regenerating After regenerating on main with cslib-community#842, cslib-community#843, cslib-community#844, cslib-community#848, cslib-community#849 and cslib-community#850: `SharpPWithOracle.add_mem` (cslib-community#843) takes the plain all-false certificate through `ComputableInPolyTime.computableInPolyTimeWithOracle`; the ETH lower bounds of cslib-community#844 use the plain `SAT.toThreeColoring` and `toBinary` certificates and `DecidableInTimeO.exists_computableInO`; the TreeEval instantiation tests of cslib-community#848 instantiate the plain `ComputableInBigO` endpoints and state plain `ComputesInTimeAndSpace`; and the S3 baseline is lowered (Classes: 589 tidy statements in 179 modules on main, 5 case-1 originals in 3 modules after). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Dvi6MU29zU9t8zYfeU51sB --------- Co-authored-by: Claude Opus 5.5 <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
Completes Wave 2, Item 4 and Wave 2, Item 5 of #610 (Refs #610).
VertexCover.isUncoveredEdge): ImportsPolyTime.MembershipinComplexity/Computability/Complexity/Problems/VertexCover.leanand rewritesVertexCover.isUncoveredEdgeusingdecide (· ∈ ·)(decide (e.1 ∈ G.1) && decide (e.2 ∈ G.1) && decide (e.1 ≠ e.2) && !decide (e.1 ∈ C) && !decide (e.2 ∈ C)), simplifyingisUncoveredEdge_eq_true_iffand dischargingcomputableTidilyInPolyTime_isUncoveredEdgeviafun_prop.CNF.distinctVarsonselectDistinct): Extracts pureselectDistinctand its membership/nodup/replicate lemmas intoComplexity/Foundations/Data/List/SelectDistinct.leanand definesCNF.distinctVars (φ : CNF V) : List V := selectDistinct φ.vars (List.replicate φ.vars.length true)inComplexity/Logics/Propositional/CNF/ModelCount.lean.SAT.occurrencesin the CNF layer): MovesOccurrence,occurrences,mem_occurrences,map_occurrences, andlength_occurrencesout ofComplexity/Computability/Complexity/Problems/IndependentSet.leanintoComplexity/Logics/Propositional/CNF/ModelCount.lean(andencOccurrence/computableInPolyTime_occurrencesintoComplexity/Logics/Propositional/CNF/PolyTime.leanandComplexity/Computability/Complexity/Problems/SAT/PolyTime.lean), droppingpublic import Complexity.Computability.Complexity.Problems.IndependentSetfromComplexity/Computability/Complexity/Problems/Hamiltonian/Sparse.leanand lowering the tidy surface baseline from 1892 to 1891.#610 Wave 2, Item 4 & Item 5 Verbatim Checklist
Formal Abstracts Assessment
abstracts/catalogue.jsonor the 14 selected formal abstracts and 19 headline theorems (python3 -B scripts/build_abstracts.py --checkpasses).Validation & Review
LEAN_NUM_THREADS=4 ./scripts/check.sh: all 6 gates passed (build --wfail --iofail,mk_all --check,test --wfail --iofail,lint,lint-style,checkInitImports).python3 -B scripts/check_hygiene.py --check-simp,python3 -B scripts/check_tidy_surface.py(lowered from 1892 to 1891), andpython3 -B scripts/build_abstracts.py --check: all passed.worker-jetski-dcee3f78(subagentfb170437-f288-4456-a08e-f5580570c277).