refactor(book): restructure chapters, extract Proof.lean, and fix the generated project

[arademaker]

The restructuring agreed in September 2026, and the defects it uncovered.
Closes #3 and its five children (#8, #9, #10, #11, #12) — already closed with
their evidence — and #22.

The book's spine

The chapter order is now IntroCS, IntroL, Logic, Sets, SeaBattle,
Morphology, InfEngine, English. Mastermind is dropped (it announced a
semantics in propositional logic it never delivered), SeaBattle is promoted
to a chapter, and Games is gone.

Prop and the tactics were presented in three places. They are now presented
once, in a new CSwL/Logic/Proof.lean, which absorbs IntroL's "O tipo Prop e
Provas", PL's "Lógica Proposicional em Lean" and FOL's "As regras dos
quantificadores". Logic holds Proof, PL, FOL in that order; IntroL is
now about Lean as a programming language, keeping only the example/theorem/
rfl kernel that Morphology needs before Logic.

FOL gained a computable Formula.eval and the bridge into Prop that PL
already had, so the two chapters now have the same three-part shape: syntax as
data, computable semantics, and the theorem relating the two readings.

The generated project never compiled

Building the extracted project for the first time showed it had never worked.
This is the part worth reviewing closely, since the diagnosis in #22 turned out
to be wrong on both counts and the emitter was never at fault:

• gapShip sat in the same ```lean +error fence as the definition meant to
  fail, so in the extracted project it was scoped inside an
  sf_expect_failure block while three examples used it at file scope.
• Three solution! uses were written in a shape that only survives while the
  marker is there — a structure instance aligned against a column the marker
  created, and tactic blocks parenthesised rather than indented. As a tactic
  solution! is replaced by all_goals, so the block must suit a single goal;
  vestidos₁ had its rcases outside the marker and its bullets inside.
• An import was dropped in silence because file := "introL" no longer matched
  import CSwL.IntroL, surfacing three chapters away as
  Unknown identifier IntroL.initS.

make now builds the generated solutions project (verify := true for that
variant alone), so a book that compiles while the student's project does not
fails loudly. The two reasons recorded for keeping that check off were stale
and are replaced with measurements: the toolchains now match, and Mathlib is
not rebuilt on every make — it is 7.5 GB vendored once, ~3 s incrementally.

Output that mirrors the source

Each section of Logic gets its own HTML page, and — following the principle
that the Lean output should mirror the source's file organisation — its own
generated module:

_out/<variant>/lean/CSwL/Logic.lean          glue
_out/<variant>/lean/CSwL/Logic/{Proof,PL,FOL}.lean

replacing one 1819-line file. The criterion is file :=, so a chapter whose
sections do not set it is untouched (Morphology is opt-in later). Each
section keeps the imports its own header declares. The silent import-dropping
path is now an error naming the file and the cause.

Checks

• make all clean; the generated solutions and grading projects build with
  zero errors.
• The split Lean was diffed against the previous single file: identical except
  that each section's headings rise one level, as a file's own headings should.
• The STYLE-CODE.md ledger was rescanned rather than patched; five rows were
  wrong. native_decide is first met in Logic/PL, two chapters before the
  ledger claimed, and is still presented nowhere — recorded in "Known gaps",
  which changes Lean features used without being presented #7's picture of the same defect.

Note for the reviewer

student and terse generated projects still fail to build, by design: their
answers are sorry. Only solutions is verified.

Three sorrys remain in the sources (Sets.lean:258, :272,
Proof.lean:158). All predate this branch and are deliberate exercise
placeholders, though Proof.lean:158 reads as a proved theorem that is not —
worth a separate decision.

AI-usage disclosure: the work in this branch was carried out with the
assistance of Claude Opus 5 (Anthropic, September 2026, via Claude Code). The
author set the direction throughout — the chapter order, the decision that the
solution! failures were misuse rather than a macro defect, the principle that
the Lean output should mirror the source — and revised the prose. The assistant
diagnosed the extraction defects, wrote the saver changes, and ran the
verification. The author takes full responsibility for the final content.

[Copilot]

🟡 Changes recommended

Unresolved critical build, extraction, and semantic issues remain, along with moderate correctness issues.

Get a fresh assessment by requesting another Copilot review.

Pull request overview

This PR restructures the book, consolidates proof material under Logic, adds computable FOL semantics, and improves generated-project extraction.

Changes:

• Reorders chapters, promotes SeaBattle, removes Games/Mastermind, and narrows IntroL.
• Adds Logic/Proof.lean and splits generated Logic modules.
• Updates extraction validation, documentation, and project verification.

File summaries

File	Summary and final comments
STYLE-CODE.md	Updates the feature ledger and extraction guidance. Three nits: inaccurate Proof description (2 votes), omitted linarith (1), and omitted Proof from the split example (1).
README.md	Updates project organization. One nit (1): document Logic/Proof.lean.
PROVENANCE.md	Updates provenance inventory. One nit (3): regenerate the incorrect count and stale identifiers/paths.
DEVIATIONS.md	Documents restructuring. Four nits (2, 3, 1, 1): stale SeaBattle, IntroL, Morphology, and migration descriptions.
CSwLMeta/Save/Project.lean	Adds generated-project validation and import checks; no final comments.
CSwLMeta/Save/Extract.lean	Adds section-level generated modules; no final comments.
CSwL/Sets.lean	Updates exercise extraction; no final comments.
CSwL/SeaBattle.lean	Promotes SeaBattle and adjusts extraction scope. One critical comment (1): exposed examples still use incompatible term-form solution markers.
CSwL/Morphology.lean	Updates chapter integration; no final comments.
CSwL/Logic/Proof.lean	Consolidates proof material. Two critical comments (1 each), one moderate (3), and four nits (2, 1, 1, 1): solution-marker extraction failures, an unproved theorem, spelling errors, and an untracked linarith example.
CSwL/Logic/PL.lean	Refactors propositional semantics. Three critical comments (3, 3, 1), two moderate (3, 2), and four nits (1 each): invalid Boolean operators/types, valuation pairing, insufficient testing, and solution-marker formatting.
CSwL/Logic/FOL.lean	Adds computable FOL semantics. One nit (1): align the model introduction with the predicates actually used.
CSwL/Logic.lean	Provides Logic glue; no final comments.
CSwL/IntroL.lean	Narrows IntroL to programming-language material; no final comments.
CSwL/Games/Mastermind.lean	Removes Mastermind material; no final comments.
CSwL/Games.lean	Removes obsolete Games glue; no final comments.
Book.lean	Applies the revised chapter order; no final comments.
Bib.lean	Adds supporting references; no final comments.

Review details

Suppressed comments (17)

CSwL/Logic/FOL.lean:396

• The model introduced below is not limited to P, R, and S: int0 interprets eight named predicates (Girl, Boy, Princess, Dwarf, Giant, Child, Love, and Defeat). As written, the semantic setup describes a different language from the one the examples evaluate; align this introduction with the concrete model.

Por conveniência, nos limitamos a um fragmento de língua com apenas três letras de predicado: `P` (unário), `R` (binário), e `S` (ternário).

Como deve ser uma estrutura extralinguística para as constantes `P`, `R` e `S`? Tal estrutura deve conter ao menos um domínio de discurso `D`, formado por entidades individuais, com uma interpretação para `P`, para `R` e para `S`. Essas interpretações são dadas por uma função `Interp`, que a cada nome de predicado e a cada lista de elementos do domínio associa um valor de verdade.

CSwL/Logic/PL.lean:354

• This proof uses the parenthesized by solution!(native_decide) shape instead of the standalone indented tactic form required by STYLE-CODE.md:184-188. Use an indented solution! block so the source follows the extraction contract consistently.

example : Form.impliesL [depo1, depo2, depo3] banguSolution = true :=
  by solution!(native_decide)

CSwL/Logic/PL.lean:247

• These proofs use the parenthesized by solution!(decide) shape instead of the standalone indented tactic form required by STYLE-CODE.md:184-188. Use an indented solution! block so the source follows the extraction contract consistently.

example : form3.eval vs1 = true := by solution!(decide)
example : form4.eval vs1 = true := by solution!(decide)
example : form5.eval vs2 = true := by solution!(decide)

CSwL/Logic/PL.lean:289

• This marker is also used in the parenthesized form inside a tactic proof. STYLE-CODE.md:184-188 requires tactic answers to use standalone indentation; change the marker to an indented block rather than relying on the term-shaped form.

  solution!(native_decide)

CSwL/Logic/PL.lean:318

• This native_decide proof uses solution!(…) as a tactic block, but the repository's extraction convention requires the standalone indented tactic form. Put the marker on its own line and indent native_decide beneath it.

  solution!(native_decide)

CSwL/Logic/Proof.lean:171

• Correct the spelling of tatica to tática.

A regra de introdução de `→` diz que para provar `P → Q`, supomos `P` e derivamos `Q`. A tatica `intro` move o antecedente para as hipóteses. A regra de eliminação é a chamada regra *modus ponens*. De `P → Q` e de `P`, conclua `Q`. Em Lean isso é aplicação `h hP` já é a prova de `Q`. A tática `apply` faz o mesmo de trás para frente, ela transforma o objetivo `Q` no objetivo `P`. A {tactic}`exact` fecha a prova indicando a hipótese cujo tipo corresponde ao _goal_ aberto. A {tactic}`assumption` fecha o _goal_ quando o tipo de alguma das hipóteses corresponde ao tipo do _goal_, sem precisarmos passar a hipótese nominalmente, como quando usamos {tactic}`exact`.

CSwL/Logic/Proof.lean:57

• Correct the spelling of identificas to idênticas.

A tática {tactic}`rfl` tem limitações, embora possamos provar que duas funções são identificas a menos da sua mudança nos nomes dos parâmetros, precisamos do teorema sobre a comutatividade dos naturais para provar o segundo exemplo.

CSwL/Logic/Proof.lean:354

• This tactic solution is still written as solution!(…); after marker stripping it is not the required standalone indented tactic block, so the generated solutions source can fail even though the book source elaborates with the marker. Use the standalone tactic form.

  solution!(
    intro hp
    apply h2
    apply h
    exact hp)

CSwL/Logic/Proof.lean:532

• This newly added non-solution example uses linarith, but the Logic/Proof row in STYLE-CODE.md does not record it and the recap below lists other tactics instead. Either record its presentation/first use in the ledger or replace this example with a tactic already accounted for, so the feature ledger remains accurate.

    linarith

CSwL/Logic/Proof.lean:368

• This is another tactic solution written as solution!(…) after by, contrary to the standalone indented form required by the saver. In the extracted solutions it does not have the intended all_goals block shape; move solution! to its own line and indent all tactics beneath it.

  solution!(
    intro h
    unfold E at h
    linarith)

CSwL/Logic/Proof.lean:381

• This proof has the same parenthesized tactic-marker shape. Keep the entire tactic sequence inside one standalone indented solution! block so the generated solution replaces the marker with all_goals without changing the block's structure.

  solution!(
    intro h
    unfold E at h
    obtain ⟨h1, h2⟩ := h
    rewrite [h1,h2]

CSwL/SeaBattle.lean:302

• Closing the +error block here exposes the following exercise examples to the extracted solutions project, but those examples still use term-form solution!(by native_decide). The teacher rewrite removes only solution!, producing parenthesized tactic terms such as (by native_decide), which is the generated-project failure reported for addShip; rewrite these examples using the indented tactic form (or fix the term-marker emitter) before enabling verification.
  DEVIATIONS.md:92
• The dependency rationale says all Morphology proofs are rfl, but CSwL/Morphology/SwedishPlural.lean:69 and :72 still use native_decide. This makes the chapter-order documentation false and hides the same known ledger gap this PR records; qualify the statement with those two exceptions.

`Morphology.lean` requires only `IntroL.lean` — its three sections are programs, and the proofs in them are `rfl` on concrete values. It is placed after `SeaBattle.lean` rather than at its old position right after `IntroL.lean` so that its exercises may use the tactics `Logic.lean` presents, rather than being confined to what `IntroL.lean` alone allows.

DEVIATIONS.md:335

• This migration note is stale after moving Morphology after Logic: it says every feature must have been presented in IntroL, while the surrounding rationale explicitly allows the chapter to use tactics from Logic and the sources include later/solution-only features. Point the check at the actual ledger/order instead.

*Migration*: check that every Lean feature used here was presented in `IntroL.lean`.

README.md:72

• The file-organization example omits the newly extracted CSwL/Logic/Proof.lean, even though Proof is the first included section and has its own generated module. Include it so the README describes all three Logic section files.

(`CSwL/Logic/PL.lean`, `CSwL/Logic/FOL.lean`) — the same pattern

STYLE-CODE.md:62

• The regenerated ledger omits linarith, although the new Proof.lean presents and uses it (Proof.lean:359-368 and :532). Add it to this first-use row; otherwise the ledger is incomplete and the feature is not tracked.

| `Logic/Proof` | `open` | `¬`, `∀`, `∃`, `∧`, `∨`, `↔`, `≠` | `intro`, `exact`, `apply`, `cases … with`, `constructor`, `obtain`, `have`, `use`, `left`, `right`, `rcases`, `by_cases`, `by_contra`, `assumption` |

STYLE-CODE.md:149

• The HTML-splitting example lists only Logic/PL/ and Logic/FOL/, but the new Proof section also has file := "Proof" and becomes Logic/Proof/. The style guidance should not omit the first section it is intended to describe.

the chapter's directory — `Logic/PL/`, `Logic/FOL/` — which is what the

• Files reviewed: 18/18 changed files
• Comments generated: 13
• Review effort level: Lite

---

💡 Add a code-review agent skill or configure MCP servers for context-aware, tailored reviews. Learn more in the docs.