From b6b8f5c682cf964261949801c867261bae74e836 Mon Sep 17 00:00:00 2001 From: Alexandre Rademaker Date: Sat, 26 Sep 2026 17:55:48 -0300 Subject: [PATCH 1/3] docs(provenance): replace the dated exercise count with a check script The count of exercises and the list of known exceptions had to be edited by hand for every new exercise, and had drifted. State only the invariant, and add `scripts/check-provenance.sh`, which checks it. Mention the script in CONTRIBUTING.md. -- AI-usage disclosure: the script and the text were drafted with the assistance of Claude Opus 5.5 (Anthropic, September 2026, via Claude Code). The author reviewed the changes and takes full responsibility for the final content. --- CONTRIBUTING.md | 2 ++ PROVENANCE.md | 13 +++------ scripts/check-provenance.sh | 53 +++++++++++++++++++++++++++++++++++++ 3 files changed, 59 insertions(+), 9 deletions(-) create mode 100755 scripts/check-provenance.sh diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index 8198921..ac385b0 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -69,6 +69,8 @@ issue. Those render as editorial notes and never reach the student. - Before opening it, check that what you touched still builds — `lake build CSwL.Sets` for a single chapter, `make all` if you changed the infrastructure or anything that affects the generated variants. +- If you added, renamed or removed an exercise, update `PROVENANCE.md` and + run `scripts/check-provenance.sh`. - Delete the branch once it is merged. Commit messages follow [Conventional diff --git a/PROVENANCE.md b/PROVENANCE.md index cde12e7..886827b 100644 --- a/PROVENANCE.md +++ b/PROVENANCE.md @@ -20,15 +20,10 @@ passage it comes from**. Keep it in step with any further rename. stated in Lean. In the source these carry a `✎` marker, which is otherwise undocumented. -The book has 76 exercises as of 2026-09-13, and all but one of them -appear somewhere below — either in a table that names its source, or -in the list of those with no counterpart. Two checks keep it that way: -no `(name := …)` in `CSwL/` should be absent from this file, and no -name cited here should have stopped existing. - -The exception is `free-vars-in-formula`, in `Logic/FOL.lean`, which has -no entry here; it predates the chapter reorganization of 2026-09-13 and -still needs one. +Every exercise of the book appears somewhere below, either in a table +that names its source or in the list of those with no counterpart; and +every id cited in a `CSwL id` column is the name of an exercise. +`scripts/check-provenance.sh` checks both and lists what disagrees. ## A correction to the numbers diff --git a/scripts/check-provenance.sh b/scripts/check-provenance.sh new file mode 100755 index 0000000..5e08e71 --- /dev/null +++ b/scripts/check-provenance.sh @@ -0,0 +1,53 @@ +#!/usr/bin/env bash +# Checks that `PROVENANCE.md` and the book's exercises agree: +# +# - every `(name := "…")` of an `:::exercise` block under `CSwL/` is +# mentioned in `PROVENANCE.md`; +# - every id in a `CSwL id` column of a table in `PROVENANCE.md` is the +# name of an exercise under `CSwL/`. +# +# Prints each discrepancy and exits with status 1 if there is any. +# +# Usage: scripts/check-provenance.sh + +set -euo pipefail + +CSWL_DIR="$(cd "$(dirname "${BASH_SOURCE[0]}")/.." && pwd)" +PROVENANCE="$CSWL_DIR/PROVENANCE.md" + +# Names of the exercises in the book. +exercises="$(grep -rhE '^:+exercise' "$CSWL_DIR/CSwL" --include='*.lean' \ + | sed -nE 's/.*\(name := "([^"]+)"\).*/\1/p' | sort -u)" + +# Ids in the `CSwL id` column of every table, skipping `—` placeholders. +cited="$(awk -F'|' ' + /^\|/ { + if (!col) { + for (i = 2; i < NF; i++) if ($i ~ /CSwL id/) col = i + } else if ($col !~ /^[ -]*$/) { + id = $col; gsub(/[ `]/, "", id) + if (id != "—") print id + } + next + } + { col = 0 } +' "$PROVENANCE" | sort -u)" + +status=0 + +while IFS= read -r name; do + if ! grep -qE "(^|[^[:alnum:]_-])${name}([^[:alnum:]_-]|$)" "$PROVENANCE"; then + echo "not in PROVENANCE.md: $name" + status=1 + fi +done <<< "$exercises" + +while IFS= read -r id; do + [ -z "$id" ] && continue + if ! grep -qxF "$id" <<< "$exercises"; then + echo "no such exercise: $id" + status=1 + fi +done <<< "$cited" + +exit $status From a519244c8195e4fd28bde692a770c23d40811ec0 Mon Sep 17 00:00:00 2001 From: Alexandre Rademaker Date: Sat, 26 Sep 2026 19:19:12 -0300 Subject: [PATCH 2/3] fix(IntroCS): simplify the possibilities exercise --- CSwL/IntroCS.lean | 67 ++++++++++------------------------------------- 1 file changed, 14 insertions(+), 53 deletions(-) diff --git a/CSwL/IntroCS.lean b/CSwL/IntroCS.lean index ad1d83e..f93e2ee 100644 --- a/CSwL/IntroCS.lean +++ b/CSwL/IntroCS.lean @@ -284,36 +284,22 @@ quatro possibilidades. Seu conhecimento cresceu pela eliminação de possibilidades. ::::exercise (rating := 1) (name := "possibilities") - -A ignorância completa sobre a verdade ou falsidade de dois fatos se modela como -incerteza entre quatro possibilidades. Com dez fatos básicos, quantas -possibilidades? E no caso geral de `n` fatos? +A ignorância completa sobre a verdade ou falsidade de dois fatos se modela como incerteza entre quatro possibilidades. Com dez fatos básicos, quantas possibilidades? E no caso geral de `n` fatos? ```lean def possibilities : Nat → Nat | 0 => 1 | n + 1 => 2 * possibilities n -``` - -```lean -#eval possibilities 10 -``` -Em Lean, podemos provar propriedades sobre funções, embora óbvio para este caso, -sabemos que a função `possibilities` computa basicamente a expressão $2^n$. -No passo indutivo é preciso desdobrar a potência, e há -dois lemas para isso: `Nat.pow_succ'` e `Nat.pow_succ`. - -```lean example (n : Nat) : possibilities n = 2 ^ n := by induction n with | zero => rfl | succ k ih => rw [possibilities, ih, Nat.pow_succ'] ``` +Em Lean, podemos provar propriedades sobre funções, embora óbvio para este caso, sabemos que a função `possibilities` computa basicamente a expressão `2^n`. No passo indutivo é preciso desdobrar a potência, e há dois lemas para isso: `Nat.pow_succ'` e `Nat.pow_succ`. :::: - Se você quiser apenas estudar a troca simples de informação factual, faz sentido concentrar-se no fragmento de língua natural que pode ser traduzido para a lógica proposicional. Mas suponha que você queira ser mais explícito ao exprimir @@ -398,60 +384,35 @@ das línguas humanas. em parte pelo contexto em que o sintagma é usado. ::::exercise (rating := 1) (name := "sentence-go-on") +Pollard e Sag dão este exemplo de recursão no inglês. -Pollard e Sag dão este exemplo de recursão que estende sentenças: - -``` -Sentences can go on. -Sentences can go on and on. -Sentences can go on and on and on. -Sentences can go on and on and on and on. -... -``` - -Dê uma descrição concisa do padrão de recursão — isto é, escreva o gerador. -`sentence n` deve produzir a sentença com `n` repetições de "and on". +- Sentences can go on. +- Sentences can go on and on. +- Sentences can go on and on and on. +- Sentences can go on and on and on and on. +- ... -Uma observação que economiza tempo: a recursão *não* cabe direto em -`sentence`, porque o ponto final tem de ficar sempre no fim. O que se repete é -o pedaço `" and on"`, e é ele que merece a função recursiva. Por isso o -esqueleto vem em duas partes. +Escreva um gerador de sentenças da forma acima. Seu gerador deve receber como parâmetro o número de repetições de "and on". -`andOn n` são as `n` repetições de `" and on"`, sem mais nada. +A recursão *não* cabe direto em `sentence`, porque o ponto final tem de ficar sempre no fim. O que se repete é o pedaço `" and on"`, e é ele que merece a função recursiva. Por isso o esqueleto vem em duas partes. A função `andOn n` gera as `n` repetições. E a sentença é o começo, mais as repetições, mais o ponto. ```lean def andOn : Nat → String | 0 => "" | n + 1 => " and on" ++ andOn n -``` -E a sentença é o começo, mais as repetições, mais o ponto. - -```lean def sentence (n : Nat) : String := "Sentences can go on" ++ andOn n ++ "." ``` - -```lean -#eval sentence 2 -``` - :::: ::::quiz -Há infinitas sentenças em inglês? Ou segue que -sentenças em inglês podem ter comprimento infinito? Ou as duas coisas? +Há infinitas sentenças em inglês? Ou as sentenças em inglês podem ter comprimento infinito? Ou as duas coisas? :::quizSolution -De fato, segue-se do exemplo que há infinitas frases. Ainda assim, cada frase -tem comprimento finito. - -Conjuntos finitos de coisas infinitas são diferentes de conjuntos infinitos de -coisas finitas. O conjunto de frases da língua inglesa é um exemplo de um -conjunto infinito de coisas finitas. Portanto, "As frases podem continuar -indefinidamente" não significa que uma única frase possa continuar -indefinidamente, mas sim que o processo de construir frases cada vez mais longas -pode continuar indefinidamente. +De fato, segue-se do exemplo que há infinitas frases. Ainda assim, cada frase tem comprimento finito. + +Conjuntos finitos de coisas infinitas são diferentes de conjuntos infinitos de coisas finitas. O conjunto de frases da língua inglesa é um exemplo de um conjunto infinito de coisas finitas. Portanto, uma única frase não pode ser infinita porque humanos sequer teriam capacidade de entende-la. Mas o processo de construir frases cada vez mais longas pode continuar indefinidamente, pela gramática do inglês. ::: :::: From 9f8bab764e45b55f6d1e22407fae62e0bbb8fc46 Mon Sep 17 00:00:00 2001 From: Alexandre Rademaker Date: Sat, 26 Sep 2026 19:19:19 -0300 Subject: [PATCH 3/3] docs: replace PROVENANCE.md with CSwFP.yaml and slim DEVIATIONS.md MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit List every CSwFP/1–6 exercise with the CSwL exercise it became or the reason it was not ported, and map every CSwFP section to where it went. Keep in DEVIATIONS.md only the design decisions, as they stand now. Move the rules it stated into STYLE-CODE.md and STYLE-WRITING.md. Replace check-provenance.sh with check-cswfp.py, which also checks that the prose does not cite CSwFP. Closes #31 Refs #6 -- AI-usage disclosure: the inventory, the script and the text were drafted with the assistance of Claude Opus 5.5 (Anthropic, September 2026, via Claude Code). The author reviewed the changes and takes full responsibility for the final content. --- CLAUDE.md | 5 +- CONTRIBUTING.md | 5 +- CSwFP.yaml | 274 +++++++++++++++ CSwL/SeaBattle.lean | 3 +- DEVIATIONS.md | 641 ++++++------------------------------ PROVENANCE.md | 352 -------------------- README.md | 2 +- STYLE-CODE.md | 16 +- STYLE-WRITING.md | 26 +- scripts/check-cswfp.py | 117 +++++++ scripts/check-provenance.sh | 53 --- 11 files changed, 538 insertions(+), 956 deletions(-) create mode 100644 CSwFP.yaml delete mode 100644 PROVENANCE.md create mode 100755 scripts/check-cswfp.py delete mode 100755 scripts/check-provenance.sh diff --git a/CLAUDE.md b/CLAUDE.md index edafab9..09b70fd 100644 --- a/CLAUDE.md +++ b/CLAUDE.md @@ -77,7 +77,8 @@ up in the book**; everything you write must conform to them. - `STYLE-WRITING.md` — prose: the project's pedagogical decisions, writing advice, and the Portuguese conventions including the term list. -`CONTRIBUTING.md` covers workflow. `DEVIATIONS.md` records what departs from -CSwFP and why. In case of conflict, the style guides win on style and this +`CONTRIBUTING.md` covers workflow. `CSwFP.yaml` maps each CSwFP section and +exercise to where it went, and `DEVIATIONS.md` records what departs from CSwFP +and why. In case of conflict, the style guides win on style and this file wins on project scope. diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index ac385b0..aa3de7c 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -69,8 +69,9 @@ issue. Those render as editorial notes and never reach the student. - Before opening it, check that what you touched still builds — `lake build CSwL.Sets` for a single chapter, `make all` if you changed the infrastructure or anything that affects the generated variants. -- If you added, renamed or removed an exercise, update `PROVENANCE.md` and - run `scripts/check-provenance.sh`. +- If you added, renamed or removed an exercise, update `CSwFP.yaml`. Run + `scripts/check-cswfp.py` (it needs PyYAML) whenever you touch an exercise + or the prose. - Delete the branch once it is merged. Commit messages follow [Conventional diff --git a/CSwFP.yaml b/CSwFP.yaml new file mode 100644 index 0000000..a474c10 --- /dev/null +++ b/CSwFP.yaml @@ -0,0 +1,274 @@ +# How CSwL uses CSwFP. +# +# `exercises` lists every CSwFP exercise, by chapter, with the page it is on. +# The value is the CSwL exercise it became, as its `(name := …)`, or, when it +# was not ported, the reason why. A reason is anything with a space in it; a +# `TODO` reason is a decision still to be made. +# +# `original` lists the CSwL exercises that have no CSwFP counterpart, by file. +# `depends` lists the exercises whose solution another exercise uses. +# +# `sections` says where each CSwFP section went, and why when the answer is +# not simply the obvious chapter. Chapter names are the files under `CSwL/`. +# +# `scripts/check-cswfp.py` checks this file against the book. + +exercises: + + CSwFP/1: + 1.1 (p. 6): possibilities + 1.2 (p. 8): sentence-go-on + 1.3 (p. 8): turned into a quiz + + CSwFP/2: + 2.1 (p. 17): empty-subset + 2.2 (p. 17): empty-vs-singleton + 2.3 (p. 17): double-complement + 2.4 (p. 18): cartesian-square + 2.5 (p. 18): successor-composition + 2.6 (p. 18): converse-subset + 2.7 (p. 19): which-are-transitive + 2.8 (p. 19): transitive-iff-comp + 2.9 (p. 19): transitive-not-idempotent + 2.10 (p. 21): successor-as-relation + 2.11 (p. 21): leq-as-function + 2.12 (p. 21): graph-is-functional + 2.13 (p. 26): TODO, was `twice`, no longer in the book + 2.14 (p. 26): in the prose of IntroL + 2.15 (p. 28): TODO, typing of lambda terms, goes with 2.5 to English + 2.16 (p. 28): in the prose of IntroL + 2.17 (p. 30): TODO, was `adjective-types`, no longer in the book + + CSwFP/3: + 3.1 (p. 36): about Haskell itself + 3.2 (p. 36): about Haskell itself + 3.3 (p. 37): about Haskell itself + 3.4 (p. 38): about Haskell itself + 3.5 (p. 41): about Haskell itself + 3.6 (p. 41): about Haskell itself + 3.7 (p. 46): about Haskell itself + 3.8 (p. 46): about Haskell itself + 3.9 (p. 46): about Haskell itself + 3.10 (p. 46): about Haskell itself + 3.11 (p. 46): about Haskell itself + 3.12 (p. 46): about Haskell itself + 3.13 (p. 46): about Haskell itself + 3.14 (p. 47): about Haskell itself + 3.15 (p. 48): about Haskell itself + 3.16 (p. 51): about Haskell itself + 3.17 (p. 51): about Haskell itself + 3.18 (p. 54): about Haskell itself # the type of `vh`; worth reconsidering + 3.19 (p. 61): yawelmani-harmony + + CSwFP/4: + 4.1 (p. 65): game-over-grammar + 4.2 (p. 67): dropped with Mastermind + 4.3 (p. 67): dropped with Mastermind + 4.4 (p. 67): dropped with Mastermind + 4.5 (p. 68): TODO + 4.6 (p. 69): TODO + 4.7 (p. 69): preposition-phrase # pending #29 + 4.8 (p. 69): complex-relative-clauses # pending #29 + 4.9 (p. 74): bangu-form + 4.10 (p. 74): exclusive-or + 4.11 (p. 74): needs Mathlib's ContextFreeGrammar + 4.12 (p. 75): count-operators + 4.13 (p. 75): formula-depth + 4.14 (p. 75): collect-atoms + 4.15 (p. 77): needs Mathlib's ContextFreeGrammar + 4.16 (p. 77): needs Mathlib's ContextFreeGrammar + 4.17 (p. 78): ex-fol-freevars + 4.18 (p. 81): ex-fol-closedform + 4.19 (p. 82): ex-fol-remove-impl_equiv + 4.20 (p. 82): ex-fol-nnf + 4.21 (p. 83): needs Mathlib's ContextFreeGrammar + 4.22 (p. 84): ex-fol-vars-in-formula + 4.23 (p. 84): ex-fol-free-vars-in-form + 4.24 (p. 84): ex-fol-open-form + + CSwFP/5: + 5.1 (p. 90): add-ship + 5.2 (p. 91): sunk + 5.3 (p. 92): grice-maxims + 5.4 (p. 92): valuations + 5.5 (p. 93): in the prose of Logic/PL + 5.6 (p. 93): ex-pl-satisfiable + 5.7 (p. 93): ex-pl-equiv + 5.8 (p. 93): pl-consequence + 5.9 (p. 93): in the prose of Logic/PL + 5.10 (p. 96): implies-from-list + 5.11 (p. 96): in the prose of Logic/PL + 5.12 (p. 96): in the prose of Logic/PL + 5.13 (p. 97): dropped with Mastermind + 5.14 (p. 97): dropped with Mastermind + 5.15 (p. 100): dropped with Mastermind + 5.16 (p. 100): dropped with Mastermind + 5.17 (p. 102): ex-fol-weak-strong + 5.18 (p. 102): ex-fol-translate + 5.19 (p. 102): ex-fol-model + 5.20 (p. 103): ex-fol-valid + 5.21 (p. 103): an alternative definition the book does not need + 5.22 (p. 103): an alternative definition the book does not need + 5.23 (p. 104): in the prose of Logic/FOL + 5.24 (p. 104): ex-fol-consequence + 5.25 (p. 105): ex-fol-entails + 5.26 (p. 106): TODO + 5.27 (p. 106): TODO + 5.28 (p. 109): soundness is within reach, completeness needs a model construction + 5.29 (p. 109): soundness is within reach, completeness needs a model construction + 5.30 (p. 110): TODO + 5.31 (p. 110): TODO + 5.32 (p. 115): TODO + + CSwFP/6: + 6.1 (p. 137): help-defeat # pending #29 + 6.2 (p. 137): TODO + 6.3 (p. 138): TODO + 6.4 (p. 139): reflexive-ditransitive # pending #29 + 6.5 (p. 141): TODO + 6.6 (p. 146): TODO + 6.7 (p. 147): check-sentence # pending #29 + +original: + IntroL.lean: [sum-of-squares, sum-to, sum-list, count-zeros] + Logic/Proof.lean: + - rfl-arithmetic + - de-morgan + - contrapositive + - exchange-prop + - implication-as-disj + - and-comm + - implication-transitivity + - unfold-direct-proof + - unfold-rw-conjunction + - dresses + - forall-exists-swap + - exists-witness + Logic/PL.lean: + - collect-atoms-alternative # `names` without `mergeSort` and `eraseDups` + - ex-pl-contingent + - bangu-proof + Logic/FOL.lean: + - ex-fol-implies-from-list # from the prose between 5.24 and 5.25 + Sets.lean: + - five-in-above2 + - one-not-in-above2 + - above5-subset-above2 + - union-contains + - intersection-contained + SeaBattle.lean: [defeated-last] + Morphology/Phonemes.lean: [append-suffix-text] + Morphology/SwedishPlural.lean: [swedish-plural] + InfEngine.lean: [inconsistent-kb, ferio] + English.lean: [fragment-translations] # pending #29 + +depends: + bangu-proof: bangu-form + pl-consequence: implies-from-list + ex-fol-entails: ex-fol-implies-from-list + +sections: + + CSwFP/1: + 1.1–1.6: IntroCS + 1.7 Overview of the Book: omitted + 1.8 Further Reading: omitted + + CSwFP/2: + 2.1 Sets and Set Notation: Sets + 2.2 Relations: Sets + 2.3 Functions: + to: IntroL + why: In Lean `A → B` is primitive, so functions come with the language. + That a function is a functional relation becomes a theorem in Sets. + 2.4 Lambda calculus: + to: IntroL + why: With Lean already on screen, lambda calculus is the theory of what + the reader has just written. Its linguistic example goes to English. + 2.5 Types in Grammar and Computation: + to: English + why: The semantic types e and t and the typing rules are about the + fragment, and are shown over its own types. + 2.6 Functional Programming: + to: absorbed + why: It bridges to a programming language the reader has already seen. + 2.7 Further reading: omitted + + CSwFP/3: + 3.1 The Programming Language Haskell: IntroL, merged with 3.2 + 3.2 Using the Book Code: IntroL, merged with 3.1 + 3.3 First Experiments: IntroL + 3.4 Type Polymorphism: IntroL + 3.5 Recursion: IntroL + 3.6 List Types and List Comprehension: IntroL + 3.7 List processing with map and filter: IntroL + 3.8 Function Composition, Conjunction, Disjunction, Quantification: IntroL + 3.9 Type Classes: IntroL + 3.10 Strings and Texts: IntroL + 3.11 Finnish Vowel Harmony: + to: Morphology + why: Split in two, FinnishVowelHarmony and SwedishPlural. + 3.12 Identifiers in Haskell: omitted + 3.13 User-defined Data Types and Pattern Matching: + to: IntroL + why: Its Subject/Predicate example goes to English, so that no fragment + of natural language appears before the one English builds. + 3.14 Application, Representing Phonemes: Morphology + 3.15 Further Reading: omitted + + CSwFP/4: + 4.1 Grammars for Games: + to: SeaBattle + why: Together with 5.1, syntax and semantics in one chapter. The + Mastermind grammar is dropped with 5.4. + 4.2 A Fragment of English: English + 4.3 A Language for Talking about Classes: + to: InfEngine + why: Together with 5.7, and after Sets, since the language is about sets. + 4.4 Propositional Logic: Logic/PL + 4.5 Predicate Logic: Logic/FOL + 4.6 Predicate Logical Formulas in Haskell: Logic/FOL + 4.7 Adding Function Symbols: Logic/FOL + 4.8 Further Reading: omitted + + CSwFP/5: + 5.1 Semantics of Sea Battle: SeaBattle + 5.2 Semantics of Propositional Logic: Logic/PL, merged with 5.3 + 5.3 Propositional Reasoning in Haskell: Logic/PL, merged with 5.2 + 5.4 Semantics of Mastermind: + to: dropped + why: Disconnected from Sea Battle, and it announces a semantics in + propositional logic that the implementation never uses. + 5.5 Semantics of Predicate Logic: + to: Logic/FOL + why: The model is the four-vertex graph of Enderton, since the model of + 6.3 belongs with the fragment it interprets. + 5.6 Semantics of Natural Language Fragments: English + 5.7 An Inference Engine with a Natural Language Interface: + to: InfEngine + why: The natural-language input, the only use of IO in the book, is not + ported. + 5.8 Further Reading: omitted + + CSwFP/6: + 6.1 Linguistic Form and Translation Into Logic: English + 6.2 Predicate Logic as Representation Language: English + 6.3 Representing a Model for Predicate Logic: English + 6.4 Evaluating Formulas in Models: English + 6.5 Evaluating Formulas with Structured Terms: + to: Logic/FOL + why: It is about the evaluator, not the fragment. The evaluation over + `[0..]` becomes a theorem, since Lean is not lazy. + 6.6 Further Reading: omitted + + CSwFP/7 The Composition of Meaning in Natural Language: not yet taken up + CSwFP/8 Extension and Intension: not yet taken up + CSwFP/9 Parsing: not yet taken up + CSwFP/10 Handling Relations and Scoping: not yet taken up + CSwFP/11 Continuation Passing Style Semantics: not yet taken up + CSwFP/12 Discourse Representation and Context: not yet taken up + CSwFP/13 Communication as Informative Action: not yet taken up + +new: + Logic/Proof.lean: Proving in Lean, condensed from logic_and_proof. It comes + before PL and FOL so that neither has to teach tactics. diff --git a/CSwL/SeaBattle.lean b/CSwL/SeaBattle.lean index 0d578e2..0ce09e4 100644 --- a/CSwL/SeaBattle.lean +++ b/CSwL/SeaBattle.lean @@ -248,8 +248,7 @@ o que deixa essas instâncias alcançarem `NoClashes`/`ShipOK` sem esforço extra — uma `def` opaca escondia essa busca. Em vez de deixar as duas condições como testes externos que um estado -pode ou não satisfazer — o que fazia o exercício `lineupOK` das versões -anteriores deste capítulo —, podemos exigi-las já na definição do tipo: +pode ou não satisfazer, podemos exigi-las já na definição do tipo: um `State` só existe se vier acompanhado da prova de que sua distribuição de navios as satisfaz. É o estilo idiomático de Lean — *proof-carrying data* —, em que a invariante não é algo a verificar depois, é parte do diff --git a/DEVIATIONS.md b/DEVIATIONS.md index 882f119..e099487 100644 --- a/DEVIATIONS.md +++ b/DEVIATIONS.md @@ -1,546 +1,115 @@ -# How CSwL uses CSwFP +# How CSwL departs from CSwFP -`CSwL` is not a section-by-section translation of CSwFP. It reorders the material so that the -presentation is natural in Lean, under one hard constraint: - -> **Nothing is used before it is presented.** - -Names of files, chapter, section tags, and exercises are English mnemonics. The prose is in -Portuguese; the identifiers inside Lean blocks are in English. - -The prose never explains the CLwL material by contrast with CSwFP. Those reasons belong in this -document. The line to hold is not "never mention an alternative". It is: - -- a **technical consequence in Lean** is content, because the reader will meet it. "A constructor - holding a `List Form` makes the type a nested inductive, and a nested inductive has no `induction` - tactic" states a fact about Lean that the chapter then depends on; -- an **editorial preference** is meta. "We preferred to keep `Game` as it is", "the columns could - have been modelled like the rows, but we chose the usual convention" — these report what the - authors decided, which is this document's subject and not the book's. - -The test: would the sentence still be worth writing if this book had no source and no alternatives? -A fact about Lean survives that; a preference does not. - -A chapter that translates keeps the original's structure — its section boundaries, its order, its -sentence boundaries and its punctuation. Subheadings that the source does not have are not added, -and headings the source has are not merged, unless something in this document says so and says why. - -Most chapters, though, are mixed: part translated, part written here because Lean makes something -sayable that the source could not say. In a mixed chapter the rule applies section by section. A -translated section follows the original; a new section has a structure of its own, chosen for what -it teaches. Which sections are which is recorded per chapter below — a reader of this document -should never have to guess whether a heading came from the source or from us. - -Any divergence from this plan is stated when it is made. A silent divergence is worse than a wrong -one: a wrong decision can be argued with, an unrecorded one cannot. - -"Presented" has one deliberate loosening and one exception. - -The loosening: Lean's own basic types may be introduced *where they are first needed*, in a sentence -or two, with a citation of the Lean Language Reference (`{citep Bib.LLR}[]`), instead of being -pushed back into `IntroL.lean`. `Fin` in `SeaBattle.lean` is the case. `IntroL.lean` presents what -the book builds on repeatedly; a type used in one chapter is better introduced there, next to its -use. The loosening covers types the language already gives us — never a construct this book defines, -and never one that needs more than a short paragraph. - -The exception: `IntroCS.lean`, described in that chapter's section below. Everywhere else, a -construct in a code block is one an earlier chapter has presented. - -This document is the migration plan: which CSwFP sections each `CSwL` chapter consumes, in which -order, and what each chapter presupposes. The order below is the book's order; the dependency -columns are what justify it. Everything through CSwFP/6 is settled — where a section records a -decision, that decision is made, not proposed. What remains is execution, tracked in [GitHub -issues](https://github.com/cslib-community/CSwL/issues). Exercise-level correspondence with CSwFP is -in `PROVENANCE.md`. - -The current state of CSwL need major review to fulfill all decisions from this document. - -## Why the order changes at all - -CSwFP runs 1, 2 (sets, relations, lambda, types), 3 (Haskell), 4 (syntax), 5 (semantics), 6 (model -checking). That works in Haskell because CSwFP/2 is *pure prose*: nothing in it is mechanised, so it -owes nothing to the chapter that introduces the language. In Lean the same material is mechanisable, -which inverts the dependency and forces the reordering below. - -CSwFP/2 also cannot be split cleanly, because its sections form a definitional chain: 2.3 opens -"Functions are relations with the following special property", so it needs 2.2, which needs 2.1; 2.4 -opens "We already talked about functions informally", so it needs 2.3; 2.5 builds on the terms of -2.4. The chapter is therefore *dissolved* rather than moved — 2.3, 2.4 and 2.5 into `IntroL.lean`, -2.1 and 2.2 into `Sets.lean`, and the natural-language examples scattered through 2.4 and 2.5 into -`English.lean`. +`CSwL` reorders CSwFP so that the presentation is natural in Lean. +`CSwFP.yaml` says where each CSwFP section and exercise went. This +file records the decisions behind that, as they stand now; how they +were reached is in the git history and the pull requests. The rules +the decisions serve are in `STYLE-CODE.md` and `STYLE-WRITING.md`. ## Chapter order -*Requires* means the chapter does not stand without it — material it uses that the earlier chapter presents. *Best after* is placement by preference: the chapter would still work earlier, but reads better here. Only the *Requires* column is a constraint. - -| # | `CSwL` chapter | CSwFP sections | Requires | Best after | -|---|----------------------|---------------------------------------------------|----------|------------| -| 1 | `IntroCS.lean` | 1.1–1.6 | — | — | -| 2 | `IntroL.lean` | 3.1–3.10, 3.13; 2.3, 2.4 | 1 | — | -| 3 | `Logic.lean` | 4.4, 4.5, 4.6, 4.7, 5.2, 5.3, 5.5 | 2 | — | -| 4 | `Sets.lean` | 2.1, 2.2 | 2, 3 | — | -| 5 | `SeaBattle.lean` | 4.1, 5.1 | 2, 3 | 4 | -| 6 | `Morphology.lean` | 3.11, 3.14 | 2 | 3 | -| 7 | `InfEngine.lean` | 4.3, 5.7 | 2, 3 | 4 | -| 8 | `English.lean` | 4.2, 5.6; 2.5 | 2, 3, 4 | — | -| 9 | `ModelChecking.lean` | 6.1–6.5 | 2, 3, 8 | 4 | - -`Sets.lean` requires `Logic.lean` because its exercises are proofs, and the tactics they need — quantifiers, `cases`, `by_contra` — arrive there. `SeaBattle.lean` requires `Logic.lean` for the same reason: it proves theorems about `WellFormed` by induction on an inductive predicate, which no earlier chapter has the machinery for. `English.lean` requires `Sets.lean` because its categorial section interprets a transitive verb over `Sets.Entity` and `Sets.likesR`, the domain and relation that chapter introduces. - -`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. +CSwFP runs sets, lambda calculus and types (2) before Haskell (3). That works +because its chapter 2 is prose. In Lean the same material is code, so the +language has to come first, and chapter 2 is split: 2.3 and 2.4 into +`IntroL`, 2.1 and 2.2 into `Sets`, 2.5 into `English`. + +| Chapter | Requires | Why | +|--------------|-----------|-----------------------------------------------------------------------------| +| `IntroCS` | — | | +| `IntroL` | `IntroCS` | | +| `Logic` | `IntroL` | | +| `Sets` | `Logic` | its exercises are proofs, and 2.3 needs classical reasoning | +| `SeaBattle` | `Logic` | its exercises prove theorems by induction on `WellFormed` | +| `Morphology` | `IntroL` | placed here so that its exercises may use tactics | +| `InfEngine` | `Sets` | the language of 4.3 is about sets, and the syllogisms are proved over `Set` | +| `English` | `Sets` | its categorial section interprets verbs over `Sets.Entity` | + +CSwFP/6 is in `English`: it is built on the fragment of 4.2, whose +categories it translates one by one. ## Reusing Mathlib and CSLib -Reusing Mathlib and CSLib is a declared intention of this project, and contributing back to CSLib is another. So the default is to reuse, and every place where this book defines something a library already has needs a reason. Two such places are recorded here; both are decisions for the chapters through CSwFP/6, and both are revisited in "Beyond CSwFP/6". - -What is reused today is modest and worth stating plainly: Mathlib supplies `Set`, `Rel`, `Setoid`, `Finset` and `Fintype` to `Sets.lean`, `List.Chain` to `SeaBattle.lean`, and the tactic library throughout. No chapter imports CSLib yet. - -### Propositional logic: why not CSLib's, for now - -CSLib has, in `Cslib.Logic.PL`: - -- `Proposition Atom` — `atom`, `and`, `or`, `imp`, with `¬A := A → ⊥` and `⊤` as derived notions; -- `Theory.Derivation : Ctx Atom → Proposition Atom → Type` — sequent-style natural deduction, `Finset` contexts, rules `ax`, `ass`, `andI`, `andE₁`, `andE₂`, `orI₁`, `orI₂`, `orE`, `implI`, `implE`, with `Γ ⊢ A` and `T⇓(Γ ⊢ A)` notation; -- weakening, cut and substitution as derived rules; `IsIntuitionistic` and `IsClassical` as *theories*, yielding `byContra`, `lem` and `pierce`. - -That is a complete natural deduction system, ready to use, and `PL.lean` does not use it. Three reasons: - -1. **It would put a third object in front of the reader at once.** The chapter already has to separate `p ∧ q : Prop` from `Form.conj p q : Form`, and that separation is the section glued to the `inductive`. Adding `Γ ⊢ A ∧ B` makes it a three-way distinction in the chapter where the reader meets all three for the first time. This is a pedagogical cost, not a technical one: CSLib solves the notation clash with a wrapper tag naming the logic (`Modal[m,w ⊨ φ]`), stated as a principle in `Cslib/Logics/README.md`. -2. **The connectives do not line up.** `CSwL`'s `Form` takes `neg`, `top` and `bot` as constructors and derives `impl` and `equi`; CSLib's `Proposition` takes `imp` as primitive and derives negation and `⊤`. Adopting CSLib's type rewrites 4.4, 5.2, 5.3 and every exercise in the chapter; keeping both means maintaining a translation between them. Note that CSLib itself does not insist: its modal chapter declares its *own* `Proposition` rather than reusing the propositional one — precedent for `CSwL` keeping its own `Form` and instantiating the interfaces around it. -3. **CSLib's presentation is minimal logic**, with intuitionistic and classical strength added as *axioms of a theory* rather than as deduction rules. The module itself notes that this differs from most on-paper presentations, and the design is still under discussion upstream. It is a defensible formalisation and an odd first contact with natural deduction for a course that is not about proof theory. - -Reasons 1 and 3 are about this book's audience and would not change if CSLib changed. Reason 2 is ours to remove, by taking `imp` as primitive in `Form`; that is the cheapest route into CSLib if the decision is ever reopened. - -**What CSLib does not have, and what its house style already prescribes.** There is no semantics for propositional logic — no valuation, no truth tables, no soundness — and no first-order logic at all (`Cslib/Logics/` holds propositional, modal, HML and linear logic). So CSwFP/5.2, 5.3 and 5.5 have nothing to reuse, and the reuse question does not even arise for `FOL.lean`. - -The *shape* such a semantics should take is not open, though. CSLib treats proof systems and semantics uniformly, both instantiating `InferenceSystem`, and the modal chapter is the worked example: `Satisfies m w φ` is an ordinary recursive function into `Prop`, bundled as a `Judgement` with `instance : HasInferenceSystem`, and the object/meta bridge is stated as theorems like - - Satisfies.and_iff_and : ⇓Modal[m,w ⊨ φ₁ ∧ φ₂] ↔ ⇓Modal[m,w ⊨ φ₁] ∧ ⇓Modal[m,w ⊨ φ₂] - -which is exactly the bridge that `PL.lean` promises, in modal clothing. - -Decision: `PL.lean` defines a plain `eval : Valuation → Form → Bool` and states the bridge as ordinary theorems, without the `Judgement` wrapper, the `HasInferenceSystem` instance or a `⇓LP[v ⊨ F]` notation. The course is not about Lean and introduces only what the material needs, and this is the reader's first logic chapter; library machinery there is machinery the book would have to explain. Adopting the shape later is mechanical — `Satisfies` is itself an ordinary recursive function, and the bundling is one structure, one instance and one notation on top of it, with nothing about `eval` changing. Packaging this chapter's semantics for CSLib is a separate deliverable from the book, and belongs in a separate module. - -### Grammars: Mathlib's `ContextFreeGrammar`, deferred - -`SeaBattle.lean` presents a BNF grammar in prose, and then models it not as a grammar but as a handful of ordinary Lean types: enumerations for the terminal categories (`Colour`, `Answer`, `Column`, `Ship`), a `structure` for each rule with a fixed shape (`Turn`, `Attack`, `Move`), and `List`, `Vector` or a subtype where the BNF recurses or bounds a length (`abbrev Game := List Turn`, `abbrev Guess := Vector Colour 4`, `Reaction := { r : List Answer // r.length ≤ 4 }`). - -This flattens the grammar. The BNF rule `game ::= turn | turn game` is recursive; `List Turn` is that recursion already collapsed, and nothing in the chapter connects the two — the correspondence between the displayed BNF and the types below it is asserted in prose and nowhere checked. Sea Battle then adds `inductive WellFormed : Game → Prop` by hand, which is a well-formedness judgement written out because the type alone does not carry it. - -Mathlib has `Mathlib.Computability.ContextFreeGrammar`, which models the missing side: - -- `ContextFreeRule T N` — `input : N`, `output : List (Symbol T N)`; -- `ContextFreeGrammar T` — a nonterminal type `NT`, an `initial : NT`, and `rules : Finset (ContextFreeRule T NT)`; -- `Produces` (one rewriting step), `Derives` (its reflexive-transitive closure), `Generates`, and `language : Language T`; -- `Language.IsContextFree`, with closure results such as closure under reversal. - -The two are not the same object, and the difference is the point. An `inductive` type *is* the parse tree — this holds for `Form` in `PL.lean` and for the `Sent`/`NP`/`VP`/`RCN` fragment in `English.lean`, where a value is a derivation already built and there is no string. `ContextFreeGrammar` is about generating strings: `Derives` is a `Prop`-valued rewriting relation over `List (Symbol T NT)`, and `w ∈ g.language` says a word is generated. - -So the library supplies exactly what neither encoding in the book states today: - -- that a grammar *generates* a given sentence, as a theorem rather than as a `#eval` — and in `SeaBattle.lean` this is the missing link between the BNF in the prose and the types below it; -- derivation in the grammar sense, a sequence of rewriting steps, which is what a BNF actually describes and what `Derives` is. `SeaBattle.lean`'s hand-written `WellFormed` is a partial substitute for it; -- unique readability, which `PL.lean` gives up precisely because there is no string to disambiguate. Against a `ContextFreeGrammar` there is one again, and the claim recovers its content: that `toString` lands in the language, and is injective. - -Deferred all the same, for now. Carrying both representations means giving each grammar twice, which is the duplication this book avoids; `Finset` rules and `Symbol T NT` are heavy machinery for the chapter right after the introduction to Lean; and proving `w ∈ g.language` for a concrete word means building `ReflTransGen` chains, which is real work with no payoff before CSwFP/6. Nothing in CSwFP/1–6 requires it, and the flattened types are what the rest of the chapter computes with. - -Taken up after the pending work is done, the natural form is a closing section of `SeaBattle.lean` — one grammar given twice, as the flattened types the chapter computes with and as a `ContextFreeGrammar` value, with the bridge theorem between them — and a back-reference from `PL.lean`'s unique-readability discussion, which is the same question in a different chapter. - -## Chapter by chapter - -### 1. `IntroCS.lean` — CSwFP/1 - -Kept in the original presentation and section order. Sections 1.7 (Overview of the Book) and 1.8 (Further Reading) are omitted. - -**The one exception to the constraint.** CSwFP/1 has no code; this chapter has some, and all of it uses Lean that `IntroL.lean` only presents later — `example … := by rfl`, a recursive definition matching on `0`/`n + 1`, an `inductive` with `deriving Repr`, and a proof by `induction … with` using `rw`. This is deliberate and stays: the code is there to provoke the reader's curiosity, showing at the outset what the book will be able to say precisely, and the reader is not expected to write it or to follow it in detail. - -What makes the exception legitimate is that this chapter *presents* nothing. Every construct it displays is presented properly later, and the prose has to say so at the point where the code appears — that the code will be explained in the chapters that follow, and that reading it now is optional. Without that sentence the chapter is not a teaser, it is an unannounced prerequisite. - -The exception is this chapter only, and only for code that presents nothing. It does not extend to later chapters: `Fin`, `Vector` and subtypes are covered by the loosening stated at the top of this document, and `instance` and `mutual` are introduced where the sections above say. - -*Migration*: this chapter is to be rewritten as a faithful translation of CSwFP/1, section by section; the current file departs from the original's presentation and organisation. The code stays for now — it is illustrative, and the formalisations in it are slight — but it is not what the chapter is for, and the rewrite decides how much of it survives. Two things are needed either way: the framing sentence, which is not in the prose yet, and the replacement of the chapter's numeric cross-references. - -### 2. `IntroL.lean` — CSwFP/3, plus 2.3, 2.4 - -Presents Lean as a functional programming language. Translated aggressively, adapting to Lean style and primitives. - -Scope and order of presentation: terms and types, functions, expressions (`let`, `if-then-else` as terms), `structure`, inductive types, recursion, `List` and polymorphism, `Option`, list processing (`map`, `filter`, `foldl`, `all`, `any`), function composition, type classes, strings, and a closing section on Lean and the lambda calculus. Only what the rest of the book actually uses. - -- 3.1 and 3.2 merge into a single section about Lean. -- 3.12 (Identifiers in Haskell) and 3.15 (Further Reading) are omitted. -- 3.13 contributes inductive types and pattern matching; its `Subject`/ `Predicate` example is dropped here, because a fragment of natural language introduced this early collides with the fragments presented later. It is absorbed into `English.lean`. - -**2.3 and 2.4 live here; 2.5 does not.** CSwFP presents lambda calculus and types before the programming language, as preliminaries justifying a language the reader has not seen. With Lean already on screen the direction inverts: `#check fun x => x * x` exhibits the lambda abstraction of 2.4, and the closing section gives the term BNF of the lambda calculus with `Lam` as the inductive that mirrors it. The chapter becomes the theory of what the reader has just written. - -2.5 — the type BNF `τ ::= b | (τ → τ)` and the three typing rules — was here and is now `English.lean`'s, with the rest of 2.5 that chapter already carries. See the note in its section below. - -Two consequences of moving 2.3 here: - -- CSwFP defines a *function as a special kind of relation* (2.3), so 2.3 depends on 2.2. In Lean `A → B` is primitive, so the definition is not needed to introduce functions. When relations arrive in `Sets.lean`, "a function is a functional relation" stops being a definition and becomes a statement to prove — new text that CSwFP does not have. -- The linguistic example of 2.4 — lambda abstraction for word formation — is not presented here, because word formation collides with `Morphology.lean`. It is in `English.lean`. -- The demonstration of the typing rules went with 2.5. It had already been adapted once — it read `opaque happy : Entity → Prop`, and `Entity` is declared in `Sets.lean`, which now comes after this chapter, so it became `opaque restful : Day → Prop` over the inductive this chapter declares itself. Whichever entity the rules are demonstrated over in `English.lean`, that constraint no longer applies there. - -**`instance` is presented here.** The chapter's "Classes de tipos" section shows type classes only from the *use* side — the `[BEq α]` in a signature, and the difference between `BEq` and `DecidableEq`. But instances are declared from `Logic.lean` onwards: `FOL.lean` gives three, `Repr` for `Variable`, `Term` and `Formula`, and `English.lean` fifteen, all of them `ToString`. Declaring an instance is a small step from the section already there, and it is the last piece of type classes the book actually needs — no chapter declares a `class` of its own. - -**`Prop` is no longer presented here.** It once was, minimally — proposition-as-type, proof-as-term, and `rfl`, `intro`, `exact`, `decide` — and the argument was one of necessity rather than preference: inductive types bring `deriving DecidableEq` and `decide`, which display `Prop`, and `SeaBattle.lean` derives `DecidableEq` in its first code block. The student would see `Prop` whether or not it was introduced. - -That argument fell with the chapter reordering. `Proof.lean` is now part of `Logic.lean`, the third chapter, and every chapter that displays `Prop` — `Sets.lean`, `SeaBattle.lean`, `Morphology.lean` — comes after it. Nothing meets `Prop` unintroduced any more, so the minimal presentation had no work left to do and went out with the revision. The chapter is left deliberately pre-proof, as the `Logic.lean` section below records. - -**Three sections left the chapter in the revision of 2026-09-14.** It had grown to fifteen sections and roughly a thousand lines, and what went out was the material that theorised rather than taught the language: - -- *As duas leituras de uma função* — the extensional/intensional distinction, with `funext`. Moved to `Proof.lean`, as the section "Extensionalidade de Funções": `funext` is a tactic, and a chapter that presents no tactics is the wrong home for it. -- *Tipos na gramática e na computação* — the type BNF and the three typing rules, which is 2.5, moved to `English.lean` as recorded above. -- *Tipos como disciplina* — a closing page arguing that "this combination of words is not well formed" and "this program does not typecheck" become the same sentence. It is the book's thesis, not this chapter's content, and it reads better where a grammar is actually being typed. - -Only the third was dropped outright; the other two moved. Gone with them: the `leanOutput` blocks throughout, and `#reduce`. The surviving *Lean e o Cálculo Lambda* keeps the term BNF, the `Lam` inductive, β-reduction as what `#eval` does, and variable capture — the part the later chapters draw on. It also keeps `λx ↦ x x`, but as the observation that its reduction loops and that Lean rejects it, without the step-by-step derivation of `σ = σ → τ` that the removed section gave. Recorded because a reader tracing CSwFP/2.4 and 2.5 through this book would otherwise look for these sections and find no note of where they went. - -2.6 (Functional Programming) exists in CSwFP to motivate its chapter 3 from its chapter 2 — "functional programming languages actually are lambda calculi". With the order inverted, that bridge is not needed and the section is absorbed. - -2.7 (Further reading) is omitted. - -### 3. `Logic.lean` — CSwFP/4.4–4.7, 5.2, 5.3, 5.5 - -Three files: `Proof.lean` (proving in Lean), `PL.lean` (propositional logic) -and `FOL.lean` (predicate logic), included in that order. - -Doing logic in Lean is doing deduction — `intro` is →-introduction, `constructor` is ∧-introduction, `cases` on ∨ is ∨-elimination. CSwFP reaches deduction only in its inference engine (5.7); here it arrives with the logic itself. Deduction lives at the meta level, in `Prop` and the tactics. - -The chapter could carry a third object: a proof system *as data*, an inductive of derivations `Γ ⊢ A` over `Form`. CSLib already has one, so leaving it out is a decision rather than an omission — argued in "Reusing Mathlib and CSLib" above, and revisited in "Beyond CSwFP/6". - -**What is translated and what is written here.** Parts 2 and 3 below are -translations — CSwFP/4.4 for the syntax, 5.2 and 5.3 for the semantics — and -follow the original's structure. Parts 1 and 4 have no source: the first -condenses `logic_and_proof`, the second states a bridge the original cannot -state. Those two carry a structure of their own, and part 1's subheadings, one -per connective, are that structure — a connective's introduction and elimination -rules are what the section teaches. - -**The chapter's opening example was not CSwFP's, and is now removed.** -`PL.lean` used to open with a potassium/chlorine example adapted from -Enderton's *A Mathematical Introduction to Logic* — `K` for "traces of -potassium were observed", `C` for "the sample contained chlorine", four -compound sentences, and a truth table over them. It had no counterpart in -CSwFP, whose chapter 4 opens with Sea Battle. It went out with the chapter -reorganization of 2026-09-13: it taught the basics of propositional logic, -which `Proof.lean` now declares a prerequisite, and the chapter's own subject -is formalizing rather than logic itself. The `enderton2001` entry is left in -`Bib.lean`, unused. Recorded because a reader checking coverage might look for -a source passage for the old opening and find none. - -**The dresses puzzle moved to `Proof.lean`.** It was a `:::quiz` in `PL.lean`'s -introduction, and the section "Lógica Proposicional em Lean" — now in -`Proof.lean` — formalized it, opening with "Continuando a partir do quiz -anterior". The move broke that reference, so the puzzle goes with the section -that solves it, no longer as a quiz but as the worked example that opens it. - -Two divergences inside the translated part. CSwFP gives the semantics in two -sections, "Semantics of Propositional Logic" and "Propositional Reasoning in -Haskell"; here they are one, because the separation does not survive the move: -the definitions are already Lean from the first line, so there is no later point -at which implementation begins. And the discussion of what an empty conjunction -should be worth does not arise, since `top` and `bot` are constructors. - -**`Formula.eval` is split in two, so that Exercise 5.12 costs one argument -instead of a second evaluator.** CSwFP's 5.12 asks the reader to reimplement -the semantics with `[String]` for valuations, presence in the list standing for -truth, and its own answer (`Sols`, 5.12) is `altEval` — the whole recursion -written out a second time. Reproducing that here would put two near-identical -six-case recursions in the chapter, which is work for the reader and confusing -to read. - -Only the `atom` case of the recursion ever consults the valuation; the other -five combine the truth values of subformulas. So the recursion is -`Formula.evalWith`, which takes the atom lookup as a parameter -(`String → Bool`), and `Formula.eval` is the one-line case that looks the atom -up in the list of pairs. `eval` keeps its signature, so `allVals`, `tautology`, -`satisfiable`, `implies`, `update`, `denote` and every existing exercise are -untouched, and the exercise becomes: define the new lookup, pass it. The cost -is paid in the metatheorem proofs, whose `simp` sets now need `evalWith` -alongside `eval` to reach the constructor cases. - -The exercise stops at evaluation and does not ask for `tautology` or -`satisfiable` over the new representation. `genVals` *produces* valuations, and -the analogue for `List String` is the powerset — a genuinely different function, -needing a second parameter threaded through `allVals`. That is where -parameterizing stops being cheaper than duplicating, and it is past what the -exercise is for. `Formula.denote` is left alone for a different reason: it is -about the `Formula`→`Prop` reading, not about how a valuation is represented. - -**Proving in Lean is a section of its own, and it comes first.** The meta -level used to be presented three times: `IntroL.lean` introduced `Prop`, and -then `PL.lean` and `FOL.lean` each opened with the tactics for their own -connectives before reaching their actual subject. `Proof.lean` now holds all of -it — `Prop`, what counts as a proof, the tactics as the rules they are -(`apply`; `constructor` and anonymous constructors for ∧ and ↔; `left`, `right` -and `cases` for ∨; `False.elim` and `absurd` for ¬; `by_contra`, `by_cases` and -`em`; `intro`/`apply` for ∀, `use` and `obtain` for ∃), and proof by induction. -`IntroL.lean` is left deliberately pre-proof: it uses `example`, `theorem` and -`rfl` only as the shape an exercise's tests take, and says so. - -The consequence is that `PL.lean` and `FOL.lean` now have the same three-part -shape, and neither teaches Lean tactics: - -1. **Syntax as data** — BNF, then the `inductive` (4.4 for `Form`, 4.5–4.7 for `Formula`). Glued to it in `PL.lean`, the section that separates the two levels: `Form.conj p q` is data, `p ∧ q` is a proposition. Glued, not deferred — the confusion is born the instant the `inductive` appears. This is a cost Lean creates and Haskell does not have: there the meta level is invisible, living in the prose, so `data Form = ...` cannot be confused with it. -2. **Computable semantics** — 5.2 and 5.3 for `Form.eval` over valuations; 5.5 for `Formula.eval` over a model. -3. **The bridge** — interpreting the syntax into `Prop` (`denote`) and proving that the two readings agree. CSwFP cannot have this section. - -**`FOL.lean` gained its bridge section.** It previously had only a `Prop`-valued -`Formula.holds` and no computable semantics at all, so the chapter did not in -fact mirror `PL.lean` — there was nothing to bridge *from*. It now follows the -same shape: `Interp` returns `Bool` and `Formula.eval` computes, `Denot` returns -`Prop` and `Formula.denote` interprets, and `Formula.eval_iff_denote` relates -them. The bridge theorem needs a hypothesis `PL.lean`'s does not: `eval` decides -a quantifier by walking a list `dom`, so it agrees with the `∀` of Lean only -when `dom` lists every element of the domain. That hypothesis is the formal -counterpart of a real limitation, and the prose says so. - -**The model in `FOL.lean` is Enderton's, not CSwFP/6's.** Chapter 6's -fairy-tale model (`src/Model.hs`) was pulled forward for a while, to give 5.5 -something concrete to evaluate against. It is not any more, for two reasons. - -The first is that it belongs to CSwFP/6, which lands in `English.lean`: the -model exists to interpret the English fragment, so presenting it here and again -there would break the rule in `STYLE-WRITING.md` against presenting a -definition that a later chapter rephrases under the same name. It also arrived -unmotivated — ten named entities and eight predicates, several chapters before -anything linguistic. - -The second is that the section needs far less. What it teaches is that deciding -a quantifier means walking the domain, and eight predicates do not teach that -better than one does. The model is now the four-vertex directed graph of -{citep Bib.enderton2001}[]: a domain `{a, b, c, d}` and a single binary -predicate `E` with `E = {⟨a,b⟩, ⟨b,a⟩, ⟨b,c⟩, ⟨c,c⟩}`. Four formulas are -evaluated against that one fixed model rather than a fixed formula against -varying predicates, which is the tighter comparison; `d`, isolated, is the -witness that makes `∃x ∀y ¬E y x` true, and Enderton's own remark that the -symbolic version reads more easily than the English one survives the move. - -Removing the fairy-tale model also removed the `FOL.Entity` / `Sets.Entity` -name collision that `Sets.lean` carried a dev note about. - -**The domain is an `inductive` plus a `List`, and a theorem joins them.** -Declaring four constructors and then repeating them in `vertices` is a -duplication, and a silent hazard: a list that omits a constructor makes `eval` -run over a smaller domain than intended, with nothing to catch it. So the -chapter proves `mem_vertices : ∀ v, v ∈ vertices` by `cases v <;> decide`. -That one line is exactly the `hdom` hypothesis `eval_iff_denote` requires, so -`eval_iff_denote_B` instantiates the bridge theorem on the model with no -hypothesis left to discharge. The completeness of the domain is thereby visible -in the source rather than assumed. - -**`Fintype` was considered for this and rejected.** The alternative was to drop -`dom : List D` and decide quantifiers with `[Fintype D]` and -`decide (∀ d : D, …)`. It works — the resulting bridge theorem has no `hdom` -and both quantifier cases close by a bare `simp` — and it is still the wrong -choice, because `Fintype.decidableForallFintype` is *defined* as -`decidable_of_iff (∀ a ∈ Finset.univ, p a)`: a fold over a finite set, walking -every element exactly as `List.all` does. It is the same mechanism with the -hypothesis relocated into an instance where the reader can no longer see it, at -the cost of a type class, a hand-written instance and a duplicated recursion. - -Three findings from building it, recorded so the question is not reopened: -`deriving Fintype` fails on this toolchain (`enumList_nodup` type mismatch), so -the instance must be written by hand and repeats the constructors anyway; there -is no computable route from a `Fintype` to a `List` of its elements -(`Finset.univ.toList` and `Multiset.toList` are noncomputable, and -`Finset.univ.val.unquot` is unsafe); and `Fintype Nat` is refutable in one line -(`not_finite Nat`), so that route reaches infinite domains no better than the -list one does. - -**One evaluator, parameterized, where CSwFP has two.** CSwFP writes `eval` for -`Formula Variable` and a near-identical `evl` for `Formula Term`, differing -only in how a term is valued. Here `Formula.eval` and `Formula.denote` take -that as a parameter, `tval : Assign D → α → D`, and one definition serves both: -`varVal` for variables, `liftAssign fint` for structured terms. The parameter -takes the assignment and not just the term because the quantifier cases update -`g` and the term valuation has to see the update. This mirrors -`Formula.freeVars`, which the chapter already parameterizes over how to extract -a term's variables, and it leaves `eval_iff_denote` unchanged — same statement, -same proof, now quantified over `α`. - -**Two families of validity, because there are two formula types.** CSwFP -states validity and consequence once, for closed formulas of predicate logic, -and never has to say over what the definition ranges — it has no types to -range over. Here `Formula` is parameterized, so the definition has to pick: -`Formula.Valid`, `Formula.Satisfiable` and `Formula.Implies` are stated for -`Formula Variable`, and `Formula.ValidT` and `Formula.ImpliesL` for -`Formula Term`. The pair is not redundant. A structure for a language without -function symbols is `(D, I)`, and for one with them it is `(D, I, F)`; the two -definitions are exactly that difference, and `ValidT` is what makes the third -component visible. The pairing is deliberately incomplete: `Satisfiable` gains -no `Term` counterpart, because nothing in the chapter needs one. - -Unifying on `Formula Term` was measured before being rejected. The three -`Variable` definitions are used in 11 places, all inside `FOL.lean` — nothing -in `Sets.lean`, `InfEngine.lean` or any later chapter — and porting the seven -affected proofs is mechanical (`x` becomes `tx`, one extra binder in `intro`, -`liftAssign` for `varVal`); all seven still close. What decided it is the -recurring cost rather than the one-off one. Every counterexample over a -formula without function symbols would have to invent an inert -`FInterp` just to satisfy the signature, and `Formula Term` reintroduces the -unchecked pairing between a quantifier's `Variable` binder and its body's -`Term`s — in `Formula Variable` the two are the same object. Both prices are -paid on every future exercise, not once. - -**Consequence from a list of premises.** CSwFP generalizes `P ⊨ C` to -`P₁, …, Pₙ ⊨ C` in the prose between 5.24 and 5.25 without new machinery. -`Formula.ImpliesL` does the same, via `Formula.conjs`, and mirrors -`PL.Formula.impliesL` from the previous chapter — which is likewise an -exercise (`implies-from-list`, CSwFP/5.10) that later exercises then call. - -**CSwFP/6.5's `[0..]` becomes a theorem.** The original evaluates over the -infinite domain `[0..]`, relying on Haskell's laziness, and observes that the -procedure "will keep on trying candidates". That cannot be ported: Lean is not -lazy and `[0..]` is not constructible, so the computation cannot even start. -What the chapter says instead is stronger, and proved — `no_list_lists_Nat` -shows `∀ dom : List Nat, ∃ n, n ∉ dom`, so `eval_iff_denote`'s `hdom` is -*unsatisfiable* over `Nat` and no domain list exists to supply. `denote` -meanwhile needs no list, and `forallExistsR_true` proves `∀x ∃y R[x,y]` for any -interpretation reading `R` as `<`. The difference worth stating in the prose is -epistemic rather than a claim of superiority: in Haskell the limitation is -demonstrable, in Lean it is provable. - -The helper `le_foldr_max` is proved inline rather than imported. Mathlib's -`List.single_le_sum` needs an `IsOrderedAddMonoid` instance that the chapter's -imports do not carry, and widening them for one side remark costs more than the -five-line induction. - -**`Formula` is binary too.** Its `conj` and `disj` take two arguments, with `top` and `bot` as constructors and `Formula.conjs`/`Formula.disjs` recovering the n-ary notation — the same design as `Form`, for the same reason. A constructor holding a `List (Formula α)` would make the type a nested inductive, costing `induction` and `deriving`. The `List α` in `atom name (args : List α)` does not: `α` is a parameter, not the type being defined, so an atom may still take any number of arguments. With that, the definition of truth in 5.5 is a plain recursion, one case per constructor, instead of three mutually recursive functions. The one `mutual` block left in the chapter belongs to `Term`, where a list of terms inside `Term` is what function symbols of arbitrary arity require. - -**`mutual` is introduced here.** Its first use in the book's order is `FOL.lean`, and `English.lean` then uses it six times over for the fragment's mutually recursive categories. A note right after that first block — why a group of types that refer to one another has to be declared together, and what `mutual` therefore does — is enough; it does not need a section of its own, and it does not belong in `IntroL.lean`, where nothing would motivate it. - -**What is taken from `logic_and_proof`.** Only the chapters that teach *proving in Lean*; the ones that present logic on paper are already CSwFP's job, and covering the same ground twice is exactly the duplication this book avoids. Reference: . - -| `logic_and_proof` chapter | Taken | -|---------------------------------------------|--------------------------------------------------------------------------------------| -| `propositional_logic` | no — CSwFP/4.4 and 5.2 do this | -| `natural_deduction_for_propositional_logic` | the rule names only, to present each tactic as the rule it is | -| `propositional_logic_in_lean` | yes, condensed — this is the core of `PL.lean`'s first section | -| `classical_reasoning` | yes — needed for the two-valued valuation of 5.2, and for `Sets.lean`'s Exercise 2.3 | -| `semantics_of_propositional_logic` | no — CSwFP/5.2 and 5.3 do this | -| `first_order_logic` | no — CSwFP/4.5–4.7 do this | -| `natural_deduction_for_first_order_logic` | the rule names only | -| `first_order_logic_in_lean` | yes, condensed | -| `semantics_of_first_order_logic` | no — CSwFP/5.5 does this | - -`sets_in_lean` and `relations_in_lean` are the corresponding reference for `Sets.lean`, not for this chapter. - -**Representation note.** 5.5 is prose in CSwFP — a model is `M = (D, I)` with `I(P) = {1,3}` and `I(R) ⊆ D²`, and the text points back at the Cartesian product of 2.2. Mechanised here, before `Sets.lean` exists, the interpretation is represented by function types (`D → Prop`, `D → D → Prop`), which `IntroL.lean` already provides. This is also what CSwFP itself does once it writes code: `Model.hs` uses `type OnePlacePred = Entity -> Bool`. Mathlib's `Set` and `Rel` are deliberately *not* used here; they arrive in `Sets.lean`. - -**Two syntactic results of 4.4 change content, not just position.** Structural induction is not a theorem to state — it is the recursor that `inductive` generates. - -Unique readability is the other. In CSwFP it is a claim about *strings*: a formula written out as a sequence of symbols has exactly one parse tree, so the notation is unambiguous. In Lean there is no string to disambiguate — a term of type `Form` already *is* the tree, and `Form.conj p q` cannot be read two ways. The claim has nothing left to assert. - -Decision: `PL.lean` does not state unique readability as a theorem. What it states instead is what survives the translation — that the constructors are injective and pairwise disjoint, provable by `injection`, which is what Exercise 4.11 already does. The prose says why the original statement dissolves: the ambiguity it rules out is a property of writing formulas down, and the type never writes them down. Recovering the original claim would take a string to disambiguate — either a parser `String → Option Form` with a round-trip theorem, or the grammar stated as a `ContextFreeGrammar` so that `toString` can be shown to land in its language and to be injective. Both are deferred for the same reason: parsing and grammars-as-data are topics of their own, and nothing before CSwFP/6 needs either. See "Reusing Mathlib and CSLib"; it is the same question this chapter and `SeaBattle.lean` both run into. - -### 4. `Sets.lean` — CSwFP/2.1, 2.2 - -What is left of CSwFP/2 after 2.3, 2.4 and 2.5 moved to `IntroL.lean` and `English.lean`: sets and relations. Renamed from `Foundation.lean`, which promised a foundations chapter that no longer exists. `Sets` covers both halves honestly, because CSwFP/2.2 *defines* a relation as a subset of A × B — a relation is a set — and because what the chapter adds in Lean is precisely the representation choice for `Set α`. - -**What the chapter is.** Sets and relations are presupposed notation from CSwFP/1 onwards, as in any mathematical text — which is why 5.5 can speak of `I(R) ⊆ D²` before this chapter exists. This chapter is where they are *mechanised in Lean*, and its opening has to say so, or it promises the wrong thing. That is also what makes it worth having: Lean forces representation choices — `Set α` vs. the predicate `α → Bool` vs. `Finset`, `Rel` vs. a list of pairs, decidability — and those choices determine how the models of `ModelChecking.lean` are built. - -**Why after `Logic.lean`.** Nothing downstream requires this chapter — no later chapter fails to compile without it — but the chapter itself requires `Logic.lean`, and that is what fixes its position. Both reasons are about the exercises: - -- The chapter's point in Lean is *proving* theorems about sets and relations, which needs quantifiers and the connective tactics. `IntroL.lean`'s minimal `Prop` does not reach them; `Logic.lean` does. -- CSwFP's Exercise 2.3 is "check that A̿ = A". In Lean one direction requires classical reasoning (`¬¬P → P` does not hold constructively). Placed early, the third exercise of the book would force a conversation about the nature of negation before any truth table exists. After `Logic.lean`, `by_contra` and `em` are already presented and the exercise is routine. - -`Logic.lean` must therefore not use `Set` or `Rel` — see the representation note above. - -From the `logic_and_proof`, the chapters `sets_in_lean` and `relations_in_lean` can give some exercises or ideas on how to present sets and relations in Lean. - -### 5. `SeaBattle.lean` — CSwFP/4.1, 5.1 - -Syntax and semantics are presented one after the other, instead of split across two chapters: 4.1 for the grammar, 5.1 for the state-transition semantics. - -The grammar here is flattened into ordinary types — enumerations, `structure`s and `List` — rather than given as a value of Mathlib's `ContextFreeGrammar`; that is a decision, argued in "Reusing Mathlib and CSLib" above. - -**`Fin` is introduced here, not in `IntroL.lean`.** It is one of Lean's own basic types, needed by this grammar and nowhere else: `Fin 10` for a board row. `DEVIATIONS.md` states this as a general loosening of "presented" — a type needed in exactly one place is introduced where it is used. - -**The chapter comes after `Logic.lean` and `Sets.lean`.** Its exercises prove theorems about `WellFormed` by induction on an inductive predicate, which needs the tactics `Logic.lean` presents. Placing it earlier would mean either weaker exercises or a chapter that uses what the book has not shown. - -**Mastermind was removed.** CSwFP/4.1 carries the syntax of two games and 5.4 gives Mastermind's implementation, and an earlier arrangement of this book had both. It is dropped: the section was disconnected from the Sea Battle material that preceded it, and it announced a semantics in propositional logic that it never delivered — 5.4 opens by calling itself an application of propositional logic, but the propositional content is about eighteen lines that the implementation never uses. Reinstating Mastermind would mean writing that encoding rather than translating it. `PROVENANCE.md` records the exercises that went with it. - - -### 6. `Morphology.lean` — CSwFP/3.11, 3.14 - -`Applications` is too vague a name; the chapter is about morphology. Section 3.11 is split into two sections, `FinnishVowelHarmony` and `SwedishPlural` (CSwFP covers Swedish plural inside 3.11, pp. 54–55). Section 3.14 becomes `Phonemes`. - -A short introduction should note that although the book is not about morphology, these examples exercise the Lean concepts just learned. - -*Migration*: check that every Lean feature used here was presented in `IntroL.lean`. - -### 7. `InfEngine.lean` — CSwFP/4.3, 5.7 - -The language for talking about classes (4.3) and the inference engine over it (5.7), together instead of split across two chapters. - -4.3 is literally about classes, which is what makes it the chapter immediately after the one that mechanises them: - -| 4.3 fragment | 2.1 vocabulary | -|----------------------|----------------| -| `All PN are PN` | `A ⊆ B` | -| `No PN are PN` | `A ∩ B = ∅` | -| `Some PN are PN` | `A ∩ B ≠ ∅` | -| `Some PN are not PN` | `A \ B ≠ ∅` | - -CSwFP's `derive kb stmt` is proof search over syllogisms. Read as deduction over set inclusion, the validity of the syllogisms becomes provable in Lean — where CSwFP can only implement and test it. - -This chapter is independent of the English fragment: `InfEngine.hs` imports nothing from the syntax module. - -**What is translated and what is written here.** CSwFP/4.3 and the theory in 5.7 — Aristotle, the square of opposition, the knowledge base as inclusion and non-inclusion, the inference rules — are translated, and so is the engine: `rSection`, relational composition, the reflexive-transitive closure, `subsetRel`, `nsubsetRel`, `derive` and `tellAbout`. The closing section, which proves the syllogisms valid over `Set`, has no source: it is the payoff the plan promises, and the reason the chapter sits after `Sets.lean`. - -Three divergences. The least fixed point is computed with a fuel bound rather than by iterating until the value stops changing, because the latter has no structural termination argument; the bound is the square of the domain size, which is beyond what the closure can need. Relations are `List (α × α)`, named `Relation` rather than `Rel`, so that Mathlib's `Rel` — which `Sets.lean` introduces and this chapter's closing section uses through `Set` — keeps its name. And CSwFP/5.7's natural-language *input* is not ported: the parser, the file I/O and the `chat` loop are the only place in the book that would need `IO`, and the chapter states its interface through `ToString` on `Statement`, which is the output half. - -### 8. `English.lean` — CSwFP/4.2, 5.6 - -The fragment of English (4.2) and its semantics (5.6), plus the natural-language fragments that CSwFP scatters earlier and that `CSwL` deliberately does not present in place: the `likes` example of 2.4, the `Subject`/`Predicate` example of 3.13, and all of 2.5 — the `S → NP VP` this chapter always carried, and now the type BNF `τ ::= b | (τ → τ)` and the three typing rules as well. CSwFP introduces a slightly larger grammar in 4.2 and then, in 5.6, sketches the semantics of an initial vocabulary largely disconnected from it. Gathering these fragments in one place is the point of this chapter. - -**What this chapter must deliver to `ModelChecking.lean`.** Gathering the fragments is the editorial goal, but the chapter also has a hard obligation: CSwFP/6 translates the 4.2 grammar category by category, so every category it destructures has to exist by the end of this chapter. `MCWPL.hs` defines one translation function per category — `lfSent`, `lfNP`, `lfDET`, `lfCN`, `lfRCN`, `lfVP`, `lfTV`, `lfDV` — so the required inventory is: - -`Sent`, `NP`, `DET`, `CN`, `RCN`, `VP`, `TV`, `DV`, plus the auxiliaries `ADJ` and `That` that `RCN` uses. - -**Semantic types are named `e` and `t`, and that is not cosmetic.** The categorial section that arrived from CSwFP/2.5 originally wrote the semantic types as `NP`, `S`, `VP` and `TV` — the category names. In this chapter those names are already taken, by the `inductive`s that *are* the fragment's syntactic categories: two meanings for one name in one namespace, which does not compile and would not be worth compiling. The types now carry Montague's letters, `e` for entities and `t` for truth values, which the prose was already naming as the conventional choice; the categories keep `NP`/`VP` where they belong, in the prose. So "the VP has type `e → t`" now says two different things with two different notations, which is exactly the distinction the section is about. - -This is where the rest of 2.5 lands. The type BNF `τ ::= b | (τ → τ)` says that `e` and `t` are the two basic types and that everything else is built from them by `→`, and the three typing rules — a variable has the type it is declared with, `(λx ↦ E) : δ → τ` when `x : δ` and `E : τ`, `(E₁ E₂) : τ` when `E₁ : δ → τ` and `E₂ : δ` — are what licenses the composition the section then performs. They were in `IntroL.lean`, demonstrated over a `Day → Prop` predicate for want of anything better so early in the book; here they are demonstrated over the fragment's own types, which is what 2.5 was about in CSwFP. In Lean `t` is `Prop`. - -`INF` is part of the 4.2 grammar but has no translation in CSwFP/6; it is not required by `ModelChecking.lean`. - -### 9. CSwFP/6 — in `English.lean` - -Sections 6.1–6.5; 6.6 (Further Reading) omitted. - -**This material lands in `English.lean`, not in a chapter of its own.** The -plan once called for a separate `ModelChecking.lean`, and the table above and -the references below still use that name for the material; they should be read -as naming CSwFP/6's content, wherever it sits. The reason it belongs with the -English fragment is the one given immediately below: it is built on that -fragment, so the two are one development, not two. - -What this means for `FOL.lean` is recorded in the `Logic.lean` section above: -the fairy-tale model of 6.3 is *not* pulled forward into it any more. It -arrives here, next to the grammar it interprets, and `FOL.lean` evaluates -against Enderton's four-vertex graph instead. Sections 6.5's structured-term -evaluation and its `[0..]` discussion, by contrast, *are* in `FOL.lean`: they -are about the evaluator rather than about the fragment, and the chapter that -defines `Term` is where they belong. - -**This material must come after the fragment of 4.2.** CSwFP/6 does not merely allude to the fragment of 4.2 — it is built on it. The text says so ("to translate the fragment from Section 4.2 into predicate logic, all we have to do is find appropriate translations for all the categories in the grammar"), and the code confirms it: `MCWPL.hs` imports the syntax module and its first definition is `lfSent :: Sent -> LF`, destructuring `Sent np vp`. Placing the English fragment after model checking would use the grammar before presenting it. - -This is also why `Sets.lean` reads best just before it, though it is not required: `Model.hs` builds the model with `OnePlacePred = Entity -> Bool` and `list2OnePlacePred xs = \x -> elem x xs` — the characteristic function of 2.3 and the set-as-predicate of 2.1, applied. The choice between `Set Entity` and `Entity → Bool` is exactly the one `Sets.lean` makes. - -## Omitted throughout - -All "Further Reading" sections (1.8, 2.7, 3.15, 4.8, 5.8, 6.6), 1.7 (Overview of the Book), and 3.12 (Identifiers in Haskell). +The default is to reuse. What is reused today: `Set`, `Rel`, `Setoid`, +`Finset` and `Fintype` from Mathlib in `Sets`, `List.Chain` in `SeaBattle`, +and the tactic library. No chapter imports CSLib yet. + +- **CSLib's propositional logic is not used.** It would put a third object, + `Γ ⊢ A`, next to `Formula` and `Prop` in the reader's first logic chapter; + it takes `imp` as primitive where `Formula` takes `neg`; and it presents + minimal logic, with classical strength as axioms of a theory. CSLib has no + semantics for propositional logic and no first-order logic, so 5.2, 5.3 and + 5.5 have nothing to reuse. +- **`PL` defines a plain `eval` and states the bridge to `Prop` as ordinary + theorems**, not in CSLib's `Satisfies`/`HasInferenceSystem` shape. Adopting + the shape later is one structure, one instance and one notation on top of + `eval`, and belongs in a separate module. +- **Mathlib's `ContextFreeGrammar` is deferred.** `SeaBattle` models its BNF as + ordinary types, and nothing checks that the types match the grammar. The + library would supply that link, derivations, and unique readability for + `PL`. It would also mean giving each grammar twice and proving membership by + building `ReflTransGen` chains. The natural place is a closing section of + `SeaBattle`. Exercises 4.11, 4.15, 4.16 and 4.21 wait on it. +- **A proof system as data** (CSLib's `Derivation`) is deferred, not rejected. + Soundness needs CSLib's derivations and this book's valuations together. + Its natural place is after `Sets`, once CSwFP/1–6 are in place. + +## By chapter + +Where a CSwFP section went, and why, is in `CSwFP.yaml`. What follows are the +decisions inside the chapters. + +### `IntroL` + +- `instance` is presented here: later chapters declare instances, and no + chapter declares a `class`. +- `Prop` is not: `Logic` presents it, and every chapter that shows `Prop` + comes after `Logic`. `IntroL` uses `example` and `rfl` only as the shape of + an exercise's tests. + +### `Logic` + +- **`PL` and `FOL` have the same three parts**: syntax as an `inductive`, a + computable semantics, and the bridge that interprets the syntax into `Prop` + and proves the two readings agree. The bridge has no source. +- `Formula` is binary in both files, with `conjs`/`disjs` for the n-ary + notation. A constructor holding a `List Formula` would make the type nested, + costing `induction` and `deriving`. `mutual` is introduced in `FOL`, for + `Term`. +- Structural induction is the recursor `inductive` generates. Unique + readability is not stated: a term of `Formula` is already a tree, so there is + no string to disambiguate. +- The domain of the model in `FOL` is an `inductive` plus a `List`, joined by + `mem_vertices`, which discharges the hypothesis of the bridge theorem. + `Fintype` does not replace the `List`: its quantifier instance is the same + walk hidden in an instance, `deriving Fintype` fails on this toolchain, and + no computable route leads back to a `List`. +- One `eval` serves `Formula Variable` and `Formula Term`, taking the term + valuation as a parameter, where CSwFP has two evaluators. +- Validity comes in two families, `Valid`/`Satisfiable`/`Implies` for + `Formula Variable` and `ValidT`/`ImpliesL` for `Formula Term`: a structure + without function symbols is `(D, I)`, with them `(D, I, F)`. +- A model in `FOL` interprets predicates as functions (`D → Prop`), not with + `Set` or `Rel`, which arrive in `Sets`. +- `no_list_lists_Nat` proves that no list covers `Nat`, so the bridge + hypothesis cannot hold over `Nat`. + +### `InfEngine` + +- The least fixed point is computed with a fuel bound, the square of the + domain size, since iterating to a fixed point has no structural termination + argument. +- Relations are `List (α × α)`, named `Relation` so that Mathlib's `Rel` keeps + its name. +- The closing section, which proves syllogisms valid over `Set`, has no source. + +### `English` + +Being written (#29). Planned: the semantic types are named `e` and `t`, since +`NP`, `VP` and the other category names are the fragment's `inductive`s, and +the typing rules of 2.5 are shown over the fragment's own types. `INF` is in +the 4.2 grammar but has no translation in CSwFP/6. ## Beyond CSwFP/6 -Everything above is settled and covers CSwFP/1 to CSwFP/6. The rest of the book is deferred, and the placements below are provisional, not decisions. - -CSwFP/7 (The Composition of Meaning in Natural Language) goes after `ModelChecking.lean`. It continues `English.lean`'s fragment and, in CSwFP, builds on the same syntax module, so the same constraint that puts `English.lean` before `ModelChecking.lean` keeps 7 downstream of both. How much of `English.lean` it absorbs — CSwFP/7 is where a consolidated semantics of a natural-language fragment actually appears — is the question to settle when that chapter is taken up. - -A proof system as data — CSLib's `Cslib.Logic.PL.Theory.Derivation` — is deferred rather than rejected, for the reasons in the `Logic.lean` section. It becomes attractive exactly where `CSwL` would have something to give back: CSLib has the derivations but no propositional semantics, and this book builds the valuation. Soundness — every derivable sequent is true under every valuation satisfying its context — needs both halves, and neither project has both today. `Cslib/Logics/README.md` invites exactly this ("we are interested in expanding them or creating new ones that can cover your use cases"). Its natural place is after `Sets.lean`, once relations and quantifiers are available. It stays out of the plan until CSwFP/1–6 are in place. - -Mathlib's `ContextFreeGrammar` for the grammar of `SeaBattle.lean` is deferred on the same footing, and for reasons that are ours rather than the library's — see "Reusing Mathlib and CSLib". It is the one deferred item that would change a chapter already written, so it belongs after the pending work already tracked, not before it. - -The related question — whether `PL.lean`'s valuation is written in CSLib's shape from the start — is settled above, and settled against it. - -Chapters 8 onwards are not planned yet. +Not planned yet. CSwFP/7 continues the fragment of `English` and builds on the +same syntax, so it comes after `English`. diff --git a/PROVENANCE.md b/PROVENANCE.md deleted file mode 100644 index 886827b..0000000 --- a/PROVENANCE.md +++ /dev/null @@ -1,352 +0,0 @@ -# Exercise provenance - -Which CSwFP exercise each `CSwL` exercise comes from. This mapping -used to live in the book's own prose, as `Ref. CSwFP/4, exercício 4.9 -(p. 74)` lines; the book must be self-contained and never name its -source, so those lines are removed and the correspondence is kept here -instead. - -This file is for the instructor: checking coverage (which of the -book's exercises are ported, which are still missing) and finding the -original statement when an exercise needs revising. It is -documentation *about* the project, not part of the book. - -The `CSwL id` column holds each exercise's `(name := …)`. Since the -rename of 2026-08-30 these are English mnemonics carrying no number, -so **this file is now the only link between an exercise and the -passage it comes from**. Keep it in step with any further rename. - -`prose` marks an exercise whose answer is given in prose rather than -stated in Lean. In the source these carry a `✎` marker, which is -otherwise undocumented. - -Every exercise of the book appears somewhere below, either in a table -that names its source or in the list of those with no counterpart; and -every id cited in a `CSwL id` column is the name of an exercise. -`scripts/check-provenance.sh` checks both and lists what disagrees. - -## A correction to the numbers - -The 17 references in `Sets.lean` were all off by one chapter: they -read `CSwFP/2, exercício 3.N` where the book has **Exercise 2.N**. The -page numbers they cite were right, which is what makes the shift -visible — CSwFP's Exercise 2.1 is on p. 17, and the file cited -"exercício 3.1 (p. 17)". The book's chapter 2 has exercises 2.1 to -2.17, and there are exactly 17 of them. - -The table below carries the corrected numbers. `IntroCS.lean`, -`Logic/PL.lean`, `Logic/FOL.lean` and `Morphology/Phonemes.lean` were -checked against the same source and are correct. - -## Exercises taken from CSwFP - -### `IntroCS.lean` — CSwFP/1 - -| CSwL id | Rating | CSwFP | Page | -|------------------|--------|--------------|------| -| `possibilities` | 1 | Exercise 1.1 | 6 | -| `sentence-go-on` | 1 | Exercise 1.2 | 8 | - -CSwFP Exercise 1.3 (infinitely many sentences, p. 8) is not ported. - -### `Morphology/Phonemes.lean` — CSwFP/3.14 - -| CSwL id | Rating | CSwFP | Page | -|---------------------|--------|-----------------------------------------|-------| -| `yawelmani-harmony` | 3 | Exercise 3.19 (Yawelmani vowel harmony) | 61–62 | - -`feature-value` (rating 2) and `append-suffix-text` (rating 3) have no counterpart: -CSwFP hands `feature-value`/`fMatch` to the reader as given code, and `CSwL` turns -them into exercises. - -### `Sets.lean` — CSwFP/2 (exercises `twice` and `adjective-types` moved on with CSwFP/2.4 and 2.5, to `IntroL.lean` and `English.lean`) - -| CSwL id | Rating | CSwFP | Page | Notes | -|-----------------------------|--------|---------------|-------|--------------------------------------| -| `empty-subset` | 1 | Exercise 2.1 | 17 | | -| `empty-vs-singleton` | 1 | Exercise 2.2 | 17 | prose | -| `double-complement` | 2 | Exercise 2.3 | 17 | prose | -| `cartesian-square` | 2 | Exercise 2.4 | 18 | | -| `successor-composition` | 2 | Exercise 2.5 | 18 | | -| `converse-subset` | 2 | Exercise 2.6 | 18 | | -| `which-are-transitive` | 2 | Exercise 2.7 | 19 | | -| `transitive-iff-comp` | 2 | Exercise 2.8 | 19 | | -| `transitive-not-idempotent` | 2 | Exercise 2.9 | 19 | | -| `successor-as-relation` | 1 | Exercise 2.10 | 21 | | -| `leq-as-function` | 1 | Exercise 2.11 | 21 | | -| `graph-is-functional` | 2 | Exercise 2.12 | 21 | | -| `twice` | 1 | Exercise 2.13 | 26 | | -| — | — | Exercise 2.14 | 26–27 | prose; not in an `:::exercise` block | -| — | — | Exercise 2.15 | 28 | prose; not in an `:::exercise` block | -| — | — | Exercise 2.16 | 28 | prose; not in an `:::exercise` block | -| `adjective-types` | 1 | Exercise 2.17 | 30 | | - - -Note that 2.14, 2.15 and 2.16 sit in the prose without an exercise -directive, so they get no rating, no solution elision and no -autograding. - -Exercises 2.1, 2.2 and 2.3 (`empty-subset`–`double-complement` above) -stay with this chapter when it moves after `Logic.lean`; 2.3 (`Ā̄ = A`) -is the one that needs classical reasoning, and is the reason for the -move. - -### `SeaBattle.lean` - CSwFP/4.1 - -- Exercise 4.1 is `game-over-grammar` (prose now, but better change to Lean code) - -### Mastermind — dropped - -| CSwL id | Rating | CSwFP | Page | Notes | -|---------|--------|-------|------|-------| -| — | — | Exercise 5.13 | — | dropped 2026-09-13 | -| — | — | Exercise 5.14 | — | dropped 2026-09-13 | -| — | — | Exercise 5.15 | — | dropped 2026-09-13 | -| — | — | Exercise 5.16 | — | dropped 2026-09-13 | - -`Games/Mastermind.lean` was removed with the chapter reorganization: it was -disconnected from what preceded it, and it promised a semantics in -propositional logic that it never gave. Two exercises went with it, -`four-turn-game` and `chess-grammar`, along with CSwFP/5.13–5.16, which had no -`CSwL` counterpart in the first place. - -### `Logic/Proof.lean` - -No exercise from CSwFP, all exercises were created. - -### `Logic/PL.lean` - -Source: CSwFP/4.4 CSwFP/5.2 CSwFP/5.3 - -Exercise 4.9 translation of NL to PL -= bangu-form -obs: temos também bangu-proof - -Exercise 4.10 xor -= exclusive-or - -Exercise 4.11 about the grammar -obs: we need ContextFreeGrammar from Mathlib - -Exercise 4.12 opsNr -= count-operators - -Exercise 4.13 depth -= formula-depth - -Exercise 4.14 propNames -= collect-atoms - -*novo* -= collect-atoms-alternative -obs: alternative for `names` without mergeSort and `eraseDups` - -Exercise 5.4 evaluation of formulas -= valuations - -Exercise 5.5 negation of a tautology is always a contradiction, and vice-verssa -obs: in the prose - -*novo* -= ex-pl-contingent -obs: definition of contingent - -Exercise 5.6 quais formulas sao sat e para elas me da v! -= ex-pl-satisfiable - -Exercise 5.7 quais equiv sao verdade! -= ex-pl-equiv - -Exercise 5.8 Which of the following are true? -= pl-consequence -dep: implies-from-list - -Exercise 5.9 Show principle of contraposition -obs: in the prose - -Exercise 5.10 implementar impliesL -= implies-from-list - -*novo* -= bangu-proof -dep: bangu-form -obs: complete problem using logical consequence - -Exercise 5.11 implement equivalence -obs: in the prose - -Exercise 5.12 redefine Valuation from [(String, Bool)] -obs: implemented in the prose - - -### `Logic/FOL.lean` — CSwFP/4.5–4.7 - -Exercise 4.15 uniq readable -obs: not applicable without ContextFreeGrammar from Mathlib - -Exercise 4.16 alternative BNF -obs: not formalizable without ContextFreeGrammar - -Exercise 4.17 bound ocurrences of x in a formula -= ex-fol-freevars - -Exercise 4.18 closedForm -= ex-fol-closedform - -Exercise 4.19 withoutIDs -= ex-fol-remove-impl_equiv - -Exercise 4.20 nnf -= ex-fol-nnf - -Exercise 4.21 parse tree of terms -obs: not applicable without ContextFreeGrammar - -Exercise 4.22 implement varsInForm -= ex-fol-vars-in-formula - -Exercise 4.23 implement freeVarsInForm -= ex-fol-free-vars-in-form - -Exercise 4.24 openForm -= ex-fol-open-form - -Exercise 5.17 all/exists weak/strong -= ex-fol-weak-strong - -Exercise 5.18 translate to FOL -= ex-fol-translate - -Exercise 5.19 check formulas model given -= ex-fol-model - -Exercise 5.20 consequence are true? -= ex-fol-valid - -Exercise 5.21 substitute vars in terms -obs: alternative definition, introduce names in the language - -Exercise 5.22 language extension -obs: alternative definition, use 5.21 semantics of language + names - assigments - -Exercise 5.23 Write out the truth definition for formulas with terms -obs: in the prose - -Exercise 5.24 logical consequences a |= b holds? -= ex-fol-consequence - -*novo* -= ex-fol-implies-from-list -obs: FOL analogue of implies-from-list (CSwFP/5.10); drawn from the prose - between 5.24 and 5.25, "We can make this slightly more general by - allowing sets of more than one premise" - -Exercise 5.25 logical consequences Delta |= b holds? -= ex-fol-entails -dep: ex-fol-implies-from-list - - -### `InfEngine.lean` — CSwFP/5.7 - -| CSwL id | Rating | CSwFP | Page | Notes | -|---------|--------|---------------|------|------------| -| — | — | Exercise 5.28 | 109 | not ported | -| — | — | Exercise 5.29 | 109 | not ported | - - -## Exercises not ported, and why - -An exercise absent from the tables above is a decision, not an oversight. The -reasons fall into three kinds. - -**It asks for alternative definitions that are irrelevante.** CSwFP/5.21 defines -substitution of a name for a variable in a term, and 5.22 asks for a truth -definition that replaces assignments by names plus substitution. Both need -rename of variables, never defines. - -CSwFP/5.23 — the truth definition extended to structured terms, we -decided to add it in the prose, many other parts of the prose would -need it, having it undefined would make the presentation harder. - -**It asks for a variant implementation.** 5.12 asks to reimplement -the semantics with `[String]` instead of `[(String, Bool)]` for -valuations. The semantics in PL now uses `Variable -> Bool`. - -CSwFP/5.28 and 5.29 ask for soundness and completeness of the Aristotelian -inference system. Soundness is within reach — `InfEngine.lean` already proves -BARBARA, CELARENT and DARII valid over `Set` — but completeness needs a model -construction the chapter does not have. - -## Exercises original to CSwL - -No CSwFP counterpart. Listed so that "absent from the table above" is not read -as an oversight. - -| File | CSwL id | Rating | -|---------------------------------|----------------------------|--------| -| `Morphology/Phonemes.lean` | `feature-value` | 2 | -| `Morphology/Phonemes.lean` | `append-suffix-text` | 3 | -| `Morphology/SwedishPlural.lean` | `swedish-plural` | 2 | -| `English.lean` | `preposition-phrase` | 1 | -| `English.lean` | `complex-relative-clauses` | 1 | -| `Sets.lean` | `five-in-above2` | 1 | -| `Sets.lean` | `one-not-in-above2` | 1 | -| `Sets.lean` | `above5-subset-above2` | 1 | -| `Sets.lean` | `union-contains` | 1 | -| `Sets.lean` | `intersection-contained` | 1 | -| `SeaBattle.lean` | `game-over-grammar` | 2 | -| `SeaBattle.lean` | `defeated-last` | 3 | -| `SeaBattle.lean` | `add-ship` | 3 | -| `SeaBattle.lean` | `sunk` | 2 | -| `SeaBattle.lean` | `grice-maxims` | 1 | -| `IntroL.lean` | `sum-of-squares` | 1 | -| `IntroL.lean` | `building-terms` | 1 | -| `IntroL.lean` | `rfl-arithmetic` | 1 | -| `IntroL.lean` | `square-unfold` | 1 | -| `IntroL.lean` | `identity-implication` | 1 | -| `IntroL.lean` | `p-implies-q-implies-p` | 1 | -| `IntroL.lean` | `and-intro` | 1 | -| `IntroL.lean` | `and-comm` | 2 | -| `IntroL.lean` | `implication-transitivity` | 1 | -| `IntroL.lean` | `apply-several-premises` | 1 | -| `IntroL.lean` | `unfold-direct-proof` | 1 | -| `IntroL.lean` | `unfold-conjunction` | 1 | -| `IntroL.lean` | `exists-witness` | 1 | -| `IntroL.lean` | `cases-on-or` | 1 | -| `IntroL.lean` | `add-zero-induction` | 1 | -| `IntroL.lean` | `sum-to` | 1 | -| `IntroL.lean` | `sum-list` | 1 | -| `IntroL.lean` | `count-zeros` | 1 | -| `Logic/PL.lean` | `contrapositive` | 1 | -| `Logic/PL.lean` | `de-morgan` | 2 | -| `Logic/PL.lean` | `exchange-prop` | 1 | -| `Logic/PL.lean` | `dresses` | 2 | -| `Logic/PL.lean` | `bangu-form` | 1 | -| `Logic/PL.lean` | `bangu-proof` | 1 | -| `Logic/FOL.lean` | `forall-exists-swap` | 2 | -| `Logic/FOL.lean` | `ex-fol-implies-from-list` | 2 | -| `InfEngine.lean` | `inconsistent-kb` | 2 | -| `InfEngine.lean` | `ferio` | 2 | - -CSwFP's chapter 3 exercises 3.1–3.18 are not ported: they are about Haskell -itself (types of Haskell functions, Haskell programs to read). Exercise 3.18 -(the type of `vh`, p. 54) belongs with Finnish vowel harmony and is the one -worth reconsidering. - -## Section-level references - -These were also `Ref.` lines in the book's prose. The chapter-level mapping now -lives in `DEVIATIONS.md`; this table records the finer-grained pointers that -existed inside chapters. - -| File | Section | CSwFP | Page | -|----------------------------|-----------------|------------------------------------------------------------|--------| -| `IntroCS.lean` | chapter opening | CSwFP/1 Formal Study of Natural Language | — | -| `IntroL.lean` | Tipos indutivos | §3.13 | 55 | -| `IntroL.lean` | Casamento de Padrões, Recursão e Indução | §3.5 | 40 | -| `IntroL.lean` | Listas | §3.6, and §3.4 for polymorphism | 41, 39 | -| `IntroL.lean` | `map`/`filter` | §3.7, §3.8 | 42–43 | -| `IntroL.lean` | Type classes | §3.9 | 45 | -| `IntroL.lean` | Strings | §3.10 | 47–48 | -| `Sets.lean` | chapter opening | CSwFP/2 Lambda Calculus, Types, and Functional Programming | — | -| `Morphology/Phonemes.lean` | chapter opening | §3.14 | 58–61 | diff --git a/README.md b/README.md index 6b2a577..1db1376 100644 --- a/README.md +++ b/README.md @@ -47,7 +47,7 @@ adapts — see [DEVIATIONS.md](DEVIATIONS.md) for why. [`CSwL/Morphology/`](CSwL/Morphology)) - [~] An inference engine — [source](CSwL/InfEngine.lean) - [~] A fragment of English — [source](CSwL/English.lean) -- [ ] Model checking with predicate logic — `CSwL/ModelChecking.lean` +- [ ] Model checking with predicate logic — in `CSwL/English.lean` - [ ] The composition of meaning - [ ] Extension and intension - [ ] Parsing diff --git a/STYLE-CODE.md b/STYLE-CODE.md index 0d39192..a8b71a1 100644 --- a/STYLE-CODE.md +++ b/STYLE-CODE.md @@ -10,10 +10,17 @@ code comments, commit messages — is in English. ## The hard constraint: nothing is used before it is presented -`DEVIATIONS.md` states the rule that governs the whole book: +One rule governs the whole book: > **Nothing is used before it is presented.** +It has one loosening and one exception. The loosening: a basic type of Lean's +own may be introduced where it is first needed, in a sentence or two with a +citation of the Lean Language Reference (`{citep Bib.LLR}[]`), rather than in +`IntroL`. `Fin` in `SeaBattle` is the case. This covers types the language +already gives, never a construct this book defines, and never one that needs +more than a short paragraph. The exception is `IntroCS`, described below. + In a book whose chapters are largely programs rather than proofs, this covers **every Lean feature**, not only tactics: commands, declaration forms, syntax, notation, standard-library types, and typeclasses alike. A reader meeting @@ -139,8 +146,9 @@ author decision, not a mechanical fix. `IntroCS` is the constraint's one accepted exception: it uses Lean that `IntroL` only presents later, deliberately, and the chapter says so where its first code block appears — the code is there to show where the book is going, -nothing in it is presented, and reading it is optional. `DEVIATIONS.md` -records the decision. +nothing in it is presented, and reading it is optional. Without that sentence +the chapter is not a teaser but an unannounced prerequisite. The exception does +not extend to any other chapter. ## Verso markup @@ -192,7 +200,7 @@ error rather than a dropped import. ### Exercises and solutions `:::exercise (rating := N) (name := "mnemonic")` — an exercise. `rating` is -difficulty, 1 to 5. `name` is the identifier used by `PROVENANCE.md` and by +difficulty, 1 to 5. `name` is the identifier used by `CSwFP.yaml` and by the grading variant, and follows the mnemonic rule. Inside an exercise, the answer is wrapped so the build variants can strip it: diff --git a/STYLE-WRITING.md b/STYLE-WRITING.md index 9b5d6a1..e585bc5 100644 --- a/STYLE-WRITING.md +++ b/STYLE-WRITING.md @@ -26,11 +26,29 @@ has not read the book this one adapts and does not need to know Haskell. The book is self-contained: it never names sections, pages, or exercises of another work, and it never explains itself by contrast with one. -`DEVIATIONS.md` draws the line precisely, and that discussion is not repeated -here: a **technical consequence in Lean** is content, because the reader will -meet it; an **editorial preference** is meta, and belongs in `DEVIATIONS.md`. +The line to hold is not "never mention an alternative". It is: + +- a **technical consequence in Lean** is content, because the reader will + meet it. "A constructor holding a `List Formula` makes the type a nested + inductive, and a nested inductive has no `induction` tactic" states a fact + about Lean that the chapter then depends on; +- an **editorial preference** is meta. "We preferred to keep `Game` as it is", + "the columns could have been modelled like the rows, but we chose the usual + convention" report what the authors decided, and belong in `DEVIATIONS.md`. + The test is whether the sentence would still be worth writing if this book had -no source and no alternatives. +no source and no alternatives. A fact about Lean survives that; a preference +does not. No search finds a sentence that fails it, so the prose has to be +read; `scripts/check-cswfp.py` only catches the explicit cases, a citation of +CSwFP or of a page, section or exercise number outside a `:::dev` note. + +**A translated section keeps the original's structure**: its section +boundaries, its order, its sentence boundaries and its punctuation. Most +chapters are mixed, part translated and part written here because Lean makes +something sayable that the source could not say. A new section has a +structure of its own, chosen for what it teaches. `CSwFP.yaml` records which +CSwFP section each chapter takes, and `DEVIATIONS.md` records any departure +from it and why. **The course is not about Lean.** Lean is introduced as far as the semantics needs it and no further. A feature that earns no work in a later chapter does diff --git a/scripts/check-cswfp.py b/scripts/check-cswfp.py new file mode 100755 index 0000000..f3fe56d --- /dev/null +++ b/scripts/check-cswfp.py @@ -0,0 +1,117 @@ +#!/usr/bin/env python3 +"""Check the book against `CSwFP.yaml` and against the rule that the book +never names its source: + + - every `:::exercise` under `CSwL/` is listed once in `CSwFP.yaml`, either + as the CSwL exercise of a CSwFP exercise or under `original`; + - every exercise named in `CSwFP.yaml` exists under `CSwL/`; + - every exercise of CSwFP/1-6 is listed, in order; + - every chapter named in `sections` is a file under `CSwL/`; + - no prose outside a `:::dev` note cites CSwFP, or a page, section or + exercise number (see `STYLE-WRITING.md`). + +Prints each problem and exits with status 1 if there is any. `TODO` reasons +are listed but are not problems. + +Needs PyYAML (`pip install pyyaml`). + +Usage: scripts/check-cswfp.py +""" + +import re +import sys +from pathlib import Path + +import yaml + +ROOT = Path(__file__).resolve().parent.parent +BOOK = ROOT / "CSwL" +DATA = yaml.safe_load((ROOT / "CSwFP.yaml").read_text()) + +# How many exercises each CSwFP chapter has. +COUNTS = {"CSwFP/1": 3, "CSwFP/2": 17, "CSwFP/3": 19, + "CSwFP/4": 24, "CSwFP/5": 32, "CSwFP/6": 7} + +EXERCISE = re.compile(r'^:+exercise\b.*\(name := "([^"]+)"\)') +CITATION = re.compile(r"CSwFP|página \d+|\(p\. \d+|§\s*\d|exemplo \(\d+\.\d+\)" + r"|Exercício \d+\.\d+|Seção \d+\.\d+") +DEV = re.compile(r"^(:+)dev\b") + + +def is_exercise_name(value): + """A value with no space in it is the name of a CSwL exercise; anything + else is the reason the exercise was not ported.""" + return (isinstance(value, str) and not re.search(r"\s", value) + and not value.startswith("TODO")) + + +problems = [] +todos = [] + +sources = sorted(BOOK.rglob("*.lean")) + +# Exercises in the book, name -> file. +book = {} +for path in sources: + for line in path.read_text().splitlines(): + if m := EXERCISE.match(line): + book[m[1]] = path.relative_to(BOOK).as_posix() + +# Exercises named in `CSwFP.yaml`, name -> times listed. +listed = {} +for chapter, exercises in DATA["exercises"].items(): + numbers = [int(re.match(r"\d+\.(\d+)", key)[1]) for key in exercises] + if numbers != list(range(1, COUNTS[chapter] + 1)): + problems.append(f"{chapter}: exercises are not numbered 1 to {COUNTS[chapter]}") + for key, value in exercises.items(): + if is_exercise_name(value): + listed[value] = listed.get(value, 0) + 1 + elif str(value).startswith("TODO"): + todos.append(f"{key}: {value}") +for names in DATA["original"].values(): + for name in names: + listed[name] = listed.get(name, 0) + 1 + +for name, path in book.items(): + if name not in listed: + problems.append(f"not in CSwFP.yaml: {name} ({path})") + elif listed[name] > 1: + problems.append(f"listed more than once: {name}") + +named = set(listed) +for exercise, needed in DATA["depends"].items(): + named |= {exercise, needed} +for name in sorted(named - set(book)): + problems.append(f"no such exercise: {name}") + +# Chapters named in `sections`. +chapters = {path.relative_to(BOOK).with_suffix("").as_posix() for path in sources} +for sections in DATA["sections"].values(): + if not isinstance(sections, dict): + continue + for section, value in sections.items(): + target = value["to"] if isinstance(value, dict) else value + chapter = re.match(r"[^,\s]+", target)[0] + if chapter not in {"omitted", "absorbed", "dropped"} | chapters: + problems.append(f"no such chapter: {chapter} ({section})") + +# Prose that cites the source. +for path in sources: + fence = None + for number, line in enumerate(path.read_text().splitlines(), 1): + if m := DEV.match(line): + fence = m[1] + elif fence and line.strip() == fence: + fence = None + elif not fence and CITATION.search(line): + problems.append(f"cites the source: " + f"{path.relative_to(ROOT).as_posix()}:{number}") + +print("\n".join(problems)) +if todos: + if problems: + print() + print(f"{len(todos)} exercises still to decide:") + for todo in todos: + print(f" {todo}") +sys.exit(1 if problems else 0) diff --git a/scripts/check-provenance.sh b/scripts/check-provenance.sh deleted file mode 100755 index 5e08e71..0000000 --- a/scripts/check-provenance.sh +++ /dev/null @@ -1,53 +0,0 @@ -#!/usr/bin/env bash -# Checks that `PROVENANCE.md` and the book's exercises agree: -# -# - every `(name := "…")` of an `:::exercise` block under `CSwL/` is -# mentioned in `PROVENANCE.md`; -# - every id in a `CSwL id` column of a table in `PROVENANCE.md` is the -# name of an exercise under `CSwL/`. -# -# Prints each discrepancy and exits with status 1 if there is any. -# -# Usage: scripts/check-provenance.sh - -set -euo pipefail - -CSWL_DIR="$(cd "$(dirname "${BASH_SOURCE[0]}")/.." && pwd)" -PROVENANCE="$CSWL_DIR/PROVENANCE.md" - -# Names of the exercises in the book. -exercises="$(grep -rhE '^:+exercise' "$CSWL_DIR/CSwL" --include='*.lean' \ - | sed -nE 's/.*\(name := "([^"]+)"\).*/\1/p' | sort -u)" - -# Ids in the `CSwL id` column of every table, skipping `—` placeholders. -cited="$(awk -F'|' ' - /^\|/ { - if (!col) { - for (i = 2; i < NF; i++) if ($i ~ /CSwL id/) col = i - } else if ($col !~ /^[ -]*$/) { - id = $col; gsub(/[ `]/, "", id) - if (id != "—") print id - } - next - } - { col = 0 } -' "$PROVENANCE" | sort -u)" - -status=0 - -while IFS= read -r name; do - if ! grep -qE "(^|[^[:alnum:]_-])${name}([^[:alnum:]_-]|$)" "$PROVENANCE"; then - echo "not in PROVENANCE.md: $name" - status=1 - fi -done <<< "$exercises" - -while IFS= read -r id; do - [ -z "$id" ] && continue - if ! grep -qxF "$id" <<< "$exercises"; then - echo "no such exercise: $id" - status=1 - fi -done <<< "$cited" - -exit $status