From f506fb0a5e6aebd5426fef8f87901c368ff93427 Mon Sep 17 00:00:00 2001 From: Alexandre Rademaker Date: Mon, 19 Oct 2026 12:11:22 -0300 Subject: [PATCH 1/3] refactor(FOL): derive Repr and add ToString for the syntax types Variable, Term and Formula now derive Repr, so #eval shows the constructor tree, and their notation moves from a hand-written Repr over Std.Format to ToString instances, so toString shows the formula. This is the pattern InfEngine and ModelChecking already follow, and it lets a chapter show both views of the same formula. ToString, its behaviour under #eval and s! strings are presented at their first use, with Variable, and the ledger moves them from InfEngine to Logic/FOL. This change was prepared with the assistance of Claude Code (Anthropic); all edits were reviewed by the author. --- CSwL/Logic/FOL.lean | 52 ++++++++++++++++++++++++----------------- CSwL/ModelChecking.lean | 6 +---- STYLE-CODE.md | 6 ++--- 3 files changed, 34 insertions(+), 30 deletions(-) diff --git a/CSwL/Logic/FOL.lean b/CSwL/Logic/FOL.lean index ba0f36c..f81ecb6 100644 --- a/CSwL/Logic/FOL.lean +++ b/CSwL/Logic/FOL.lean @@ -45,37 +45,44 @@ Os _termos_ podem ser variáveis ou funções aplicadas a outros termos. Uma var structure Variable where name : String index : List Nat - deriving DecidableEq + deriving DecidableEq, Repr -def Variable.format : Variable → Std.Format +def Variable.toText : Variable → String | ⟨name, []⟩ => name - | ⟨name, [i]⟩ => name ++ toString i + | ⟨name, [i]⟩ => s!"{name}{i}" | ⟨name, is⟩ => name ++ String.intercalate "_" (is.map toString) -instance : Repr Variable := ⟨fun v _ => v.format⟩ +instance : ToString Variable := ⟨Variable.toText⟩ def x : Variable := ⟨"x", []⟩ def y : Variable := ⟨"y", []⟩ def z : Variable := ⟨"z", []⟩ ``` +A instrução `deriving Repr` gera, como em {ref "IntroL"}[IntroL], uma instância de {lean}`Repr`, que o `#eval` usa para exibir o valor como um termo Lean, mostrando sua estrutura. Para exibir uma variável na notação usual da lógica, implementamos também uma instância da classe {lean}`ToString`, que converte um valor em `String`. Quando um tipo tem as duas instâncias, `#eval` usa a de `Repr`; para ver a notação, escrevemos `#eval toString`. As cadeias `s!"…"` funcionam como as `f!"…"` de {ref "IntroL"}[IntroL], mas produzem uma `String`. + +```lean +#eval Variable.mk "x" [1] +#eval toString $ Variable.mk "x" [1] +``` + Termos denotam objetos do domínio, e diferentes termos podem denotar um mesmo objeto como os termos `(5 + 3) × 4`, `8 × 4` e `32`. Para representar termos mais complexos que apenas variáveis, a solução é introduzir símbolos funcionais para as operações entre termos. ```lean inductive Term where | var (v : Variable) | struct (name : String) (args : List Term) + deriving Repr -def Term.format : Term → Std.Format - | .var v => repr v +def Term.toText : Term → String + | .var v => toString v | .struct name [] => name | .struct name args => name ++ "[" ++ - Std.Format.joinSep - (args.map Term.format) "," ++ "]" + String.intercalate "," (args.map Term.toText) ++ "]" -instance : Repr Term := ⟨fun t _ => t.format⟩ +instance : ToString Term := ⟨Term.toText⟩ def tx : Term := .var x def ty : Term := .var y @@ -104,6 +111,7 @@ inductive Formula (α : Type) where | disj (f1 f2 : Formula α) | forall_ (v : Variable) (f : Formula α) | exists_ (v : Variable) (f : Formula α) + deriving Repr ``` A conjunção e a disjunção são binárias, e `top` e `bot` são construtores próprios, o mesmo que fizemos para as fórmulas proposicionais. @@ -124,31 +132,31 @@ def Formula.disjs {α : Type} : List (Formula α) → Formula α | f :: fs => .disj f (Formula.disjs fs) ``` -Um termo (Lean) do tipo `Formula` não é muito legível, vamos implementar a instância de `Repr` para controlar a exibição destes termos. Note que ela demanda que o tipo `α` tenha também uma instância de `Repr`, que já implementamos para {name}`Variable` e {name}`Term`. +Como para {name}`Variable` e {name}`Term`, o `#eval` de uma fórmula exibe sua árvore de construtores, e uma instância de {lean}`ToString` dá a notação mais legível. Note que a instância demanda que o tipo `α` tenha também uma instância de `ToString`, que já implementamos para {name}`Variable` e {name}`Term`. ```lean -def Formula.format {α} [Repr α] : Formula α → Std.Format +def Formula.toText {α} [ToString α] : Formula α → String | .atom name [] => name | .atom name args => name ++ "[" ++ - Std.Format.joinSep (args.map (repr ·)) ", " ++ "]" - | .eq t1 t2 => f!"{repr t1} = {repr t2}" - | .neg f => f!"~{f.format}" + String.intercalate ", " (args.map toString) ++ "]" + | .eq t1 t2 => s!"{t1} = {t2}" + | .neg f => s!"~{f.toText}" | .impl f1 f2 => - f!"({f1.format} ==> {f2.format})" + s!"({f1.toText} ==> {f2.toText})" | .equi f1 f2 => - f!"({f1.format} <=> {f2.format})" + s!"({f1.toText} <=> {f2.toText})" | .top => "⊤" | .bot => "⊥" | .conj f1 f2 => - f!"({f1.format} & {f2.format})" + s!"({f1.toText} & {f2.toText})" | .disj f1 f2 => - f!"({f1.format} | {f2.format})" - | .forall_ v f => f!"∀{repr v} {f.format}" - | .exists_ v f => f!"∃{repr v} {f.format}" + s!"({f1.toText} | {f2.toText})" + | .forall_ v f => s!"∀{v} {f.toText}" + | .exists_ v f => s!"∃{v} {f.toText}" -instance {α} [Repr α] : Repr (Formula α) := - ⟨fun f _ => f.format⟩ +instance {α} [ToString α] : ToString (Formula α) := + ⟨Formula.toText⟩ ``` A seguir, `R_reflexive` expressa que o predicado `R` é reflexivo enquanto `R_simetric` expressa que ele é simétrico. Note que para estes dois exemplos, usamos apenas variáveis, logo basta {lean}`Formula Variable`. diff --git a/CSwL/ModelChecking.lean b/CSwL/ModelChecking.lean index 5ef8aa3..1d1e7c1 100644 --- a/CSwL/ModelChecking.lean +++ b/CSwL/ModelChecking.lean @@ -542,10 +542,6 @@ def lfDV : DV → Term → Term → Term → LF A tradução de um determinante toma dois argumentos de tipo `Term → LF` — formas lógicas com um buraco de termo dentro — e produz uma forma lógica. No caso dos quantificadores, o primeiro argumento é a *restrição* e o segundo o *escopo*. -```display -lfDET : DET → (Term → LF) → (Term → LF) → LF -``` - A tradução dos determinantes precisa ser feita com algum cuidado, porque envolve construir uma forma lógica em que uma variável fica ligada. Para garantir a ligação correta, temos de nos assegurar de que a variável recém-introduzida não seja capturada por um quantificador já presente na forma lógica. Mas, se refletirmos sobre como as variáveis são introduzidas, veremos que elas sempre aparecem junto de quem as liga, e que nenhuma ligação é vazia. Basta então colher os índices das ocorrências ligadas. ```lean @@ -694,7 +690,7 @@ Construa as árvores de análise das quatro sentenças a seguir, todas geradas p 3. Every princess loved every dwarf that defeated a giant. 4. Every boy admired a girl that no wizard helped. -Os teoremas conferem que cada árvore devolve a sentença certa. Depois disso, `#eval lfSent tr1` exibe a forma lógica da primeira. +Os teoremas conferem que cada árvore devolve a sentença certa. Depois disso, `#eval toString (lfSent tr1)` exibe a forma lógica da primeira. ```lean def tr1 : Sent := diff --git a/STYLE-CODE.md b/STYLE-CODE.md index 9785565..a5f8d5a 100644 --- a/STYLE-CODE.md +++ b/STYLE-CODE.md @@ -77,11 +77,11 @@ this way is usually a mistake; see "Known gaps." | `IntroL` | `#check`, `#print`, `theorem`, `structure … where`, `instance` (named and anonymous), `opaque` | `Type`, `Bool`, `Int`, `Float`, `List`, `Option`, `Char`, `fun`/`λ`, `↦`, `match`, `if … then … else`, `⟨…⟩`, structure literal `{ x := … }` and update `{ s with … }`, implicit `{α : Type}`, instance-implicit `[Repr α]`, `∘`, `::`, `BEq`, `f!` strings, `List.all`/`List.any` | *(none — the chapter is deliberately pre-proof)* | | `Logic/Proof` | `open`, `section`, `variable` | `Prop`, `¬`, `∀`, `∃`, `∧`, `∨`, `↔`, `≠`, `False`, `absurd` (term), focus dots `·`, `h.1`/`h.2` | `intro`, `exact`, `apply`, `cases … with`, `constructor`, `obtain`, `have`, `use`, `left`, `right`, `by_cases`, `by_contra`, `assumption`, `funext`, `linarith`, `native_decide`, `simp`, `simp only [...]`, `simp … at h`, `rcases` and `Or.inl`/`Or.inr` **(solution only)** | | `Logic/PL` | `abbrev`, docstrings `/-- … -/`, `deriving DecidableEq`, `open … in` | `×` and tuples, `DecidableEq`, `True`, `≤`, section notation `(· ≤ ·)`, `\|>` **(solution only)** | `decide`, tactic locations `… at … ⊢`, `rw [← …]`, `all_goals`, `simpa … using` | -| `Logic/FOL` | `mutual`, polymorphic `inductive … (α : Type)`, `def` whose body is a type (`def Assign (D : Type) := Variable → D`), theorem defined by equations | `Fin`, `∈`, `∉`, `Std.Format` and a hand-written `Repr`, bare implicit `{α}`, `∀ (D : Type)`, anonymous-constructor patterns (`\| ⟨name, []⟩`), `match e₁, e₂ with` **(solution only)** | `induction … generalizing`, `<;>`, `refine` with `?_`, `omega` | +| `Logic/FOL` | `mutual`, polymorphic `inductive … (α : Type)`, `def` whose body is a type (`def Assign (D : Type) := Variable → D`), theorem defined by equations | `Fin`, `∈`, `∉`, `ToString` and its instance, `s!` strings, bare implicit `{α}`, `∀ (D : Type)`, anonymous-constructor patterns (`\| ⟨name, []⟩`), `match e₁, e₂ with` **(solution only)** | `induction … generalizing`, `<;>`, `refine` with `?_`, `omega` | | `Sets` | — | `Set`, `Rel`, `Finset`, `Fintype`, `Setoid`, `⊆`, `∪`, `∩`, `trivial` (term), `show … by …` **(solution only)** | `simp_all` | | `SeaBattle` | inductive predicate (`inductive WellFormed : Game → Prop where`) | structure fields that carry proofs, bounded `∀ x ∈ xs`, `by` as a structure-field value, `Fin.val`, dependent `if h : … then … else` **(solution only)**, `▸` **(solution only)** | *(none new)* | | `Morphology` | `open` of constructor namespaces (`open Attr Value`) | `match e₁, e₂ with` (first use outside a solution), `mapM` over `Option` **(solution only)** | *(none new)* | -| `InfEngine` | `let rec` | `do`-notation, `ToString` and its instance, `s!` strings | — | +| `InfEngine` | `let rec` | `do`-notation | — | | `ModelChecking` | `mutual` over `inductive` types (`Logic/FOL` only uses it over `def`) | guillemet identifiers (`«with»`), pattern-matching `fun \| … => …` (first use outside a solution) | *(none new)* | `ModelChecking` is where `abbrev` and `ToString` instances become the @@ -97,7 +97,7 @@ 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. Library functions are not tracked either — `String.intercalate`, -`List.zip`, `Std.Format.joinSep`, `List.Nodup` and their kind arrive with the +`List.zip`, `List.Nodup` and their kind arrive with the code that needs them. (`List.all`/`List.any` under `IntroL` is an older inconsistency; do not take it as licence to add siblings.) From 5e5b514e7de3d213baace1f058683ee8b05b305c Mon Sep 17 00:00:00 2001 From: Alexandre Rademaker Date: Mon, 19 Oct 2026 12:13:52 -0300 Subject: [PATCH 2/3] docs(FOL): use <| instead of $ in the ToString example `$` appears nowhere else in the book; `<|` is the idiomatic Lean form and IntroL already uses it. Record `<|` in the ledger under IntroL. This change was prepared with the assistance of Claude Code (Anthropic); all edits were reviewed by the author. --- CSwL/Logic/FOL.lean | 4 +++- STYLE-CODE.md | 2 +- 2 files changed, 4 insertions(+), 2 deletions(-) diff --git a/CSwL/Logic/FOL.lean b/CSwL/Logic/FOL.lean index f81ecb6..a6566fd 100644 --- a/CSwL/Logic/FOL.lean +++ b/CSwL/Logic/FOL.lean @@ -64,9 +64,11 @@ A instrução `deriving Repr` gera, como em {ref "IntroL"}[IntroL], uma instânc ```lean #eval Variable.mk "x" [1] -#eval toString $ Variable.mk "x" [1] +#eval toString <| Variable.mk "x" [1] ``` +No segundo `#eval`, `toString <| Variable.mk "x" [1]` é o mesmo que `toString (Variable.mk "x" [1])`: o operador `<|`, que já usamos em {ref "IntroL"}[IntroL], aplica a função à sua esquerda a tudo o que está à sua direita e dispensa os parênteses. O Lean também aceita `$` com o mesmo sentido, mas `<|` é a forma idiomática. + Termos denotam objetos do domínio, e diferentes termos podem denotar um mesmo objeto como os termos `(5 + 3) × 4`, `8 × 4` e `32`. Para representar termos mais complexos que apenas variáveis, a solução é introduzir símbolos funcionais para as operações entre termos. ```lean diff --git a/STYLE-CODE.md b/STYLE-CODE.md index a5f8d5a..54c961a 100644 --- a/STYLE-CODE.md +++ b/STYLE-CODE.md @@ -74,7 +74,7 @@ this way is usually a mistake; see "Known gaps." | Chapter | Commands and declarations | Types and syntax | Tactics | | --- | --- | --- | --- | | `IntroCS` | `namespace`, `def` (by pattern matching), `inductive`, `deriving Repr`, `example`, `#eval` | `Nat`, `String`, function type `→`, `++`, dot-notation constructors (`.num`) | `rfl`, `induction … with`, `rw`, `rewrite`, `unfold`, `repeat` | -| `IntroL` | `#check`, `#print`, `theorem`, `structure … where`, `instance` (named and anonymous), `opaque` | `Type`, `Bool`, `Int`, `Float`, `List`, `Option`, `Char`, `fun`/`λ`, `↦`, `match`, `if … then … else`, `⟨…⟩`, structure literal `{ x := … }` and update `{ s with … }`, implicit `{α : Type}`, instance-implicit `[Repr α]`, `∘`, `::`, `BEq`, `f!` strings, `List.all`/`List.any` | *(none — the chapter is deliberately pre-proof)* | +| `IntroL` | `#check`, `#print`, `theorem`, `structure … where`, `instance` (named and anonymous), `opaque` | `Type`, `Bool`, `Int`, `Float`, `List`, `Option`, `Char`, `fun`/`λ`, `↦`, `match`, `if … then … else`, `⟨…⟩`, structure literal `{ x := … }` and update `{ s with … }`, implicit `{α : Type}`, instance-implicit `[Repr α]`, `∘`, `::`, `BEq`, `f!` strings, `<|`, `List.all`/`List.any` | *(none — the chapter is deliberately pre-proof)* | | `Logic/Proof` | `open`, `section`, `variable` | `Prop`, `¬`, `∀`, `∃`, `∧`, `∨`, `↔`, `≠`, `False`, `absurd` (term), focus dots `·`, `h.1`/`h.2` | `intro`, `exact`, `apply`, `cases … with`, `constructor`, `obtain`, `have`, `use`, `left`, `right`, `by_cases`, `by_contra`, `assumption`, `funext`, `linarith`, `native_decide`, `simp`, `simp only [...]`, `simp … at h`, `rcases` and `Or.inl`/`Or.inr` **(solution only)** | | `Logic/PL` | `abbrev`, docstrings `/-- … -/`, `deriving DecidableEq`, `open … in` | `×` and tuples, `DecidableEq`, `True`, `≤`, section notation `(· ≤ ·)`, `\|>` **(solution only)** | `decide`, tactic locations `… at … ⊢`, `rw [← …]`, `all_goals`, `simpa … using` | | `Logic/FOL` | `mutual`, polymorphic `inductive … (α : Type)`, `def` whose body is a type (`def Assign (D : Type) := Variable → D`), theorem defined by equations | `Fin`, `∈`, `∉`, `ToString` and its instance, `s!` strings, bare implicit `{α}`, `∀ (D : Type)`, anonymous-constructor patterns (`\| ⟨name, []⟩`), `match e₁, e₂ with` **(solution only)** | `induction … generalizing`, `<;>`, `refine` with `?_`, `omega` | From 2c28c5b36b249d834f899bdcaeb391b085cd48ff Mon Sep 17 00:00:00 2001 From: Alexandre Rademaker Date: Mon, 19 Oct 2026 13:31:06 -0300 Subject: [PATCH 3/3] wip: operaor <| --- CSwL/Logic/FOL.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/CSwL/Logic/FOL.lean b/CSwL/Logic/FOL.lean index a6566fd..bdf390d 100644 --- a/CSwL/Logic/FOL.lean +++ b/CSwL/Logic/FOL.lean @@ -67,7 +67,7 @@ A instrução `deriving Repr` gera, como em {ref "IntroL"}[IntroL], uma instânc #eval toString <| Variable.mk "x" [1] ``` -No segundo `#eval`, `toString <| Variable.mk "x" [1]` é o mesmo que `toString (Variable.mk "x" [1])`: o operador `<|`, que já usamos em {ref "IntroL"}[IntroL], aplica a função à sua esquerda a tudo o que está à sua direita e dispensa os parênteses. O Lean também aceita `$` com o mesmo sentido, mas `<|` é a forma idiomática. +No segundo `#eval`, o operador `<|`, que já usamos em {ref "IntroL"}[IntroL], aplica a função à sua esquerda a tudo o que está à sua direita e dispensa os parênteses. Termos denotam objetos do domínio, e diferentes termos podem denotar um mesmo objeto como os termos `(5 + 3) × 4`, `8 × 4` e `32`. Para representar termos mais complexos que apenas variáveis, a solução é introduzir símbolos funcionais para as operações entre termos.