From 0d16e25d7b3870e6578fc02ab00d3ffea98c44ce Mon Sep 17 00:00:00 2001 From: Alexandre Rademaker Date: Wed, 9 Sep 2026 09:32:23 -0300 Subject: [PATCH 1/5] drafts --- CSwL/Logic/FOL.lean | 2 + doc/entailment.md | 124 ++++++++++++++++++++++ doc/fol-semantics.md | 246 +++++++++++++++++++++++++++++++++++++++++++ 3 files changed, 372 insertions(+) create mode 100644 doc/entailment.md create mode 100644 doc/fol-semantics.md diff --git a/CSwL/Logic/FOL.lean b/CSwL/Logic/FOL.lean index 6609976..92b2d2c 100644 --- a/CSwL/Logic/FOL.lean +++ b/CSwL/Logic/FOL.lean @@ -5,6 +5,8 @@ import Mathlib.Tactic.Use open Verso.Genre Manual open CSwLMeta +set_option verso.code.warnLineLength 100 + #doc (Manual) "Lógica de predicados" => %%% tag := "FOL" diff --git a/doc/entailment.md b/doc/entailment.md new file mode 100644 index 0000000..3b3b773 --- /dev/null +++ b/doc/entailment.md @@ -0,0 +1,124 @@ + +### Exemplo + +Suponha três proposições: + +* \(p\): Alice está na sala. +* \(q\): Bob está na sala. +* \(r\): Carol está na sala. + +Sem nenhuma informação adicional, temos \(2^3=8\) interpretações possíveis: + +| \(p\) | \(q\) | \(r\) | +| ----- | ----- | ----- | +| F | F | F | +| F | F | V | +| F | V | F | +| F | V | V | +| V | F | F | +| V | F | V | +| V | V | F | +| V | V | V | + +Agora suponha que sabemos: + +$$ +\Gamma = \{p \lor q,\quad \neg r\} +$$ + +Ou seja: + +1. **Alice ou Bob está na sala.** +2. **Carol não está na sala.** + +A pergunta passa a ser: + +> Quais interpretações são compatíveis com \(\Gamma\)? + +As interpretações admissíveis são apenas: + +| \(p\) | \(q\) | \(r\) | \(p\lor q\) | \(\neg r\) | +| ----- | ----- | ----- | ----------- | ---------- | +| F | V | F | V | V | +| V | F | F | V | V | +| V | V | F | V | V | + +Ou seja, podemos definir: + +$$ +\operatorname{Mod}(\Gamma) += +\{I\mid I\models\varphi\text{ para toda }\varphi\in\Gamma\}. +$$ + +E então temos a ideia que eu enfatizaria para os alunos: + +> **Uma fórmula não determina uma interpretação; ela elimina interpretações que não são compatíveis com ela. Um conjunto de fórmulas elimina ainda mais interpretações.** + +Isso prepara muito naturalmente a definição de consequência lógica: + +$$ +\Gamma\models\varphi +$$ + +significa: + +> **toda interpretação que sobrevive às restrições impostas por \(\Gamma\) também satisfaz \(\varphi\).** + +### Um passo particularmente didático + +Depois pergunte: + +> A partir de \(\Gamma=\{p\lor q,\neg r\}\), podemos concluir \(p\)? + +Não, porque ainda sobrevive a interpretação \(p=F,q=V,r=F\). + +Podemos concluir \(p\lor q\)? Sim — trivialmente, porque essa é uma das restrições. + +Podemos concluir \(\neg r\)? Sim. + +Agora acrescente: + +$$ +q\rightarrow \neg p +$$ + +Então as interpretações sobreviventes passam a ser apenas: + +| \(p\) | \(q\) | \(r\) | +| ----- | ----- | ----- | +| F | V | F | +| V | F | F | + +E agora **\(p\) e \(q\) continuam indeterminados individualmente**. + +Se acrescentarmos ainda: + +$$ +q +$$ + +resta uma única interpretação: + +$$ +p=F,\quad q=V,\quad r=F. +$$ + +Esse é um excelente momento para mostrar a diferença entre: + +* **satisfatibilidade:** existe uma interpretação que satisfaz \(\Gamma\); +* **consequência lógica:** todas as interpretações que satisfazem \(\Gamma\) satisfazem \(\varphi\); +* **teoria completa:** \(\Gamma\) restringe as interpretações a uma única valuation, nesse exemplo. + +E isso conecta diretamente com dedução natural: + +$$ +\Gamma\vdash\varphi +$$ + +é a afirmação sintática correspondente à ideia semântica + +$$ +\Gamma\models\varphi. +$$ + diff --git a/doc/fol-semantics.md b/doc/fol-semantics.md new file mode 100644 index 0000000..d10b0b8 --- /dev/null +++ b/doc/fol-semantics.md @@ -0,0 +1,246 @@ + +A grande mudança em relação à lógica proposicional é justamente esta: + +> Na proposicional, uma interpretação diz quais proposições são verdadeiras. + +> Na primeira ordem, uma interpretação precisa dizer **quais são os +> objetos do mundo e como os símbolos da linguagem se referem a +> eles**. + +### MWE: alunos e disciplinas + +Comece com a assinatura: + +* constante `alice` +* constante `bob` +* predicado unário `Student(x)` +* predicado binário `Likes(x,y)` + +E uma sentença: + +$$ +\forall x\,(Student(x)\rightarrow Likes(x,alice)). +$$ + +Pergunte: + +> **O que precisamos saber para decidir se essa fórmula é verdadeira?** + +Isso leva naturalmente à estrutura semântica. + +Escolha um domínio minúsculo: + +$$ +D=\{a,b,c\}. +$$ + +E uma interpretação \(I\): + +$$ +I(alice)=a,\qquad I(bob)=b +$$ + +e, por exemplo, + +$$ +Student^I=\{a,b\} +$$ + +$$ +Likes^I=\{(a,a),(a,b),(b,a),(b,b)\}. +$$ + +Agora podemos avaliar: + +$$ +I\models\forall x(Student(x)\rightarrow Likes(x,alice)). +$$ + +Porque para cada elemento de \(D\), se ele pertence a \(Student^I\), então o par correspondente está em \(Likes^I\). + +--- + +### O detalhe que eu acho mais importante para a sua aula + +Depois de apresentar **uma** estrutura, mude apenas \(Likes^I\): + +$$ +Likes^I=\{(a,a),(a,b),(b,b)\}. +$$ + +Agora a fórmula é **falsa**, pois: + +$$ +Student(b) +$$ + +é verdadeira, mas + +$$ +Likes(b,alice) +$$ + +é falsa. + +Isso dá uma demonstração muito concreta de que: + +> **A mesma fórmula pode ser verdadeira em uma interpretação e falsa em outra.** + +E aí você pode fazer a analogia com a aula anterior: + +### Proposicional + +$$ +p\land q +$$ + +Uma interpretação é essencialmente: + +$$ +I:\{p,q\}\to\{\mathsf{true},\mathsf{false}\}. +$$ + +### Primeira ordem + +Para + +$$ +\forall x(Student(x)\rightarrow Likes(x,alice)) +$$ + +uma interpretação precisa fornecer muito mais: + +$$ +\mathcal M=(D,I) +$$ + +onde: + +* \(D\) é o **domínio**; +* \(I\) diz a que objeto cada constante se refere; +* \(I\) diz quais objetos satisfazem cada predicado; +* \(I\) diz quais pares (ou \(n\)-uplas) satisfazem cada relação. + +--- + +### E então vem o MWE realmente interessante + +Eu faria uma pequena mudança na fórmula: + +$$ +\forall x(Student(x)\rightarrow Likes(x,alice)) +$$ + +para + +$$ +\exists x(Student(x)\land Likes(x,alice)). +$$ + +Pergunte: + +> O que mudou semanticamente? + +A resposta não é simplesmente "agora procuramos um aluno". Você pode **mostrar a avaliação recursivamente**: + +$$ +\mathcal M,g\models\exists x\,\varphi +$$ + +sse existe \(d\in D\) tal que + +$$ +\mathcal M,g[x\mapsto d]\models\varphi. +$$ + +Aqui aparece, de maneira bastante natural, a necessidade de uma **valoração \(g\)** para variáveis. + +Isso é, na minha opinião, o ponto em que vale introduzir formalmente: + +$$ +\boxed{\mathcal M,g\models\varphi} +$$ + +em vez de apenas + +$$ +\mathcal M\models\varphi. +$$ + +Você pode dizer: + +> Constantes são interpretadas pela estrutura; variáveis são interpretadas pela valoração. + +E então mostrar: + +$$ +g(x)=b +$$ + +e avaliar + +$$ +Student(x)\land Likes(x,alice) +$$ + +como + +$$ +Student(b)\land Likes(b,a). +$$ + +--- + +### Uma sequência de 15–20 minutos + +Eu estruturaria o MWE assim: + +1. **Assinatura** + + $$ + alice,\ bob,\ Student,\ Likes + $$ + +2. **Uma estrutura concreta** + + $$ + D=\{a,b,c\} + $$ + +3. **Interpretar os símbolos** + +4. Avaliar uma fórmula fechada: + + $$ + \forall x(Student(x)\to Likes(x,alice)) + $$ + +5. Alterar a estrutura e mostrar que o valor de verdade muda. + +6. Introduzir variável livre: + + $$ + Student(x)\to Likes(x,alice) + $$ + +7. Perguntar: + + > "Isso tem um valor de verdade?" + + **Não sem uma valoração \(g\).** + +8. Introduzir: + + $$ + \mathcal M,g\models\varphi + $$ + +9. Finalmente, mostrar que: + + $$ + \mathcal M\models\varphi + $$ + + é o caso em que \(\varphi\) é uma **sentença**, portanto seu valor não depende da valoração. + +Isso faz a semântica de FOL parecer uma extensão muito natural da proposicional, em vez de uma coleção de novas definições. From d9db3e524bd85eb085687f51f6174f1f7f69b10b Mon Sep 17 00:00:00 2001 From: Alexandre Rademaker Date: Thu, 10 Sep 2026 22:46:54 -0300 Subject: [PATCH 2/5] docs: add style guides and a contributor guide MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Adapted from sf-in-lean's project documentation, keeping what fits a one-author book with a course monitor as alpha tester and dropping the machinery for coordinating several contributors across branches (Zulip, CODEOWNERS, the branch-activity dashboard, the draft-PR protocol). New files: * STYLE-CODE.md — Lean and Verso conventions. Its core is a ledger of which Lean feature is first used in which chapter, derived from a sweep of the code inside `lean` blocks: it makes checkable the constraint DEVIATIONS.md states, that nothing is used before it is presented. Because the book is mostly programs rather than proofs, the ledger covers every Lean feature, not only tactics. It also documents the directive vocabulary already implemented in CSwLMeta/ (`:::exercise`, `solution!`, `:::gradeTheorem`, `:::dev`, `:::quiz`, the build variants), which had no documentation at all. * STYLE-WRITING.md — prose conventions. Absorbs the "Pedagogical decisions" section from CLAUDE.md, adds writing advice adapted from sf-in-lean, and starts a Portuguese term list. The list is deliberately short: it records decisions actually taken rather than a vocabulary invented in advance. * CONTRIBUTING.md — workflow, and who decides what. Content and structure remain the author's; the objective tasks open to a contributor are listed explicitly. Its AI policy is this project's own, not sf-in-lean's: AI never writes prose on its own initiative, translates as literally as the target language allows, and produces drafts for human revision. Other changes: * CLAUDE.md points at the two style guides instead of carrying the pedagogical section itself. * README.md stops restating conventions that are now normative elsewhere. * DEVIATIONS.md refers to GitHub issues, TODO.md having been retired in favour of them. * CSwLMeta/Save/Project.lean — the generated project's README was in Portuguese and said only "do not edit here". It is now in English, like every other document about the project, and the `student` variant carries a full setup guide: how to build, how to work an exercise, where to report a problem. That variant is what reaches the students. The pending work the retired TODO.md tracked is now in GitHub issues #3–#20; everything it recorded as done was discarded rather than filed to be closed. These documents were drafted with Claude Code (Opus 5) from decisions taken in conversation with the author, who directed the scope, rejected several proposals, and reviewed the result. The feature ledger in STYLE-CODE.md was derived by script from the chapter sources and then corrected by hand where the scan proved too narrow. --- CLAUDE.md | 23 ++-- CONTRIBUTING.md | 107 +++++++++++++++++++ CSwLMeta/Save/Project.lean | 50 +++++++-- DEVIATIONS.md | 4 +- README.md | 16 +-- STYLE-CODE.md | 212 +++++++++++++++++++++++++++++++++++++ STYLE-WRITING.md | 149 ++++++++++++++++++++++++++ 7 files changed, 538 insertions(+), 23 deletions(-) create mode 100644 CONTRIBUTING.md create mode 100644 STYLE-CODE.md create mode 100644 STYLE-WRITING.md diff --git a/CLAUDE.md b/CLAUDE.md index 27e6ff6..cf8cf95 100644 --- a/CLAUDE.md +++ b/CLAUDE.md @@ -64,11 +64,20 @@ AI-usage disclosure paragraph at the end of commit messages is important wheneve When migrating material, AI should try to translate (English to Portuguese) but not rewrite or invent new text. Only humans should deviate from the original CSwFP texts. -# Pedagogical decisions - -We will avoid fragmented presentation of material. That is why we will largely reorder CSwFP. - -We should avoid presenting definitions that will be rephrased later, with the same name that in another chapter would have a new definition. Eventually, namespaces would avoid conflicts, but students may get confused. But exceptions can occur. - -We will never discuss `haskell vs Lean` decisions in the book. The reader does not necessarily know Haskell and should not worry about it. We also do not expect the reader to have read the original CSwFP. This book is self-contained. As a result, we never mention CSwFP sections, pages, etc. +# Style guides + +The normative conventions live in two files, which are to be read in addition +to this one. **Read both in full before creating or editing any file that ends +up in the book**; everything you write must conform to them. + +- `STYLE-CODE.md` — Lean code and Verso markup: the ledger of which Lean + feature is first used in which chapter (the book's hard constraint is that + nothing is used before it is presented), the directive vocabulary, the build + variants, and naming. +- `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 +file wins on project scope. diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md new file mode 100644 index 0000000..8198921 --- /dev/null +++ b/CONTRIBUTING.md @@ -0,0 +1,107 @@ +# Contributing to CSwL + +This file covers workflow and mechanics. For conventions, read `STYLE-CODE.md` +(Lean and Verso) and `STYLE-WRITING.md` (prose and Portuguese) — both are +normative, and both should be read before you edit anything that reaches the +book. + +Everything about the project is in English: this file, identifiers, code +comments, commit messages, issues. Only the book's prose is in Portuguese. + +## Who decides what + +The book's content and its structure — what a chapter says, what order the +material comes in, which exercises exist, how chapters are divided — are the +author's. Contributions are welcome on everything else, and are most valuable +where a task is objective: + +- reporting anything that does not build, or builds with an unexpected warning; +- reporting prose that is wrong, unclear, or badly translated; +- working the exercises and reporting those that are unsolvable, ambiguous, or + mis-rated; +- checking that a chapter uses no Lean feature the book has not yet presented + (`STYLE-CODE.md` has the ledger); +- fixes to typos, markup slips, and broken references. + +A change that reorganizes material, adds or removes an exercise, or introduces +a Lean feature earlier than the ledger records is a proposal, not a fix: open +an issue and let the author decide. + +## Getting set up + +Install Lean via [elan](https://lean-lang.org/install), then clone the +repository and fetch the prebuilt Mathlib — without this, `lake build` +compiles all of Mathlib from scratch: + +```sh +lake exe cache get +lake build +``` + +Use VS Code with the Lean 4 extension. Opening any file under `CSwL/` will +prompt to install the toolchain the book pins. + +To build and read the book locally: + +```sh +make serve # http://127.0.0.1:8000/ +``` + +`make all` generates all four variants under `_out/`. See `STYLE-CODE.md` for +what each variant is. + +## Issues + +Pending work is tracked in [GitHub +issues](https://github.com/cslib-community/CSwL/issues). Anything you find that +you are not fixing yourself belongs there. + +For a comment that is local to one passage and only makes sense with that +section in view, use a `:::dev` note in the Lean file itself rather than an +issue. Those render as editorial notes and never reach the student. + +## Branches and pull requests + +- `main` must always build. +- Do not commit to `main`; work on a branch and open a pull request. +- Keep a pull request to one coherent piece of work. Smaller and sooner beats + bigger and later. +- 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. +- Delete the branch once it is merged. + +Commit messages follow [Conventional +Commits](https://www.conventionalcommits.org/): `feat:`, `fix:`, `docs:`, +`refactor:`, with an optional scope — `docs(readme): …`, `fix(logic): …`. + +## Editing the right file + +The book's sources are the Lean files under `CSwL/`. Everything under `_out/` +is generated and is overwritten by the next `make` — never edit there. + +That includes the generated projects' `README.md`, which comes from +`readmeTemplate` in `CSwLMeta/Save/Project.lean`. + +## AI usage + +AI may be used in this project, under conditions that differ from the ones +some related projects adopt. The rules: + +- **AI never writes prose on its own initiative.** It produces text only when + explicitly asked, and what it produces is a draft for a human to revise. +- **When migrating material, AI translates.** English to Portuguese, as + literally as the target language allows. It does not rewrite, expand, + restructure, or invent. Deviating from the source is a human decision. +- **AI-generated commentary is marked as such**, and belongs in `:::dev` + blocks, which never reach the student. +- **Infrastructure is different.** Code under `CSwLMeta/` and the scripts + around the build are not book content, and AI may write them — but a file + that is mostly AI-written says so at the top, because it will typically be + less carefully considered than hand-written code. +- **Commit messages** that describe AI-assisted work carry a disclosure + paragraph in English, added only after a human approves it. Never + `Co-Authored-By: Claude`. + +`CLAUDE.md` holds the instructions Claude Code reads at the start of a +session; it points at this file and the two style guides. diff --git a/CSwLMeta/Save/Project.lean b/CSwLMeta/Save/Project.lean index 5f12454..080e2ce 100644 --- a/CSwLMeta/Save/Project.lean +++ b/CSwLMeta/Save/Project.lean @@ -112,15 +112,49 @@ private def lakefileTemplate (vol : String) (v : Variant) "name = \"" ++ vol ++ "\"\n" ++ libs +/-- The `student` variant is the one the students receive, so its README is +the whole set-up guide: how to build, how to work an exercise, how to report a +problem. The other variants are read by the instructor, who has the repository +itself, and get only the note saying where they came from. + +Written in English, like every other document about the project; only the +book's prose is in Portuguese. -/ private def readmeTemplate (vol : String) (v : Variant) : String := - s!"# {vol} — variante `{v}`\n\n" ++ - "Gerado a partir do livro (Verso, gênero `Manual`) por " ++ - s!"`lake exe cswl-book {v}` — **não edite aqui**: a fonte é o `CSwL`.\n\n" ++ - (if v.isGrading then - "Esta variante traz as provas completas e os atributos " ++ - "`[autogradedProof …]`. Para corrigir uma entrega:\n\n" ++ - " lake exe autograder --local \n\n" ++ - "Ela nunca sai do repositório privado.\n" + s!"# {vol} — `{v}` variant\n\n" ++ + "Generated from the book (Verso, `Manual` genre) by " ++ + s!"`lake exe cswl-book {v}` — **do not edit here**: the source is `{vol}`, " ++ + "and the next build overwrites this directory.\n\n" ++ + (if v.isStudent then + "## Setting up\n\n" ++ + "Install Lean with [elan](https://lean-lang.org/install). Then, in this\n" ++ + "directory, fetch the prebuilt Mathlib and build:\n\n" ++ + " lake exe cache get\n" ++ + " lake build\n\n" ++ + "`lake exe cache get` matters: without it, `lake build` compiles all of\n" ++ + "Mathlib from scratch.\n\n" ++ + "Use VS Code with the Lean 4 extension, and open **this directory** as\n" ++ + "the folder — not a file inside it, or the extension will not find the\n" ++ + "project.\n\n" ++ + "## Working the exercises\n\n" ++ + "Each exercise is a `sorry` to replace. Lean checks your answer as you\n" ++ + "type: while a `sorry` remains, the file reports a warning, and when the\n" ++ + "proof or definition is complete the warning disappears. The InfoView\n" ++ + "panel shows the goal at the cursor.\n\n" ++ + "The exercises are in the same order as the book, and each one sits in\n" ++ + "the chapter section that discusses it. Read the corresponding section\n" ++ + "of the book alongside the code.\n\n" ++ + "Keep your own copy of anything you want to survive: this directory is\n" ++ + "regenerated from the book, and a rebuild overwrites whatever is here.\n\n" ++ + "## Reporting a problem\n\n" ++ + "If something does not build, a statement is ambiguous, or the prose is\n" ++ + "wrong, open an issue at\n" ++ + ". Say which chapter and\n" ++ + "which exercise, and paste the message Lean gave you.\n" + else if v.isGrading then + "This variant carries the complete proofs and the `[autogradedProof …]`\n" ++ + "attributes. To grade a submission:\n\n" ++ + " lake exe autograder --local \n\n" ++ + "It never leaves the private repository.\n" else "") /-- Writes the generated project to `dest`: the extracted files, plus diff --git a/DEVIATIONS.md b/DEVIATIONS.md index 98d384a..100e649 100644 --- a/DEVIATIONS.md +++ b/DEVIATIONS.md @@ -61,7 +61,7 @@ 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 `TODO.md`. Exercise-level correspondence with CSwFP is in `PROVENANCE.md`. +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. @@ -353,7 +353,7 @@ CSwFP/7 (The Composition of Meaning in Natural Language) goes after `ModelChecki 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 grammars of `Games.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 in `TODO.md`, not before it. +Mathlib's `ContextFreeGrammar` for the grammars of `Games.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. diff --git a/README.md b/README.md index 5026137..7f08e23 100644 --- a/README.md +++ b/README.md @@ -66,16 +66,20 @@ exercises not reused later in the chapter itself). ## Conventions -Mnemonic file names. A short chapter is a single file (`CSwL/Sets.lean`, -`namespace Sets`); a chapter whose sections are long enough to deserve -their own file is a "glue" file (`CSwL/Games.lean`) that only gathers, via -`{include 1 ...}`, sections living in a same-named directory +Mnemonic file names, never numbers. A short chapter is a single file +(`CSwL/Sets.lean`, `namespace Sets`); a chapter whose sections are long enough +to deserve their own file is a "glue" file (`CSwL/Games.lean`) that only +gathers them, via `{include 1 ...}`, from a same-named directory (`CSwL/Games/SeaBattle.lean`, `CSwL/Games/Mastermind.lean`) — the same pattern -used by [Functional Programming in Lean](https://lean-lang.org/functional_programming_in_lean/). Each content file has its own `namespace`, -mnemonic and necessary: the book redefines the same names in different chapters. +used by [Functional Programming in Lean](https://lean-lang.org/functional_programming_in_lean/). CSwL developments connect with those in [CSLib](https://github.com/leanprover/cslib/) where possible. We aim to reuse CSLib and contribute to CSLib. +The normative conventions are in [STYLE-CODE.md](STYLE-CODE.md) (Lean and +Verso, including which Lean feature each chapter is allowed to use) and +[STYLE-WRITING.md](STYLE-WRITING.md) (prose, pedagogy, and Portuguese). +[CONTRIBUTING.md](CONTRIBUTING.md) covers workflow. + ## Deviations from CSwFP `CSwL` is inspired by CSwFP, not a 1-to-1 port of it: chapters get diff --git a/STYLE-CODE.md b/STYLE-CODE.md new file mode 100644 index 0000000..e2a88b5 --- /dev/null +++ b/STYLE-CODE.md @@ -0,0 +1,212 @@ +# CSwL Code Style Guide + +This file records the conventions for the Lean code and the Verso markup that +make up the book. `STYLE-WRITING.md` covers prose, pedagogy, and translation; +`CONTRIBUTING.md` covers workflow. In case of conflict with `CLAUDE.md`, the +style guides win on style and `CLAUDE.md` wins on project scope. + +The book's prose is in Portuguese. Everything else — this file, identifiers, +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: + +> **Nothing is used before it is presented.** + +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 +`instance` for the first time inside a chapter on morphology has been given a +feature the book never introduced, exactly as much as one meeting `by_contra` +would have been. + +The table below is the ledger that makes the rule checkable. + +### How to read the table + +It records the chapter where each feature is **first used in the sources**, in +book order (`Book.lean`). It is derived from the code inside ```` ```lean ```` +blocks and must be kept in sync as chapters are rewritten. + +First use is evidence, not compliance. The rule is about first *presentation* — +the prose that introduces the feature — and a row whose feature is used but +never presented is a defect, not an entry. Rows known to be in that state are +marked, and the open ones are listed under "Known gaps" below. + +**A feature can be presented outside a `lean` block**, so the table's first-use +column does not by itself settle whether the rule holds. `IntroL.lean` presents +fourteen tactics in a plain code fence — one line each, `rfl` through `funext` — +and a scan that reads only ```` ```lean ```` blocks misses it. Check the prose +before recording a gap. + +A feature marked **(solution only)** first appears inside a `solution!(…)` +block. Those rows are a distinct case: the feature is invisible in the +`student` and `terse` variants and visible in `solutions` and `grading`, so a +reader working the exercise meets it only in the answer. Introducing a feature +this way is usually a mistake; see "Known gaps." + +### Features by chapter of first use + +| Chapter | Commands and declarations | Types and syntax | Tactics | +| --- | --- | --- | --- | +| `IntroCS` | `namespace`, `def` (by pattern matching), `inductive`, `deriving Repr`, `example`, `#eval` | `Nat`, function type `→`, dot-notation constructors (`.num`) | `rfl`, `induction … with`, `rw`, `rewrite`, `unfold`, `repeat` | +| `IntroL` | `#check`, `#print`, `theorem`, `structure`, `instance`, `section`, `variable` | `Type`, `Prop`, `Bool`, `List`, `Option`, `Char`, `String`, `fun`/`λ`, `match`, `if … then … else`, `⟨…⟩`, implicit `{}`, instance-implicit `[]`, `∘`, `BEq`, `∀`, `∃`, `∧`, `∨`, `↔`, `≠` | `intro`, `exact`, `apply`, `cases … with`, `constructor`, `obtain`, `show`, `funext`, `omega`, `decide` (solution only) | +| `Morphology` | `abbrev`, `open`, `deriving BEq` | `×` | `native_decide` (solution only) | +| `Games` | — | `DecidableEq`, `Vector`, subtypes (`{ x : T // p x }`), `¬`, `∈` | `simp` (solution only) | +| `Logic` | `mutual`, `private` | `\|>` | `have`, `use`, `left`, `right`, `rcases`, `by_cases`, `by_contra` | +| `Sets` | — | `Set`, `Rel`, `Finset`, `Fintype`, `Setoid`, `⊆`, `∪`, `∩` | `assumption`, `trivial`, `symm`, `simp_all` | +| `InfEngine` | — | `do`-notation | — | +| `English` | *(none new)* | *(none new)* | *(none new)* | + +`English` introduces no new feature: it is where `abbrev` and `ToString` +instances become the dominant idiom, but both arrive earlier. + +`Games` introduces `Vector` and subtypes in `Games/Mastermind.lean`, and the +subtype gets a paragraph of prose before its first use — the rule working as +intended. + +The table records features, not every piece of notation. Type ascription, +list literals, projection dots, and the like are not tracked: they arrive with +the constructs that use them and tracking them would produce a ledger nobody +maintains. + +### Known gaps + +Open questions about the table, recorded so they are not lost. Each needs an +author decision, not a mechanical fix. + +- **`native_decide`** (`Morphology/SwedishPlural.lean:69`, `:72`) is used + inside solutions and is not in `IntroL`'s tactic table. It closes a goal by + compiling and running it, trusting the compiler rather than the kernel — a + materially different promise from `decide`. Its use is justified where it + appears, and a comment at `:63-66` says why, but that comment is inside the + solution and in Portuguese, so the explanation reaches neither the student + nor the English code-comment rule. +- **`trivial`** — one term-level use in `Sets.lean:507`, not presented + anywhere. Give it a line or replace it when that chapter is revised. +- **`Sets.lean` uses `Setoid`, `Fintype` and `Finset` with no presentation.** + A short paragraph plus a citation for each would settle it, under the + loosening `DEVIATIONS.md` describes. + +`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. + +## Verso markup + +The book is written in [Verso](https://verso.lean-lang.org), in the `Manual` +genre. The directives below are defined in `CSwLMeta/` and are the vocabulary +available to a chapter. + +### Chapter structure + +A chapter file opens with its imports, the `#doc` declaration, and a metadata +block: + +``` +#doc (Manual) "Title in Portuguese" => +%%% +tag := "ChapterTag" +htmlSplit := .never +file := "ChapterTag" +%%% +``` + +Mnemonic names, never numbers — for files, tags, and exercise names alike. +Material moves between chapters, and a number would be wrong the moment it +did. + +A short chapter is a single file (`CSwL/Sets.lean`). A chapter whose sections +are long enough to deserve their own files is a "glue" file (`CSwL/Games.lean`) +that only gathers them via `{include 1 …}` from a same-named directory. Each +content file has its own `namespace`: the book redefines the same names in +different chapters, deliberately. + +### 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 +the grading variant, and follows the mnemonic rule. + +Inside an exercise, the answer is wrapped so the build variants can strip it: + +- `solution!(…)` — an inline solution, for a term or a `by` block. +- `solution!` on its own line, followed by an indented block — a multi-line + solution. +- `:::solution` — a prose solution, for exercises answered in words. + +The `student` and `terse` variants replace these with `sorry`; `solutions` and +`grading` keep them. This is why a feature first used inside `solution!` is +invisible to the student. + +### Grading + +`:::gradeTheorem …` marks theorems the autograder scores. +Points may be a decimal in double quotes (`"0.25"`); an integer needs no +quotes. The directive is defined in `CSwLMeta/Grade.lean` and emitted as an +`[autogradedProof]` attribute by `CSwLMeta/Save/Extract.lean`, into the +`grading` variant only. + +The theorems must be `theorem`s and not `example`s, since the attribute needs +a name to refer to. + +### Build variants + +Four variants are generated by `make all`, from the same sources: + +| Variant | Solutions | Audience | +| --- | --- | --- | +| `student` | stripped to `sorry` | the students, published to the book repository | +| `terse` | stripped to `sorry` | the instructor, opened in VS Code during class | +| `solutions` | kept | the instructor | +| `grading` | kept, plus grading attributes | the autograder; never leaves the private repository | + +Prose can be routed to a variant: + +- `:::full` — appears in the full-prose variants, omitted from `terse`. +- `:::terse` — appears only in `terse`. +- `:::suppressPreviousHeaderWhenTerse` — drops the preceding heading in the + `terse` build, where the prose under it is gone and the heading would dangle. + +### Notes and commentary + +- `:::dev` — an internal note to the authors. It renders with the heading + "Nota editorial" and must never carry anything the student should not read. + AI-generated commentary belongs here and is marked as such. +- `:::quiz` and `:::quizSolution` — a comprehension check. +- `:::diagramWithAlt` — a diagram with its textual alternative, for + accessibility. + +### Other blocks + +- ```` ```lean ```` — live Lean, elaborated by `lake build`. Everything in the + book's code is checked; there are no illustrative-only Lean blocks. +- ```` ```lean (name := tag) ```` with ```` ```leanOutput tag ```` — code whose + output is shown and checked against the block. +- `{include N Module}` — pulls a section file into its glue chapter at heading + depth `N`. + +## Lean style + +Follow the Mathlib +[style guide](https://leanprover-community.github.io/contribute/style.html) +and [naming conventions](https://leanprover-community.github.io/contribute/naming.html), +except where pedagogy asks otherwise. In particular: + +- Types and propositions in `PascalCase` (`Phoneme`, `WellFormed`). +- Functions and values in `camelCase` (`appendSuffixF`, `surfaceTable`). +- Theorems in `snake_case` (`defeated_last`), keeping the casing of the + definitions they are about (`WellFormed.ne_nil`). +- Greek letters for type variables (`α`, `β`). + +All identifiers and all code comments are in English, including in the code +the students read. + +Prefer `cases … with` and `induction … with`, one alternative per line, over +goal selectors. + +Reuse Mathlib and CSLib where they fit; `DEVIATIONS.md` records where they +deliberately do not, and why. diff --git a/STYLE-WRITING.md b/STYLE-WRITING.md new file mode 100644 index 0000000..5dd3f3a --- /dev/null +++ b/STYLE-WRITING.md @@ -0,0 +1,149 @@ +# CSwL Writing Style Guide + +This file records the conventions for the book's prose: pedagogy, +presentation, and the Portuguese it is written in. `STYLE-CODE.md` covers Lean +code and Verso markup; `CONTRIBUTING.md` covers workflow. + +The book's prose is in Portuguese. This guide, like every other document about +the project, is in English — the rule is about the medium, not the audience. + +## Pedagogical decisions + +These are the project's standing decisions about how material is presented. + +**Avoid fragmented presentation.** A topic is developed in one place, as far +as the material allows. This is the reason the book largely reorders its +source: a presentation that is natural in Lean is not the one the source +needed. + +**Do not present a definition that a later chapter will rephrase under the +same name.** Namespaces would keep such a pair compiling, but the reader is +not a compiler and will read the second definition as a correction of the +first. Exceptions happen; they should be deliberate and visible. + +**Never discuss the book's sources or alternatives in the prose.** The reader +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 test is whether the sentence would still be worth writing if this book had +no source and no alternatives. + +**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 +not need a section. + +**Exercises should not be load-bearing.** Prefer exercises whose solutions are +not required by later presentations; a reader who skips one, or gets it wrong, +should not be locked out of the next chapter. + +**Prefer naming a chapter over naming a position.** "O capítulo anterior", +"mais adiante", "já vimos" are true only of one arrangement, and material +moves between chapters — that is why nothing in this book is numbered. A +`{ref "Tag"}[…]` survives a reorder; "the previous chapter" silently becomes +false. + +Where a positional phrase is genuinely the clearest thing to write, it is a +liability to be repaid: **after moving any chapter or section, sweep for the +prose the move invalidated.** The search that has caught them so far: + +``` +capítulo anterior | capítulos anteriores | próximo capítulo | +no capítulo seguinte | adiante | mais adiante | já vimos | vimos no | visto no +``` + +plus every `{ref "…"}`, whose target still resolves but may now be so far away +that the sentence around it stops making sense. + +## Writing advice + +This section adapts the guidance developed for SF-in-Lean, whose exercise-led +structure this book follows. It is about how to write a section, not about +what the project has decided. + +**Imagine your audience.** What do the students know before this course? They +arrive by different paths. What do they know *so far in this book*, at the +point you are writing? Use concepts they have; do not use terms they have not +met. Do not re-explain what they know well — but do remind them of something +introduced a while back, because they will have forgotten it. + +**Context, Gap, Solution.** Readers want to know why they are reading +something. They will suspend impatience, but not for long. Three parts: what +do we want to do, what stops us, what do we do about it. + +Two near-misses to watch for. The problem may be stated too big, so the path +to the solution is long and its rightness is not obvious — break it into +smaller problems, each with the three parts. Or the solution may not +obviously match the problem, appearing to do more than was asked — then either +simplify it or explain the excess. + +**Start from something specific the reader knows; work toward the general.** +You begin on the same page as the reader and make small deltas before the +bigger leaps. Use good examples, simple before general. + +**Minimize complexity.** Ask what would make this simpler. Reuse an example +rather than introducing a new one. Prefer a multi-step development where the +concerns separate. Avoid an expert-level solution that solves problems you do +not want to explain yet. + +**Do not forget exercises.** This book's signature is that each interesting +concept comes with something to do. An explanation plus an example can often +become an explanation plus an exercise. + +**Cutting is good.** Material grows and the temptation is to keep everything. +Ask: does this serve the goal, does the audience need it? If some readers +would benefit but not all, a `:::details` block or an appendix will hold it. + +## Portuguese conventions + +The book is in Brazilian Portuguese. + +Where AI is used to translate, the translation is as literal as the target +language allows, produced as a draft for a human to revise. Prose is never +invented, expanded, or restructured on the AI's initiative — see `CLAUDE.md`. +The failure mode this section guards against is the systematic one: a +translation that is fluent, plausible, and consistently wrong about a term. + +### Terms + +The preferred form, then the form to avoid. This list is short on purpose: it +records decisions actually taken, not a vocabulary invented in advance. +Prescribing a term the book has never used, against an alternative it has +never used, is the same failure this section exists to catch. Add an entry +when a bad translation is found and corrected. + +The chapters are already consistent on their main terms — "tática", +"tipo indutivo", "hipótese de indução", "predicado" — and those need no +entry until something contradicts them. What the sweep found instead: + +- "supor" / "assumir" (in the sense of English *to assume*; the Portuguese + verb means *to take on*, and the false friend is the commonest + translation error in this material) +- "avaliar" / "rodar" (for `#eval`) + +### Code and prose + +Lean identifiers, keywords, and literal values keep their Lean spelling and go +in code font: write `true` and `false`, not "verdadeiro" and "falso", when the +term is the Lean value. Use the Portuguese words when the sense is the +ordinary one — a proposition is *verdadeira*, a `Bool` is `true`. + +Keep a term's translation stable across the whole book. A concept that +acquires a second name in a later chapter reads as a second concept. + +### Punctuation and typography + +- Em dashes for parenthetical breaks, spaced as the surrounding prose does. +- Portuguese quotation marks or straight quotes, consistently within a file. +- Lean code in prose always in code font, never italicized. +- Every sentence starts with a capital letter. If a sentence would open with a + lowercase Lean identifier, rephrase it — `Nat.add` may open a sentence, + `omega` may not. + +## Informal proofs + +The book uses informal proofs sparingly: to teach a reasoning principle in the +abstract, as opposed to a Lean tactic. When one appears, it ends with *QED*. From 09be026f6b4fbe02c4152e71148f9876b6c1e16a Mon Sep 17 00:00:00 2001 From: Alexandre Rademaker Date: Fri, 11 Sep 2026 00:00:16 -0300 Subject: [PATCH 3/5] docs(logic): revise the PL opening and drop two working notes MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit PL.lean — the chapter opens with the acronym PL, from the English, which is what the file and section tags already use; the Portuguese LP appeared only here. The paragraph now states the chapter's aim as making precise that one proposition follows from another, rather than as escaping the imprecision of natural language. FOL.lean — the ∀-introduction example binds `n`, so the introduced name differs from the bound variable it replaces and the tactic's effect is visible. doc/entailment.md and doc/fol-semantics.md were working notes toward this material; nothing references them. --- CSwL/Logic/FOL.lean | 4 +- CSwL/Logic/PL.lean | 4 +- doc/entailment.md | 124 ---------------------- doc/fol-semantics.md | 246 ------------------------------------------- 4 files changed, 4 insertions(+), 374 deletions(-) delete mode 100644 doc/entailment.md delete mode 100644 doc/fol-semantics.md diff --git a/CSwL/Logic/FOL.lean b/CSwL/Logic/FOL.lean index 92b2d2c..636d7c4 100644 --- a/CSwL/Logic/FOL.lean +++ b/CSwL/Logic/FOL.lean @@ -59,8 +59,8 @@ arbitrário e prove que vale para ele. É a mesma `intro` agora sobre um objeto ```lean example (h : ∀ x, P x) : ∀ y, P y := by - intro y - exact h y + intro n + exact h n ``` A introdução de `∃` exige exibir a testemunha. A tática `use` substitui a variável quantificada pelo objeto passado, e deixa como objetivo o que falta provar sobre ele. diff --git a/CSwL/Logic/PL.lean b/CSwL/Logic/PL.lean index 8b8615b..3664984 100644 --- a/CSwL/Logic/PL.lean +++ b/CSwL/Logic/PL.lean @@ -19,9 +19,9 @@ namespace PL # Introdução -A lógica proposicional (LP, ou cálculo sentencial) trata de fórmulas construídas a partir de variáveis proposicionais usando os conectivos `¬`, `∧`, `∨`, `→` e `↔`. Intuitivamente, uma variável proposicional `p` representa uma sentença ou proposição que pode ser verdadeira ou falsa. Queremos usar lógica proposicional para fugir das impressões das línguas naturais. Formalizar proposições e provas quando podemos concluir uma proposição a partir de outras proposições tomadas como premissas. +A lógica proposicional (PL, "Propositional Logic") trata de fórmulas construídas a partir de variáveis proposicionais usando os conectivos `¬`, `∧`, `∨`, `→` e `↔`. Intuitivamente, uma variável proposicional `p` representa uma sentença ou proposição que pode ser verdadeira ou falsa. Podemos usar lógica proposicional para fugir das impressões das línguas naturais. Queremos tornar precisa a noção de que uma proposição `α` decorre de outra proposição `β`. -Como primeiro exemplo, adaptado de {citet Bib.enderton2001}[], a sentença "traços de potássio foram observados" pode ser traduzida para a linguagem formal como o símbolo `K`. Já para a sentença fortemente relacionada "traços de potássio não foram observados", podemos usar `¬ K`. Aqui `¬` é o nosso símbolo de negação, lido como "não". Poderíamos também pensar em traduzir "traços de potássio não foram observados" por algum símbolo novo `J`, mas preferimos decompor sentenças em suas partes atômicas tanto quanto possível. Para uma sentença não relacionada, "a amostra continha cloro" escolhemos o símbolo `C`. Assim, as seguintes sentenças compostas podem ser formalizadas. +Como primeiro exemplo, adaptado de {citet Bib.enderton2001}[], a sentença "traços de potássio foram observados" pode ser traduzida para a linguagem formal como o símbolo `K`. Já para a sentença relacionada "traços de potássio não foram observados", podemos usar `¬ K`. Aqui `¬` é o nosso símbolo de negação, lido como "não". Poderíamos também pensar em traduzir "traços de potássio não foram observados" por algum símbolo novo `J`, mas preferimos decompor sentenças em suas partes atômicas tanto quanto possível. Para uma sentença não relacionada, "a amostra continha cloro" escolhemos o símbolo `C`. Assim, as seguintes sentenças compostas podem ser formalizadas. - A sentença "Se traços de potássio foram observados, então a amostra não continha cloro." é formalizada como `(K → (¬C))` com símbolo `→` significando "se ... então ...". - A sentença "A amostra continha cloro, e traços de potássio foram observados." é formalizada como `(C ∧ K)` com símbolo `∧` significando a conjunção "e". diff --git a/doc/entailment.md b/doc/entailment.md deleted file mode 100644 index 3b3b773..0000000 --- a/doc/entailment.md +++ /dev/null @@ -1,124 +0,0 @@ - -### Exemplo - -Suponha três proposições: - -* \(p\): Alice está na sala. -* \(q\): Bob está na sala. -* \(r\): Carol está na sala. - -Sem nenhuma informação adicional, temos \(2^3=8\) interpretações possíveis: - -| \(p\) | \(q\) | \(r\) | -| ----- | ----- | ----- | -| F | F | F | -| F | F | V | -| F | V | F | -| F | V | V | -| V | F | F | -| V | F | V | -| V | V | F | -| V | V | V | - -Agora suponha que sabemos: - -$$ -\Gamma = \{p \lor q,\quad \neg r\} -$$ - -Ou seja: - -1. **Alice ou Bob está na sala.** -2. **Carol não está na sala.** - -A pergunta passa a ser: - -> Quais interpretações são compatíveis com \(\Gamma\)? - -As interpretações admissíveis são apenas: - -| \(p\) | \(q\) | \(r\) | \(p\lor q\) | \(\neg r\) | -| ----- | ----- | ----- | ----------- | ---------- | -| F | V | F | V | V | -| V | F | F | V | V | -| V | V | F | V | V | - -Ou seja, podemos definir: - -$$ -\operatorname{Mod}(\Gamma) -= -\{I\mid I\models\varphi\text{ para toda }\varphi\in\Gamma\}. -$$ - -E então temos a ideia que eu enfatizaria para os alunos: - -> **Uma fórmula não determina uma interpretação; ela elimina interpretações que não são compatíveis com ela. Um conjunto de fórmulas elimina ainda mais interpretações.** - -Isso prepara muito naturalmente a definição de consequência lógica: - -$$ -\Gamma\models\varphi -$$ - -significa: - -> **toda interpretação que sobrevive às restrições impostas por \(\Gamma\) também satisfaz \(\varphi\).** - -### Um passo particularmente didático - -Depois pergunte: - -> A partir de \(\Gamma=\{p\lor q,\neg r\}\), podemos concluir \(p\)? - -Não, porque ainda sobrevive a interpretação \(p=F,q=V,r=F\). - -Podemos concluir \(p\lor q\)? Sim — trivialmente, porque essa é uma das restrições. - -Podemos concluir \(\neg r\)? Sim. - -Agora acrescente: - -$$ -q\rightarrow \neg p -$$ - -Então as interpretações sobreviventes passam a ser apenas: - -| \(p\) | \(q\) | \(r\) | -| ----- | ----- | ----- | -| F | V | F | -| V | F | F | - -E agora **\(p\) e \(q\) continuam indeterminados individualmente**. - -Se acrescentarmos ainda: - -$$ -q -$$ - -resta uma única interpretação: - -$$ -p=F,\quad q=V,\quad r=F. -$$ - -Esse é um excelente momento para mostrar a diferença entre: - -* **satisfatibilidade:** existe uma interpretação que satisfaz \(\Gamma\); -* **consequência lógica:** todas as interpretações que satisfazem \(\Gamma\) satisfazem \(\varphi\); -* **teoria completa:** \(\Gamma\) restringe as interpretações a uma única valuation, nesse exemplo. - -E isso conecta diretamente com dedução natural: - -$$ -\Gamma\vdash\varphi -$$ - -é a afirmação sintática correspondente à ideia semântica - -$$ -\Gamma\models\varphi. -$$ - diff --git a/doc/fol-semantics.md b/doc/fol-semantics.md deleted file mode 100644 index d10b0b8..0000000 --- a/doc/fol-semantics.md +++ /dev/null @@ -1,246 +0,0 @@ - -A grande mudança em relação à lógica proposicional é justamente esta: - -> Na proposicional, uma interpretação diz quais proposições são verdadeiras. - -> Na primeira ordem, uma interpretação precisa dizer **quais são os -> objetos do mundo e como os símbolos da linguagem se referem a -> eles**. - -### MWE: alunos e disciplinas - -Comece com a assinatura: - -* constante `alice` -* constante `bob` -* predicado unário `Student(x)` -* predicado binário `Likes(x,y)` - -E uma sentença: - -$$ -\forall x\,(Student(x)\rightarrow Likes(x,alice)). -$$ - -Pergunte: - -> **O que precisamos saber para decidir se essa fórmula é verdadeira?** - -Isso leva naturalmente à estrutura semântica. - -Escolha um domínio minúsculo: - -$$ -D=\{a,b,c\}. -$$ - -E uma interpretação \(I\): - -$$ -I(alice)=a,\qquad I(bob)=b -$$ - -e, por exemplo, - -$$ -Student^I=\{a,b\} -$$ - -$$ -Likes^I=\{(a,a),(a,b),(b,a),(b,b)\}. -$$ - -Agora podemos avaliar: - -$$ -I\models\forall x(Student(x)\rightarrow Likes(x,alice)). -$$ - -Porque para cada elemento de \(D\), se ele pertence a \(Student^I\), então o par correspondente está em \(Likes^I\). - ---- - -### O detalhe que eu acho mais importante para a sua aula - -Depois de apresentar **uma** estrutura, mude apenas \(Likes^I\): - -$$ -Likes^I=\{(a,a),(a,b),(b,b)\}. -$$ - -Agora a fórmula é **falsa**, pois: - -$$ -Student(b) -$$ - -é verdadeira, mas - -$$ -Likes(b,alice) -$$ - -é falsa. - -Isso dá uma demonstração muito concreta de que: - -> **A mesma fórmula pode ser verdadeira em uma interpretação e falsa em outra.** - -E aí você pode fazer a analogia com a aula anterior: - -### Proposicional - -$$ -p\land q -$$ - -Uma interpretação é essencialmente: - -$$ -I:\{p,q\}\to\{\mathsf{true},\mathsf{false}\}. -$$ - -### Primeira ordem - -Para - -$$ -\forall x(Student(x)\rightarrow Likes(x,alice)) -$$ - -uma interpretação precisa fornecer muito mais: - -$$ -\mathcal M=(D,I) -$$ - -onde: - -* \(D\) é o **domínio**; -* \(I\) diz a que objeto cada constante se refere; -* \(I\) diz quais objetos satisfazem cada predicado; -* \(I\) diz quais pares (ou \(n\)-uplas) satisfazem cada relação. - ---- - -### E então vem o MWE realmente interessante - -Eu faria uma pequena mudança na fórmula: - -$$ -\forall x(Student(x)\rightarrow Likes(x,alice)) -$$ - -para - -$$ -\exists x(Student(x)\land Likes(x,alice)). -$$ - -Pergunte: - -> O que mudou semanticamente? - -A resposta não é simplesmente "agora procuramos um aluno". Você pode **mostrar a avaliação recursivamente**: - -$$ -\mathcal M,g\models\exists x\,\varphi -$$ - -sse existe \(d\in D\) tal que - -$$ -\mathcal M,g[x\mapsto d]\models\varphi. -$$ - -Aqui aparece, de maneira bastante natural, a necessidade de uma **valoração \(g\)** para variáveis. - -Isso é, na minha opinião, o ponto em que vale introduzir formalmente: - -$$ -\boxed{\mathcal M,g\models\varphi} -$$ - -em vez de apenas - -$$ -\mathcal M\models\varphi. -$$ - -Você pode dizer: - -> Constantes são interpretadas pela estrutura; variáveis são interpretadas pela valoração. - -E então mostrar: - -$$ -g(x)=b -$$ - -e avaliar - -$$ -Student(x)\land Likes(x,alice) -$$ - -como - -$$ -Student(b)\land Likes(b,a). -$$ - ---- - -### Uma sequência de 15–20 minutos - -Eu estruturaria o MWE assim: - -1. **Assinatura** - - $$ - alice,\ bob,\ Student,\ Likes - $$ - -2. **Uma estrutura concreta** - - $$ - D=\{a,b,c\} - $$ - -3. **Interpretar os símbolos** - -4. Avaliar uma fórmula fechada: - - $$ - \forall x(Student(x)\to Likes(x,alice)) - $$ - -5. Alterar a estrutura e mostrar que o valor de verdade muda. - -6. Introduzir variável livre: - - $$ - Student(x)\to Likes(x,alice) - $$ - -7. Perguntar: - - > "Isso tem um valor de verdade?" - - **Não sem uma valoração \(g\).** - -8. Introduzir: - - $$ - \mathcal M,g\models\varphi - $$ - -9. Finalmente, mostrar que: - - $$ - \mathcal M\models\varphi - $$ - - é o caso em que \(\varphi\) é uma **sentença**, portanto seu valor não depende da valoração. - -Isso faz a semântica de FOL parecer uma extensão muito natural da proposicional, em vez de uma coleção de novas definições. From 520ae254c58f85c91b9b1d08eb53c71adc88e0f6 Mon Sep 17 00:00:00 2001 From: Alexandre Rademaker Date: Fri, 11 Sep 2026 00:44:07 -0300 Subject: [PATCH 4/5] fix(dev): keep `:::dev` notes out of the student build MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit `Block.devcomment`'s `traverse` returned `none` unconditionally and never consulted `getCurrVariant`, so an editorial note survived into every variant. The one note in the book — a design observation about `PredSymbol` in `Logic/FOL.lean` — was reaching students in both the HTML and the generated `.lean`. The student variant now drops every dev note during traversal. Both surfaces are produced from the per-variant traversed tree, so the one guard covers them; the extractor needs no change. `terse`, `solutions` and `grading` keep every note: the first is the instructor's, where a note on screen during a class is harmless, and the other two are the authors'. Verified by regenerating all four variants and grepping both surfaces: VARIANT HTML LEAN student 0 0 terse 1 1 solutions 1 1 grading 1 1 The docstrings that recorded the old behaviour as deliberate ("every variant is a reader of the book") are rewritten, and `STYLE-CODE.md` now documents the two independent filters — by variant in `traverse`, by urgency in `devNoteShown`. `CONTRIBUTING.md` needs no edit: the promise it already makes, that `:::dev` blocks never reach the student, is now true. Closes #4. --- CSwLMeta/Comment.lean | 42 +++++++++++++++++++++++++++++------------- STYLE-CODE.md | 23 ++++++++++++++++++++--- 2 files changed, 49 insertions(+), 16 deletions(-) diff --git a/CSwLMeta/Comment.lean b/CSwLMeta/Comment.lean index 383c2da..38d730f 100644 --- a/CSwLMeta/Comment.lean +++ b/CSwLMeta/Comment.lean @@ -77,10 +77,13 @@ def decodeDevData? (data : Json) : Option (Option String × Option String × Opt some (str? a, str? u, nat? y) | _ => none -/-- Should a dev note surface in reader-facing outputs (the HTML book and the -generated `.lean` files)? Only *actionable* notes are shown: those with urgency -`NOW` or `BeforeNextRelease`, or with no urgency at all. `PotentialImprovement` -notes remain suppressed. -/ +/-- Should a dev note be rendered at all, in the variants that keep it (every +one but `student`)? Only *actionable* notes are: those with urgency `NOW` or +`BeforeNextRelease`, or with no urgency at all. `PotentialImprovement` notes +remain suppressed. + +This is the second of two filters and is about urgency alone; which variants +keep a note is decided in `Block.devcomment`'s `traverse`. -/ def devNoteShown (urgency : Option String) : Bool := match urgency with | none => true @@ -98,8 +101,9 @@ def devUrgencyText (urgency : String) : String := /-- Label for a rendered dev note — `Nota editorial (Alexandre Rademaker, before next release, 2026)` — with absent fields omitted. The heading names the note without naming the source -this book adapts: `CSwL` is self-contained, and a rendered note reaches every -variant, the student one included. -/ +this book adapts, since `CSwL` is self-contained: the note does not reach the +student build, but it does reach the `terse` one the instructor opens in +class. -/ def devNoteLabel (author urgency : Option String) (year : Option Nat) (heading : String := "Nota editorial") : String := let fields := author.toList ++ (urgency.map devUrgencyText).toList ++ (year.map toString).toList @@ -107,17 +111,29 @@ def devNoteLabel (author urgency : Option String) (year : Option Nat) else s!"{heading} ({String.intercalate ", " fields})" /-! `Block.devcomment` carries the note body as its children and records its -author/urgency metadata in `data`. All notes survive traversal (the CSwL has -no student/solutions split on this block — every variant is a "reader" of the -book). Among the surviving blocks, a note is rendered only when its urgency -passes `devNoteShown` (`NOW`, `BeforeNextRelease`, or none): highlighted in the -HTML book, and passed through as a labelled comment in generated `.lean` files -by `CSwLMeta.Save.Extract.walkBlock`. `PotentialImprovement` notes render +author/urgency metadata in `data`. + +A dev note is addressed to the book's authors, so **no note survives traversal +in the `student` variant** — neither the HTML nor the generated `.lean`, since +both are produced from the per-variant traversed tree. The other three +variants keep every note: `solutions` and `grading` are the authors' own, and +`terse` is the instructor's, where a note on screen during a class is +harmless. + +Among the surviving blocks, a note is rendered only when its urgency passes +`devNoteShown` (`NOW`, `BeforeNextRelease`, or none): highlighted in the HTML +book, and passed through as a labelled comment in generated `.lean` files by +`CSwLMeta.Save.Extract.walkBlock`. `PotentialImprovement` notes render nothing. -/ block_extension Block.devcomment (author : Option String) (urgency : Option String) (year : Option Nat) where data := Json.arr #[toJson author, toJson urgency, toJson year] - traverse _ _ _ := return none + traverse _ _ _ := do + if (← getCurrVariant).isStudent then + -- Dev notes are for the authors; the student build gets none of them. + return some (.concat #[]) + else + return none toHtml := open Verso.Output.Html in some fun _ goB _ data contents => do diff --git a/STYLE-CODE.md b/STYLE-CODE.md index e2a88b5..9fd4018 100644 --- a/STYLE-CODE.md +++ b/STYLE-CODE.md @@ -173,9 +173,26 @@ Prose can be routed to a variant: ### Notes and commentary -- `:::dev` — an internal note to the authors. It renders with the heading - "Nota editorial" and must never carry anything the student should not read. - AI-generated commentary belongs here and is marked as such. +- `:::dev` — an internal note to the authors, rendered under the heading + "Nota editorial". AI-generated commentary belongs here, and is marked as + such. + + It takes an optional author (a string, as `Full Name (github-handle)`), an + optional urgency (`NOW`, `BeforeNextRelease` or `PotentialImprovement`, a + bare identifier), and an optional `(year := N)`. + + Two filters decide where a note appears, and they are independent: + + - **By variant**, in `Block.devcomment`'s `traverse`: the `student` build + drops every note, from the HTML and from the generated `.lean` alike. + `terse`, `solutions` and `grading` keep them all — `terse` is the + instructor's, so a note on screen during a class is harmless. + - **By urgency**, in `devNoteShown`: a `PotentialImprovement` note renders + nothing even where it is kept. Notes marked `NOW` or `BeforeNextRelease`, + and unmarked ones, render. + + So a dev note never reaches a student, and nothing in one has to be written + with a student in mind. - `:::quiz` and `:::quizSolution` — a comprehension check. - `:::diagramWithAlt` — a diagram with its textual alternative, for accessibility. From 2a6244c2f9eca41b3f467c8f5b97020d09369f47 Mon Sep 17 00:00:00 2001 From: Alexandre Rademaker Date: Fri, 11 Sep 2026 00:58:07 -0300 Subject: [PATCH 5/5] fix: fixes proposed by Co-Pilot small fixes proposed by the Co-Pilot review of the PR. --- CSwL/Sets.lean | 4 ++++ CSwLMeta/Save/Project.lean | 14 +++++++------- STYLE-CODE.md | 3 --- 3 files changed, 11 insertions(+), 10 deletions(-) diff --git a/CSwL/Sets.lean b/CSwL/Sets.lean index 0ab3e93..110c3ea 100644 --- a/CSwL/Sets.lean +++ b/CSwL/Sets.lean @@ -583,6 +583,10 @@ modelo a um fragmento — um domínio de entidades e, para cada verbo, a relação que ele denota — e à qual o tratamento de verbos de mais de dois lugares, e do escopo entre eles, volta mais tarde. +:::dev "Alexandre (arademaker)" +Estamos apresentando conceitos dentro do enunciado de um exercício. Talvez seja melhor evitar isso. +::: + ::::exercise (rating := 2) (name := "cartesian-square") Tome `A` como o conjunto `{Kasparov, Karpov, Anand}`. Encontre `A × A`. diff --git a/CSwLMeta/Save/Project.lean b/CSwLMeta/Save/Project.lean index 080e2ce..be15fd9 100644 --- a/CSwLMeta/Save/Project.lean +++ b/CSwLMeta/Save/Project.lean @@ -112,13 +112,13 @@ private def lakefileTemplate (vol : String) (v : Variant) "name = \"" ++ vol ++ "\"\n" ++ libs -/-- The `student` variant is the one the students receive, so its README is -the whole set-up guide: how to build, how to work an exercise, how to report a -problem. The other variants are read by the instructor, who has the repository -itself, and get only the note saying where they came from. - -Written in English, like every other document about the project; only the -book's prose is in Portuguese. -/ +/-- The `student` variant is the one the students receive, so its README is the + whole set-up guide: how to build, how to work an exercise, how to report a + problem. The `solutions` and `terse` variants are read by the instructor, who + has the repository itself, and get only the note saying where they came from. + The `grading` variant gets additional instructions for its private autograder + below. Written in English, like every other document about the project; only + the book's prose is in Portuguese. -/ private def readmeTemplate (vol : String) (v : Variant) : String := s!"# {vol} — `{v}` variant\n\n" ++ "Generated from the book (Verso, `Manual` genre) by " ++ diff --git a/STYLE-CODE.md b/STYLE-CODE.md index 9fd4018..6b3a722 100644 --- a/STYLE-CODE.md +++ b/STYLE-CODE.md @@ -85,9 +85,6 @@ author decision, not a mechanical fix. nor the English code-comment rule. - **`trivial`** — one term-level use in `Sets.lean:507`, not presented anywhere. Give it a line or replace it when that chapter is revised. -- **`Sets.lean` uses `Setoid`, `Fintype` and `Finset` with no presentation.** - A short paragraph plus a citation for each would settle it, under the - loosening `DEVIATIONS.md` describes. `IntroCS` is the constraint's one accepted exception: it uses Lean that `IntroL` only presents later, deliberately, and the chapter says so where its