diff --git a/CSwL/Logic/FOL.lean b/CSwL/Logic/FOL.lean index ba0f36c..bdf390d 100644 --- a/CSwL/Logic/FOL.lean +++ b/CSwL/Logic/FOL.lean @@ -45,37 +45,46 @@ 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] +``` + +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. ```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 +113,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 +134,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..54c961a 100644 --- a/STYLE-CODE.md +++ b/STYLE-CODE.md @@ -74,14 +74,14 @@ 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`, `∈`, `∉`, `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.)