diff --git a/Bib.lean b/Bib.lean index c4d7b9c..af1ab53 100644 --- a/Bib.lean +++ b/Bib.lean @@ -16,6 +16,8 @@ the text — the same convention as `sf-in-lean/Bib.lean`, which records books namespace Bib + + def logicandproof : Article where title := inlines!"Logic and Proof" authors := #[inlines!"Jeremy Avigad", inlines!"Joseph Hua", @@ -113,6 +115,16 @@ def nederpelt2014 : Article where volume := inlines!"" number := inlines!"" +def wadler2003 : Article where + title := inlines!"A Prettier Printer" + authors := #[inlines!"Philip Wadler"] + journal := inlines!"The Fun of Programming: A symposium in honour of Richard Bird's 60th birthday, Oxford" + year := 2003 + month := none + volume := inlines!"" + number := inlines!"" + url := "https://homepages.inf.ed.ac.uk/wadler/papers/prettier/prettier.pdf" + def FAA2025 : Article where title := inlines!"Formalizing Analysis of Algorithms, Autumn 2025" authors := #[inlines!"Sorrachai Yingchareonthawornchai"] diff --git a/CLAUDE.md b/CLAUDE.md index cf8cf95..edafab9 100644 --- a/CLAUDE.md +++ b/CLAUDE.md @@ -39,7 +39,7 @@ Using Verso, we could also create slides; see https://github.com/arademaker/sviL The textbook will be written in Portuguese. Later, we plan to translate it back into English. -But all names in the Lean code are in English; comments in the Lean code are also in English. This applies to the code presented to the students and also the code of the project itself, the Lean code that produces the book (verso extensions, infrastructure, etc) +But all identifiers in the Lean code are in English; comments and docstrings in the Lean code are also in English. This applies to the code presented to the students and also the code of the project itself, the Lean code that produces the book (verso extensions, infrastructure, etc) The repo README is in English. All documentation *about* the project should be in English. Use English for git commit messages as well. diff --git a/CSwL/English.lean b/CSwL/English.lean index d9b2fbf..ac34671 100644 --- a/CSwL/English.lean +++ b/CSwL/English.lean @@ -16,744 +16,33 @@ file := "English" namespace English ``` -# Um fragmento linguístico +# Formas Linguísticas e Traduções para Lógica -Vamos construir uma sentença a partir de um sujeito e um predicado. Não se -trata da concatenação de strings, é um construtor de sentenças que -respeitam uma estrutura esperada. O verificador de tipos passa a recusar -as combinações que não são sentenças. Um embrião do que vamos ver pela -frente. - -A keyword `deriving` pede que uma instância para a classe `Repr` seja -automaticamente gerada para cada tipo. - -```lean -inductive Subject where - | Chomsky - | Montague -deriving Repr - -inductive Predicate where - | Wrote (title : String) -deriving Repr - -inductive Sentence where - | S (subj : Subject) (pred : Predicate) -deriving Repr -``` - -A abreviações são como `def` mas são `unfold` automaticamente. - -```lean -abbrev Sentences := List Sentence - -#eval Subject.Chomsky - -#eval Sentence.S Subject.Chomsky - (Predicate.Wrote "Syntactic Structures") -``` - -A última saida acima lembra uma árvore, o que iremos chamar de _árvore -sintática_. - -```display - Sentence - |- Subject - |- Predicate -``` - -O passo inverso é a _geração_, serializar uma estrutura que representa -uma sentença. Para isso temos que transformar a representação interna em -uma String. Já existe a classe `ToString` e `IO.println` pede como entrada -um tipo que seja instância desta classe. Então só precisamos definir as -instâncias para `ToString` de nossos tipos. Criar uma instância de uma -classe é implementar os campos que a classe demanda e classes são -`structure`. Algumas variações de sintaxe na declaração das instâncias. - -```lean -instance : ToString Subject where - toString - | .Chomsky => "Chomsky" - | .Montague => "Montague" - -instance : ToString Predicate := - ⟨ fun p => match p with - | .Wrote t => s!"wrote \"{t}\"" ⟩ - -instance : ToString Sentence := - ⟨ fun | .S s p => s!"{s} {p}" ⟩ -``` - -Algumas funções auxiliares para conveniência. - -```lean -def makeP (title : String) : Predicate := .Wrote title -def makeS (s : Subject) (p : Predicate) : Sentence := .S s p -``` - -```lean (name := c2eval39) -#eval IO.println $ - makeS .Chomsky (makeP "Syntactic Structures") -``` - - -## Por que isso serve à semântica - -Um verbo transitivo é uma função de dois lugares. _Likes_ se escreve -`λxλy ↦ y likes x`, onde `likes` é a função característica da relação -de gostar — a mesma `Sets.likesR` de {ref "Sets"}[Conjuntos e Relações], só -que agora vista -como instrução curried em vez de par de argumentos. - -Aqui a aplicação parcial deixa de ser conveniência de -programação e passa a ter conteúdo linguístico. `add 3` era uma função -à espera do segundo número; do mesmo modo, o verbo aplicado ao seu -objeto é uma expressão à espera do sujeito — que é precisamente o que -se chama de sintagma verbal. A currificação não modela o VP por acaso: -ela é o VP. - -Repare no que a notação *não* diz. Ela não diz o que _likes_ significa -no mundo. Diz apenas com que outras expressões o verbo se combina e que -papel desempenha na expressão maior — e é justamente por dizer só isso -que o cálculo lambda serve à semântica composicional. A derivação do -significado pode então acompanhar, passo a passo, a estrutura sintática -da sentença. - -Tipos, em programação e no cálculo lambda, se comportam como -*categorias sintáticas* em gramática — e essa observação amarra as -duas metades do argumento acima. - -Categorias como NP correspondem a tipos básicos: expressões completas, -que carregam significado por si. Categorias como VP correspondem a -tipos de função: expressões incompletas, cujo significado consiste na -contribuição que dão à expressão em que aparecem. - -Sob essa leitura, uma regra de reescrita como `S → NP VP` diz uma coisa -sobre tipos: se `a : NP` e `b : VP`, então a concatenação de `a` e `b` é -um `S`. E se o VP é o que combina com um NP para dar um S, então o -próprio VP tem tipo `e → t` — a categoria deixa de ser um rótulo e -passa a ser uma função. - -Essa é a ideia da *gramática categorial*, que vem de Ajdukiewicz. Um -verbo transitivo, que combina com dois NPs, tem tipo `e → (e → t)` — -e é justamente o tipo de `Sets.likesR`, `Entity → Entity → Prop`, lido com -`e := Entity` e `t := Prop`. A relação binária da seção anterior já -era, sem que se precisasse dizer, um verbo transitivo em potencial: *o -verbo transitivo denota uma relação binária, e o tipo de `Sets.likesR` já -dizia isso.* - -A regra de combinação é uma só: uma expressão de categoria `A` combina -com uma de categoria `A → B` e produz uma de categoria `B` — isto é, -aplicação. Em Lean isso se escreve diretamente, e o verificador de -tipos passa a validar a derivação: - -```lean -abbrev e := Sets.Entity -abbrev t := Prop - -def dorothy : e := .dorothy -def toto : e := .toto -``` - -O verbo, como função de dois lugares: recebe o objeto, depois o -sujeito. - -```lean -opaque likes : e → e → t -``` - -O VP: o verbo já recebeu o objeto e espera o sujeito. - -```lean -def likesToto : e → t := likes toto -``` - -E a sentença, com o sujeito no lugar. - -```lean -def dorothyLikesToto : t := likesToto dorothy - -#check dorothyLikesToto -``` - - -A derivação da sentença é uma sequência de duas aplicações, e cada -passo é conferido pelos tipos. Uma combinação mal formada não chega a -ser um termo. - -Atribua tipos às expressões lambda da derivação a seguir: - -``` -S = Dorothy likes Toto -NP = Dorothy -VP = λy ↦ y likes Toto -V = λx λy ↦ y likes x -NP = Toto -``` - -Com os dois tipos básicos já em uso acima — `e := Entity` e `t := Prop`, -as letras de Montague: - -* S — `Dorothy likes Toto` — tipo `t` -* NP — `Dorothy` — tipo `e` -* VP — `λy ↦ y likes Toto` — tipo `e → t` -* V — `λx λy ↦ y likes x` — tipo `e → (e → t)` -* NP — `Toto` — tipo `e` - -A operação que leva do tipo de `V` ao tipo de `VP` é a *aplicação de -função*: aplicar `likes : e → (e → t)` ao objeto `toto : e` satura o -primeiro argumento e devolve `e → t`, que é o tipo de `VP` — é -exatamente `likesToto` acima. O mesmo passo, aplicado outra vez com o -sujeito `dorothy : e`, leva até `t` — é `dorothyLikesToto`. Em suma, a -árvore sintática é lida como uma cadeia de aplicações, e cada -combinação de nós consome um argumento; a frase completa é o ponto em -que não falta mais nada, e é por isso que seu tipo é `t` e não uma -função. - -Observação sobre convenção: como o léxico escreve `V = λx λy ↦ y likes -x`, o _objeto_ é o primeiro argumento e o _sujeito_ o segundo — é o que -`likesToto := likes toto` e `dorothyLikesToto := likesToto dorothy` -acima já fazem, na ordem certa. - -::::exercise (rating := 1) (name := "adjective-types") - -Adjetivos combinam com nomes para formar nomes complexos: _friendly_ -combina com _wizard_ para formar _friendly wizard_. Adjetivos são, -portanto, de tipo `N → N`. - -Ache um tipo para o advérbio _very_, tal que se possa construir _very -friendly wizard_ e _very very friendly wizard_. (Assuma que as -expressões se estruturam como `(very friendly) wizard` e `(very (very -friendly)) wizard`.) - -`very : Adj → Adj`: um advérbio de grau não modifica um nome, modifica -um _adjetivo_, e devolve outro adjetivo. É exatamente isso que permite -as duas construções pedidas — como o resultado de `very` é de novo um -`Adj`, ele serve como argumento de si mesmo. - -```lean -abbrev N := String -abbrev Adj := N → N - -def wizard : N := "wizard" -def friendly : Adj := fun n => "friendly " ++ n - -def very : Adj → Adj := - solution!(fun a => fun n => "very " ++ a n) - -theorem very_test1 : - very friendly wizard = "very friendly wizard" := - solution!(by rfl) -theorem very_test2 : - very (very friendly) wizard = - "very very friendly wizard" := - solution!(by rfl) -``` - -:::gradeTheorem "1" very_test1 very_test2 +:::dev "Alexandre (arademaker)" +aqui entra seção CSwFP/6.1 ::: -:::: - -O ponto teórico é que o tipo de `very` é _endomórfico_ na categoria dos -adjetivos (entra `Adj`, sai `Adj`), e por isso a iteração é ilimitada -com um único tipo, sem precisar de um tipo novo para cada nível de -encaixe. As duas verificações por `rfl` acima compilam — o que faz do -próprio verificador de tipos a confirmação da resposta. - -Para ver a recusa acontecer, tente dar ao verbo um objeto que não é uma -entidade: `#check likes "Toto"` não compila, e o erro aponta o -argumento — uma `String` onde se esperava um `e`. É a versão tipada de -dizer que a combinação não é bem formada. - - -# Um fragmento do inglês - -Em seguida, vamos implementar um fragmento um pouco mais realistico do inglês. Ela é deliberadamente básica e grosseira, queremos capturar a sintaxe de sentenças como: - -1. The girl laughed. -2. No dwarf admired some princess that shuddered. -3. Every girl that some boy loved cheered. -4. The wizard that helped Snow White defeated the giant. - -Então o que precisamos é uma regra para uma sentença sujeito-predicado. Uma regra para a estrutura interna de um sintagma nominal. Uma regra para substantivos com ou sem clausulas relativas. Nossa gramática poderia ser: - -```bnf -S ::= NP VP ; -NP ::= "Snow White" | "Alice" | "Dorothy" | "Goldilocks" | "Little Mook" | "Atreyu" - | DET CN | DET RCN ; -DET ::= "the" | "a" | "every" | "some" | "no" | "most" ; -CN ::= "girl" | "boy" | "princess" | "dwarf" | "giant" | "wizard" | "sword" | "dagger" ; -RCN ::= CN "that" VP | CN "that" NP TV ; -VP ::= "laughed" | "cheered" | "shuddered" | TV NP | DV NP NP ; -TV ::= "loved" | "admired" | "helped" | "defeated" | "caught" ; -DV ::= "gave" ; -``` - -A implementação abaixo acrescenta tipos auxiliares aos oito não-terminais da BNF, introduzidos para ilustrar intensionalidade mais adiante. - -A tradução para Lean é direta: cada categoria sintática é um construtor de um `inductive` mutuamente recursivo — a árvore de análise de uma sentença é um termo desse tipo, sem passo de tradução string→árvore a definir. - -```lean -inductive DET where - | a | the | every | some | no | most - deriving Repr - -instance : ToString DET := - ⟨fun | .a => "a" | .the => "the" - | .every => "every" | .some => "some" - | .no => "no" | .most => "most"⟩ - -inductive CN where - | girl | boy | princess | dwarf | giant | wizard | sword - | dagger - deriving Repr - -instance : ToString CN := - ⟨fun | .girl => "girl" | .boy => "boy" - | .princess => "princess" | .dwarf => "dwarf" - | .giant => "giant" | .wizard => "wizard" - | .sword => "sword" | .dagger => "dagger"⟩ - -inductive ADJ where - | fake - deriving Repr - -instance : ToString ADJ := ⟨fun | .fake => "fake"⟩ - -inductive That where - | that - deriving Repr - -inductive TV where - | loved | admired | helped | defeated | caught - deriving Repr - -instance : ToString TV := - ⟨fun | .loved => "loved" | .admired => "admired" - | .helped => "helped" | .defeated => "defeated" - | .caught => "caught"⟩ -inductive DV where - | gave - deriving Repr +# Um fragmento do Inglês -instance : ToString DV := ⟨fun | .gave => "gave"⟩ - -inductive AV where - | hoped | wanted - deriving Repr - -instance : ToString AV := - ⟨fun | .hoped => "hoped" | .wanted => "wanted"⟩ - -inductive TINF where - | love | admire | help | defeat | catch - deriving Repr - -instance : ToString TINF := - ⟨fun | .love => "love" | .admire => "admire" - | .help => "help" | .defeat => "defeat" - | .catch => "catch"⟩ - -inductive To where - | to - deriving Repr -``` - -Estes nove tipos não se referem uns aos outros nem a -`NP`/`VP`/`RCN`/`INF`/`Sent` — cada um é um enum simples ou tem campos -só desses enums, então não precisam entrar no bloco `mutual` abaixo. -Isolá-los deixa visível qual é a recursão real do fragmento: só `NP`, -`RCN`, `VP` e `INF` se referenciam (e a `Sent` que os fecha). - -```lean -mutual - inductive Sent where - | sent (np : NP) (vp : VP) - deriving Repr - - inductive NP where - | snowWhite | alice | dorothy | goldilocks | littleMook - | atreyu - | everyone | someone - | np1 (det : DET) (cn : CN) - | np2 (det : DET) (rcn : RCN) - deriving Repr - - inductive RCN where - | rcn1 (cn : CN) (compl : That) (vp : VP) - | rcn2 (cn : CN) (compl : That) (np : NP) (tv : TV) - | rcn3 (adj : ADJ) (cn : CN) - deriving Repr - - inductive VP where - | laughed | cheered | shuddered - | vp1 (tv : TV) (np : NP) - | vp2 (dv : DV) (np1 np2 : NP) - | vp3 (av : AV) (marker : To) (inf : INF) - deriving Repr - - inductive INF where - | laugh | cheer | shudder - | inf1 (tinf : TINF) (np : NP) - deriving Repr -end -mutual - -def Sent.toStringImpl : Sent → String - | .sent np vp => s!"{np.toStringImpl} {vp.toStringImpl}" - -def NP.toStringImpl : NP → String - | .snowWhite => "Snow White" | .alice => "Alice" - | .dorothy => "Dorothy" | .goldilocks => "Goldilocks" - | .littleMook => "Little Mook" | .atreyu => "Atreyu" - | .everyone => "everyone" | .someone => "someone" - | .np1 det cn => s!"{det} {cn}" - | .np2 det rcn => s!"{det} {rcn.toStringImpl}" - -def RCN.toStringImpl : RCN → String - | .rcn1 cn _ vp => s!"{cn} that {vp.toStringImpl}" - | .rcn2 cn _ np tv => s!"{cn} that {np.toStringImpl} {tv}" - | .rcn3 adj cn => s!"{adj} {cn}" - -def VP.toStringImpl : VP → String - | .laughed => "laughed" | .cheered => "cheered" - | .shuddered => "shuddered" - | .vp1 tv np => s!"{tv} {np.toStringImpl}" - | .vp2 dv np1 np2 => - s!"{dv} {np1.toStringImpl} {np2.toStringImpl}" - | .vp3 av _ inf => s!"{av} to {inf.toStringImpl}" - -def INF.toStringImpl : INF → String - | .laugh => "laugh" | .cheer => "cheer" - | .shudder => "shudder" - | .inf1 tinf np => s!"{tinf} {np.toStringImpl}" -end - -instance : ToString Sent := ⟨Sent.toStringImpl⟩ -``` - -`That` e `To` são tipos com um único construtor. `catch` colide com a palavra reservada do Lean para captura de exceções; o construtor de `TINF` fica `catch` mesmo assim, dentro do namespace `TINF`, sem conflito (o Lean resolve pelo namespace, `TINF.catch` não é `catch` do núcleo). - -A árvore de análise de "The dwarf that Snow White helped admired every -princess" é como segue, construir esta árvore a partir da string é o que chamamos de _parsing_. - -``` -S -├── NP -│ ├── DET — the -│ └── RCN -│ ├── CN — dwarf -│ ├── That — that -│ ├── NP — Snow White -│ └── TV — helped -└── VP - ├── TV — admired - └── NP - ├── DET — every - └── CN — princess -``` - -O termo Lean correspondente segue. Note que a sentença em inglês é uma sequencia de caracteres em um alfabeto, uma string no computador. A árvore é a representação abstrata da estrutura da sentença, o termo Lean é a formalização desta representação. `Repr` imprime o termo; `ToString` faz o caminho inverso do _parsing_, devolve, a partir do termo, a sentença de superfície. - -```lean -def snowWhile : Sent := - .sent (.np2 .the (.rcn2 .dwarf .that .snowWhite .helped)) - (.vp1 .admired (.np1 .every .princess)) - -#eval snowWhile -#eval toString snowWhile -``` - -::::exercise (rating := 1) (name := "preposition-phrase") - -Estenda o fragmento com sintagmas preposicionais, de modo que a -sentença "A dwarf defeated a giant with a sword" seja gerada de duas -formas estruturalmente diferentes, enquanto "A dwarf defeated Little -Mook with a sword" só tenha uma forma de ser gerada. - -Primeiro acrescentamos duas regras para construir PPs a partir de uma -preposição e um NP. Em seguida estendemos a regra de NPs, para gerar NPs -como a giant with a sword. Note que não simplesmente acrescentamos uma -produção recursiva `NP → NP PP`. Se fizéssemos isso, não só permitiríamos -um número arbitrário de PPs como modificadores de NP, mas também -geraríamos NPs como "Little Mook with a sword" (o que queremos excluir). -Por fim, também estendemos a regra de VP para construir VPs com sintagmas -preposicionais. - -```bnf -P ::= "with" ; -PP ::= P NP ; -NP ::= _NP | DET CN PP ; -VP ::= _VP | TV NP PP ; -``` - -Como `inductive` em Lean é fechado — não dá para acrescentar construtores a um tipo já definido —, a extensão exige redefinir todo o agrupamento mutuamente recursivo (`Sent`, `NP`, `RCN`, `VP`, `INF`), acrescentando `PP` a ele, em vez de simplesmente estender `NP`/`VP` originais. Isolamos o restante num namespace próprio, para não afetar o fragmento original de `NP`/`VP` sem PPs. - -```lean -namespace WithPP - -inductive P where - | «with» - deriving Repr - -instance : ToString P := ⟨fun | .with => "with"⟩ - -mutual - inductive Sent where - | sent (np : NP) (vp : VP) - deriving Repr - - inductive NP where - | snowWhite | alice | dorothy | goldilocks | littleMook - | atreyu - | everyone | someone - | np1 (det : DET) (cn : CN) - | np2 (det : DET) (rcn : RCN) - | np3 (det : DET) (cn : CN) (pp : PP) - deriving Repr - - inductive RCN where - | rcn1 (cn : CN) (compl : That) (vp : VP) - | rcn2 (cn : CN) (compl : That) (np : NP) (tv : TV) - | rcn3 (adj : ADJ) (cn : CN) - deriving Repr - - inductive VP where - | laughed | cheered | shuddered - | vp1 (tv : TV) (np : NP) - | vp2 (dv : DV) (np1 np2 : NP) - | vp3 (av : AV) (marker : To) (inf : INF) - | vp4 (tv : TV) (np : NP) (pp : PP) - deriving Repr - - inductive INF where - | laugh | cheer | shudder - | inf1 (tinf : TINF) (np : NP) - deriving Repr - - inductive PP where - | pp1 (p : P) (np : NP) - deriving Repr -end - -mutual - -def Sent.toStringImpl : Sent → String - | .sent np vp => s!"{np.toStringImpl} {vp.toStringImpl}" - -def NP.toStringImpl : NP → String - | .snowWhite => "Snow White" - | .alice => "Alice" - | .dorothy => "Dorothy" - | .goldilocks => "Goldilocks" - | .littleMook => "Little Mook" - | .atreyu => "Atreyu" - | .everyone => "everyone" | .someone => "someone" - | .np1 det cn => s!"{det} {cn}" - | .np2 det rcn => s!"{det} {rcn.toStringImpl}" - | .np3 det cn pp => s!"{det} {cn} {pp.toStringImpl}" - -def RCN.toStringImpl : RCN → String - | .rcn1 cn _ vp => s!"{cn} that {vp.toStringImpl}" - | .rcn2 cn _ np tv => s!"{cn} that {np.toStringImpl} {tv}" - | .rcn3 adj cn => s!"{adj} {cn}" - -def VP.toStringImpl : VP → String - | .laughed => "laughed" | .cheered => "cheered" - | .shuddered => "shuddered" - | .vp1 tv np => s!"{tv} {np.toStringImpl}" - | .vp2 dv np1 np2 => - s!"{dv} {np1.toStringImpl} {np2.toStringImpl}" - | .vp3 av _ inf => s!"{av} to {inf.toStringImpl}" - | .vp4 tv np pp => - s!"{tv} {np.toStringImpl} {pp.toStringImpl}" - -def INF.toStringImpl : INF → String - | .laugh => "laugh" | .cheer => "cheer" - | .shudder => "shudder" - | .inf1 tinf np => s!"{tinf} {np.toStringImpl}" - -def PP.toStringImpl : PP → String - | .pp1 p np => s!"{p} {np.toStringImpl}" - -end - -instance : ToString Sent := ⟨Sent.toStringImpl⟩ -``` - -A ambiguidade pedida está em `giantWithSword1`/`giantWithSword2`: o PP -`with a sword` pode se ligar dentro do NP (modificando `a giant`) ou -direto na VP (modificando o evento de derrotar); as duas árvores são -diferentes, mas produzem a mesma sentença de superfície. Já -`mookWithSword` só admite a segunda leitura, porque `NP ::= DET CN PP` -exige um determinante e `CN`, e "Little Mook" é um nome próprio sem -determinante — não há como formar `Little Mook with a sword` como um -único NP. - -```lean --- PP dentro do NP objeto ("a giant with a sword" é um NP). -def giantWithSword1 : Sent := - .sent (.np1 .a .dwarf) - (.vp1 .defeated - (.np3 .a .giant (.pp1 .with (.np1 .a .sword)))) - --- mesma sentença, PP ligado à VP em vez do NP. -def giantWithSword2 : Sent := - .sent (.np1 .a .dwarf) - (.vp4 .defeated (.np1 .a .giant) - (.pp1 .with (.np1 .a .sword))) - --- única leitura possível -def mookWithSword : Sent := - .sent (.np1 .a .dwarf) - (.vp4 .defeated .littleMook - (.pp1 .with (.np1 .a .sword))) - -end WithPP -``` - -```lean (name := c4evalPP1) -#eval toString WithPP.giantWithSword1 -#eval toString WithPP.giantWithSword2 -#eval toString WithPP.mookWithSword -``` - -As duas árvores diferentes imprimem a mesma sentença de superfície, -a ambiguidade pedida. -:::: - -::::exercise (rating := 1) (name := "complex-relative-clauses") - -Estenda o fragmento com orações relativas complexas, em que a oração relativa coordena duas VPs paralelas ou dois pares NP-TV paralelos (não sentenças completas). O fragmento deve gerar, entre outras, a sentença "The dwarf that Snow White helped and Goldilocks admired cheered". Que problemas você encontra? - -Acrescentamos `COORD` e duas regras para `RCN`, cada uma coordenando -duas ocorrências da mesma forma — ou duas VPs, ou dois pares NP-TV: - -```bnf -COORD ::= "and" ; -RCN ::= _RCN | CN "that" VP COORD VP - | CN "that" NP TV COORD NP TV ; -``` - -Como antes, `inductive` fechado obriga a redefinir todo o agrupamento -mutual só para acrescentar construtores a `RCN`. - -```lean -namespace WithCoord - -inductive COORD where - | and - deriving Repr - -instance : ToString COORD := ⟨fun | .and => "and"⟩ - -mutual - inductive Sent where - | sent (np : NP) (vp : VP) - deriving Repr - - inductive NP where - | snowWhite | alice | dorothy | goldilocks | littleMook - | atreyu - | everyone | someone - | np1 (det : DET) (cn : CN) - | np2 (det : DET) (rcn : RCN) - deriving Repr - - inductive RCN where - | rcn1 (cn : CN) (compl : That) (vp : VP) - | rcn2 (cn : CN) (compl : That) (np : NP) (tv : TV) - | rcn3 (adj : ADJ) (cn : CN) - | rcn4 (cn : CN) (compl : That) - (vp1 : VP) (coord : COORD) (vp2 : VP) - | rcn5 (cn : CN) (compl : That) - (np1 : NP) (tv1 : TV) (coord : COORD) - (np2 : NP) (tv2 : TV) - deriving Repr - - inductive VP where - | laughed | cheered | shuddered - | vp1 (tv : TV) (np : NP) - | vp2 (dv : DV) (np1 np2 : NP) - | vp3 (av : AV) (marker : To) (inf : INF) - deriving Repr - - inductive INF where - | laugh | cheer | shudder - | inf1 (tinf : TINF) (np : NP) - deriving Repr -end - -mutual - -def Sent.toStringImpl : Sent → String - | .sent np vp => s!"{np.toStringImpl} {vp.toStringImpl}" - -def NP.toStringImpl : NP → String - | .snowWhite => "Snow White" | .alice => "Alice" - | .dorothy => "Dorothy" | .goldilocks => "Goldilocks" - | .littleMook => "Little Mook" | .atreyu => "Atreyu" - | .everyone => "everyone" | .someone => "someone" - | .np1 det cn => s!"{det} {cn}" - | .np2 det rcn => s!"{det} {rcn.toStringImpl}" - -def RCN.toStringImpl : RCN → String - | .rcn1 cn _ vp => s!"{cn} that {vp.toStringImpl}" - | .rcn2 cn _ np tv => s!"{cn} that {np.toStringImpl} {tv}" - | .rcn3 adj cn => s!"{adj} {cn}" - | .rcn4 cn _ vp1 coord vp2 => - s!"{cn} that {vp1.toStringImpl} {coord} " ++ - s!"{vp2.toStringImpl}" - | .rcn5 cn _ np1 tv1 coord np2 tv2 => - s!"{cn} that {np1.toStringImpl} {tv1} {coord} " ++ - s!"{np2.toStringImpl} {tv2}" - -def VP.toStringImpl : VP → String - | .laughed => "laughed" | .cheered => "cheered" - | .shuddered => "shuddered" - | .vp1 tv np => s!"{tv} {np.toStringImpl}" - | .vp2 dv np1 np2 => - s!"{dv} {np1.toStringImpl} {np2.toStringImpl}" - | .vp3 av _ inf => s!"{av} to {inf.toStringImpl}" - -def INF.toStringImpl : INF → String - | .laugh => "laugh" | .cheer => "cheer" - | .shudder => "shudder" - | .inf1 tinf np => s!"{tinf} {np.toStringImpl}" - -end +:::dev "Alexandre (arademaker)" +aqui entra seção CSwFP/4.2. os exercícios pedem expansoes de uma gramatica inicial, vamos tentar fazer evitando ao máximo redefinições de tipos indutivos. +::: -instance : ToString Sent := ⟨Sent.toStringImpl⟩ +# FOL como Linguagem de representação -end WithCoord -``` +:::dev "Alexandre (arademaker)" +aqui entra seção CSwFP/6.2. Ela usa o fragmento definido na seção anterior que veio da CSwFP/4.2 +::: -Dois exemplos: a sentença do enunciado usa `rcn5` (coordenação de -pares NP-TV, a RCN é sobre o objeto em ambos os ramos); a outra usa -`rcn4` (coordenação de VPs, a RCN é sobre o sujeito em ambos os ramos). +# Uma Estrutura de Primeira Ordem -```lean (name := c4evalCoord1) -#eval toString (WithCoord.Sent.sent - (.np2 .the (.rcn5 .dwarf .that .snowWhite .helped - .and .goldilocks .admired)) - .cheered) -``` +:::dev "Alexandre (arademaker)" +aqui entra seção CSwFP/6.3. Deve definir a estrutura para avaliação das fórmulas da seção anterior. -```lean (name := c4evalCoord2) -#eval toString (WithCoord.Sent.sent - (.np2 .the (.rcn4 .dwarf .that - (.vp1 .helped .goldilocks) .and - (.vp1 .admired .snowWhite))) - .laughed) -``` - -`rcn4` e `rcn5` só coordenam formas paralelas (VP com VP, ou NP-TV com NP-TV), exatamente porque são regras separadas; misturá-las produziria "the dwarf that Goldilocks helped and admired Snow White", que é agramatical: na primeira RCN o vazio (_gap_) está no objeto ("Goldilocks helped ␣"), na segunda está no sujeito ("␣ admired Snow White"), e não há como coordenar as duas leituras numa só sentença. Coordenar `Sent` inteiras em vez de VPs/pares NP-TV geraria justamente essa mistura, por isso o fragmento não faz isso. +Como já implementamos a semantica de FOL no `FOL.lean`, nesta mesma seção podemos absorver CSwFP/6.4 usando o que já temos em `FOL.lean` +::: -O _gap_ é a posição, dentro da `RCN`, onde entraria o `CN` que ela modifica — em `rcn1` (`CN "that" VP`) o gap é o sujeito da VP; em `rcn2` (`CN "that" NP TV`) é o objeto do TV. `rcn4` sempre coordena dois gaps-sujeito e `rcn5` dois gaps-objeto; nenhuma das duas mistura um tipo de gap com o outro. -O problema é que `rcn4`/`rcn5` não são recursivas: cada uma coordena exatamente duas ocorrências. Não é possível gerar "the dwarf that helped Goldilocks and admired the princess that shuddered and laughed" sem acrescentar mais uma regra para RCNs de três coordenadas, depois quatro, e assim por diante — o fragmento não captura a generalização "coordenação de qualquer número de VPs paralelas". -:::: ```lean diff --git a/CSwL/IntroL.lean b/CSwL/IntroL.lean index 38ef735..72858fe 100644 --- a/CSwL/IntroL.lean +++ b/CSwL/IntroL.lean @@ -490,14 +490,7 @@ def kelvinToFahrenheit : Int → Int := celsiusToFahrenheit ∘ kelvinToCelsius tag := "classes" %%% -Vamos definir uma função para contar as ocorrências de um valor de um tipo `α`, em qualquer lista de valores do tipo `α`. Para esta função, nossa única exigência é garantir que poderemos comparar valores do tipo `α`. Essa exigência entra na assinatura entre colchetes, `[BEq α]`, uma instância de igualdade para `α`, que Lean encontra sozinho no ponto de uso. - -Duas noções de igualdade convivem, e vale separá-las desde já: - -* `BEq α` devolve `Bool` e se escreve `==`. -* `DecidableEq α` devolve uma _prova_ de igualdade ou de desigualdade. Permite usar `=` num `if` e usar o resultado numa demonstração. - -Tente remover `[BEq α]` na definição abaixo. +Vamos definir uma função para contar as ocorrências de um valor de um tipo `α`, em qualquer lista de valores do tipo `α`. Para esta função, nossa única exigência é garantir que poderemos comparar valores do tipo `α`. Essa exigência entra na assinatura entre colchetes, `[BEq α]`. Isto significa que uma instância de igualdade para `α` deve estar disponível para o Lean encontrar no ponto de uso. Tente remover `[BEq α]` na definição abaixo, o erro irá aparecer no uso do operador `==`. ```lean def count {α : Type} [BEq α] (x : α) : List α → Nat @@ -515,6 +508,31 @@ deriving instance BEq for Day #eval count Day.friday [.friday, .sunday, .friday, .monday] ``` +Note que para outros tipos, a noção de igualdade pode não ser tão trivial, e exigir uma implementação específica. Por exemplo: + +```lean +structure Angle where + deg : Int +deriving Repr + +def Angle.norm (a : Angle) : Int := + a.deg % 360 + +instance : BEq Angle where + beq a b := a.norm == b.norm + +#eval (⟨-90⟩ : Angle) == ⟨270⟩ +``` + +Em tempo, em Lean, duas noções de igualdade convivem: + +* `BEq α` devolve `Bool` e se escreve `==`. +* `DecidableEq α` devolve uma _prova_ de igualdade ou de desigualdade. Permite usar `=` num `if` e usar o resultado numa demonstração. + +Outra classe relevante em Lean é a classe {name}`Repr` para especificar como valores de um tipo devem ser representados textualmente. Uma instância de {name}`Repr` não produz diretamente uma {name}`String`; ela produz um valor de tipo {name}`Std.Format`, uma representação intermediária que descreve o texto a ser exibido e permite incluir informações sobre indentação e possíveis quebras de linha. Assim, ao definir uma instância de {name}`Repr` para um tipo, estamos essencialmente dizendo ao Lean como representar valores desse tipo, deixando para uma etapa posterior a decisão de como essa representação será efetivamente apresentada. + +Essa separação entre a estrutura a ser impressa e sua apresentação concreta é a ideia central de _pretty printing_. Em vez de decidir antecipadamente onde cada linha deve terminar, construímos um documento que pode ser renderizado de diferentes maneiras conforme o espaço disponível: uma expressão pode aparecer em uma única linha quando couber ou ser distribuída em várias linhas, com indentação apropriada, quando necessário. A abordagem foi sistematizada por Wadler {citep Bib.wadler2003}[] e é usada pelo {name}`Std.Format` do Lean. Para nós, isso é particularmente interessante porque mostra mais um exemplo de como classes e instâncias permitem associar uma operação a um tipo sem modificar sua definição: a estrutura sintática ou semântica permanece a mesma, enquanto sua forma de apresentação é fornecida por uma instância de Repr. + A seguir, vamos customizar a instância de {name}`Day` para a classe {name}`Repr`. Usamos a palavra-chave `instance`. Não precisamos dar nome a instâncias, mas neste caso usamos `insReprDay`. ```lean diff --git a/CSwL/Logic/FOL.lean b/CSwL/Logic/FOL.lean index 5ebd443..a2a19e0 100644 --- a/CSwL/Logic/FOL.lean +++ b/CSwL/Logic/FOL.lean @@ -1,13 +1,15 @@ import CSwLMeta import Bib import Mathlib.Tactic.Use +import CSwL.Logic.PL +import CSwLCompat open Verso.Genre Manual open CSwLMeta set_option verso.code.warnLineLength 100 -#doc (Manual) "Lógica de predicados" => +#doc (Manual) "Lógica de Primeira Ordem" => %%% tag := "FOL" file := "FOL" @@ -22,47 +24,22 @@ namespace FOL tag := "fol-intro" %%% -Se usarmos lógica proposicional para formalizar a frase "Toda maça é vermelha", teremos uma letra proposicional, um átomo indivisível que não nos permitiria capturar a idéia do quantificador e da dependencia declarada entre as _coisas_ que são maças e a cor destas mesmas _coisas_. Lógica de predicados acrescenta os seguintes ingredientes a sintaxe de Lógica Proposicional: +Se usarmos lógica proposicional para formalizar a frase "Toda maçã é vermelha", teremos uma letra proposicional, um átomo indivisível que não nos permitiria capturar a idéia do quantificador e da dependencia declarada entre as _coisas_ que são maçãs e a cor destas mesmas _coisas_. A lógica de predicados, também chamada lógica de primeira ordem (FOL, "first order logic") acrescenta os seguintes ingredientes a sintaxe da lógica proposicional: -* termos para representar indivíduos de um domínio. Os termos poderão ser variáveis ou funções aplicadas sobre termos; -* proposições básicas serão predicados `n`-ários sobre termos; -* fórmulas universalmente quantificadas, `∀` seguido de variável e fórmula; -* fórmulas existencialmente quantificadas, `∃` seguido de variável e fórmula. +* Termos para representar indivíduos de um domínio. Os termos poderão ser variáveis ou funções aplicadas sobre termos; +* Proposições básicas serão predicados `n`-ários sobre termos; +* Fórmulas universalmente quantificadas, `∀` seguido de variável e fórmula; +* Fórmulas existencialmente quantificadas, `∃` seguido de variável e fórmula. -# Sintaxe de Lógica de Primeira Ordem +# Sintaxe de FOL %%% tag := "fol-syntax" %%% -Também chamada de "lógica de primeira ordem" (FOL, "first order logic"). Vamos assumir que predicados terão aridade de 1 até 3 (relações unárias, binárias e ternárias). Relações com mais de três argumentos quase nunca são necessárias para capturar a semântica de linguagem natural. +Nossa sintaxe terá dois elementos principais, *termos* e *fórmulas*. Como fizemos em {ref "pl-syntax"}[pl-syntax], nossa sintaxe será formalizada como tipos indutivos. -A BNF completa segue abaixo e gera fórmulas como `¬P x`, `∀ x R x x` e `∀ x ∃ y R x y`. Note que não podemos aidna construir fórmulas com termos complexos como `∃ x P (f x)`, onde temos a função `f` recebendo uma variável e este termo passado como argumento para o predicado `P`. Nossos termos são apenas variáveis. - -```bnf -v ::= "x" | "y" | "z" | v "'" ; -P ::= "P" | P "'" ; -R ::= "R" | R "'" ; -S ::= "S" | S "'" ; -atom ::= P v | R v v | S v v v ; -F ::= atom - | "(" v "=" v ")" ("identidade") - | "¬" F ("negação") - | "(" F "∧" F ")" ("conjunção") - | "(" F "∨" F ")" ("disjunção") - | "∀" v F ("quantificação universal") - | "∃" v F ("quantificação existencial") ; -``` - -:::dev "Alexandre (arademaker)" -Em Lean, indexar por aridade é mais natural do que empilhar primos: um -`structure PredSymbol` com campos `name : String` e `arity : Nat` já -representa "infinitos predicados de cada aridade finita" sem precisar -de uma família de gramáticas, uma por aridade. Fica como observação, -`Formula` (abaixo) não adota `PredSymbol`. -::: - -Como fizemos em {ref "pl-syntax"}[pl-syntax], vamos agora definir um tipo para representar fórmulas FOL. Uma variável carrega nome e um índice (lista de naturais usada para gerar variáveis "frescas" a partir de uma dada variável): +Os _termos_ podem ser variáveis ou funções aplicadas a outros termos. Uma variável carrega nome e um índice (lista de naturais usada para gerar "novas" variáveis a partir de uma dada variável): ```lean structure Variable where @@ -83,7 +60,36 @@ def y : Variable := ⟨"y", []⟩ def z : Variable := ⟨"z", []⟩ ``` -`Formula α` é parametrizado no tipo dos termos que preenchem os predicados. Por ora nossos termos são apenas `Variable`. +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) + +def Term.format : Term → Std.Format + | .var v => repr v + | .struct name [] => name + | .struct name args => + name ++ "[" ++ + Std.Format.joinSep + (args.map Term.format) "," ++ "]" + +instance : Repr Term := ⟨fun t _ => t.format⟩ + +def tx : Term := .var x +def ty : Term := .var y +def tz : Term := .var z +def tf : Term := .struct "f" [tx, .struct "g" [ty]] +``` + +Constantes podem ser representadas como funções com aridade zero, ou seja, com a lista de argumentos vazia, {lean}`Term.struct "c" []` + +:::dev "Alexandre (arademaker)" +Nothing stopping us for using symbols with inconsistent arity, say `R[x,y]` and `R[x,y,z]` in the same formula. We could define a structure for holding the number and its arity (say `PredSymbol`) and implement a function for checking if a formula is well-formed. +::: + +As *fórmulas* usarão os mesmos conectivos da lógica proposicional, mas acrescentaremos os quantificadores existencial e universal. O nome lógica de primeira ordem vem da idéia de que estamos quantificando sobre indivíduous de um domínio, objetos de primeira ordem. O tipo `Formula α` é parametrizado no tipo dos termos que preenchem os predicados. Se usarmos `Formula Variable` nossos termos são apenas variáveis. Se usarmos `Formula Term` temos nossa sintaxe completa com termos arbitrários. ```lean inductive Formula (α : Type) where @@ -100,7 +106,11 @@ inductive Formula (α : Type) where | exists_ (v : Variable) (f : Formula α) ``` -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, pelo mesmo motivo. O `α` em `atom` não cria esse problema, porque é parâmetro, não o próprio tipo. A notação n-ária se recupera com as funções abaixo. Uma conjunção vazia é `top`, uma disjunção vazia é `bot`, como fizemos em LP. +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. + +Note que o tipo {lean}`Formula` é diferente do tipo {lean}`PL.Formula` definido em {ref "pl-syntax"}[pl-syntax], cada um em seu próprio `namespace`. Mais uma vez, estamos usando Lean como metalinguagem para implementar FOL.. Em tipos dependentes, não fazemos a distinção entre termos e fórmulas. Como vimos em {ref "IntroL"}[IntroL], em Lean toda expressão é um termo e todo termo tem um tipo. Então quando falarmos em termos, ora estamos falando do termo Lean que pode representar uma {lean}`Formula` ou {lean}`Term` de FOL. + +Também como fizemos para {lean}`PL.Formula`, a notação n-ária de {name}`Formula.conj` e {name}`Formula.disj` introduzimos com as funções abaixo. ```lean def Formula.conjs {α : Type} : List (Formula α) → Formula α @@ -114,7 +124,7 @@ def Formula.disjs {α : Type} : List (Formula α) → Formula α | f :: fs => .disj f (Formula.disjs fs) ``` -Um termo 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`. +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`. ```lean def Formula.format {α} [Repr α] : Formula α → Std.Format @@ -128,37 +138,95 @@ def Formula.format {α} [Repr α] : Formula α → Std.Format f!"({f1.format} ==> {f2.format})" | .equi f1 f2 => f!"({f1.format} <=> {f2.format})" - | .top => "true" - | .bot => "false" + | .top => "⊤" + | .bot => "⊥" | .conj f1 f2 => f!"({f1.format} & {f2.format})" | .disj f1 f2 => f!"({f1.format} | {f2.format})" - | .forall_ v f => f!"∀ {repr v} {f.format}" - | .exists_ v f => f!"∃ {repr v} {f.format}" + | .forall_ v f => f!"∀{repr v} {f.format}" + | .exists_ v f => f!"∃{repr v} {f.format}" instance {α} [Repr α] : Repr (Formula α) := ⟨fun f _ => f.format⟩ - ``` -A seguir, `formula1` expressa que o predicado `R` é reflexivo enquanto `formula2` expressa que ele é simétrico. Quando escrevermos `#eval formula1`, Lean irá procurar por esta instância de `Repr` para o tipo `Formula` declarada acima. O {name}`Std.Format` não é uma `String`, é um tipo que representa um documento com quebras de linha e identação. Nossa implementação está bastante simplificada. +A seguir, `R_reflexive` expressa que o predicado `R` é reflexivo enquanto `R_simetric` expressa que ele é simétrico. Note que para estes dois exemplos, não precisamos usar termos envolvendo funções, logo usamos apenas {lean}`Formula Variable`. ```lean -def formula1 : Formula Variable := +def R_reflexive : Formula Variable := .forall_ x (.atom "R" [x, x]) -def formula2 : Formula Variable := +def R_simetric : Formula Variable := .forall_ x (.forall_ y (.impl (.atom "R" [x, y]) (.atom "R" [y, x]))) ``` -Em uma fórmula `∀x F` (ou `∃x F`), o quantificador liga toda ocorrência de -`x` em `F` que não esteja já ligada por um `∀x`/`∃x` interno a `F`. Uma fórmula é *aberta* se tem ao menos uma ocorrência livre de variável, e *fechada* (também chamada *sentença*) caso contrário. Por exemplo, `(P x ∧ ∃x, R x x)` é aberta, o `x` de `P x` está fora do escopo do `∃x`. Mas `∃x (P x ∧ ∃x R x x)` é uma sentença. +Assim como definimos em {ref "pl-syntax"}[pl-syntax], chamamos de uma linguagem de primeira ordem o conjunto de todas as fórmulas que podem ser construídas a partir de um vocabulário de símbolos predicativos e funcionais. + +::::exercise (rating := 2) (name := "ex-fol-translate") +Considere a linguagem de primeira ordem com o vocabulário definido pelos símbolos abaixo. + +- `R(x,y)` - `x` respeita `y` +- `M(x,y)` – `x` esta matriculado na disciplina `y` +- `P(x)` – x é um professor +- `A(x)` – `x` é um aluno +- `D(x)` – `x` é uma disciplina +- `Maria` - uma constante denotando a pessoa chamada Maria. + +Vamos traduzir cada uma das sentenças a seguir para fórmulas em lógica de primeira ordem. + +- (`Fa`) Maria respeita todos os professores. +- (`Fb`) Alguns professores respeitam Maria. +- (`Fc`) Maria respeita a si própria +- (`Fd`) Nenhum aluno esta matriculado em todas as disciplina +- (`Fe`) Não há disciplinas em que todos os alunos estejam nela matriculados +- (`Ff`) Não há disciplinas sem alunos matriculados + +```lean +namespace ExSchool +def R (tx ty : Term) : Formula Term := .atom "R" [tx, ty] +def M (tx ty : Term) : Formula Term := .atom "M" [tx, ty] + +def P (tx : Term) : Formula Term := .atom "P" [tx] +def A (tx : Term) : Formula Term := .atom "A" [tx] +def D (tx : Term) : Formula Term := .atom "D" [tx] + +def Maria : Term := .struct "Maria" [] + +def Fa : Formula Term := + solution!( .forall_ x (.impl (P tx) (R Maria tx)) ) + +def Fb : Formula Term := + solution!( .exists_ x (.conj (P tx) (R tx Maria)) ) + +def Fc : Formula Term := + solution!(R Maria Maria) + +def Fd : Formula Term := + solution!( + .neg (.exists_ x (.conj (A tx) + (.forall_ y (.impl (D ty) (M tx ty))))) ) -Essa distinção é o que motiva a ambiguidade de escopo de "Todo príncipe viu uma dama". Existem duas leituras possíveis. A primeira seria "para cada príncipe existe uma dama (talvez diferente) que ele viu" que podemos formalizar como `∀x (Prince x → ∃y (Lady y ∧ Saw x y))`. A segunda leitura seria "existe uma dama que todo príncipe viu" formalizada como `∃y (Lady y ∧ ∀x (Prince x → Saw x y))`. Repare que a leitura universal usa `→` como conectivo principal dentro da subfórmula, e a existencial usa `∧`. Já "Algum príncipe viu uma dama bonita" admite apenas uma formalização, `∃x∃y (Prince x ∧ Lady y ∧ Beautiful y ∧ Saw x y)`. +def Fe : Formula Term := + solution!( + .neg (.exists_ x (.conj (D tx) + (.forall_ y (.impl (A ty) (M ty tx))))) ) + +def Ff : Formula Term := + solution!( + .neg (.exists_ x (.conj (D tx) + (.neg (.exists_ y (.conj (A ty) (M ty tx)))))) ) + +end ExSchool +``` +:::: + + +Em uma fórmula `∀x F` (ou `∃x F`), o quantificador liga toda ocorrência de +`x` em `F` que não esteja já ligada por um `∀x` (ou `∃x`) interno a `F`. Uma fórmula é *aberta* se tem ao menos uma ocorrência livre de variável, e *fechada* (também chamada *sentença*) caso contrário. Por exemplo, `(P[x] ∧ ∃x, R[x,x])` é aberta, o `x` de `P[x]` está fora do escopo do `∃x`. Mas `∃y (P[y] ∧ ∃x R[x,x])` é uma sentença. -Coletar as variáveis livres de uma fórmula é uma operação recorrente. Definimos uma só vez, deixando como parâmetro a função que extrai as variáveis de um termo — o que muda de um caso para outro é apenas ela. Nos quantificadores, `filter` remove a variável ligada, e remove *todas* as suas ocorrências. +Coletar as variáveis livres de uma fórmula é uma operação recorrente. Abaixo, definimos a função freeVars que recebe como parâmetro uma função que extrai as variáveis de um termo. Para {lean}`R_reflexive`, só precisamos de uma função que transforme uma variável em uma lista com ela mesma. Para fórmulas que podem conter termos complexos, {lean}`Formula Term`, nossa função terá que percorrer todo o termo coletando as variáveis. Nos quantificadores, `filter` preserva apenas as variáveis diferentes da variável que o quantificador introduz. ```lean def Formula.freeVars {α} (vars : α → List Variable) : @@ -176,8 +244,22 @@ def Formula.freeVars {α} (vars : α → List Variable) : | .exists_ v f => (f.freeVars vars).filter (· != v) ``` -::::exercise (rating := 2) (name := "closed-form") -Escreva uma função `closedForm : Formula Variable → Bool` que verifica +:::exercise (rating := 1) (name := "ex-fol-freevars") +Complete o enunciado do exemplo com o termo que torna possível provar o exemplo apenas usando a tática {tactic}`native_decide`. + +```lean +def F : Formula Variable := + .exists_ x + (.conj (.disj (.atom "R" [x, y]) (.atom "S" [x, y, z])) + (.atom "P" [x])) + +example : F.freeVars (fun x => [x]) = solution!([y, y, z]) := + solution!(by native_decide) +``` +::: + +:::exercise (rating := 1) (name := "ex-fol-closedform") +Complete o código da função `closedForm` abaixo que verifica se uma fórmula é fechada. Aqui cada termo é uma variável, então extrair as variáveis de um termo é devolvê-lo numa lista de um elemento. As fórmulas fechadas são as que têm a lista de livres vazia. @@ -186,57 +268,51 @@ elemento. As fórmulas fechadas são as que têm a lista de livres vazia. def closedForm (f : Formula Variable) : Bool := solution!((f.freeVars (fun x => [x])).isEmpty) ``` -:::: +::: -::::exercise (rating := 1) (name := "implication-as-abbrev") -Implicações e equivalências podem ser vistas como abreviações, pois se -definem a partir de negação, conjunção e disjunção — as mesmas -equivalências usadas na lógica proposicional. Escreva uma função -`withoutIDs : Formula Variable → Formula Variable` que substitui cada -fórmula por uma equivalente sem ocorrências de `impl` ou `equi`. +:::exercise (rating := 1) (name := "ex-fol-remove-impl_equiv") +Implicações e equivalências podem ser vistas como abreviações, pois se definem a partir de negação, conjunção e disjunção — as mesmas equivalências usadas na lógica proposicional. Escreva uma função `minimal` que substitui cada fórmula por uma equivalente sem ocorrências de `impl` ou `equi`. Note que a função não depende do tipo `α`. ```lean -def withoutIDs (frm : Formula Variable) : - Formula Variable := +def Formula.minimal {α : Type} (frm : Formula α) : Formula α := solution!( match frm with - | .atom name args => .atom name args + | .atom name as => .atom name as | .eq t1 t2 => .eq t1 t2 | .top => .top | .bot => .bot - | .neg f => .neg (withoutIDs f) + | .neg f => .neg (minimal f) | .impl f1 f2 => - .disj (.neg (withoutIDs f1)) (withoutIDs f2) + .disj (.neg (minimal f1)) (minimal f2) | .equi f1 f2 => - let g1 := withoutIDs f1 - let g2 := withoutIDs f2 + let g1 := minimal f1 + let g2 := minimal f2 .conj (.disj (.neg g1) g2) (.disj (.neg g2) g1) | .conj f1 f2 => - .conj (withoutIDs f1) (withoutIDs f2) + .conj (minimal f1) (minimal f2) | .disj f1 f2 => - .disj (withoutIDs f1) (withoutIDs f2) - | .forall_ v f => .forall_ v (withoutIDs f) - | .exists_ v f => .exists_ v (withoutIDs f)) + .disj (minimal f1) (minimal f2) + | .forall_ v f => .forall_ v (minimal f) + | .exists_ v f => .exists_ v (minimal f)) ``` -:::: +::: -::::exercise (rating := 2) (name := "negation-normal-form") +:::exercise (rating := 2) (name := "ex-fol-nnf") Toda fórmula de lógica de predicados pode ser transformada em uma equivalente na *forma normal da negação* (NNF, "negation normal form"), onde negações só ocorrem diante de átomos. A receita é "empurrar" as negações através dos quantificadores por `¬ ∀x F ≡ ∃x ¬F` e `¬ ∃x F ≡ ∀x ¬F`, e através de disjunções e conjunções pelas leis de De Morgan: `¬(F1 ∧ F2) ≡ ¬F1 ∨ ¬F2` e `¬(F1 ∨ F2) ≡ ¬F1 ∧ ¬F2`. Finalmente, `¬¬F ≡ F` elimina dupla negação. Complete o código da função `nnf`. -Dica: a receita acima diz o que fazer com `¬` diante de alguma subfórmula. Isso sugere duas funções, uma para cada situação em que uma subfórmula pode aparecer. As duas se chamam mutuamente, e por isso vão num bloco `mutual`. +Dica: a receita acima diz o que fazer com a negação diante de alguma subfórmula. Isso sugere duas funções, uma para cada situação em que uma subfórmula pode aparecer. As duas se chamam mutuamente, e por isso vão num bloco `mutual`. - `nnfPos f` devolve a NNF de `f`; - `nnfNeg f` devolve a NNF de `¬f`. -Trate `impl` e `equi` diretamente nas duas funções, sem passar por -`withoutIDs`. +Trate `impl` e `equi` diretamente nas duas funções, sem passar por {name}`Formula.minimal`. E novamente, observe que a função não depende do tipo `α`. ```lean mutual -def nnfPos (frm : Formula Variable) : Formula Variable := +def nnfPos {α} (frm : Formula α) : Formula α := solution!( match frm with - | .atom n a => .atom n a + | .atom n as => .atom n as | .eq t1 t2 => .eq t1 t2 | .top => .top | .bot => .bot @@ -250,10 +326,10 @@ def nnfPos (frm : Formula Variable) : Formula Variable := | .forall_ v f => .forall_ v (nnfPos f) | .exists_ v f => .exists_ v (nnfPos f)) -def nnfNeg (frm : Formula Variable) : Formula Variable := +def nnfNeg {α} (frm : Formula α) : Formula α := solution!( match frm with - | .atom n a => .neg (.atom n a) + | .atom n as => .neg (.atom n as) | .eq t1 t2 => .neg (.eq t1 t2) | .top => .bot | .bot => .top @@ -268,40 +344,16 @@ def nnfNeg (frm : Formula Variable) : Formula Variable := | .exists_ v f => .forall_ v (nnfNeg f)) end -def Formula.nnf (f : Formula Variable) : Formula Variable := +def Formula.nnf {α : Type} (f : Formula α) : Formula α := solution!(nnfPos f) ``` -:::: - -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) - -def Term.format : Term → Std.Format - | .var v => repr v - | .struct name [] => name - | .struct name args => - name ++ "[" ++ - Std.Format.joinSep - (args.map Term.format) "," ++ "]" - -instance : Repr Term := ⟨fun t _ => t.format⟩ - -def tx : Term := .var x -def ty : Term := .var y -def tz : Term := .var z -``` - -Um termo `t` é *livre para* a variável `v` na fórmula `F` se toda ocorrência livre de `v` em `F` pode ser substituída por `t` sem que nenhuma das variáveis de `t` fique ligada. Por exemplo, `y` é livre para `x` em `Px → ∀x Px`, mas o mesmo termo não é livre para `x` em `∀y Rxy → ∀x Rxx`. Da mesma forma, `g(x,y)` não é livre para `x` em `∀y Rxy → ∀x Rxx`. +::: -Um termo livre para uma variável `v` pode ser substituído nas ocorrências livres de `v` sem uma mudança não intencional de significado. Considere a fórmula aberta `∀y Rxy → ∀x Rxx`. Se substituirmos a ocorrência livre de `x` nessa fórmula por `y`, obtemos uma fórmula fechada `∀y Ryy → ∀x Rxx`. Uma variável que originalmente era livre acabou capturada. +Um termo `t` é *livre para* a variável `v` na fórmula `F` se toda ocorrência livre de `v` em `F` pode ser substituída por `t` sem que nenhuma das variáveis de `t` fique ligada. Por exemplo, `y` é livre para `x` em `P[x] → ∀x P[x]`, mas o mesmo termo não é livre para `x` em `∀y R[x,y] → ∀x R[x,x]`. Da mesma forma, `g[x,y]` não é livre para `x` em `∀y R[x,y] → ∀x R[x,x]`. -Se `t` não é livre para `v` em `F`, podemos sempre renomear as variáveis ligadas de `F` para garantir que a substituição de `t` por `v` em `F` tenha o significado correto. Embora `g(y,c)` não seja livre para `x` em `∀y Rxy → ∀x Rxx`, o termo é livre para `x` em `∀z Rxz → ∀x Rxx`, que é uma chamada *variante alfabética* da fórmula original. Uma variante alfabética de uma fórmula é uma fórmula que difere da original apenas por usar variáveis ligadas diferentes. +Um termo livre para uma variável `v` pode ser substituído nas ocorrências livres de `v` sem uma mudança não intencional de significado. Considere a fórmula aberta `∀y R[x,y] → ∀x R[x,x]`. Se substituirmos a ocorrência livre de `x` nessa fórmula por `y`, obtemos uma fórmula fechada `∀y R[y,y] → ∀x R[x,x]`, uma variável acabou capturada. Se `t` não é livre para `v` em `F`, podemos sempre renomear as variáveis ligadas de `F` para garantir que a substituição de `t` por `v` em `F` tenha o significado correto. Embora `g[y,c]` não seja livre para `x` em `∀y R[x,y] → ∀x R[x,x]`, o termo é livre para `x` em `∀z R[x,z] → ∀x R[x,x]`, que é uma chamada *variante alfabética* (nomes diferentes para as variáveis ligadas) da fórmula original. -A função `isVar` verifica se um termo é uma variável. As funções `varsInTerm` e `varsInTerms` retornam as variáveis que ocorrem num termo ou numa lista de termos sem duplicatas. +A função `isVar` verifica se um termo é uma variável. As funções `varsInTerm` e `varsInTerms` retornam a lista das variáveis que ocorrem num termo ou em uma lista de termos, sem duplicatas. ```lean def isVar : Term → Bool @@ -315,19 +367,11 @@ def varsInTerm : Term → List Variable def varsInTerms (ts : List Term) : List Variable := ts.map varsInTerm |>.flatten |>.eraseDups - end ``` -Agora que temos o tipo `Term` podemos usar `Formula Term` ao invés de `Formula Variable`. - -::::exercise (rating := 1) (name := "vars-in-formula") - -Implemente uma função `varsInForm : Formula Term → List Variable` que -dá a lista de variáveis que ocorrem numa fórmula. Aqui não se trata de -ocorrências *livres*: conte todas, inclusive a variável que cada -quantificador liga. Mantenha a lista sem duplicatas, como fazem -`varsInTerm` e `varsInTerms`. +::::exercise (rating := 2) (name := "ex-fol-vars-in-formula") +Implemente a função `varsInForm` que retorna a lista de todas as variáveis que ocorrem em uma fórmula. Retorne a lista sem duplicatas, como em `varsInTerm` e `varsInTerms`. ```lean def Formula.varsInForm (frm : Formula Term) : List Variable := @@ -349,9 +393,9 @@ def Formula.varsInForm (frm : Formula Term) : List Variable := ``` :::: -::::exercise (rating := 2) (name := "free-vars-in-formula") -Implemente `freeVarsInForm : Formula Term → List Variable`, que dá a -lista de variáveis com ocorrências livres numa fórmula. + +::::exercise (rating := 1) (name := "ex-fol-free-vars-in-form") +Complete a definição de `freeVarsInForm`, que retorna a lista de variáveis com ocorrências livres em uma fórmula que contenha termos além de variáveis. ```lean def Formula.freeVarsInForm (f : Formula Term) : List Variable := @@ -360,8 +404,8 @@ def Formula.freeVarsInForm (f : Formula Term) : List Variable := :::: -::::exercise (rating := 2) (name := "open-form") -Usando a função `freeVarsInForm`, complete a função `openForm`, que verifica se uma fórmula é aberta. Reaproveite as funções anteriores. +::::exercise (rating := 1) (name := "ex-fol-open-form") +Complete a função `openForm`, que verifica se uma fórmula é aberta. Reaproveite as funções anteriores. ```lean def openForm (f : Formula Term) : Bool := @@ -370,373 +414,402 @@ def openForm (f : Formula Term) : Bool := :::: -# Semântica da lógica de predicados +# Semântica de FOL %%% tag := "fol-semantics" %%% -Por conveniência, nos limitamos a um fragmento de língua com apenas três letras de predicado: `P` (unário), `R` (binário), e `S` (ternário). +Em {ref "PL"}[PL], uma função de atribuição de valor de verdade para os símbolos proposicionais nos permite determinar o valor de verdade de uma fórmula. Em FOL, uma interpretação de um vocabulário é uma estrutura que atribui significado aos símbolos do vocabulário. -Como deve ser uma estrutura extralinguística para as constantes `P`, `R` e `S`? Tal estrutura deve conter ao menos um domínio de discurso `D`, formado por entidades individuais, com uma interpretação para `P`, para `R` e para `S`. Essas interpretações são dadas por uma função `Interp`, que a cada nome de predicado e a cada lista de elementos do domínio associa um valor de verdade. +Uma estrutura `𝔸` é como um dicionário para traduzir a linguagem de primeira ordem `L`. Uma estrutura nos dirá sobre qual coleção de coisas os símbolos `∀` e `∃` quantificam, isto é, o conjunto `D`. A estrutura também associa os símbolos predicativos de `L` a relações no domínio e os símbolos funcionais a funções no domínio. Formalmente, a estrutura é o par, domínio e interpretação. + +Mas nossos termos podem ser conter variáveis então também precisamos interpretar variávei em elementos do domínio. O tipo `Assign` mapea variávies em elementos do domínio. A função `Assign.update` atualiza um mapeamento de variáveis em elementos do domínio associando a variável `v` e um novo elemento `d`, normalmente escrevemos `g[v := d]` para representar esta idéia de que `g` ```lean -abbrev Interp (D : Type) := String → List D → Bool -``` +def Assign (D : Type) := Variable → D -Um conjunto de símbolos de relação, com suas aridades, especifica uma linguagem -de lógica de predicados `L`. Uma estrutura `M = (D, I)`, formada por um domínio -não vazio `D` com uma função de interpretação para os símbolos de relação de `L`, -é chamada de *modelo* para `L`. Sempre suporemos que o domínio de um modelo é não -vazio. +def Assign.update {D : Type} + (g : Assign D) (v : Variable) (d : D) : Assign D := + fun w => if w = v then d else g w +``` -Eis um modelo concreto: dez entidades de contos de fadas, nomeadas por letras. -Nada aqui depende da escolha das letras — o que importa é que o domínio seja -finito e que cada predicado diga, de cada entidade, se vale ou não. +A idéia é demostrada nos exemplos a seguir. Em um domínio dos naturais, a partir de um mapeamento inicial onde qualquer variável é mapeada no `0`, podemos atualizar indicando que se a variável `x` for passada, ela deve agora estar associada ao valor `1`. ```lean -inductive Entity where - | A | B | D | E | G | M | R | S | T | Y -deriving Repr, DecidableEq, BEq +def g0 : Assign Nat := λ x ↦ 0 +def g1 : Assign Nat := g0.update x 1 -def entities : List Entity := - [.A, .B, .D, .E, .G, .M, .R, .S, .T, .Y] +#eval [g0 x, g0 y, g1 x, g1 y] ``` -`S` é Branca de Neve, `A` é Alice, `D` é Dorothy, `G` é Cachinhos Dourados, -`M` é o Pequeno Mook, `Y` é Atreyu, `E` é a princesa, `B` e `R` são os anões, -e `T` é o gigante. - -Os predicados unários são a pertinência a uma lista, exatamente como no -original. Os binários se dão por enumeração dos pares, ou por uma regra. +Definido o mapeamento de variáveis, definimos agora o tipo `FInterp` para a interpretação de termos em elementos de um domínio `D`. ```lean -def girl : Entity → Bool := ([Entity.S, .A, .D, .G].contains ·) -def boy : Entity → Bool := ([Entity.M, .Y].contains ·) -def princess : Entity → Bool := ([Entity.E].contains ·) -def dwarf : Entity → Bool := ([Entity.B, .R].contains ·) -def giant : Entity → Bool := ([Entity.T].contains ·) -def child : Entity → Bool := fun x => girl x || boy x - -def love (x y : Entity) : Bool := - [(.Y, .E), (.B, .S), (.R, .S)].contains (x, y) - -def defeat (x y : Entity) : Bool := - dwarf x && giant y +abbrev FInterp (D : Type) := String → List D → D ``` -A função de interpretação amarra os nomes de predicado ao modelo. Nomes fora -da lista, ou usados com o número errado de argumentos, recebem `false`. +A partir de {lean}`FInterp`, definimos a interpretação de um termo na função `liftAssign`, recursiva sobre a estrutura do termo. Nossa recursão é parecida com {name}`varsInTerm`, avaliando cada argumento e combinando os resultados para interpretar os símbolos funcionais. Note que `fint name` tem tipo `List D → D` e `(args.map (liftAssign fint g))` irá retornar um termo do tipo `List D`. ```lean -def int0 : Interp Entity - | "Girl", [x] => girl x - | "Boy", [x] => boy x - | "Princess", [x] => princess x - | "Dwarf", [x] => dwarf x - | "Giant", [x] => giant x - | "Child", [x] => child x - | "Love", [x, y] => love x y - | "Defeat", [x, y] => defeat x y - | _, _ => false +def liftAssign {D : Type} (fint : FInterp D) (g : Assign D) : Term → D + | .var v => g v + | .struct name args => fint name (args.map (liftAssign fint g)) ``` -Dada uma estrutura com função de interpretação `M = (D, I)`, podemos definir uma -valoração para as fórmulas da lógica de predicados, desde que saibamos lidar com -os valores das variáveis individuais. Seja `V` o conjunto das variáveis da -linguagem. Uma função `g : V → D` é chamada de *atribuição de variáveis*, ou -valoração. +Agora podemos definir quando uma fórmula `α` é verdadeira em uma estrutura `𝔸`. Vamos usar a notação `𝔸 ⊧ α [g]` ou `⊧ α [𝔸,g]` para indicar que esta relação de consequência depende da interpretação dos símbolos em `α` dada por `𝔸` e da atribuição de variáveis a elementos do domínio dada por `g`. A segunda notação é mais precisa, preservando a idéia de que consequência lógica é uma relação entre fórmulas `β ⊧ α` ou entre uma listas de fórmulas e uma fórmula `Δ ⊧ α`. -Escrevemos `g[v := d]` para a valoração que é como `g` exceto pelo fato de que -`v` recebe o valor `d` — onde `g` poderia ter atribuído um valor diferente. +O tipo `Interp` define o que é a interpretação de símbolos predicativos e seus argumentos para um valor boleano. ```lean -def Assign (D : Type) := Variable → D - -def Assign.update {D : Type} (g : Assign D) - (v : Variable) (d : D) : Assign D := - fun w => if w = v then d else g w +abbrev Interp (D : Type) := String → List D → Bool ``` -Seja `M` um modelo para a linguagem `L`, seja `g` uma atribuição de variáveis -para `L` em `M`, e seja `F` uma fórmula de `L`. Estamos prontos para definir a -noção `M ⊨ᵍ F`, "F é verdadeira em M sob a atribuição g", ou: "g satisfaz F no -modelo M". +Em seguida definimos como avaliar fórmulas. Como em {ref "PL"}[lógica proposicional], a definição calcula o resultado `Bool`. As cláusulas dos quantificadores são as que alteram a atribuição de valores à variáveis. `∀v F` vale quando `F` vale para toda escolha de valor de `v`, e `∃v F` quando vale para ao menos uma. -O que segue é uma definição recursiva de verdade para as fórmulas da lógica de -predicados. Como em {ref "PL"}[lógica proposicional], a definição *calcula*: o -resultado é um `Bool`, e o valor de uma fórmula pode ser obtido com `#eval`. As -cláusulas dos quantificadores são as que fazem a atribuição mudar: `∀v F` vale -quando `F` vale para toda escolha de valor de `v`, e `∃v F` quando vale para ao -menos uma. +Aqui aparece a diferença em relação à lógica proposicional. Em nossa implementação, para avaliar uma fórmula com quantificador é preciso percorrer o domínio, e percorrer exige que o domínio seja enumerável e finito. Por isso `eval` recebe um argumento a mais, `dom`, e usa `List.all` e `List.any`, versões computáveis de `∀` e `∃`. Em FOL, domínios não precisam ser finitos, mas não existe processo de decisão para avaliação de fórmulas em domínios infinitos e não enumeráveis. -Aqui aparece a diferença em relação à lógica proposicional. Para decidir um -quantificador é preciso percorrer o domínio, e percorrer exige que o domínio -esteja disponível como uma lista. Por isso `eval` recebe um argumento a mais, -`dom`, e usa `List.all` e `List.any` — as versões computáveis de `∀` e `∃`. +Uma fórmula `Formula α` tem termos do tipo `α`, que pode ser `Variable` ou `Term`. Quando os termos são apenas variáveis, basta consultar `g`; quando forem termos estruturados, será necessário promover, com `liftAssign`, um mapeamento de variáveis no domínio para um mapemanto de termos no domínio. Em vez de escrever duas funções de avaliação, passamos essa tarefa como um parâmetro `tval`, do mesmo modo que {name}`Formula.freeVars` recebeu a função que extrai as variáveis de um termo. ```lean -def Formula.eval {D : Type} [DecidableEq D] +def Formula.eval {D α : Type} [DecidableEq D] + (f : Formula α) (dom : List D) (I : Interp D) - (g : Assign D) : Formula Variable → Bool - | .atom name args => I name (args.map g) - | .eq t1 t2 => g t1 == g t2 + (g : Assign D) (tval : Assign D → α → D) : Bool := + match f with + | .atom name args => I name (args.map (tval g)) + | .eq t1 t2 => tval g t1 == tval g t2 | .top => true | .bot => false - | .neg f => !(Formula.eval dom I g f) + | .neg f => !(f.eval dom I g tval) | .impl f1 f2 => - !(Formula.eval dom I g f1) || Formula.eval dom I g f2 + !(f1.eval dom I g tval) || f2.eval dom I g tval | .equi f1 f2 => - Formula.eval dom I g f1 == Formula.eval dom I g f2 + f1.eval dom I g tval == f2.eval dom I g tval | .conj f1 f2 => - Formula.eval dom I g f1 && Formula.eval dom I g f2 + f1.eval dom I g tval && f2.eval dom I g tval | .disj f1 f2 => - Formula.eval dom I g f1 || Formula.eval dom I g f2 + f1.eval dom I g tval || f2.eval dom I g tval | .forall_ v f => - dom.all fun d => Formula.eval dom I (g.update v d) f + dom.all fun d => f.eval dom I (g.update v d) tval | .exists_ v f => - dom.any fun d => Formula.eval dom I (g.update v d) f + dom.any fun d => f.eval dom I (g.update v d) tval ``` -Um caso por construtor, e cada caso troca o construtor pela operação -correspondente sobre `Bool`. Se avaliamos fórmulas fechadas, isto é, sem -variáveis livres, a atribuição `g` se torna irrelevante — mas ainda é preciso -fornecer alguma. +Para `Formula Variable`, a interpretação de `Variable` é a própria `g`. ```lean -def g0 : Assign Entity := fun _ => .S +def varVal {D : Type} (g : Assign D) (v : Variable) : D := g v +``` + +Vamos considerar uma linguagem FOL, tomado de {citep Bib.enderton2001}[], com um único símbolo predicado binário, `E`. Chamaremos esta linguagem de `L₁`. Uma estrutura para `L₁` deve conter um domínio de discurso `D`, formado por entidades e uma interpretação para `E`. O domínio tem quatro objetos, e uma única relação binária para interpretar o símbolo `E` da linguagem `L₁`. -def someDwarfDefeatsSomeGiant : Formula Variable := - .exists_ x (.conj (.atom "Dwarf" [x]) - (.exists_ y (.conj (.atom "Giant" [y]) - (.atom "Defeat" [x, y])))) +```lean +inductive Vertex where + | a | b | c | d +deriving Repr, DecidableEq + +def edge : Vertex → Vertex → Bool + | .a, .b => true + | .b, .a => true + | .b, .c => true + | .c, .c => true + | _, _ => false +``` -def everyChildIsGirlOrBoy : Formula Variable := - .forall_ x (.impl (.atom "Child" [x]) - (.disj (.atom "Girl" [x]) (.atom "Boy" [x]))) +O tipo indutivo {name}`Vertex` determinar quais são os objetos do nosso domínio. Para avaliar uma fórmula quantificada, porém, será preciso percorrer o domínio, e para isso ele tem de estar disponível em uma coleção que possa ser percorrida, vamos usar uma lista. Então o tipo indutivo declara o domínio, a lista o exibe na ordem em que será percorrido. -def everyDwarfLovesAPrincess : Formula Variable := - .forall_ x (.impl (.atom "Dwarf" [x]) - (.exists_ y (.conj (.atom "Princess" [y]) - (.atom "Love" [x, y])))) +```lean +def vertices : List Vertex := [.a, .b, .c, .d] -#eval (Formula.eval entities int0 g0 someDwarfDefeatsSomeGiant, - Formula.eval entities int0 g0 everyChildIsGirlOrBoy, - Formula.eval entities int0 g0 everyDwarfLovesAPrincess) +theorem mem_vertices (v : Vertex) : v ∈ vertices := by + cases v <;> decide ``` -A terceira é falsa no modelo: os anões `B` e `R` amam `S`, que é Branca de -Neve, e Branca de Neve não é a princesa. Quem ama a princesa é `Y`, que não é -anão. +O teorema {name}`mem_vertices` nos garante que na lista estão todos os elementos do tipo `Vertex`. A tática `decide` é combinada com `cases v`, que abre um caso por construtor, ela verifica os quatro casos um a um. + +Um domínio com um só predicado binário pode ser visto como um grafo direcionado: os objetos são os vértices, e `E x y` vale quando há uma aresta de `x` para `y`. -A definição de verdade faz uso essencial das atribuições e, ainda assim, nos -exercícios em que se olha apenas para fórmulas fechadas, a verdade ou a falsidade -não depende de qual atribuição se use. Poder-se-ia pensar, portanto, que é -possível dispensar as atribuições por completo, contanto que nos limitemos a -definir os valores de verdade das fórmulas fechadas da lógica de predicados. +:::diagramWithAlt +```diagram (cssWidth := "22em") (texWidth := "16em") +CSwLMeta.Diagrams.edgeGraph +``` -O problema é que, ao aplicar a definição de verdade acima a uma sentença, por -exemplo a `∀x(Px → ∃yRxy)`, a cláusula que trata do quantificador universal faz -referência à noção de verdade para a fórmula `(Px → ∃yRxy)`, que é uma fórmula -aberta. Para determinar se ela é verdadeira temos de saber que objeto `x` denota. -A situação é inteiramente análoga à interpretação de sentenças de língua natural: +``` + ┌───┐ + │ ↓ + a ⇄ b ──→ c ──┘ d +O grafo tem quatro vértices: a, b, c e d. Há uma aresta de a para b e outra de b para a. Há uma aresta de b para c, e um laço de c para si mesmo. O vértice d está isolado: dele não sai aresta alguma, e nenhuma chega nele. ``` -Todo mestre tem um aprendiz. -Ele tem um aprendiz. +::: + +A seguir `intB` interpreta o predicado de `E` à relação no modelo {name}`edge`. + +```lean +def intB : Interp Vertex + | "E", [x, y] => edge x y + | _, _ => false ``` -Para determinar a verdade da segunda temos de saber quem é o referente do pronome -_ele_. +Uma importante observação é que nomes fora da lista, ou usados com o número errado de argumentos, recebem {lean}`false`. Isto quer dizer que fórmulas mal formadas, como por exemplo `∃ x E[x]` com o predicado `E` sendo usado com um único argumento, serão silenciosamente avaliadas como {lean}`false`. + +Finalmente podemos declarar algumas fórmulas para avaliarmos em nossa estrutura. -Uma sentença da lógica de predicados é *logicamente válida* se é verdadeira em -todo modelo; a notação é `⊨ F`. Da convenção de que os domínios de nossos modelos -são sempre não vazios segue que `⊨ ∀xF → ∃xF`, para toda `F` com no máximo a -variável `x` livre. +```lean +def E (s t : Variable) : Formula Variable := + .atom "E" [s, t] -Uma sentença `C` *se segue logicamente* de uma sentença `P` (`P` de premissa, `C` -de conclusão; dizemos também que `P` implica logicamente `C`) se todo modelo que -torna `P` verdadeira também torna `C` verdadeira. A notação é `P ⊨ C`. +def someVertexUnreached : Formula Variable := + .exists_ x (.forall_ y (.neg (E y x))) -Como julgar afirmações da forma `P ⊨ C`? É claro como podemos refutá-la: achando -um contraexemplo. Um contraexemplo a `P ⊨ C` é um modelo `M` com `M ⊨ P` mas não -`M ⊨ C`. +def everyVertexHasSuccessor : Formula Variable := + .forall_ x (.exists_ y (E x y)) -::::exercise (rating := 2) (name := "quantifier-strength") +def someVertexLoops : Formula Variable := + .exists_ x (E x x) -Mostre que `∀x(Ax ∧ Bx)` significa algo mais forte que "todo A é B", e que -`∃x(Ax → Bx)` significa algo mais fraco que "algum A é B". +def edgeIsSymmetric : Formula Variable := + .forall_ x (.forall_ y (.impl (E x y) (E y x))) +``` -:::solution -`∀x(Ax ∧ Bx)` diz que tudo no domínio é A e é B — não apenas que os A são B. Ela -é falsa em qualquer modelo que tenha um objeto fora de A, mesmo que todos os A -sejam B. A tradução correta de "todo A é B" é `∀x(Ax → Bx)`. +A primeira é a sentença corresponde a afirmação de que existe um vértice para o qual nenhuma aresta aponta. É verdadeira, e a testemunha é o nó `d`. A segunda é falsa pelo mesmo motivo, de `d` não sai aresta alguma. A terceira é verdadeira por causa do laço em `c`. A quarta é falsa: há aresta de `b` para `c`, mas não de `c` para `b`. Vale notar como a primeira soa em língua natural mais complicada do que a versão simbólica. -`∃x(Ax → Bx)` é verdadeira assim que houver um objeto que não seja A, porque a -implicação vale vacuamente para ele. Ela não afirma que existe um A que é B; a -tradução correta de "algum A é B" é `∃x(Ax ∧ Bx)`. -::: +Quando avaliamos fórmulas fechadas, sem variáveis livres, a atribuição `g` é irrelevante, mas ainda é preciso fornecer alguma para {name}`Formula.eval`. -:::: +```lean +def g : Assign Vertex := + fun _ => .a + +#eval (someVertexUnreached.eval vertices intB g varVal, + everyVertexHasSuccessor.eval vertices intB g varVal, + someVertexLoops.eval vertices intB g varVal, + edgeIsSymmetric.eval vertices intB g varVal) +``` -::::exercise (rating := 2) (name := "translate-quantified") - -Traduza as sentenças a seguir para lógica de predicados, garantindo que as -condições de verdade sejam capturadas. - -1. _Someone walks and someone talks._ -2. _No wizard cast a spell or mixed a potion._ -3. _Every ballad that is sung by a princess is beautiful._ -4. _If a knight finds a dragon, he fights it._ - -```lean -def someoneWalksAndTalks : Formula Variable := - solution!(.conj - (.exists_ x (.atom "Walk" [x])) - (.exists_ y (.atom "Talk" [y]))) - -def noWizardCastOrMixed : Formula Variable := - solution!(.forall_ x - (.impl (.atom "Wizard" [x]) - (.neg (.disj (.atom "CastSpell" [x]) - (.atom "MixedPotion" [x]))))) - -def everyBalladBeautiful : Formula Variable := - solution!(.forall_ x - (.impl - (.conj (.atom "Ballad" [x]) - (.exists_ y (.conj (.atom "Princess" [y]) - (.atom "Sung" [y, x])))) - (.atom "Beautiful" [x]))) - -def knightFightsDragon : Formula Variable := - solution!(.forall_ x (.forall_ y - (.impl - (.conj (.atom "Knight" [x]) - (.conj (.atom "Dragon" [y]) - (.atom "Finds" [x, y]))) - (.atom "Fights" [x, y])))) -``` - -A fórmula é uma proposta; a verificação de que ela afirma o que se queria fica -para a seção seguinte, que dá o meio de enunciar a condição de verdade -pretendida com os quantificadores do próprio Lean e exigir que as duas -coincidam. - -:::solution -As duas primeiras são diretas, mas repare no escopo da negação em (2): _no -wizard cast a spell or mixed a potion_ nega a disjunção inteira, não cada -disjunto separadamente. Escrever `∀x(Wizard x → (¬CastSpell x ∨ ¬MixedPotion -x))` afirmaria algo mais fraco — que nenhum mago fez as duas coisas. - -A terceira mostra por que a cláusula relativa entra como conjunto na -antecedente: _every ballad that is sung by a princess_ restringe o domínio da -quantificação, e a restrição é `Ballad x ∧ ∃y(Princess y ∧ Sung y x)`. - -A quarta é a mais instrutiva. Os artigos indefinidos de _a knight_ e _a dragon_ -parecem pedir `∃`, mas dentro do antecedente de uma condicional eles ganham -força universal: a sentença diz que *todo* par cavaleiro-dragão que se encontra -luta. Traduzir com `∃` daria `∃x∃y(Knight x ∧ Dragon y ∧ Finds x y → Fights x -y)`, que é quase trivialmente verdadeira — basta haver um par que não se -encontra. E os pronomes _he_ e _it_ retomam justamente as variáveis ligadas -pelos quantificadores, que é o que permite a tradução funcionar. +A seguir, vamos usar o tipo {lean}`Fin` que constrói um tipo dos números naturais menores que um limite superior. O {lean}`Fin 2` corresponde aos naturais menores que `2`. Quando escrevemos {lean}`(1 : Fin 2)`, a instância {lean}`OfNat (Fin 2) 1` normaliza o literal armazenando o resto da divisão {lean}`1 % 2`. + +```lean +example : (3 : Fin 2) = 1 := rfl +example : ⟨0, by omega⟩ = (0 : Fin 2) := rfl +example : Fin.mk 0 (by omega) = (0 : Fin 2) := rfl +``` + +Usando o construtor `Fin.mk n` (ou o construtor anônimo `⟨...⟩`), temos que passar uma prova de que o número informado é menor que o limite do tipo. Não conseguimos abaixo construir uma prova de que `3 < 2`. + +```lean +error +example : ⟨3, by omega⟩ = (3 : Fin 2) := rfl +``` + +:::exercise (rating := 1) (name := "ex-fol-model") +Complete a definição das interpretações `int₁` e `int₂` que permitam os exemplos serem provados com a tática {tactic}`native_decide`. Note que nosso domínio contém apenas 3 valores, isto não deve ser alterado. + +```lean +namespace ExModel + +abbrev Values := Fin 3 +def dom : List Values := [0, 1, 2] + +def int₁ (name : String) (as : List Values) : Bool := + solution!( + match name, as with + | "P", [x] => [1].contains x + | "R", [x,y] => [(0,0),(1,0)].contains (x,y) + | _ , _ => false) + +def int₂ (name : String) (as : List Values) : Bool := + solution!( + match name, as with + | "P", [x] => [0,1].contains x + | "R", [x,y] => [(0,0),(1,0)].contains (x,y) + | _ , _ => false) + +def P (x : Variable) : Formula Variable := + .atom "P" [x] + +def R (x y : Variable) : Formula Variable := + .atom "R" [x, y] + +def α₁ : Formula Variable := + .exists_ x (.conj (P x) (R x x)) + +def α₂ : Formula Variable := + .forall_ x (.impl (P x) (.exists_ y (R x y))) + +def α₃ : Formula Variable := + .forall_ x (.impl (.exists_ y (R y x)) (R x x)) + +def g0 : Assign Values := + fun _ => 0 + +example : α₁.eval dom int₁ g0 varVal = false := + solution!(by native_decide) + +example : α₂.eval dom int₂ g0 varVal := + solution!(by native_decide) + +example : α₃.eval dom int₁ g0 varVal := + solution!(by native_decide) + +end ExModel +``` ::: -:::: +:::exercise (rating := 2) (name := "ex-fol-weak-strong") +Neste exercício, queremos mostrar que: -::::exercise (rating := 2) (name := "valid-consequence") +1. `∀ x, Ax ∧ Bx` significa algo mais forte que `∀ x, Ax → Bx` (todo A é B). +2. `∃ x, Ax → Bx` é mais fraco que `∃ x, Ax ∧ Bx` (alguns A são B). -Quais das afirmações seguintes valem? Se uma vale, explique por quê; se não, -dê um contraexemplo. +Para confirmar (1), complete a definição de `int₁` construíndo uma interpretação onde `∀ x, Ax → Bx` é verdadeira mas `∀ x, Ax ∧ Bx` é falsa. Isto é, seja `M = (dom, int₁)` é um modelo que não satisfaz a restrição mais forte `∀ x, Ax ∧ Bx`. Para confirmar (2), complete `int₂` com uma interpretação onde `∃ x, Ax → Bx` é verdadeira mas `∃ x, Ax ∧ Bx` é falsa. -1. `∀xPx ⊨ ∃xPx` -2. `∃x∃yRxy ⊨ ∃xRxx` -3. `∃y∀xRxy ⊨ ∀x∃yRxy` +Todos os exemplos deverão ser provados apenas com a tática {tactic}`native_decide`. Note que nosso domínio é definido sobre os únicos dois possíveis valore de {lean}`Fin 2` e isso não deve ser alterado. -:::solution -1. Vale, e é aqui que a exigência de domínio não vazio faz trabalho: tomando - qualquer `d` do domínio, de `∀xPx` sai `Pd`, que testemunha `∃xPx`. Num - domínio vazio a premissa seria vacuamente verdadeira e a conclusão falsa. -2. Não vale. Contraexemplo: domínio `{1, 2}` com `R` valendo apenas de `1` para - `2`. A premissa é verdadeira, e nenhum objeto se relaciona consigo mesmo. -3. Vale. Se há um `d` tal que todo `x` se relaciona com `d`, então para cada `x` - esse mesmo `d` testemunha `∃yRxy`. +```lean +namespace ExWeakStrong + +abbrev Values := Fin 2 +def dom : List Values := [0, 1] + +def int₁ (name : String) (as : List Values) : Bool := + solution!( + match name, as with + | "A", [x] => [0].contains x + | "B", [x] => [0, 1].contains x + | _ , _ => false) + +def int₂ (name : String) (as : List Values) : Bool := + solution!( + match name, as with + | "A", [x] => false + | "B", [x] => [1].contains x + | _ , _ => false) + +-- All x are A and B +def F₁ : Formula Variable := + .forall_ x (.conj (.atom "A" [x]) (.atom "B" [x])) + +-- All A are B +def F₂ : Formula Variable := + .forall_ x (.impl (.atom "A" [x]) (.atom "B" [x])) + +-- There is x such that, if x is A, then x is B +def F₃ : Formula Variable := + .exists_ x (.impl (.atom "A" [x]) (.atom "B" [x])) + +-- Some A are B +def F₄ : Formula Variable := + .exists_ x (.conj (.atom "A" [x]) (.atom "B" [x])) + +def g0 : Assign Values := + fun _ => 0 + +example : F₁.eval dom int₁ g0 varVal = false := + solution!(by native_decide) + +example : F₂.eval dom int₁ g0 varVal := + solution!(by native_decide) + +example : F₃.eval dom int₂ g0 varVal := + solution!(by native_decide) + +example : F₄.eval dom int₂ g0 varVal = false := + solution!(by native_decide) + +end ExWeakStrong +``` ::: -:::: +Como segundo exemplo, vamos considerar uma linguagem `L₂` com interpretação também sobre os naturais. Precisamos de uma interpretação para os símbolos funcionais, uma para o símbolo de relação, e uma atribuição. -# Traduzindo `Formula` para `Prop` +```lean +def intFNat : FInterp Nat + | "zero", [] => 0 + | "s", [i] => i + 1 + | "plus", [i, j] => i + j + | "times", [i, j] => i * j + | _, _ => 0 + +def intNat : Interp Nat + | "R", [i, j] => i < j + | _, _ => false + +def g3 : Assign Nat + | ⟨ "x", []⟩ => 1 + | ⟨ _ , _ ⟩ => 0 + +def zero : Term := .struct "zero" [] +``` -Como em {ref "PL"}[lógica proposicional], fechamos o capítulo ligando as duas -leituras de uma fórmula. `Formula.eval` calcula um `Bool`; `Formula.denote` -produz a proposição que a fórmula afirma. A interpretação muda junto: onde -`Interp` devolvia um `Bool`, `Denot` devolve uma `Prop`. +Uma constante é um símbolo funcional de aridade zero, como {name}`zero` acima. Seguem dois exemplos do que {name}`liftAssign` calcula. O valor de `s[zero]` não depende de `g`, pois nenhuma variável ocorre nele, mas o de `plus[x, zero]` é `g x`, e muda com `g`. Note que os dois fecham por {tactic}`simp`, e não por {tactic}`rfl`. O casamento de strings não é processado por {tactic}`rfl`. ```lean -abbrev Denot (D : Type) := String → List D → Prop +theorem s_zero_is_one (g : Assign Nat) : + liftAssign intFNat g (.struct "s" [zero]) = 1 := by + simp [liftAssign, intFNat, zero] -def Formula.denote {D : Type} (I : Denot D) - (g : Assign D) : Formula Variable → Prop - | .atom name args => I name (args.map g) - | .eq t1 t2 => g t1 = g t2 - | .top => True - | .bot => False - | .neg f => ¬ Formula.denote I g f - | .impl f1 f2 => - Formula.denote I g f1 → Formula.denote I g f2 - | .equi f1 f2 => - Formula.denote I g f1 ↔ Formula.denote I g f2 - | .conj f1 f2 => - Formula.denote I g f1 ∧ Formula.denote I g f2 - | .disj f1 f2 => - Formula.denote I g f1 ∨ Formula.denote I g f2 - | .forall_ v f => - ∀ d : D, Formula.denote I (g.update v d) f - | .exists_ v f => - ∃ d : D, Formula.denote I (g.update v d) f +theorem plus_x_zero_is_x (g : Assign Nat) : + liftAssign intFNat g (.struct "plus" [tx, zero]) = g x := by + simp [liftAssign, intFNat, zero, tx] +``` + +Segue um exemplo de avaliação de uma fórmula de `L₂` no domínio `[0, 1, 2, 3, 4]`. A fórmula diz que existe um número maior que `0`. + +```lean +def frm₁ : Formula Term := .exists_ x (.atom "R" [zero, tx]) +def frm₂ : Formula Term := .forall_ x (.exists_ y (.atom "R" [tx, ty])) + +#eval + let dom : List Nat := [0, 1, 2, 3, 4] + (frm₁.eval dom intNat g3 (liftAssign intFNat), + frm₂.eval dom intNat g3 (liftAssign intFNat)) ``` -Cada caso troca um construtor de `Formula` pelo conectivo correspondente de -`Prop` — o `conj` do dado vira o `∧` da proposição, e o `forall_` vira o `∀` -do próprio Lean. +Vale destacar os limites de nossa implemenação. Em FOL, `frm₂` sob o domínio dos naturais é verdadeira. Nossa implementação, no entanto, para ser decidível, processa apenas domínios finitos, listas. + +A definição de verdade faz uso essencial das atribuições e, ainda assim, para sentenças, a verdade ou a falsidade não depende da atribuição. O problema é que, ao aplicar a definição de verdade acima a uma sentença, por exemplo a `∀x (P[x] → ∃y R[x,y])`, a cláusula que trata do quantificador universal faz referência à noção de verdade para a fórmula `(P[x] → ∃y R[x,y])`, que é uma fórmula aberta. Para determinar se ela é verdadeira temos de saber qual elemento do domínio associar a `x`. A situação é análoga à interpretação de pronomes nas linguas naturais. -Com isso podemos voltar às traduções do exercício anterior e verificá-las. -Enunciamos a condição de verdade pretendida à direita, com os quantificadores -do Lean, e exigimos que coincida com o que a fórmula proposta afirma. Como -`denote` calcula, cada teorema fecha por `Iff.rfl`. +1. Todo mestre tem um aprendiz. +2. Ele tem um aprendiz. + +Assim como definimos em {ref "PL"}[PL]. Uma sentença `α` em FOL é *válida*, `⊨ α`, se é verdadeira em toda possível interpretação para a linguagem de `α`. Uma sentença `C` é consequência lógica de uma sentença `P` (`P` de premissa, `C` de conclusão) se todo modelo que torna `P` verdadeira também torna `C` verdadeira. A notação é `P ⊨ C`. + +Mas como julgar afirmações da forma `P ⊨ C`? Em FOL não temos a função {name}`PL.Formula.allVals`, que enumera todas as possíveis valorações. Logo não podemos decidir `P ⊧ C`. Podemos refutar a afirmação achando um contraexemplo. Um contraexemplo para `P ⊨ C` é uma interpretação `I` com `I ⊨ P` mas `I ⊭ C`. + + +# Traduzindo `Formula` para `Prop` + +Como fizemos em {ref "PL"}[PL], agora podemos mapear termos do tipo `Formula` em `Prop`. Temos {name}`Formula.eval` que calcula o valor verdade de uma fórmula para uma dada interpretação em {name}`Bool`; `Formula.denote` produz a proposição que a fórmula afirma. O tipo para interpretaçõa também precisa mudar, {name}`Interp` devolvia um `Bool`, `Denot` devolve uma `Prop`. ```lean -theorem someoneWalksAndTalks_means {D : Type} - (I : Denot D) (g : Assign D) : - Formula.denote I g someoneWalksAndTalks ↔ - ((∃ d : D, I "Walk" [d]) ∧ (∃ d : D, I "Talk" [d])) := - solution!(Iff.rfl) +abbrev Denot (D : Type) := String → List D → Prop -theorem knightFightsDragon_means {D : Type} - (I : Denot D) (g : Assign D) : - Formula.denote I g knightFightsDragon ↔ - (∀ a : D, ∀ b : D, - I "Knight" [a] ∧ I "Dragon" [b] ∧ I "Finds" [a, b] → - I "Fights" [a, b]) := - solution!(Iff.rfl) +def Formula.denote {D α : Type} + (f : Formula α) (I : Denot D) + (g : Assign D) (tval : Assign D → α → D) : Prop := + match f with + | .atom name args => I name (args.map (tval g)) + | .eq t1 t2 => tval g t1 = tval g t2 + | .top => True + | .bot => False + | .neg f => ¬ f.denote I g tval + | .impl f1 f2 => f1.denote I g tval → f2.denote I g tval + | .equi f1 f2 => f1.denote I g tval ↔ f2.denote I g tval + | .conj f1 f2 => f1.denote I g tval ∧ f2.denote I g tval + | .disj f1 f2 => f1.denote I g tval ∨ f2.denote I g tval + | .forall_ v f => ∀ d : D, f.denote I (g.update v d) tval + | .exists_ v f => ∃ d : D, f.denote I (g.update v d) tval ``` -O segundo é o que torna verificável a discussão sobre os indefinidos: a força -universal de _a knight_ e _a dragon_ não é uma opinião sobre a tradução, é o -que o `∀` do lado direito diz, e o `Iff.rfl` confirma que a fórmula proposta -diz o mesmo. +Cada caso troca um construtor de `Formula` pelo conectivo correspondente de `Prop` — o `conj` do dado vira o `∧` da proposição, e o `forall_` vira o `∀` do próprio Lean. -Falta o teorema que diz que as duas leituras concordam. Ele precisa de uma -hipótese que não aparecia em lógica proposicional: `eval` decide um -quantificador percorrendo `dom`, então só podemos esperar que ele concorde com -o `∀` do Lean — que fala de *todo* elemento do tipo `D` — se `dom` de fato -listar todos eles. É isso que `hdom` exige. +O teorema a seguir nos diz que a denotação de uma fórmula conside com sua avaliação. Mas precisamos de uma hipótese que não aparecia em lógica proposicional. A função `eval` decide um quantificador percorrendo `dom`, então só podemos esperar que ele concorde com o `∀` do Lean, que fala de todo elemento do tipo `D` — se `dom` de fato listar todos eles. É isso que `hdom` exige. ```lean -theorem Formula.eval_iff_denote {D : Type} [DecidableEq D] +theorem Formula.eval_iff_denote {D α : Type} [DecidableEq D] (dom : List D) (hdom : ∀ d : D, d ∈ dom) - (I : Interp D) (g : Assign D) (f : Formula Variable) : - f.eval dom I g = true ↔ - f.denote (fun n as => I n as = true) g := by + (I : Interp D) (tval : Assign D → α → D) + (g : Assign D) (f : Formula α) : + f.eval dom I g tval = true ↔ f.denote (λ n as ↦ I n as = true) g tval := by induction f generalizing g with | atom name args => simp [Formula.eval, Formula.denote] | eq t1 t2 => simp [Formula.eval, Formula.denote] @@ -745,7 +818,7 @@ theorem Formula.eval_iff_denote {D : Type} [DecidableEq D] | neg f ih => simp [Formula.eval, Formula.denote, ← ih] | impl f1 f2 ih1 ih2 => simp [Formula.eval, Formula.denote, ← ih1, ← ih2] - cases Formula.eval dom I g f1 <;> simp + cases f1.eval dom I g tval <;> simp | equi f1 f2 ih1 ih2 => simp [Formula.eval, Formula.denote, ← ih1, ← ih2] | conj f1 f2 ih1 ih2 => @@ -761,10 +834,244 @@ theorem Formula.eval_iff_denote {D : Type} [DecidableEq D] fun ⟨d, h⟩ => ⟨d, hdom d, h⟩⟩ ``` -A hipótese `hdom` é a contrapartida formal de uma limitação real: só se pode -calcular o valor de uma fórmula quantificada quando o domínio é finito e -conhecido. Para domínios infinitos, `denote` continua dizendo o que a fórmula -afirma, mas nenhum `#eval` responde. +O teorema {name}`mem_vertices` é exatamente a hipótese `hdom` que o teorema {name}`Formula.eval_iff_denote` pede. As duas leituras de qualquer fórmula, portanto, concordam naquele modelo, e não sobra hipótese alguma aberta. + +```lean +theorem eval_iff_denote_B (I : Interp Vertex) (g : Assign Vertex) + (f : Formula Variable) : + f.eval vertices I g varVal = true ↔ + f.denote (fun n as => I n as = true) g varVal := + Formula.eval_iff_denote vertices mem_vertices I varVal g f +``` + +A hipótese `hdom` é a contrapartida formal de uma limitação real de que só podemos calcular o valor de uma fórmula quantificada quando o domínio é finito. + +::::details "Interpretação nos Naturais não é decidível" +Considere o domínio dos naturais para interpretação da fórmula `∀x ∃y R[x,y]` que vimos acima. Fácil ver que a fórmula é verdadeira. Mas {name}`Formula.eval` precisa de uma {lean}`List Nat` que contenha *todos* os naturais. É fácil aceitar que não teríamos como provar que {lean}`∀ d : ℕ, d ∈ [0, 1, 2, 3, 4]`, justificando porque a avaliação de `∀x ∃y R[x,y]` não corresponde a denotação desta fórmula em `Prop`. Mas podemos provar esta afirmação. + +```lean +theorem le_foldr_max : + ∀ (l : List Nat) (m : Nat), m ∈ l → m ≤ l.foldr max 0 + | [], _, hm => absurd hm (by simp) + | a :: as, m, hm => by + cases hm with + | head => exact Nat.le_max_left _ _ + | tail _ hm => + exact Nat.le_trans (le_foldr_max as m hm) + (Nat.le_max_right _ _) + +theorem no_list_lists_Nat (dom : List Nat) : + ∃ n : Nat, n ∉ dom := by + refine ⟨dom.foldr max 0 + 1, fun h => ?_⟩ + have := le_foldr_max dom _ h + omega +``` + +O lema auxiliar diz que todo elemento de uma lista de naturais é menor ou igual ao máximo da lista. Com ele, o candidato `dom.foldr max 0 + 1` não pode estar em `dom`: se estivesse, seria menor ou igual ao máximo, e é maior. Logo a hipótese `hdom` é insatisfazível quando `D` é `Nat`: não há domínio a fornecer, e a avaliação não tem como nem começar. +:::: + +Mas `denote` não depende de nenhuma lista. Ela traduz a fórmula numa proposição de Lean. Uma vez traduzida, a proposição pode ser provada sem recorrermos a noção de consequência lógica e construção de uma interpretação. + +```lean +theorem frm₂_is_valid_aux (I : Denot Nat) (g : Assign Nat) + : frm₂.denote I g (liftAssign intFNat) ↔ (∀ a, ∃ b, I "R" [a, b]) := by + simp [frm₂, Formula.denote, liftAssign, Assign.update, tx, ty, x, y] + +theorem frm₂_is_valid (I : Denot Nat) + (hI : ∀ i j, I "R" [i, j] ↔ i < j) (g : Assign Nat) + : frm₂.denote I g (liftAssign intFNat) := by + apply (frm₂_is_valid_aux I g).mpr + intro a + exact ⟨a + 1, (hI a (a + 1)).mpr (by omega)⟩ +``` + +O teorema {name}`frm₂_is_valid_aux` é só tradução. Por isso `simp` fecha o teorema, sem nenhuma aritmética. O teorema {name}`frm₂_is_valid` é que demonstra, e é ele que precisa de matemática. A hipótese `hI` interpreta `R` como `<` em `Prop`, a testemunha de `∃y` é `a + 1`, e `omega` verifica que `a < a + 1`. Com isso, temos {name}`Formula.eval` que calcula, e por isso exige um domínio finito e dado. E {name}`Formula.denote` traduz para `Prop`. + +A função {name}`Formula.denote` nos permite definir em `Prop` o que são fórmulas válidas, satisfatíveis e quando existe uma consequência lógica entre duas fórmulas. + +```lean +/-- A formula is valid when it is true in every model. -/ +def Formula.Valid (f : Formula Variable) : Prop := + ∀ (D : Type) (I : Denot D) (g : Assign D), f.denote I g varVal + +/-- A formula is satisfiable when some model makes it true. -/ +def Formula.Satisfiable (f : Formula Variable) : Prop := + ∃ (D : Type) (I : Denot D) (g : Assign D), f.denote I g varVal + +/-- `f ⊨ g` holds exactly when `f → g` is valid. -/ +def Formula.Implies (f g : Formula Variable) : Prop := + (Formula.impl f g).Valid +``` + +::::exercise (rating := 2) (name := "ex-fol-valid") +Complete as provas dos exemplos abaixo. Note que uma das afirmações não é válida: para ela, vamos precisar da interpretação `intR` como testemunha onde a relação `R` é interpretada como o conjunto unitário `{(0,0)}`. + +```lean +namespace ExValid + +def P (x : Variable) : Formula Variable := .atom "P" [x] +def R (x y : Variable) : Formula Variable := .atom "R" [x, y] + +def intR : Denot Nat + | "R", [i, j] => i = 0 ∧ j = 0 + | _, _ => False + +def g : Assign Nat := fun _ => 0 + +example : + (Formula.disj (.forall_ x (P x)) + (.exists_ x (.neg (P x)))).Valid := by + solution! + intro D I g + simp [Formula.denote, P, Assign.update, x, varVal] + by_contra hc + apply hc + left + intro d + by_contra hd + exact hc (Or.inr ⟨d, hd⟩) + +example : + (Formula.impl (.exists_ x (.exists_ y (R x y))) + (.exists_ x (.exists_ y (R y x)))).Valid := by + solution! + intro D I g + simp [Formula.denote, R, Assign.update, x, y, varVal] + intro a b hab + exact ⟨b, a, hab⟩ + +example : + (Formula.impl (.forall_ x (R x x)) + (.forall_ x (.exists_ y (R x y)))).Valid := by + solution! + intro D I g + simp [Formula.denote, R, Assign.update, x, y, varVal] + intro h a + exact ⟨a, h a⟩ + +example : + ¬ (Formula.impl (.exists_ x (R x x)) + (.forall_ x (.exists_ y (R x y)))).Valid := by + solution! + intro h + have h₁ := h Nat intR g + simp [Formula.denote, R, Assign.update, x, y, varVal, intR] at h₁ + have := h₁ 1 + omega + +end ExValid +``` +:::: + +::::exercise (rating := 2) (name := "ex-fol-consequence") +Complete as provas dos exemplos abaixo. Note que uma das consequências lógicas não é válida. Apeans para este exemplo vamos precisar da interpretação `intR`. + +```lean +namespace ExEntailsOnlyVars + +def P (x : Variable) : Formula Variable := .atom "P" [x] +def R (x y : Variable) : Formula Variable := .atom "R" [x, y] + +def intR : Denot Nat + | "R", [i, j] => i < j + | _, _ => False + +def g : Assign Nat := fun _ => 0 + +example : (Formula.forall_ x (P x)).Implies (.exists_ x (P x)) := by + solution! + intro D I g + simp [Formula.denote, P] + intro hh + exact ⟨g x, hh (g x)⟩ + +example : + ¬ (Formula.exists_ x (.exists_ y (R x y))).Implies + (Formula.exists_ x (R x x)) := by + solution! + intro h + have h₁ := h Nat intR g + simp [Formula.denote, R, Assign.update, x, y, varVal, intR] at h₁ + have := h₁ 0 1 + omega + +example : + (Formula.exists_ y (.forall_ x (R x y))).Implies + (.forall_ x (.exists_ y (R x y))) := by + solution! + intro D I g + simp [Formula.denote, R, Assign.update, x, y, varVal] + intro b hb a + exact ⟨b, hb a⟩ + +end ExEntailsOnlyVars +``` +:::: + +Definimos {name}`Formula.Valid` para {lean}`Formula Variable`, onde os argumentos dos predicados são apenas variáveis. Em {lean}`Formula Variable`, uma estrutura é o par `(D, I)`, o domínio e a interpretação dos símbolos predicativos. Quando há símbolos funcionais, a estrutura passa a ser a tripla`(D, I, F)` onde `F` que diz qual elemento do domínio cada símbolo funcional nomeia. A definição abaixo torna isso explícito: ela quantifica também sobre {name}`FInterp`, e usa {name}`liftAssign` no lugar de {name}`varVal` para avaliar os termos. + +```lean +/-- A formula with terms is valid when it is true in every +structure `(D, I, F)` and under every assignment. -/ +def Formula.ValidT (f : Formula Term) : Prop := + ∀ (D : Type) (I : Denot D) (F : FInterp D) (g : Assign D), + f.denote I g (liftAssign F) +``` + +Até aqui, nossa noção de consequência lógica relaciona *duas* fórmulas. Mas o argumento mais comum tem várias premissas: dizemos que `C` é consequência de `P₁, …, Pₙ` quando todo modelo que torna todas as premissas verdadeiras também torna `C` verdadeira. Assim como fizemos em {ref "PL"}[PL], no próximo exercício vamos definir a consequência lógica de um conjunto de premissas em uma conclusão. + +::::exercise (rating := 2) (name := "ex-fol-implies-from-list") +Assim como {name}`PL.Formula.impliesL` fez em {ref "PL"}[PL], complete a definição abaixo para que possamos falar de `Δ ⊧ α`, a consequência lógica de uma lista de fórmulas. Use {name}`Formula.ValidT` e {name}`Formula.conjs`. + +```lean +def Formula.ImpliesL (hs : List (Formula Term)) (c : Formula Term) : Prop := + solution!(Formula.ValidT (.impl (Formula.conjs hs) c)) +``` +:::: + +::::exercise (rating := 2) (name := "ex-fol-entails") +Complete os exemplos a seguir que envolvem provar a consequência lógica a partir de uma lista de premissas que envolvem fórmulas com termos. A segunda não vale, e para mostrar isso basta exibir um modelo que satisfaça as duas premissas e refute a conclusão. + +```lean +namespace ExEntailsTerms + +def R (t u : Term) : Formula Term := .atom "R" [t, u] + +def ta : Term := .struct "a" [] +def tb : Term := .struct "b" [] + +def symmR : Formula Term := + .forall_ x (.forall_ y (.impl (R tx ty) (R ty tx))) + +def intNe : Denot Nat + | "R", [i, j] => i ≠ j + | _, _ => False + +def fab : FInterp Nat + | "a", [] => 0 + | "b", [] => 1 + | _, _ => 0 + +def g : Assign Nat := fun _ => 0 + +example : Formula.ImpliesL [symmR, R ta tb] (R tb ta) := by + solution! + intro D I F g + simp [Formula.conjs, Formula.denote, symmR, R, liftAssign, + Assign.update, tx, ty, x, y] + intro hsym hab + exact hsym _ _ hab + +example : ¬ Formula.ImpliesL [symmR, R ta tb] (R ta ta) := by + solution! + intro h + have h₁ := h Nat intNe fab g + simp [Formula.conjs, Formula.denote, symmR, R, ta, tb, liftAssign, + fab, Assign.update, tx, ty, x, y, intNe] at h₁ + +end ExEntailsTerms +``` +:::: ```lean end FOL diff --git a/CSwL/Logic/PL.lean b/CSwL/Logic/PL.lean index 8c8bac8..3ccecf2 100644 --- a/CSwL/Logic/PL.lean +++ b/CSwL/Logic/PL.lean @@ -1,6 +1,8 @@ import CSwLMeta import Bib import Mathlib.Tactic.ByContra +import Mathlib.Data.List.Sort +import Mathlib.Data.List.Dedup import CSwLCompat open Verso.Genre Manual @@ -8,7 +10,7 @@ open CSwLMeta set_option verso.code.warnLineLength 100 -#doc (Manual) "Lógica proposicional" => +#doc (Manual) "Lógica Proposicional" => %%% tag := "PL" file := "PL" @@ -25,26 +27,17 @@ tag := "pl-intro" Em {ref "Proof"}["Proof"] as fórmulas proposicionais foram escritas diretamente como termos do tipo `Prop`, e usando táticas construimos provas de proposições `α` a partir de um conjunto de hipóteses `Γ`. Isto é, mostramos como derivar `α` a partir de `Γ`, isto é `Γ ⊢ α`. -Mas em Lean, `Prop` é um tipo e proposições particulares também são tipos. A variável `h` abaixo pode ser entendida como um identificador para uma "prova qualquer" da proposição `p ∧ q`. E Lean adota o princípio da "irrelevância da prova", ou seja, Lean não distingue diferentes provas de uma proposição. Como consequência, o tipo `Prop` não é computável, não é um "dado" que pode ser manipulado. Por exemplo, não conseguimos extrair os componentes de uma conjunção `a ∧ b`. Lean sabe que todas as provas de `a ∧ b` são irrelevantes e iguais, então ele não permite que você use uma prova para tomar decisões no mundo dos dados programáveis (`Type`). Em outras palavras, não podemos realizar casamento de padrões em `h` abaixo. +Em Lean, `Prop` é um tipo assim como qualquer particular proposição também é um tipo. A variável `h` abaixo pode ser entendida como um identificador para uma "prova qualquer" da proposição `p ∧ q`. E Lean adota o princípio da "irrelevância da prova", ou seja, Lean não distingue diferentes provas de uma proposição. Como consequência, o tipo `Prop` não é computável, não é um "dado" que pode ser manipulado. Por exemplo, não conseguimos extrair os componentes de uma conjunção `a ∧ b`. Lean sabe que todas as provas de `a ∧ b` são irrelevantes e iguais, então ele não permite que você use uma prova como qualquer outro dado de um `Type`. Não podemos, por exemplo, realizar casamento de padrões em `h` abaixo. ```lean +error -section -variable (p q : Prop) - -variable (h : p ∧ q) -#check p ∧ q -#check h - -def doesNotWork (h : p ∧ q) : Type := +def doesNotWork (p q : Prop) (h : p ∧ q) : Type := match h with | And.intro ha hb => ha - -end ``` -Nesta seção, queremos manipular fórmulas e decidir quando uma fórmula `α` é consequência lógica de `β`, isto é `β ⊧ α `. A noção de consequência lógica é semântica. Para toda possível escolha de valores verdade para os símbolos proposicionais em `α` e `β`, sempre que `β` for verdade, `α` deve ser verdade. Para _computar_ o valor verdade de uma fórmula, vamos precisar manipula a formula como dado, e calcular seu valor verdade a partir do mapeamento de variáveis proposicionais em valores verdade. Em tempo, a relação dentre duas fórmulas pode ser naturalmente estendida para uma relação entre um conjunto de fórmulas `Γ` e uma fórmula, `Γ ⊧ α`. +Nesta seção, queremos manipular fórmulas e decidir quando uma fórmula `α` é consequência lógica de `β`, isto é, `β ⊧ α `. A noção de consequência lógica é semântica. Para toda possível escolha de valores verdade para os símbolos proposicionais em `α` e `β`, sempre que `β` for verdade, `α` deve ser verdade. Para _computar_ o valor verdade de uma fórmula, vamos precisar manipula a formula como dado, e calcular seu valor verdade a partir do mapeamento de variáveis proposicionais em valores verdade. -Em um problema com um número finito de proposições, e os números costumam ser pequenos o suficiente para que a análise sistemática de todas as combinações de valores verdade seja viável na prática. Para demonstrar que todo número par maior que dois pode ser escrito como uma soma de dois números primos esta estratégia não seria válida. +Em um problema com um número finito de proposições, e os números costumam ser pequenos o suficiente para que a análise sistemática de todas as combinações de valores verdade seja viável na prática. # Sintaxe de Lógica Proposicional @@ -52,30 +45,30 @@ Em um problema com um número finito de proposições, e os números costumam se tag := "pl-syntax" %%% -Para construir fórmulas como dados, não poderemos mais usar a notação de Lean disponível para os termos do tipo `Prop`. Quando escrevemos `p ∧ q`, o símbolo `∧` é um operador infixado (aparece no meio dos argumentos) e representa o construtor {lean}`And.intro` do tipo {lean}`And`. Os operadores, para serem usados de forma infixada, precisam ter um mecanismo de precedência para permitir que possamos escrever termos ambiguos como `p ∧ q ∧ r` que terão sua leitura associada a `p ∧ (q ∧ r)` e não `(p ∧ q) ∧ r`. Nada disso estará ao nosso dispor. +Para construir fórmulas, não poderemos mais usar a notação de Lean disponível para `Prop`. Quando escrevemos `p ∧ q`, o símbolo `∧` é um operador infixado (aparece no meio dos argumentos) e representa o construtor {lean}`And.intro` do tipo {lean}`And`. Os operadores, para serem usados de forma infixada, precisam ter um mecanismo de precedência para permitir que termos como `p ∧ q ∧ r` sejam interpretados como `p ∧ (q ∧ r)` e não `(p ∧ q) ∧ r`, ou seja, tenham sempre uma leitura não ambigua. Nada disso estará ao nosso dispor na sintaxe que iremos introduzir nesta seção. -Nossas fórmulas serão representadas por termos do tipo indutivo `Form`. Um átomo é identificado por um nome, e o nome é uma `String`. Isso dá o inventário ilimitado que a gramática pede sem precisar enumerar símbolo por símbolo. +Nossas fórmulas serão representadas por termos do tipo indutivo `Formula`. Um átomo é identificado por um nome, e o nome é uma {lean}`String`. ```lean -inductive Form where +inductive Formula where | atom (name : String) | top | bot - | neg (f : Form) - | conj (f g : Form) - | disj (f g : Form) + | neg (f : Formula) + | conj (f g : Formula) + | disj (f g : Formula) deriving DecidableEq, Repr ``` -Os contrutores {name}`Form.top` e {name}`Form.bot` representam as proposições "sempre verdadeira" e "sempre falsa". São objetos sintáticos que serão sempre interpretados como os valores verdade {lean}`true` e {lean}`false` na semântica. Com este tipo, podemos representar fórmulas arbitrariamente complexas. +Os contrutores {name}`Formula.top` e {name}`Formula.bot` representam as proposições "sempre verdadeira" e "sempre falsa". São objetos sintáticos que serão sempre interpretados como os valores verdade {lean}`true` e {lean}`false` na semântica. Com este tipo, podemos representar fórmulas arbitrariamente complexas. ```lean #eval - let p : Form := .atom "p" - let q : Form := .atom "q" - let f₁ : Form := .neg (.neg p) - let f₂ : Form := .disj (.neg p) q - Form.conj f₁ f₂ + let p : Formula := .atom "p" + let q : Formula := .atom "q" + let f₁ : Formula := .neg (.neg p) + let f₂ : Formula := .disj (.neg p) q + Formula.conj f₁ f₂ ``` Como não temos símbolos infixados, não temos ambiguidade. As duas possíveis interpretações para a sentença ambigua em português "Maira é jovem e bonita ou triste" seriam: @@ -83,38 +76,115 @@ Como não temos símbolos infixados, não temos ambiguidade. As duas possíveis ```lean namespace Maria -def j : Form := .atom "MJ" -def b : Form := .atom "MB" -def t : Form := .atom "MT" +def j : Formula := .atom "MJ" +def b : Formula := .atom "MB" +def t : Formula := .atom "MT" -#eval Form.conj j (.disj b t) -#eval Form.disj (.conj j b) t +def form₁ := Formula.conj j (.disj b t) +def form₂ := Formula.disj (.conj j b) t end Maria ``` -Vale observar que a biblioteca `cslib` define o tipo `Cslib.Logic.PL.Proposition` que poderia ser usado nesta seção, mas isto introduziria uma complexidade desnecessária. +:::dev "Alexandre (rademaker)" +We need to think how to use `Cslib.Logic.PL.Proposition` here instead of the local definitions. +::: + +Na lógica proposicional (PL, "propotional logic"), uma *linguagem proposicional* é o conjunto de todas as fórmulas que podem ser construídas a partir de um *vocabulário* de símbolos não lógicos (os átomos representados por {lean}`Formula.atom`). Acima, a partir dos átomos construídos com as strings "MJ", "MB" e "MT", infinitas fórmulas de complexidade arbitrária podem ser construídas pela combinação dos demais construtores de {lean}`Formula`. Cada um destes construtores representam um operador lógico. + +Podemos também pensar que uma dada fórmula (ou conjunto de fórmulas) induz um vocabulário, o conjunto de todos os símbolos que ocorreram na fórmula (ou conjunto de fórmulas). No exemplo anterior, `j`, `b` e `t` são identificadores em Lean para termos do tipo {lean}`Formula`, representam fórmulas em PL mas não estão em PL, estão na metalinguagem. As strings "MJ", "MB" e "MT" são os nomes dos átomos usados nas formulas, o vocabulário destas fórmulas. + +A função `names` abaixo extrai o vocabulário de uma fórmula. A lista resultante deve estar ordenada e sem repetições. + +```lean +def Formula.namesRaw : Formula → List String + | .atom name => [name] + | .top => [] + | .bot => [] + | .neg f => f.namesRaw + | .conj f g => f.namesRaw ++ g.namesRaw + | .disj f g => f.namesRaw ++ g.namesRaw + +def Formula.names (f : Formula) : List String := + solution!(f.namesRaw.dedup.mergeSort (· ≤ ·)) + +#eval Maria.form₁.names +``` + +:::exercise (rating := 1) (name := "collect-atoms") +Complete a definição da função `namesL` abaixo, que estende a função `names` para um conjunto de fórmulas. Se sua definição estiver correta, a prova do exemplo deve ser obtida diretamente com a tática {tactic}`native_decide`. Dica: não repita ordenações. + +```lean +def Formula.namesL (fs : List Formula) : List String := + solution!( + fs.foldl (λ acc f => f.namesRaw ++ acc) [] |>.dedup.mergeSort (· ≤ ·)) + +example : Formula.namesL [Maria.form₁, Maria.form₂] == ["MB", "MJ", "MT"] := + solution!(by native_decide) +``` +::: + +:::exercise (rating := 1) (name := "collect-atoms-alternative") +Complete a definição da função `Formula.names₁` com uma implementação alternativa para {lean}`Formula.names` que ao invés de eliminar duplicatas e ordenar no final da recursão, constrói a lista de saída sem duplicatas e ordenada. Se sua definição estiver correta, a prova do exemplo deve ser obtida diretamente com a tática {tactic}`native_decide`. Dica: não repita ordenações. + +```lean +def Formula.namesRaw₁ (f : Formula) (sofar : List String) : List String := + solution!( + match f with + | .atom name => sofar.insertP (· == name) name + | .top => [] + | .bot => [] + | .neg f => f.namesRaw₁ sofar + | .conj f g => + let as := f.namesRaw₁ sofar + let bs := g.namesRaw₁ sofar + as.merge bs + | .disj f g => + let as := f.namesRaw₁ sofar + let bs := g.namesRaw₁ sofar + as.merge bs) + +def Formula.names₁ (f : Formula) : List String := + solution!(f.namesRaw₁ []) + +#eval Maria.form₁.names₁ + +example : Maria.form₁.names₁ == ["MB", "MJ", "MT"] := + solution!(by native_decide) +``` +::: + Nem todos os conectivos precisam ser definidos como "primitivos". Como vimos na seção {ref "pl-lean"}[pl-lean] a implicação pode ser definida como uma dijunção. E a dupla implicação como uma conjunção de implicações. ```lean -def Form.impl (f g : Form) : Form := .disj (.neg f) g -def Form.equi (f g : Form) : Form := - .conj (Form.impl f g) (Form.impl g f) +def Formula.impl (f g : Formula) : Formula := .disj (.neg f) g +def Formula.iff (f g : Formula) : Formula := + .conj (Formula.impl f g) (Formula.impl g f) ``` -A conjunção e a disjunção são binárias. Poderiam receber uma lista de fórmulas `conj (fs : List Form)`, mas um construtor que guarda uma `List Form` dentro do próprio tipo o torna um indutivo _nested_, mais complicado de manipular em Lean. Mas podemos definir funções que recebem listas de fórmulas e constrem conjunções e disjunções. Abaixo `top`/`bot` são a base da recursão de `conjs`/`disjs`. Uma conjunção vazia é sempre verdadeira, uma disjunção vazia é sempre falsa. +A conjunção e a disjunção são binárias. Poderiam receber uma lista de fórmulas `conj (fs : List Formula)`, mas um construtor que guarda uma `List Form` dentro do próprio tipo o torna um indutivo _nested_, mais complicado de manipular em Lean. Mas podemos definir funções que recebem listas de fórmulas e constrem conjunções e disjunções. Abaixo `top`/`bot` são a base da recursão de `conjs`/`disjs`. ```lean -def Form.conjs : List Form → Form +def Formula.conjs : List Formula → Formula | [] => .top | [f] => f - | f :: fs => .conj f (Form.conjs fs) + | f :: fs => .conj f (Formula.conjs fs) -def Form.disjs : List Form → Form +def Formula.disjs : List Formula → Formula | [] => .bot | [f] => f - | f :: fs => .disj f (Form.disjs fs) + | f :: fs => .disj f (Formula.disjs fs) +``` + +Note que {name}`Formula.bot` é o elemento neutro da dijunção, `bot ∨ a`. E {name}`Formula.top` é o elemento neutro da conjunção, `top ∧ a`. Uma conjunção vazia é sempre verdadeira, uma disjunção vazia é sempre falsa. O que sugere as implementações alternativas a seguir. + +```lean +def Formula.conjs₁ (fs : List Formula) : Formula := + fs.foldl .conj .top + +def Formula.disjs₁ (fs : List Formula) : Formula := + fs.foldl .disj .bot ``` :::exercise (rating := 1) (name := "bangu-form") @@ -124,18 +194,19 @@ Três pessoas são suspeitas de torcer pelo Bangu F.C. Aparecido entrevistou os - Joaquim: Se Auro não torce pelo BFC, Cláudia também não torce pelo BFC. - Cláudia: Eu torço pelo BFC, mas pelo menos um dos outros não torce pelo BFC. -Termine a formalização dos depoimentos construindo uma expressão no tipo `Form`. +Considerando que as fórmulas atômicas `A`, `J` e `C` representam, respectivamente, que Auro, Joaquim e Cláudia torcem pelo BFC, complete a formalização dos três depoimentos construindo as expressões correspondentes do tipo {name}`Formula`. + ```lean namespace Bangu -def A : Form := Form.atom "Auro" -def J : Form := Form.atom "Joaquim" -def C : Form := Form.atom "Claudia" +def A : Formula := .atom "Auro" +def J : Formula := .atom "Joaquim" +def C : Formula := .atom "Claudia" -def depo1 : Form := solution!(.conj (.neg J) C) -def depo2 : Form := solution!(.impl (.neg A) (.neg C)) -def depo3 : Form := solution!(.conj C (.disj (.neg A) (.neg J))) +def depo1 : Formula := solution!(.conj (.neg J) C) +def depo2 : Formula := solution!(.impl (.neg A) (.neg C)) +def depo3 : Formula := solution!(.conj C (.disj (.neg A) (.neg J))) end Bangu ``` @@ -145,40 +216,40 @@ end Bangu A expressão `p ∨ q` é verdadeira mesmo quando `p` e `q` são ambos verdadeiros. Em português, "ou" costuma ser exclusivo, como em "Você pode ficar com o sorvete ou com o algodão-doce, mas não com os dois." Defina um conectivo `xor` para "ou exclusivo", usando os conectivos já definidos. ```lean -def Form.xor (f g : Form) : Form := +def Formula.xor (f g : Formula) : Formula := solution!(.disj (.conj f (.neg g)) (.conj (.neg f) g)) ``` ::: -O tipo `Form` é um `inductive`. Um valor de `Form` é dado. Nenhum dos exercícios abaixo seriam possíveis em `Prop`. Não há como perguntar "quantos `∧` tem esta proposição" a um valor de tipo `Prop`, porque `Prop` não guarda a fórmula que o provou. Vamos definir duas fórmulas para usar nos exercícios seguintes. +Um termo do tipo {lean}`Formula` é um dado. Nenhum dos exercícios abaixo seriam possíveis em `Prop`. Não há como perguntar "quantos `∧` tem esta proposição" a um valor de tipo `Prop`, porque `Prop` não guarda a fórmula que o provou. Vamos definir duas fórmulas para usar nos exercícios seguintes. ```lean -def form1 : Form := +def form1 : Formula := .conj (.atom "p") (.neg (.atom "p")) -def form2 : Form := +def form2 : Formula := .disjs [.atom "p1", .atom "p2", .atom "p3", .atom "p4"] -def form3 : Form := - let p : Form := .atom "p" - let q : Form := .atom "q" - .equi (.impl p q ) (.disj (.neg p) q) +def form3 : Formula := + let p : Formula := .atom "p" + let q : Formula := .atom "q" + .iff (.impl p q ) (.disj (.neg p) q) ``` :::exercise (rating := 1) (name := "count-operators") -Implemente uma função `opsNr` para contar o número de operadores de uma fórmula. a tática {tactic}`decide` é como pedir ao Lean para executar a decisão de uma proposição booleana e, se o resultado for true, transformar esse resultado em uma prova. +Implemente uma função `countOps` para contar o número de operadores lógicos de uma fórmula. A tática {tactic}`decide` é como pedir ao Lean para executar a decisão de uma proposição boleana e, se o resultado for true, transformar esse resultado em uma prova. ```lean -def Form.opsNr : Form → Nat := +def Formula.countOps : Formula → Nat := solution!(fun | .atom _ => 0 | .top => 0 | .bot => 0 - | .neg f => 1 + f.opsNr - | .conj f g => 1 + f.opsNr + g.opsNr - | .disj f g => 1 + f.opsNr + g.opsNr) + | .neg f => 1 + f.countOps + | .conj f g => 1 + f.countOps + g.countOps + | .disj f g => 1 + f.countOps + g.countOps) -example : form2.opsNr = 3 := by decide +example : form2.countOps = 3 := by decide ``` ::: @@ -186,7 +257,7 @@ example : form2.opsNr = 3 := by decide Implemente uma função `depth` para calcular a profundidade da árvore de análise de uma fórmula. ```lean -def Form.depth : Form → Nat := +def Formula.depth : Formula → Nat := solution!(fun | .atom _ => 0 | .top => 0 @@ -199,25 +270,6 @@ example : form2.depth = 3 := by decide ``` ::: -:::exercise (rating := 2) (name := "collect-atoms") -Implemente `propNames` para coletar a lista de nomes de átomos proposicionais que ocorrem numa fórmula. A lista resultante deve estar ordenada e sem repetições. O exemplo pode ser provado com {tactic}`native_decide`. - -```lean -def Form.propNamesRaw (f : Form) : List String := solution!( - match f with - | .atom name => [name] - | .top => [] - | .bot => [] - | .neg f => f.propNamesRaw - | .conj f g => f.propNamesRaw ++ g.propNamesRaw - | .disj f g => f.propNamesRaw ++ g.propNamesRaw) - -def Form.propNames (f : Form) : List String := - solution!(f.propNamesRaw.eraseDups.mergeSort (· ≤ ·)) - -example : form1.propNames == ["p"] := solution!(by native_decide) -``` -::: # Semântica de Lógica Proposicional @@ -227,89 +279,105 @@ tag := "pl-semantics" Todas as regras de derivação que usamos em {ref "Proof"}["Proof"] são justificadas por uma noção semântica de *consequência lógica*. Entendemos que `P` deve ser verdade sempre que `P ∧ Q` for verdade, para qualquer possível tradução de `P` e `Q` de volta para expressões em uma linguagem natural, por isso aceitamos `P ∧ Q ⊧ P`. Para formalizar esta noção de "todas as possíveis traduções", vamos precisar de um processo para avaliar fórmulas lógicas em valores verdade. -Vamos chamar de *valorações* um mapeamento de símbolos proposicionais no conjunto dos booleanos, que em Lean correspondem aos valores `True` e `False` do tipo `Bool`. - -Podemos representar uma valoração como uma lista de pares, e um átomo ausente da lista conta como falso. - -```lean -abbrev Valuation := List (String × Bool) -``` - -Se `V` é uma valoração, ela se estende a uma função que mapea qualquer fórmula para um valor de verdade. A extensão é definida por recursão sobre a estrutura da fórmula, um caso por construtor. Os construtores `top` e `bot` são constantes, nenhuma valoração os afeta. Se um átomo ocorrer mais de uma vez, vamos assumir que seu valor verdade é a primeira ocorrência dele na lista, isto corresponde ao comportamento da função {name}`List.lookup`. +A partir de um mapeamento inicial de símbolos proposicionais em valores boleanos, o tipo {name}`Bool` em Lean, obtemos de forma recursiva o valor verdade de qualquer termo do tipo {name}`Formula`. Os construtores {name}`Formula.top` e {name}`Formula.bot` são constantes, nenhuma valoração os afeta. Podemos perceber que, de todos os casos da recursão, só o caso do átomo (construtor {name}`Formula.atom`) consulta a valoração passada; os outros casos apenas combinam os valores verdade das subfórmulas. ```lean -def Form.eval (f : Form) (v : Valuation) : Bool := +/-- The evaluation of a formula `f`, given the function `value` + that gives each atom its truth value. -/ +def Formula.eval (f : Formula) (value : String → Bool) : Bool := match f with - | .atom name => (v.lookup name).getD false + | .atom name => value name | .top => true | .bot => false - | .neg g => !g.eval v - | .conj g h => g.eval v && h.eval v - | .disj g h => g.eval v || h.eval v + | .neg g => !g.eval value + | .conj g h => g.eval value && h.eval value + | .disj g h => g.eval value || h.eval value ``` +A função {name}`Formula.eval` faz a recursão e recebe como parâmetro a função que dá o valor verdade de um átomo. Toda a semântica que construímos a seguir passa por {name}`Formula.eval`. + Chamamos as fórmulas que são sempre verdade para qualquer valoração de suas variáveis proposicionais de *tautologias*, ou, simplesmente, fórmulas *válidas*. Se `α` é uma tautologia, significa que `⊨ α`, não depende de nenhuma hipótese para ser verdade. As fórmulas que são sempre falsas para toda valoração são chamadas de *contradições* (ou insatisfatíveis). Uma fórmula é *satisfatível* se há pelo menos uma valoração que a torna verdadeira. Uma fórmula é *contingente* se existe pelo menos uma valoração que torna a fórmula verdadeira e pelo menos uma que a torna falsa. Podemos concluir que se `α` é uma contradição, então `⊨ ¬ α` (sua negação é válida). Toda tautologia é satisfatível, mas nem toda fórmula satisfatível é uma tautologia. -:::exercise (rating := 1) (name := "taut-contradiction") -Construa as valorações `vs1` e `vs2` de tal forma que os exemplos possam ser provados com a tática {tactic}`decide`. +:::exercise (rating := 1) (name := "valuations") +Construa as valorações `v₁` e `v₂` de tal forma que os exemplos possam ser provados com a tática {tactic}`decide` os exemplos seguintes. ```lean namespace TestVals -def p : Form := .atom "p" -def q : Form := .atom "p" -def r : Form := .atom "r" - -def form3 : Form := .disj p (.conj q r) - -def form4 : Form := .neg (.conj p (.neg q)) - -def form5 : Form := - .conj (.atom "a") (.impl (.neg (.atom "b")) (.atom "c")) - -def vs1 : List (String × Bool) := solution!([("p", true),("q", true)]) -def vs2 : List (String × Bool) := solution!([("a", true),("b", true)]) - -example : form3.eval vs1 = true := solution!(by decide) -example : form4.eval vs1 = true := solution!(by decide) -example : form5.eval vs2 = true := solution!(by decide) +def p : Formula := .atom "p" +def q : Formula := .atom "q" +def r : Formula := .atom "r" + +def form1 : Formula := .neg (.disj (.conj p r) (.neg q)) +def form2 : Formula := .disj (.impl q p) (.conj r (.neg q)) +def form3 : Formula := .impl (.conj q (.neg p)) (.neg r) + +def v₁ (v : String) : Bool := + solution!( + match v with + | "p" => false | "q" => true | "r" => false + | o => false + ) + +def v₂ (v : String) : Bool := + solution!( + match v with + | "p" => true | "q" => false | "r" => false + | o => false + ) + +example : form1.eval v₁ = true := solution!(by decide) +example : form1.eval v₂ = false := solution!(by decide) +example : form2.eval v₁ = false := solution!(by decide) +example : form3.eval v₂ = true := solution!(by decide) end TestVals ``` ::: -A função a seguir gera a lista de todas as valorações sobre o conjunto dos nomes de átomos presentes em um termo do tipo `Form`. +A seguir, definimos a função `allVals` que gera a lista de todas as valorações possíveis sobre o vocabulário de uma {name}`Formula`. ```lean +abbrev Valuation := List (String × Bool) + +/-- return an evaluation function from `Valuation`. -/ +def Valuation.toFun (vs : Valuation) : String → Bool := + fun n => (vs.lookup n).getD false + def genVals : List String → List Valuation | [] => [[]] | n :: ns => let vs := (genVals ns) vs.map ((n, true) :: ·) ++ vs.map ((n, false) :: ·) -def Form.allVals (f : Form) : List Valuation := - genVals f.propNames +/-- return all possible valuations for `f`. -/ +def Formula.allVals (f : Formula) : List Valuation := + genVals f.names ``` Com estas funções, podemos construir a tabela verdade de uma fórmula. ```lean -#eval List.zip form1.allVals (form2.allVals.map (form2.eval ·)) +#eval + let as := form1.allVals + List.zip as (as.map (fun vs => form1.eval vs.toFun)) ``` Para decidir se uma fórmula é tautologia, satisfatível ou contradição, podemos percorrer todas as valorações possíveis, que são finitas, porque uma fórmula tem finitos átomos. ```lean -def Form.tautology (f : Form) : Bool := - f.allVals.all (fun v => f.eval v) +def Formula.tautology (f : Formula) : Bool := + f.allVals.all (fun v => f.eval v.toFun) -def Form.satisfiable (f : Form) : Bool := - f.allVals.any (fun v => f.eval v) +def Formula.satisfiable (f : Formula) : Bool := + f.allVals.any (fun v => f.eval v.toFun) -def Form.contradiction (f : Form) : Bool := +def Formula.contradiction (f : Formula) : Bool := !f.satisfiable -#eval (form1.contradiction, (Form.neg form1).tautology, form1.satisfiable) +#eval form1.contradiction +#eval (Formula.neg form1).tautology +#eval form1.satisfiable ``` E como já sabemos da seção {ref "pl-lean"}[pl-lean], podemos mostrar que {name}`form3` é uma tautologia. @@ -318,18 +386,40 @@ E como já sabemos da seção {ref "pl-lean"}[pl-lean], podemos mostrar que {nam #eval form3.tautology ``` -:::exercise (rating := 1) (name := "def-contingente") +:::exercise (rating := 1) (name := "ex-pl-contingent") Complete a definição de fórmula contingente. Para provar o exemplo, use {tactic}`native_decide`. ```lean -def Form.contingent (f : Form) : Bool := +def Formula.contingent (f : Formula) : Bool := solution!(f.satisfiable && !f.tautology) -example : (Form.atom "q").satisfiable = true := by +example : (Formula.atom "q").satisfiable := by solution!(native_decide) ``` ::: +:::exercise (rating := 1) (name := "ex-pl-satisfiable") +Complete a definição de `F` que só deverá usar os átomos `p` e `q`. E prove o exemplo. + +```lean +namespace ExSat + +def p : Formula := .atom "p" +def q : Formula := .atom "q" + +def F : Formula := solution!(.impl p (.impl (.disj q p) p)) + +example : F.satisfiable ∧ F.depth = 4 := by + solution! + constructor + · native_decide + · rw [F, Formula.impl] + decide + +end ExSat +``` +::: + A seguir, escrevemos implies para a relação de consequência lógica, chamando atenção para a relação entre `P ⊨ Q` e `⊨ P → Q`. Uma proposição `Q` é consequência lógica de `P` se, e somente se, a implicação `P → Q` é uma tautologia. Se `P → Q ≡ ¬ P ∨ Q ≡ ¬ (P ∧ ¬ Q)` então podemos também dizer que `P ⊧ Q` se e somente se `⊨ ¬ (P ∧ ¬ Q)`. Podemos estender para uma consequência lógica de fórmulas `{P₁, …, Pₙ} ⊧ α`, indicando que toda valoração que torna as fórmulas `P₁, …, Pₙ` verdadeiras também torna `α` verdadeira. O que equivale afirmar que a implicação da conjunção das premissas na conclusão é válida `⊧ (P₁ ∧ … ∧ Pₙ) → α`. @@ -337,50 +427,83 @@ Podemos estender para uma consequência lógica de fórmulas `{P₁, …, Pₙ} Duas fórmulas `α` e `β` são *logicamente equivalentes*, escrevemos `α ≡ β`, se têm o mesmo valor de verdade para toda valoração possível. Segue da definição que todas as tautologias são logicamente equivalentes entre si, e o mesmo vale para as contradições. ```lean -def Form.implies (f g : Form) : Bool := - (Form.conj f (.neg g)).contradiction +def Formula.implies (f g : Formula) : Bool := + (Formula.conj f (.neg g)).contradiction -def Form.equivalent (f g : Form) : Bool := +def Formula.equivalent (f g : Formula) : Bool := f.implies g && g.implies f ``` -:::exercise (rating := 2) (name := "equiv-cases") -Complete a definição de `Feq2` com uma fómula equivalente a `Feq1` e feche o exemplo com {tactic}`native_decide`. +:::exercise (rating := 1) (name := "ex-pl-equiv") +Complete os exemplos com fórmulas equivalentes mas sintaticamente diferentes de `F0`, `F1` e `F2`. Todos os `example` podem ser provados com a tática {tactic}`native_decide`. Suas fórmulas devem usar apenas os átomos `p` e `q` já definidos. ```lean -def p : Form := Form.atom "p" -def q : Form := Form.atom "q" +namespace ExEquiv +def p : Formula := .atom "p" +def q : Formula := .atom "q" -def Feq1 : Form := Form.neg (.equi p q) -def Feq2 : Form := solution!(.disj (.conj (.neg p) q) (.conj (.neg q) p)) +def F0 : Formula := .neg (.neg p) +def F1 : Formula := .impl p q +def F2 : Formula := .neg (.iff p q) -example : Feq1.equivalent Feq2 = true := - solution!(by native_decide) +example : F0.equivalent solution!(p) := + solution!(by native_decide) + +example : F1.equivalent solution!(.disj (.neg p) q) := + solution!(by native_decide) + +example : F2.equivalent + solution!(.disj (.conj (.neg p) q) (.conj (.neg q) p)) := + solution!(by native_decide) +end ExEquiv ``` ::: -A semântica da lógica proposicional também pode ser dada em formato de *atualização*. Fixe primeiro um conjunto de valorações como estado corrente e depois defina uma função de atualização que deixa apenas as valorações que satisfazem uma dada fórmula. +::::exercise (rating := 2) (name := "implies-from-list") +Nossa definição {name}`Formula.implies` relaciona duas fórmulas. Complete a definição abaixo para que possamos falar de `Γ ⊧ α`, a consequência lógica de um conjunto de fórmulas. ```lean -def update (vals : List Valuation) (f : Form) : List Valuation := - vals.filter (fun v => f.eval v) +def Formula.impliesL (hs : List Formula) (c : Formula) : Bool := + solution!((Formula.conjs hs).implies c) ``` +:::: -Atualizar o estado de todas as valorações com uma contradição não deixa nada; atualizar com uma tautologia não tira nada. Atualizar com uma fórmula contingente tira alguma coisa, e atualizar com sua negação tira o complemento. +::::exercise (rating := 2) (name := "pl-consequence") +Formalize as consequências lógicas abaixo completando o código como novos exemplos usnado termos do tipo {name}`Formula`. As duas primeiras já foram formalizada. -```lean -#eval form1.allVals -#eval (update form1.allVals form1) -#eval (update form1.allVals (.neg form1)) -#eval (update form2.allVals (.neg form2)) -``` +1. `p ⊧ p ∨ q` +2. `p, q ⊧ ¬ p` +3. `p → q ⊧ ¬p → ¬q` +4. `¬q ⊧ p→q` +5. `¬p, q→p ⊧ ¬q` -::::exercise (rating := 2) (name := "implies-list") -Estenda a checagem de implicação proposicional para o caso de uma lista de premissas. O tipo é `Form.impliesL : List Form → Form → Bool`. +Em todos os casos, para fechar ou não as provas, você só precisa da tática {tactic}`native_decide`. Note que quando existe consequência lógica, o tipo {lean}`Bool` pode ser promovido à `Prop` automaticamente pelo Lean, então você não precisa escrever `P.implies Q = true`, basta `P.implies Q`. Mas quando queremos mostrar que a consequência não é verdadeira, precisamos de `P.implies Q = false`. ```lean -def Form.impliesL (ps : List Form) (c : Form) : Bool := - solution!((Form.conjs ps).implies c) +namespace Cons + +def p : Formula := .atom "p" +def q : Formula := .atom "q" + +example : p.implies (.disj p q) := + by native_decide + +example : Formula.impliesL [p,q] (.neg p) = false := + by native_decide + +-- SOLUTION +example : (Formula.impl p q).implies (.impl (.neg p) (.neg q)) = false := + by native_decide + +example : (Formula.neg q).implies (.impl p q) = false := + by native_decide + +example + : Formula.impliesL [.neg p, .impl q p] (.neg q) = true := + by native_decide +-- END SOLUTION + +end Cons ``` :::: @@ -390,9 +513,9 @@ Complete a definição de `banguSolution` para que a fórmula represente a solu ```lean namespace Bangu -def banguSolution : Form := solution!(.conjs [A, (.neg J), C]) +def banguSolution : Formula := solution!(.conjs [A, (.neg J), C]) -example : Form.impliesL [depo1, depo2, depo3] banguSolution = true := +example : Formula.impliesL [depo1, depo2, depo3] banguSolution = true := solution!(by native_decide) end Bangu @@ -400,17 +523,90 @@ end Bangu ::: -# Traduzindo `Form` para `Prop` +A semântica da lógica proposicional também pode ser dada na forma de atualizações sobre valorações. Fixe primeiro um conjunto de valorações como estado corrente e depois defina uma função de atualização que deixa apenas as valorações que satisfazem uma dada fórmula. + +```lean +def update (vals : List Valuation) (f : Formula) : List Valuation := + vals.filter (fun v => f.eval v.toFun) +``` + +Atualizar o estado de todas as valorações com uma contradição não deixa nada; atualizar com uma tautologia não tira nada. Atualizar com uma fórmula contingente tira alguma coisa, e atualizar com sua negação tira o complemento. + +```lean +#eval form1.allVals +#eval (update form1.allVals form1) +#eval (update form1.allVals (.neg form1)) +#eval (update form2.allVals (.neg form2)) +``` + + +# Traduzindo `Formula` para `Prop` %%% tag := "pl-to-prop" %%% -O mapeamento de `Form` em `Prop` pode ser definido como uma função que interpreta cada fórmula como a proposição que ela afirma, dada uma valoração. +Dadas as definições da sintaxe e semântica de `PL`, Podemos provar alguns meta-teoremas sobre elas. Nos capítulos seguintes, estes resultados não serão necessariamente úteis, mas mostram que nossas definições estão consistentes. Os teoremas a seguir estão no nível da linguagem Lean, isto quer dizer que não são teoremas na linguagem `PL` mas sobre a linguagem `PL`. Abaixo provamos dois teoremas. O teorema `top_equiv_taut` diz que toda tautologia é equivalente a {name}`Formula.top`. O teorema `neg_taut_is_contradiction` diz que se uma fórmula é uma tautologia, sua negação é uma contradição. + +```lean +namespace MetaTheorems +open Formula + +theorem top_equiv_taut (f : Formula) : f.tautology ↔ f.equivalent top := by + have hv : (conj top (neg f)).allVals = f.allVals := rfl + simp only [equivalent, implies, + contradiction, satisfiable, tautology, hv, eval] + simp [List.all_eq_true] + +theorem neg_taut_is_contradiction (f : Formula) : + f.tautology ↔ (Formula.neg f).contradiction := by + have hv : (neg f).allVals = f.allVals := rfl + simp only [contradiction, satisfiable, tautology, eval, hv] + simp [List.all_eq_true] +``` + +E também podemos provar o princípio da contraposição. Temos que `F₁ ⊧ F₂` se e somente se `¬ F₂ ⊧ ¬F₁`. Expandindo a definição de {name}`Formula.implies` e {name}`Formula.satisfiable`, temos o enunciado do teorema `contraposition_principle₁`. A prova dele é direta, corresponde a avaliação da definição de {name}`Formula.eval` seguida da aplicação da comutativade da conjunção boleana. Mas ele não é o princípio diretamente. + +```lean +theorem contraposition_principle₁ (F₁ F₂ : Formula) (v : Valuation) : + (conj F₁ (neg F₂)).eval v.toFun = + (conj (neg F₂) (neg (neg F₁))).eval v.toFun := by + simp [Formula.eval] + exact Bool.and_comm _ _ +``` + +O teorema `contraposition_principle₂`, por outro lado, corresponde exatamente ao enunciado do princípio. Mas, para prová-lo, precisamos de alguns passos adicionais. Primeiro precisamos provar que todas as valorações possíveis para `F₁` coincidem com as de `F₂`. esta é nossa hipótese `hv`. Também precisamos mostrar que se duas listas são permutações entre si, então ordená-las irá produzir a mesma lista. Este é o teorema auxiliar `mergeSort_eq_of_perm`. A notação `List.perm_append_comm.dedup` corresponde a uma composição de provas. Lean resolve para a composição de {name}`List.Perm.dedup` com {name}`List.perm_append_comm`. Como o leitor pode imaginar, estes resultados auxiliares combinados com alguns outros teoremas adicionais, seriam suficientes para melhor automação da prova de `contraposition_principle₂` e outros teoremas ainda mais relevantes sobre `PL`. Mas nosso objetivo é somente ilustrar a capacidade de Lean em provar estes resultados. Finalmente, sugerimos que o leitor consulte {citep Bib.LLR}[] ou navegue pelas definições no seu editor, se desejar entender os todos os teoremas e tácticas usadas nas provas a seguir. ```lean -def Form.denote (f : Form) (v : Valuation) : Prop := +theorem mergeSort_eq_of_perm {xs ys : List String} + (h : xs.Perm ys) + : xs.mergeSort (· ≤ ·) = ys.mergeSort (· ≤ ·) := + ((List.mergeSort_perm xs _).trans + (h.trans (List.mergeSort_perm ys _).symm)).eq_of_pairwise' + (List.pairwise_mergeSort' _ _) (List.pairwise_mergeSort' _ _) + +theorem contraposition_principle₂ (F₁ F₂ : Formula) : + F₁.implies F₂ ↔ (Formula.neg F₂).implies (.neg F₁) := by + have hv : + (conj F₁ (neg F₂)).allVals = (conj (neg F₂) (neg (neg F₁))).allVals := by + simp [Formula.allVals, Formula.names, Formula.namesRaw] + exact congrArg genVals + (mergeSort_eq_of_perm List.perm_append_comm.dedup) + simp only [Formula.implies, Formula.contradiction, + Formula.satisfiable, hv, Formula.eval] + constructor + all_goals + · intro h + simpa [Bool.and_comm, Bool.not_not] using h + +end MetaTheorems +``` + +Finalmente, o mapeamento de {lean}`Formula` em `Prop` pode ser definido como uma função que interpreta cada fórmula como a proposição que ela afirma, dado um mapeamento de átomos em `Bool`. + +```lean +def Formula.denote (f : Formula) (v : String → Bool) : Prop := match f with - | .atom name => (v.lookup name).getD false = true + | .atom name => v name | .top => True | .bot => False | .neg g => ¬ g.denote v @@ -418,23 +614,27 @@ def Form.denote (f : Form) (v : Valuation) : Prop := | .disj g h => g.denote v ∨ h.denote v ``` -Repare no que cada caso faz: ele troca um construtor de `Form` pelo conectivo correspondente de `Prop`. O `conj` do dado vira o `∧` da proposição, o `neg` vira o `¬`. O teorema que fecha o capítulo diz que as duas leituras concordam. Dada uma valoração, computar o valor verdade de uma fórmula resulta em `true` exatamente quando a proposição resultande da fórmula para a mesma valoração tem prova. +Repare no que cada caso faz: ele troca um construtor de {lean}`Formula` pelo conectivo correspondente de `Prop`. O {lean}`Formula.conj` do dado vira o `∧` da proposição, o {name}`Formula.neg` vira o `¬`. O teorema que fecha o capítulo diz que as duas leituras concordam. Dada uma valoração, computar o valor verdade de uma fórmula resulta em `true` exatamente quando a proposição resultande da fórmula para a mesma valoração tem prova. ```lean -theorem Form.eval_iff_denote (f : Form) (v : Valuation) : +open Formula in + +theorem Formula.eval_iff_denote (f : Formula) (v : String → Bool) : f.eval v = true ↔ f.denote v := by induction f with - | atom name => simp [Form.eval, Form.denote] - | top => simp [Form.eval, Form.denote] - | bot => simp [Form.eval, Form.denote] + | atom name => simp [eval, denote] + | top => simp [eval, eval, denote] + | bot => simp [eval, eval, denote] | neg g ih => - simp only [Form.eval, Form.denote] + simp only [eval, eval, denote] at ih ⊢ rw [← ih] simp | conj g h ihg ihh => - simp [Form.eval, Form.denote, ihg, ihh] + simp only [eval, eval, denote] at ihg ihh ⊢ + simp [ihg, ihh] | disj g h ihg ihh => - simp [Form.eval, Form.denote, ihg, ihh] + simp only [eval, eval, denote] at ihg ihh ⊢ + simp [ihg, ihh] ``` ```lean diff --git a/CSwL/Logic/Proof.lean b/CSwL/Logic/Proof.lean index 69b01fb..6f75da0 100644 --- a/CSwL/Logic/Proof.lean +++ b/CSwL/Logic/Proof.lean @@ -24,9 +24,9 @@ namespace Proof # O tipo {lean}`Prop` e Provas -O que diferencia Lean de outras linguagens como Python e Java é a capacidade de na mesma linguagem que usamos para 'programar' funções, escrevermos 'provas' sobre estas funções. +O que diferencia Lean de outras linguagens como Python ou Java, é a capacidade de usarmos a mesma linguagem para programar funções e escrever provas sobre estas funções. -Uma proposição é um enunciado que pode ser verdadeiro ou falso. O enunciado `1 = 1` é verdadeiro, enquanto `square₁ 12 = 2` é falso. Toda proposição é todo tipo `Prop` {citep Bib.FAA2025}[]. Podemos declarar proposições, mas não podemos _avaliar_ uma proposição. Note que perguntar pelo tipo não é o mesmo que decidir se ela é verdadeira. +Uma proposição é um enunciado que pode ser verdadeiro ou falso. O enunciado `1 = 1` é verdadeiro, enquanto `square₁ 12 = 2` é falso. Toda proposição é um tipo em `Prop` {citep Bib.FAA2025}[]. Podemos declarar proposições, mas não podemos _avaliar_ uma proposição. Note que perguntar pelo tipo não é o mesmo que decidir se ela é verdadeira. ```lean def p₁ : Prop := 1 = 1 @@ -46,7 +46,7 @@ theorem OneEqSelf : 1 = 1 := Eq.refl 1 Acontece que, para propriedades um pouco menos triviais, o termo para provar uma proposição pode ficar grande e pouco natural de escrever manualmente. É aí que entra a palavra `by`. Ela introduz um _modo_ chamado 'tactic mode' onde usamos uma pequena linguagem de comandos (táticas) em que descrevemos como a prova deve ser montada e deixamos o Lean construir o termo por nós. -A tática {tactic}`rfl` prova igualdades quando os dois lados são iguais por definição, isto é, quando Lean consegue reduzi-los até a mesma expressão por computação. Essa redução inclui, por exemplo, a expansão de definições, a aplicação de funções e a avaliação de `let`. Isso é uma consequência importante da fundação de Lean em Calculus of Inductive Constructions (CiC) {citep Bib.nederpelt2014}[]: expressões de tipos e programas podem ser computadas e comparadas por redução. Assim, `rfl` é frequentemente usado para dizer que os dois lados são iguais porque são o mesmo valor depois de reduzir o código. O comando `#print double_theorem` irá mostrar que a tática {tactic}`rfl` construiu o termo {name}`Eq.refl`. +A tática {tactic}`rfl` prova igualdades quando os dois lados são iguais por definição, isto é, quando Lean consegue reduzi-los até a mesma expressão por computação. Essa redução inclui, por exemplo, a expansão de definições, a aplicação de funções e a avaliação de `let`. Isso é uma consequência importante da fundação de Lean em _Calculus of Inductive Constructions_ (CIC) {citep Bib.nederpelt2014}[]: expressões de tipos e programas podem ser computadas e comparadas por redução. Assim, `rfl` é frequentemente usado para dizer que os dois lados são iguais porque são o mesmo valor depois de reduzir o código. O comando `#print double_theorem` irá mostrar que a tática {tactic}`rfl` construiu o termo {name}`Eq.refl`. ```lean def double (n : Nat) := n + n @@ -54,7 +54,7 @@ def double (n : Nat) := n + n theorem double_theorem : double 5 = 5 + 5 := by rfl ``` -A tática {tactic}`rfl` tem limitações, embora possamos provar que duas funções são identificas a menos da sua mudança nos nomes dos parâmetros, precisamos do teorema sobre a comutatividade dos naturais para provar o segundo exemplo. +A tática {tactic}`rfl` só funciona quando os dois lados são idênticos por definição. Para propriedades que exigem leis algébricas (como a comutatividade da multiplicação), precisamos aplicar teoremas específicos, como {name}`Nat.mul_comm`. ```lean example (z : Nat) : (λ x ↦ 2 * x) z = (fun y => 2 * y) z := by @@ -64,13 +64,9 @@ example (z : Nat) : (λ x ↦ 2 * x) z = (fun y => y * 2) z := by exact Nat.mul_comm 2 z ``` -Além de {tactic}`rfl`, um pequeno repertório de táticas resolve o que os capítulos -seguintes precisam. - - ::::exercise (rating := 1) (name := "rfl-arithmetic") -Complete a prova abaixo usando a tática {tactic}`rfl`. Esta é a primeira prova que do [Natural Number Game](https://adam.math.hhu.de/#/g/leanprover-community/nng4/). O leitor está convidado a jogar NNG para uma boa introdução a provas no Lean. +Complete a prova abaixo usando a tática {tactic}`rfl`. Esta é a primeira prova do [Natural Number Game](https://adam.math.hhu.de/#/g/leanprover-community/nng4/). O leitor está convidado a jogar NNG para uma boa introdução a provas no Lean. ```lean example (x q : Nat) : 37 * x + q = 37 * x + q := @@ -89,7 +85,7 @@ namespace PL Os conectivos lógicos `∧`, `∨`, `→`, `↔` e `¬` estão disponíveis diretamente no Lean, de modo que uma fórmula proposicional pode ser representada como uma proposição em Lean. Isso nos fornece uma ponte conveniente entre a semântica da linguagem natural e o raciocínio formal. Podemos traduzir o conteúdo semântico de uma sentença para uma proposição em Lean e, em seguida, usar Lean para verificar se uma conclusão decorre de um conjunto de hipóteses. -Chamamos "sistema dedutivo" um conjunto das regras de dedução. Existem vários sistemas dedutivos. A formalização de Prop em Lean corresponde a implementação do sistema chamado *dedução natural* definido por Gerhard Gentzen em 1930s. Usando as regras de dedução natural, podemos provar que uma fórmula `α` pode ser derivada a partir de um conjunto de fórmulas `Γ`, dizemos que `Γ ⊢ α`. Dizemos que `⊢ α` quando a fórmula `α` é válida, uma tautologia. +Chamamos "sistema dedutivo" um conjunto das regras de dedução. Existem vários sistemas dedutivos. A formalização de Prop em Lean corresponde a implementação do sistema chamado *dedução natural* definido por Gerhard Gentzen em 1930. Usando as regras de dedução natural, podemos provar que uma fórmula `α` pode ser derivada a partir de um conjunto de fórmulas `Γ`, dizemos que `Γ ⊢ α`. Dizemos que `⊢ α` quando a fórmula `α` é válida, uma tautologia. Neste sistema dedutivo, cada conectivo vem com dois tipos de regra. As de *introdução*, que dizem como construir uma prova cuja conclusão usa o conectivo, e as de *eliminação*, que dizem como usar uma prova cuja hipótese o usa. @@ -97,7 +93,9 @@ Neste sistema dedutivo, cada conectivo vem com dois tipos de regra. As de *intro variable {P Q R : Prop} ``` -A regra de introdução de `→` diz que para provar `P → Q`, supomos `P` e derivamos `Q`. A tatica `intro` move o antecedente para as hipóteses. A regra de eliminação é a chamada regra *modus ponens*. De `P → Q` e de `P`, conclua `Q`. Em Lean isso é aplicação `h hP` já é a prova de `Q`. A tática `apply` faz o mesmo de trás para frente, ela transforma o objetivo `Q` no objetivo `P`. A {tactic}`exact` fecha a prova indicando a hipótese cujo tipo corresponde ao _goal_ aberto. A {tactic}`assumption` fecha o _goal_ quando o tipo de alguma das hipóteses corresponde ao tipo do _goal_, sem precisarmos passar a hipótese nominalmente, como quando usamos {tactic}`exact`. +A regra de introdução de `→` diz que para provar `P → Q`, supomos `P` e derivamos `Q`. A tatica `intro` move o antecedente para as hipóteses. + +A regra de eliminação é a chamada regra *modus ponens*. A partir de `P → Q` e de `P`, podemos concluir `Q`. O termo Lean `h hP` já é a prova de `Q`. A tática `apply` faz o mesmo de trás para frente, ela transforma o objetivo `Q` no novo objetivo `P`. A {tactic}`exact` fecha a prova fornecendo a hipótese cujo tipo coincide com o tipo do objetivo. A {tactic}`assumption` busca automaticamente se alguma hipótese do contexto coincide com o objetivo, sem que seja necessário nomeá-la explicitamente. ```lean example : P → (Q → P) := by @@ -113,7 +111,7 @@ example (h₁ : P → Q) (h₂ : Q → R) : P → R := by example (h : P → Q) (hP : P) : Q := h hP ``` -Para a conjunção. Provar `P ∧ Q` depende de uma prova de `P` e `Q`. A tática `constructor` parte o objetivo em dois; o construtor anônimo `⟨_, _⟩` faz o mesmo em forma de termo. A eliminação de `∧` em `P ∧ Q` significa que podemos concluir `P` ou `Q`. São duas regras, e em Lean são as projeções `.1` (ou `.left`) e `.2` (ou `.right`). A tática `obtain` desmonta a hipótese de uma vez, dando nome às duas partes. +Para a conjunção, provar `P ∧ Q` depende de uma prova de `P` e de uma prova de `Q`. A tática {tactic}`constructor` divide o objetivo em dois novos objetivos; o construtor anônimo `⟨_, _⟩` faz o mesmo em forma de termo. A eliminação de `∧` em `P ∧ Q` significa que podemos concluir `P` ou `Q`. São duas regras, e em Lean são as projeções `.1` (ou `.left`) e `.2` (ou `.right`). A tática `obtain` desmonta a hipótese de uma vez, dando nome às duas partes. ```lean @@ -132,8 +130,7 @@ example (h : P ∧ Q) : Q ∧ P := by example (h : P ∧ Q) : Q ∧ P := ⟨h.2, h.1⟩ ``` -Para provar `P ∨ Q` basta provar um dos dois lados. São duas regras, e as táticas `left` e `right` escolhem qual. A eliminação de `∨` é a prova por casos. De `P ∨ Q` não se sabe qual dos dois vale. Para concluir `R` a partir dela é preciso concluir `R` nos dois casos. A tática `cases` abre exatamente esses dois objetivos. - +Para provar `P ∨ Q` basta provar um dos dois lados. São duas regras, e os construtores {name}`Or.inl` (aplicado pela tática {tactic}`left`) e {name}`Or.inr` (aplicado pela tática {tactic}`right`) formalizam elas. A regra de eliminação da disjunção é o teorema {name}`Or.elim`, a chamada "prova por casos". Dada a hipótese `P ∨ Q`, não sabemos qual das duas proposições é verdadeira. Portanto, para concluir `R`, precisamos provar `R` em ambos os casos (assumindo `P` no primeiro e `Q` no segundo). A tática {tactic}`cases` gera exatamente esses dois cenários. ```lean example (hP : P) : P ∨ Q := by @@ -146,8 +143,7 @@ example (h : P ∨ Q) : Q ∨ P := by | inr hQ => left; exact hQ ``` -Não há um conectivo primitivo para a negação: `¬ P` é notação para `P → False` onde `False` é a proposição sem nenhuma prova. A introdução de `¬` é a introdução de `→`, para provar `¬P`, suponha `P` e derive `False`. A eliminação é a eliminação de `→`. A regra que a tradição chama de *ex falso quodlibet* (princípio da explosão), é uma regra que dita que, a partir de uma contradição ou de uma premissa falsa, qualquer conclusão pode ser deduzida. `False.elim` em Lean. As duas juntas são `absurd`. - +Não há um conectivo primitivo para a negação: `¬ P` é notação para `P → False` onde `False` é a proposição que não possui prova. Desta forma, a introdução da negação usa a mesma regra da introdução da implicação `→`. Para provar `¬P`, supomos `P` para derivar `False`. A eliminação é a eliminação de `→`. A regra que a tradição chama de *ex falso quodlibet* (princípio da explosão), a partir de uma contradição ou de uma premissa falsa, qualquer conclusão pode ser deduzida. `False.elim` em Lean. As duas juntas são `absurd`. ```lean example (h : P → Q) : ¬Q → ¬P := by @@ -159,7 +155,7 @@ example (h : False) : P := False.elim h example (hP : P) (hn : ¬P) : Q := absurd hP hn ``` -A `P ↔ Q` é a conjunção das duas implicações, e as regras seguem disso. A tática `constructor` parte o objetivo nas duas direções, e `.mp` e `.mpr` são as eliminações de `P → Q` e de `Q → P`. +A bicondicional `P ↔ Q` é definida como a conjunção das duas implicações ((P → Q) ∧ (Q → P)), a tática {tactic}`constructor` evoca {name}`Iff.intro` que transforma o objetivo da prova em duas provas, uma para cada implicação. Os parâmetros do construtor explicam as regras de eliminação, duas regras dado tratar-se de uma conjunção de implicações, {name}`Iff.mpr` e {name}`Iff.mp`. ```lean example : P ∧ Q ↔ Q ∧ P := by @@ -170,7 +166,10 @@ example : P ∧ Q ↔ Q ∧ P := by example (h : P ↔ Q) (hP : P) : Q := h.mp hP ``` -Até aqui não usamos em nenhum momento "ou `P` vale ou não vale". Todas as regras até aqui são *construtivas*, uma prova de `P ∨ Q` traz consigo qual dos dois lados foi usado. Uma prova de `P` é uma construção de `P`. O raciocínio *clássico* acrescenta o princípio chamado de terceiro excluído. Dele saem as duas táticas. A primeira é `by_cases`, que parte a prova em dois casos, supondo `P` num e `¬P` no outro. E a tatica `by_contra` prova `P` supondo `¬P` e derivando `False`, a redução ao absurdo. +Até este ponto, todas as regras que utilizamos pertencem à *lógica construtiva* (ou intuicionista). Nela, provar uma disjunção `P ∨ Q` exige construir explicitamente uma prova de `P` ou uma prova de `Q`. Não é permitido afirmar que "um dos dois é verdade" sem saber qual. Em particular, a lógica construtiva não assume que toda proposição é necessariamente verdadeira ou falsa. A *lógica clássica* acrescenta o princípio do terceiro excluído, {name}`Classical.em`, que afirma que para qualquer proposição `P`, vale `P ∨ ¬P`. A partir desse princípio, derivamos duas táticas fundamentais para provas clássicas: + +- {tactic}`by_cases`. Quando usamos `by_cases (hP : P)`, o objetivo atual é dividido em dois casos independentes, um assumindo `hP : P` (`P` é verdadeiro) e outro assumindo `hP : ¬P` (`P` é falso). +- {tactic}`by_contra`: Realiza a prova por redução ao absurdo. Para provar `P`, supõe-se que `¬ P` e o objetivo torna-se derivar uma contradição (False). ```lean example : P ∨ ¬P := Classical.em P @@ -230,19 +229,13 @@ example : (P → Q) ↔ (¬Q → ¬P) := solution!(by ::::exercise (rating := 1) (name := "exchange-prop") -Complete a representação do argumento abaixo em linguagem lógica. - Se o câmbio cair, temos inflação. Se as exportações crescerem, diminuímos o déficit. O câmbio cai ou diminuímos o déficit. Logo, temos inflação ou as exportações crescem. +complete a definição `exchange` para formalizar o parágrafo anterior. Você deverá usar as variáveis proposicionais declaradas para `p` (câmbio cai), `q` (temos inflação), `r` (exportações crescem) e `s` (diminuimos o déficit) para construir a proposição esperada. + ```lean section - -variable ( - p -- o câmbio cai - q -- temos inflação - r -- as exportações crescem - s -- Diminuimos o déficit - : Prop) +variable (p q r s : Prop) def exchange : Prop := solution!( @@ -254,7 +247,7 @@ end ::::exercise (rating := 2) (name := "implication-as-disj") -Complete a prova abaixo. Note que esta prova precisa do fragmento clássico, tente usar {tactic}`by_cases`. +Complete a prova abaixo. Note que esta prova precisa do fragmento clássico. Tente usar {tactic}`by_cases`. ```lean example (P Q : Prop) : (P → Q) → ¬ P ∨ Q := by @@ -302,7 +295,7 @@ example (P Q R : Prop) (h : P → Q) (h2 : Q → R) : P → R := by :::: ::::exercise (rating := 1) (name := "unfold-direct-proof") -Em algumas provas, podemos precisar expandir uma definição antes de qualquer outro passo de manipulação dos conectivos lógicos. Logo após introduzir o antecedente da implicaçõa como hipótese, considere `unfold E at h` para expandir a definição de `E` na hipótese recém introduzida `h`. Feche a prova com a táctica {tactic}`linarith`. +Em algumas provas, podemos precisar expandir uma definição antes de qualquer outro passo de manipulação dos conectivos lógicos. Logo após introduzir o antecedente da implicação como hipótese, considere `unfold E at h` para expandir a definição de `E` na hipótese recém introduzida `h`. Feche a prova com a táctica {tactic}`linarith`. ```lean def E (x y : Nat) : Prop := x = y @@ -351,7 +344,7 @@ namespace Dresses variable (Aa Ab Ap Ma Mb Mp Ca Cb Cp : Prop) ``` -A ideia é que as condições do problema sejam traduzidas em fórmulas proposicionais. Por exemplo, podemos formalizar a sentença "Ana veste azul, branco ou preto" como {lean}`Aa ∨ Ab ∨ Ap`. Note que a fórmula não foi obtida diretamente a partir da construção linguística original, uma oração coordenando seus constituintes no predicado. Intuitivamente, a sentença foi antes interpretada como três orações coordenadas, "Ana veste azul ou Ana veste branco ou Ana veste preto". +A ideia é que as condições do problema sejam traduzidas em fórmulas proposicionais. Por exemplo, podemos formalizar a sentença "Ana veste azul, branco ou preto" como {lean}`Aa ∨ Ab ∨ Ap`. Note que a fórmula não foi obtida diretamente a partir da construção linguística original, uma oração coordenando seus constituintes no predicado. Intuitivamente, a sentença foi antes interpretada como três orações coordenadas: "Ana veste azul ou Ana veste branco ou Ana veste preto". A formalização completa do problema deve levar em consideração não apenas o que foi dito explicitamente mas algumas condições implicitamente assumidas. Primeiro que cada irmã veste uma das cores. @@ -393,15 +386,10 @@ variable (h4 : Ap → Cb) variable (h5 : Cp → ¬ Cb) ``` -Complete a prova do teorema, provando que o problema dos vestidos tem a solução onde Ana veste preto, Cláudia veste branco e Maria veste azul. A declaração `include ... in` irá incluir todas as variáveis declaradas anteriormente como parâmetros para o teorema seguinte. +Complete a prova do teorema, provando que o problema dos vestidos tem a solução onde Ana veste preto, Cláudia veste branco e Maria veste azul. A declaração `include ... in` irá incluir as variáveis declaradas (as hipóteses) anteriormente que efetivamente são necessárias como parâmetros para o teorema seguinte. A inclusão de hipóteses desnecessárias irá emitir um alerta, mas não um erro. ```lean -include - hA hM hC - ha hb hp - hA1 hM1 hC1 - ha1 hb1 hp1 - h1 h2 h3 h4 h5 in +include hA ha hC1 h1 h3 h4 in theorem vestidos : Ap ∧ Cb ∧ Ma := by @@ -444,14 +432,14 @@ end Dresses end PL ``` -# As regras dos quantificadores em Lean +# As regras dos Quantificadores em Lean %%% tag := "quantificadores-lean" %%% -O mesmo tipo `Prop` em Lean não está limitado ao raciocínio proposicional. Também podemos representar lógica de primeira ordem em `Prop`. Como já falamos, o Lean se baseia em na teoria dos tipos, na qual se assume que cada variável pertence a algum tipo. Você pode pensar em um tipo como um "universo" ou um "domínio de discurso", no sentido da lógica de primeira ordem. Com a diferença importante de que em lógica de primeira ordem, entedemos o domínio da interpretação com um conjunto não vazio, e um tipo em Lean não necessariamente precisa ser _habitado_. +O tipo {lean}`Prop` não está limitado ao raciocínio proposicional; ele também nos permite representar proposições da lógica de primeira ordem. Como vimos, o Lean é fundamentado na teoria dos tipos, na qual toda variável pertence a algum tipo. Podemos entender um tipo como o "universo" ou "domínio de discurso" da lógica formal. No entanto, como veremos, há uma diferença importante: enquanto a lógica de primeira ordem clássica exige que o domínio de interpretação seja sempre um conjunto não-vazio, em Lean um tipo não precisa ser necessariamente habitado. -A expressividade de `Prop` vai além de lógica de primeira ordem. Poderíamos ainda falar de lógicas [polissortidas](https://en.wikipedia.org/wiki/First-order_logic) onde poderíamos ter mais de um tipo usado em uma mesma expressão lógica. Por exemplo, podemos querer usar a lógica de primeira ordem para geometria, com quantificadores sobre pontos e linhas. Mas nesta seção, nos restringimos os predicados a um único universo `U`. +A expressividade de {lean}`Prop` vai além de lógica de primeira ordem. Poderíamos ainda falar de lógicas [polissortidas](https://en.wikipedia.org/wiki/First-order_logic) onde poderíamos ter mais de um tipo usado em uma mesma expressão lógica. Por exemplo, podemos querer usar a lógica de primeira ordem para geometria, com quantificadores sobre pontos e linhas. Mas nesta seção, nos restringimos os predicados a um único universo `U`. ```lean section FOL @@ -460,10 +448,9 @@ variable (U : Type) variable (P Q : U → Prop) ``` -Seguindo a apresentação de Lógica Proposicional, quatro novas regras precisam ser explicadas, duas para cada quantificador. +Seguindo a estrutura da seção anterior, explicaremos quatro novas regras: duas para o quantificador universal (`∀`) e duas para o existencial (`∃`). -A introdução de `∀` diz que para provar que algo vale de todo `x`, tome um `x` -arbitrário e prove que vale para ele. É a mesma `intro` agora sobre um objeto em vez de uma hipótese. A eliminação de `∀` é aplicação: de `∀ x P x` e de um objeto `d`, sai `P d`. +A introdução de `∀` estabelece que, para provar que uma propriedade vale para todo `x`, basta tomar um `x` arbitrário e demonstrar que a propriedade se aplica a ele. Em modo de tática, usamos a mesma tática {tactic}`intro`, mas agora ela adiciona um novo objeto no contexto, também como variável do tipo apropriado, em vez de uma hipótese do tipo {lean}`Prop`. A eliminação de `∀` é feita por aplicação direta: se temos uma prova `h : ∀ x, P x` e um objeto `d`, a aplicação `h d` nos fornece uma prova de `P d`, desde que os tipos obviamente sejam compatíveis. ```lean example (h : ∀ x, P x) : ∀ y, P y := by @@ -471,7 +458,7 @@ example (h : ∀ x, P x) : ∀ y, P y := by 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. +A introdução de `∃` exige uma testemunha (o objeto que satisfaz a propriedade). Em modo de tática, a tática {tactic}`use` substitui a variável quantificada pelo objeto fornecido e deixa como novo objetivo a prova de que tal objeto satisfaz o predicado. Em modo de termo, isso é feito pelo construtor {name}`Exists.intro`. ```lean example (y : U) (h : P y) : ∃ x, P x := @@ -481,7 +468,7 @@ example (y : U) (h : P y) : ∃ x, P x := by use y ``` -A eliminação de `∃` é a mais delicada. De `∃ x P x` sabe-se que há uma testemunha, mas não sabemos qual elemento do domínio ela é. A tática `obtain` aplica o teorema `Exists.elim`, introduz com um nome, junto com a propriedade que ele satisfaz. +A eliminação de `∃` é a regra mais delicada. De `∃ x, P x` sabe-se que há uma testemunha, mas não sabemos qual elemento do domínio usar. A tática {tactic}`obtain` aplica o teorema {name}`Exists.elim`, introduzindo a testemunha com um nome no contexto, junto com a propriedade que ela satisfaz. ```lean example (h : ∃ x, P x ∧ Q x) : ∃ x, Q x := by @@ -495,7 +482,9 @@ example (h : ∃ x, P x ∧ Q x) : ∃ x, Q x := by exact ⟨d, hQ⟩ ``` -A demonstração abaixo não é válida se não declararmos uma variável `u : U`, mesmo que `u` não apareça no enunciado do teorema. Isso destaca uma diferença entre a lógica de primeira ordem e a lógica implementada em Lean. Na dedução natural, podemos provar `∀ x P x → ∃ x P x`, o que mostra que nosso sistema de prova assume implicitamente que o universo tem pelo menos um objeto. Em contraste, em Lean, é possível que um tipo esteja vazio, e, portanto, a prova requer uma suposição explícita de que existe um elemento `u : U`. +Tendo apresentado as regras de introdução e eliminação dos quantificadores, é importante observar como o Lean trata a existência de valores em um tipo na prática. + +A demonstração abaixo de `(∀ x, P x) → ∃ x, P x` só é válida se declararmos previamente uma variável `u : U`. Isso evidencia uma diferença sutil entre a lógica de primeira ordem tradicional e a implementação no Lean: enquanto a dedução natural clássica assume implicitamente que o universo de discurso é sempre não-vazio, no Lean um tipo pode ser vazio (não-habitado). Assim, para instanciar a testemunha com `use u`, precisamos fornecer a suposição explícita de que existe ao menos um elemento `u : U`. Uma outra forma de ter o mesmo efeito seria demandar que o tipo `U` implemente a classe {name}`Nonempty`. ```lean variable (u : U) @@ -540,9 +529,9 @@ end FOL tag := "induction" %%% -Outra tática de prova que podemos precisar é a {tactic}`induction`. Ela prova algo para todo valor de um tipo indutivo, e não para um valor de cada vez. +Uma das ferramentas fundamentais no Lean é a tática {tactic}`induction`. Em vez de provar uma propriedade para elementos individuais, ela permite demonstrar que uma afirmação é válida para todos os valores de um tipo indutivo (como os `Nat`). -Considere o exemplo abaixo e a esperada _prova por indução_ que faríamos no papel. Mostramos para o caso base, que em `Nat` é o `zero` e depois o passo indutivo, cuja hipótese de indução é nomeada como `ih`. +Considere o exemplo abaixo de uma prova por indução. Primeiro, demonstramos a propriedade para o caso onde `n` é o termo {name}`Nat.zero`. Em seguida, provamos o passo indutivo, quando `n` é um termo gerado pelo construtor {name}`Nat.succ` e quando assumimos que a propriedade vale para um `a` (armazenada na hipótese de indução `ih`) e demonstramos que ela se mantém para o seu sucessor `a + 1`. ```lean example (n : Nat) : n + 0 = n := by @@ -552,16 +541,14 @@ example (n : Nat) : n + 0 = n := by linarith ``` -Ao longo do texto, outras táticas poderão ser usadas como: {tactic}`decide`, {tactic}`omega`, -{tactic}`simp` e {tactic}`funext`, discutiremos quando forem necessárias. - - # Extensionalidade de Funções %%% tag := "funext" %%% -Uma função admite duas leituras. Na leitura extensional, a função é uma tabela: o conjunto de pares entrada e saída. Uma conversão de Celsius para Fahrenheit é a tabela `[(0, 32), (100, 212),...]`. Na leitura intensional, a função indica como a saída é obtida a partir da entrada `λ x ↦ x * 9 / 5 + 32`. Uma receita que produz a tabela sem precisar listá-la. Em Lean, `def` escreve sempre a versão intensional, mas duas instruções diferentes podem ser a mesma função, no sentido extensional, se produzem a mesma tabela. É isso que `funext` verifica: duas funções são iguais quando concordam em todo ponto do domínio. +Uma função pode ser compreendida sob duas perspectivas. Na perspectiva extensional, a função é vista como uma relação ou tabela de mapeamento — o conjunto de todos os pares de entrada e saída, como a tabela `{(0, 32), (100, 212), ...}`. Na perspectiva intensional, a função é o próprio algoritmo ou instrução que calcula a saída a partir da entrada, como a expressão {lean}`λ x ↦ x * 9 / 5 + 32`, uma "receita" que gera a tabela sem precisar enumerá-la. + +No Lean, o comando `def` sempre define funções no sentido intensional. No entanto, duas definições intencionalmente distintas podem representar a mesma função no sentido extensional, desde que produzam a mesma saída para cada entrada. É esse o princípio da extensionalidade de funções: a tática {tactic}`funext` transforma o objetivo de provar que duas funções são iguais (`f = g`) no objetivo de demonstrar que elas coincidem para todo ponto do domínio para o qual são definidas. ```lean def double₁ (x : Nat) := 2 * x @@ -573,6 +560,21 @@ example : double₁ = double₂ := by exact (Nat.two_mul n) ``` +# Outras Táticas +%%% +tag := "tactics" +%%% + +No Lean, as táticas {tactic}`decide` e {tactic}`native_decide` têm a mesma ideia básica. São usadas para provar uma proposição por computação, como existe uma instância {name}`Decidable`. Mas executam essa computação de formas diferentes. A {tactic}`decide` executa dentro do próprio kernel do Lean. É simples e totalmente baseada na redução dos termos para formas normais do Lean, mas pode ser lenta para computações grandes. A {tactic}`native_decide` faz a mesma decisão, porém compila a computação para código nativo antes de executá-la. + +```lean +example : (List.range 100000).length = 100000 := by + native_decide +``` + +Outras táticas como {tactic}`omega` e {tactic}`simp` aparecerão em momentos específicos dos capítulos seguintes e serão explicadas à medida que se fizerem necessárias. + + ```lean end Proof ``` diff --git a/CSwL/SeaBattle.lean b/CSwL/SeaBattle.lean index b00e9c0..0d578e2 100644 --- a/CSwL/SeaBattle.lean +++ b/CSwL/SeaBattle.lean @@ -17,8 +17,7 @@ htmlSplit := .never file := "SeaBattle" %%% -Como definir uma língua — no sentido amplo: um conjunto de strings bem -formadas — por meio de uma gramática. O exemplo é a linguagem de um jogo. +Como definir uma língua — no sentido amplo: um conjunto de strings bem formadas — por meio de uma gramática. O exemplo é a linguagem de um jogo. # Sintaxe @@ -82,19 +81,7 @@ structure Turn where deriving DecidableEq, Repr ``` -Um `Attack` basicamente corresponde a uma coordenada, as colunas poderiam ter sido modeladas como as linhas, o que tornaria o design mais simples. Mas preferimos seguir o estilo de coordenadas usual, que facilita a leitura e associação de letras a colunas e números para linhas. - -O tipo `Fin 10` corresponde os números naturais menores que 10. O termo `(10 : Fin 10)` corresponde ao `0` (`10 % 10`, via `OfNat`), mas isso só vale para o literal `10` interpretado nesse tipo. A instância `OfNat (Fin 10) 10` (usada ao escrever `10 : Fin 10`) normaliza o literal por `% 10` antes de guardá-lo. O construtor `⟨n, prova⟩` (`Fin.mk`) exige uma prova de `n < 10` como dado — para `n = 10` essa prova não existe (`10 < 10` é falso), então `⟨10, by omega⟩` sequer elabora. Ou seja, `(10 : Fin 10)` sempre existe via módulo, e `(⟨10, _⟩ : Fin 10)` só existe para `n` de fato menor que `10`. - -```lean -#eval (10 : Fin 10) -#eval (11 : Fin 10) - -example : (11 : Fin 10) = 1 := rfl -example : ⟨0, by omega⟩ = (0 : Fin 10) := rfl -``` - -Se `Column` também fosse um `Fin 10` então poderíamos modelar com um par `Attack : Fin 10 × Fin 10`. +Um `Attack` basicamente corresponde a uma coordenada, as colunas poderiam ter sido modeladas como as linhas, o que tornaria o design mais simples. Mas preferimos seguir o estilo de coordenadas usual, que facilita a leitura e associação de letras a colunas e números para linhas. Se `Column` também fosse um `Fin 10` então poderíamos modelar com um par `Attack : Fin 10 × Fin 10`. Uma possível extensão de nossa gramática seria representar como sentença um jogo completo entre dois jogadores. diff --git a/CSwL/Sets.lean b/CSwL/Sets.lean index 6df090e..2832fe8 100644 --- a/CSwL/Sets.lean +++ b/CSwL/Sets.lean @@ -453,16 +453,6 @@ um domínio de duas entidades, e a relação de gostar entre elas. O domínio de entidades. Duas bastam para os exemplos deste capítulo. -:::dev -`Sets.Entity` and `FOL.Entity` are two different types with the same name. -Nothing breaks — each lives in its own namespace, and no file opens both — but -a reader who meets `Entity` twice with different constructors may take them for -one type. The collision was accepted deliberately: `Entity` is the right name -in both places, and renaming either to something like `Ent2` or `SetEntity` -would cost more in clarity than the ambiguity costs. If a later chapter ever -needs both in scope at once, that is when to revisit it. -::: - ```lean inductive Entity where | dorothy | toto diff --git a/CSwLMeta.lean b/CSwLMeta.lean index 2dc8fe7..41245ae 100644 --- a/CSwLMeta.lean +++ b/CSwLMeta.lean @@ -1,9 +1,11 @@ -- Adapted from sf-in-lean/SFLMeta.lean, with only the modules --- CSwL uses (`sf-in-lean` also has Details, Epigraph, Hide, Ignore, +-- CSwL uses (`sf-in-lean` also has Epigraph, Hide, Ignore, -- Instructors, SlideBreak, Theme, Version, and Volume). -- Adding one of those is copying the file and adding an `import` here. import CSwLMeta.Bnf import CSwLMeta.Comment +import CSwLMeta.Details +import CSwLMeta.Diagrams import CSwLMeta.DisplayMath import CSwLMeta.Exercise import CSwLMeta.Grade diff --git a/CSwLMeta/Details.lean b/CSwLMeta/Details.lean new file mode 100644 index 0000000..7af11ad --- /dev/null +++ b/CSwLMeta/Details.lean @@ -0,0 +1,127 @@ +-- Adapted from sf-in-lean/SFLMeta/Details.lean +-- (namespace SFLMeta -> CSwLMeta). +import VersoManual + +open Lean Elab +open Verso ArgParse Doc Elab Genre.Manual +open Verso.Output.Html + +namespace CSwLMeta + +/-! ## `:::details` directive + +A collapsible disclosure block: the optional positional `summary` string is +shown by default as a one-line teaser; the contents are revealed only when the +reader expands the block. When omitted, the summary is empty. +Useful for tucking away encoding details (macro plumbing, helper notation) that +aren't part of the main narrative. + +Author syntax: + +````markdown +:::details "Lean encoding" +The macros below set up the `<{ … }>` notation for STLC terms. + +```lean +… +``` +::: +```` + +HTML output uses native `
` / `` so it works without JS. +TeX output renders the summary as italic running text followed by the +contents. The saver emits the contents unwrapped — collapsibility is a UI +concern, not part of the source. -/ + +/-- Configuration for `:::details`. -/ +structure DetailsConfig where + /-- The clickable teaser shown when the block is collapsed. Empty when + omitted. -/ + summary : Option String +deriving Repr + +section +variable [Monad m] [MonadError m] + +def DetailsConfig.parse : ArgParse m DetailsConfig := + DetailsConfig.mk <$> ((some <$> .positional `summary .string) <|> pure none) + +instance : FromArgs DetailsConfig m := ⟨DetailsConfig.parse⟩ + +end + +block_extension Block.details (summary : String) where + data := Json.str summary + traverse _ _ _ := pure none + toHtml := + open Verso.Output.Html in + some fun _ goB _ data contents => do + let summary := + match data with + | .str s => s + | _ => "" + let body : Verso.Output.Html ← contents.foldlM (init := .empty) fun acc b => + return acc ++ (← goB b) + return {{ +
+ {{summary}} + {{body}} +
+ }} + toTeX := + open Verso.Output.TeX in + some fun _ goB _ data contents => do + let summary := + match data with + | .str s => s + | _ => "" + let body : Verso.Output.TeX ← contents.foldlM (init := .empty) fun acc b => + return acc ++ (← goB b) + if summary.isEmpty then + pure body + else + pure <| .seq #[.raw s!"\\textit\{{summary}.} ", body] + extraCss := [ +r##" +details.sf-details { + margin: 1em 0; + padding: 0.4em 0.8em; + border-left: 3px solid var(--sf-rule, #ccc); + background: rgba(0, 0, 0, 0.015); + border-radius: 2px; +} +details.sf-details > summary { + cursor: pointer; + font-family: var(--verso-structure-font-family); + font-weight: 600; + color: var(--sf-heading, inherit); + list-style: none; +} +details.sf-details > summary::-webkit-details-marker { display: none; } +details.sf-details > summary::before { + content: "▸ "; + display: inline-block; + width: 1em; + transition: transform 120ms ease-in-out; +} +details.sf-details[open] > summary::before { + content: "▾ "; +} +details.sf-details[open] { + background: rgba(0, 0, 0, 0.03); +} +"## + ] + +/-- A `:::details "…"` directive wraps its contents in a collapsible +disclosure block. The summary string is optional (defaults to the empty +string, in which case no teaser text is shown). -/ +@[directive] +def details : DirectiveExpanderOf DetailsConfig + | cfg, contents => do + let blocks ← contents.mapM elabBlock + ``(Verso.Doc.Block.other + (CSwLMeta.Block.details $(quote (cfg.summary.getD ""))) + #[$blocks,*]) + +end CSwLMeta diff --git a/CSwLMeta/Diagrams.lean b/CSwLMeta/Diagrams.lean new file mode 100644 index 0000000..9d1a8e0 --- /dev/null +++ b/CSwLMeta/Diagrams.lean @@ -0,0 +1,65 @@ +-- Adapted from sf-in-lean/SFLMeta/Diagrams.lean. +-- +-- Vector diagrams used by the book chapters. +-- +-- These live under `CSwLMeta` rather than beside the chapter that uses them +-- because they are authoring-framework code: the extracted `.lean` projects +-- drop `CSwLMeta` imports (a diagram is replaced there by its ASCII alt text), +-- whereas a module under a chapter prefix would be bundled into them verbatim, +-- carrying an `Illuminate` dependency the extracted project does not have. + +import Illuminate + +open Illuminate + +namespace CSwLMeta.Diagrams + +/-- +A self-loop drawn above the node at `p`: a cubic that leaves the node's +upper left, arcs over it, and re-enters at the upper right. + +This is built by hand because `commDiag`'s own arrows cannot draw one. For a +morphism whose source and target coincide, `buildArrow` computes a zero +direction vector, so both the bend offset (`bend * dir.length * 0.3`) and the +arrowhead direction collapse to zero: the emitted path is `M30 0 C30 0 30 0 30 +0`, a curve from a point to itself, and nothing is visible. +-/ +private def selfLoop (p : Vec2) : Diagram SVG := + let r : Float := 11 -- where the loop meets the node + let h : Float := 18 -- how far above the node it arcs + let start : Vec2 := ⟨p.x - r, p.y - r⟩ + let stop : Vec2 := ⟨p.x + r, p.y - r⟩ + let c1 : Vec2 := ⟨p.x - h, p.y - h - r⟩ + let c2 : Vec2 := ⟨p.x + h, p.y - h - r⟩ + let shaft := Diagram.fromStroke + (PathData.empty |>.moveTo start |>.curveTo c1 c2 stop) + Stroke.defaultArrow + let (head, _) := ArrowDraw.drawArrowhead ({} : Arrowhead) stop + (Vec2.sub stop c2) Stroke.defaultArrow + Diagram.atop head shaft + +/-- +The directed graph of the model in `Logic/FOL`'s semantics section: four +vertices `a`, `b`, `c`, `d` and the edge relation +`{⟨a,b⟩, ⟨b,a⟩, ⟨b,c⟩, ⟨c,c⟩}`. + +`a` and `b` point at each other, so their two arrows are bent apart to keep +both visible. `c` carries a loop, and `d` is isolated — it is the witness for +`∃x ∀y ¬E y x`, which is what the section's first example formula asserts. +-/ +def edgeGraph : Diagram SVG := + let base : Diagram SVG := commDiag do + let a ← CommDiagM.node "a" + let b ← CommDiagM.node "b" + let c ← CommDiagM.node "c" + let d ← CommDiagM.node "d" + CommDiagM.grid #[#[some a, some b, some c, some d]] + CommDiagM.arrowWith a b { bend := 0.35 } + CommDiagM.arrowWith b a { bend := 0.35 } + CommDiagM.arrow b c + -- `CommDiagM.node` names nodes `node_0`, `node_1`, … in creation order, so + -- `c` is `node_2`; its position is only known once the grid is laid out. + let cPos := (base.find (Lean.Name.mkSimple "node_2")).origin.toVec2 + Diagram.atop (selfLoop cPos) base + +end CSwLMeta.Diagrams diff --git a/CSwLMeta/Save/Extract.lean b/CSwLMeta/Save/Extract.lean index 40654b8..84d5a03 100644 --- a/CSwLMeta/Save/Extract.lean +++ b/CSwLMeta/Save/Extract.lean @@ -2,10 +2,11 @@ -- (namespace SFLMeta -> CSwLMeta), with the cuts that go along with the -- modules CSwL did not port (see `CSwLMeta.lean`): -- --- * the `walkBlock` cases for Details/SlideBreak are left out -- the --- corresponding modules don't exist here; --- (DevComment was ported -- see the `Block.devcomment` case below; Bnf and --- DisplayMath were also ported, but with no case of their own here -- +-- * the `walkBlock` case for SlideBreak is left out -- the corresponding +-- module doesn't exist here; +-- (DevComment and Details were ported -- see the `Block.devcomment` and +-- `Block.details` cases below; Bnf and DisplayMath were also ported, but +-- with no case of their own here -- -- they fall through to the generic branch below, which already suffices: -- `Block.bnf`/`Block.display` wrap the original text as a `Block.code` -- child, and the generic branch recurses into the children, so the text @@ -29,6 +30,7 @@ import VersoManual import CSwLMeta.Comment +import CSwLMeta.Details import CSwLMeta.Exercise import CSwLMeta.Quiz import CSwLMeta.Grade @@ -56,6 +58,12 @@ def appendAll (buf : SaveBuffers) (file : String) (s : String) : SaveBuffers := let vs := buf.getD file default buf.insert file <| vs.map (· ++ s) +/-- Collapse the blank line a just-appended block left behind, so the next +appended comment line lands directly under it rather than after a gap. -/ +def dropBlankLine (buf : SaveBuffers) (file : String) : SaveBuffers := + let vs := buf.getD file default + buf.insert file <| vs.map fun s => if s.endsWith "\n\n" then (s.dropEnd 1).toString else s + def appendOnly (buf : SaveBuffers) (file : String) (variant : Variant) (s : String) : SaveBuffers := let vs := buf.getD file default |>.mapV fun v x => if v == variant then x ++ s else x buf.insert file vs @@ -419,6 +427,24 @@ partial def walkBlock (width : Nat) (file : String) (b : Verso.Doc.Block Manual) match findAlt? contents with | .some alt => return buf.appendAll file (asModuleDoc alt.trimAscii.toString) | .none => return buf + if name == ``Block.details then + -- The contents are inlined verbatim, bracketed by skip markers so the + -- reader of the `.lean` can tell this was a collapsed, skippable aside in + -- the book. The summary (if any) rides along on the opening marker. + let summary := + match which.data with + | .str s => s + | _ => "" + let opener := if summary.isEmpty + then "THE FOLLOWING DETAILS CAN BE SKIPPED" + else s!"THE FOLLOWING DETAILS CAN BE SKIPPED ({summary})" + -- Both markers hug the content they bracket: the opener drops the blank + -- line `asModuleDoc` would leave after it, and the closer collapses the + -- one the last content block left behind. + let mut buf := buf.appendAll file ((asModuleDoc opener).dropEnd 1).toString + buf := walkBlocks width file contents buf + buf := (buf.dropBlankLine file).appendAll file (asModuleDoc "END DETAILS") + return buf if name == ``Block.quiz then -- A quiz is shown in every build product; label it so the reader of the -- generated `.lean` can tell the question apart from surrounding prose. diff --git a/DEVIATIONS.md b/DEVIATIONS.md index 382636b..882f119 100644 --- a/DEVIATIONS.md +++ b/DEVIATIONS.md @@ -240,6 +240,32 @@ 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 @@ -268,17 +294,116 @@ 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 CSwFP/6's, in fragment.** Chapter 6's model -(`src/Model.hs`) is pulled forward to give 5.5 something concrete to evaluate -against: ten of the twenty-seven entities, and eight predicates -(`girl`, `boy`, `princess`, `dwarf`, `giant`, `child`, `love`, `defeat`) with -the original's extensions, restricted to the entities kept. The one place this -bites is `defeat`, which in the original is the dwarf/giant rule *plus* the -pairs `(A,W)` and `(A,V)`; the wizards `W` and `V` are outside the fragment, so -only the rule survives. The natural-language translation that chapter 6 -builds on it is not pulled forward — only the model. The previous example was a -three-element `Nat` domain with predicates named `P` and `R`, which could not -show why a *finite, listed* domain is what makes evaluation possible. +**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. @@ -379,11 +504,26 @@ This is where the rest of 2.5 lands. The type BNF `τ ::= b | (τ → τ)` says `INF` is part of the 4.2 grammar but has no translation in CSwFP/6; it is not required by `ModelChecking.lean`. -### 9. `ModelChecking.lean` — CSwFP/6 +### 9. CSwFP/6 — in `English.lean` Sections 6.1–6.5; 6.6 (Further Reading) omitted. -**This chapter must come after `English.lean`.** 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 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. diff --git a/PROVENANCE.md b/PROVENANCE.md index a663ed0..2b1483b 100644 --- a/PROVENANCE.md +++ b/PROVENANCE.md @@ -115,71 +115,141 @@ 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/PL.lean` — CSwFP/4.4 - -| CSwL id | Rating | CSwFP | Page | Notes | -|-------------------|--------|---------------|------|--------------------| -| — | — | Exercise 4.9 | 74 | dropped 2026-09-02 | -| `exclusive-or` | 1 | Exercise 4.10 | 74 | | -| — | — | Exercise 4.11 | 74 | dropped 2026-09-02 | -| `count-operators` | 1 | Exercise 4.12 | 75 | | -| `formula-depth` | 1 | Exercise 4.13 | 75 | | -| `collect-atoms` | 2 | Exercise 4.14 | 75 | | - -Exercises 4.9 and 4.11 were ported and then dropped when the chapter -was restructured around worked arguments. 4.9 asked for three -sentences to be translated into propositional logic; `exchange-prop`, -`dresses` and `bangu-form` ask the same thing of arguments the reader -then has to prove or settle, which is the same skill with a use -attached. 4.11 asked for unique readability — see `DEVIATIONS.md` on -why the original claim dissolves — and the section that carried it, -along with the parenthesis-counting results of Theorem 4.1 and -Proposition 4.2, went with the restructuring. +### `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 -| CSwL id | Rating | CSwFP | Page | Notes | -|-------------------------|--------|-------------------------|------|---------| -| - | 2 | Exercise 4.15 | 77 | dropped | -| - | 1 | Exercise 4.16 | 77 | dropped | -| - | 1 | Exercise 4.17 | 78 | dropped | -| `closed-form` | 2 | Exercise 4.18 | 81 | | -| `implication-as-abbrev` | 1 | Exercise 4.19 | 82 | | -| `negation-normal-form` | 2 | Exercise 4.20 | 82 | | -| - | 1 | Exercise 4.21 | 83 | dropped | -| `vars-in-formula` | 1 | Exercise 4.22 | 84 | | -| `open-form` | 2 | Exercises 4.23 and 4.24 | 84 | merged | - -All ten are `:::exercise` directives. Nine of them were plain `#` headings -carrying the source's page number until 2026-08-30; 4.23 and 4.24 became one -exercise, since 4.23 asked for the function that 4.24 builds on. - -### `Logic/PL.lean` — CSwFP/5.2, 5.3 - -| CSwL id | Rating | CSwFP | Page | Notes | -|---------------------|--------|---------------|------|------------| -| `valuation-table` | 1 | Exercise 5.4 | 92 | | -| `negated-tautology` | 1 | Exercise 5.5 | 93 | prose | -| — | — | Exercise 5.6 | 93 | not ported | -| — | — | Exercise 5.7 | 93 | not ported | -| — | — | Exercise 5.8 | 93 | not ported | -| — | — | Exercise 5.9 | 93 | not ported | -| `implies-list` | 2 | Exercise 5.10 | 96 | | -| — | — | Exercise 5.11 | 96 | not ported | -| — | — | Exercise 5.12 | 96 | not ported | - -### `Logic/FOL.lean` — CSwFP/5.5 - -| CSwL id | Rating | CSwFP | Page | Notes | -|------------------------|--------|---------------|------|------------| -| `quantifier-strength` | 2 | Exercise 5.17 | 102 | prose | -| `translate-quantified` | 2 | Exercise 5.18 | 102 | | -| — | — | Exercise 5.19 | 102 | not ported | -| — | — | Exercise 5.20 | 103 | not ported | -| — | — | Exercise 5.21 | 103 | not ported | -| — | — | Exercise 5.22 | 103 | not ported | -| — | — | Exercise 5.23 | 104 | not ported | -| `valid-consequence` | 2 | Exercise 5.24 | 104 | prose | +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 @@ -194,44 +264,24 @@ exercise, since 4.23 asked for the function that 4.24 builds on. An exercise absent from the tables above is a decision, not an oversight. The reasons fall into three kinds. -**It asks for a construction the chapter does not have.** CSwFP/5.21 defines -substitution of a name for a variable in a term; 5.22 asks for a truth -definition that replaces assignments by names plus substitution; 5.23 asks for -the truth definition extended to structured terms. All three need substitution, -which `FOL.lean` never defines, and 5.23 additionally needs the interpretation -of function symbols. Writing those constructions is a chapter's worth of work, -not an exercise's. - -**It is answered by something the chapter already states.** CSwFP/5.6 asks which -of three formulas are satisfiable, 5.7 which equivalences hold, 5.8 which -consequences hold, 5.19 and 5.20 the same for predicate logic. In this book -`satisfiable`, `equivalent` and `implies` are computable, so each of these is -`#eval` rather than a question — the answer is a keystroke, and the exercise -loses its point. They are worth keeping only if reformulated as proofs about -the definitions rather than queries against them. - -For 5.19 and 5.20 this became true only with the chapter reorganization of -2026-09-13, which gave `FOL.lean` a computable `Formula.eval`; before that the -chapter had no way to evaluate a formula at all, and the two were unported for -want of a semantics rather than for having too easy an answer. They are now the -strongest candidates for reformulation as proofs, since the model to state them -against is in the chapter. - -**It asks for a variant implementation.** CSwFP/5.11 asks for a check of logical -equivalence, which `Form.equivalent` already is; 5.12 asks to reimplement the -semantics with `[String]` instead of `[(String, Bool)]` for valuations. - -CSwFP/5.18 is ported as `translate-quantified`. Its propositional counterpart, -4.9, was dropped; the two chapters no longer mirror each other here. +**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. -Nine of the `Logic/FOL.lean` entries above were plain headings carrying the -book's page number rather than exercise directives; that is fixed. - ## Exercises original to CSwL No CSwFP counterpart. Listed so that "absent from the table above" is not read @@ -280,6 +330,7 @@ as an oversight. | `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 | diff --git a/STYLE-CODE.md b/STYLE-CODE.md index b0b5b31..0d39192 100644 --- a/STYLE-CODE.md +++ b/STYLE-CODE.md @@ -47,6 +47,15 @@ with `--` comments stripped to find *uses*, then search the prose separately to find *presentations*; the rule is satisfied only when a presentation precedes the first use in book order. +Two further traps, both of which have already produced wrong rows. A ```` ```lean ++error ```` block is code shown *because it fails to compile*, so what it +contains is not a use: `IntroL` has `def omega := (fun x => x x) (fun x => x x)`, +which is a definition named `omega` in a block that errors, not the `omega` +tactic. And a name can be a field or a definition rather than the tactic it +looks like — `symm` in `Sets` is the `Equivalence.symm` field, `contradiction` +in `Logic/PL` is `Formula.contradiction` inside a `simp only [...]` list. +Read the line before recording a row. + 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 @@ -57,55 +66,75 @@ 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`, 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`, `DecidableEq`, `List.all`/`List.any` | `funext` (solution only), `show` (solution only), `omega` (solution only), `decide` (solution only) | -| `Logic/Proof` | `open` | `¬`, `∀`, `∃`, `∧`, `∨`, `↔`, `≠` | `intro`, `exact`, `apply`, `cases … with`, `constructor`, `obtain`, `have`, `use`, `left`, `right`, `rcases`, `by_cases`, `by_contra`, `assumption` | -| `Logic/PL` | `abbrev`, `private` | `×` | `simp`, `native_decide` | -| `Logic/FOL` | `mutual`, `deriving BEq` | `\|>`, `List.contains` | `induction … generalizing` | -| `Sets` | — | `Set`, `Rel`, `Finset`, `Fintype`, `Setoid`, `∈`, `⊆`, `∪`, `∩`, `trivial` (term) | `symm`, `simp_all` | -| `SeaBattle` | — | `Fin` | — | -| `Morphology` | *(none new)* | — | — | -| `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. +| `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)* | +| `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`, `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`, `simp`, `simp only [...]`, 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` | +| `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 | — | +| `English` | `mutual` over `inductive` types (`Logic/FOL` only uses it over `def`) | guillemet identifiers (`«with»`) | *(none new)* | + +`English` is where `abbrev` and `ToString` instances become the dominant +idiom, but both arrive earlier; what is genuinely new there is the mutually +recursive *grammar*, a `mutual` block over `inductive` declarations rather +than over `def`s, and `«with»`, which quotes a Lean keyword so it can be used +as a constructor name. 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. +maintains. Library functions are not tracked either — `String.intercalate`, +`List.zip`, `Std.Format.joinSep`, `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.) ### Known gaps Open questions about the table, recorded so they are not lost. Each needs an author decision, not a mechanical fix. -- **`native_decide`** is named in the prose of three `Logic/PL` exercises - (`:282`, `:308`, `:348`) and used in their solutions, then used eleven times - in `SeaBattle.lean` (from `:290`) and twice in - `Morphology/SwedishPlural.lean` (`:69`, `:72`). It is told to the reader but - never *presented*: it closes a goal by compiling and running it, trusting - the compiler rather than the kernel — a materially different promise from - `decide`, and a reader who meets it without being told will draw the wrong - conclusion about what a Lean proof is worth. The only explanation anywhere - is a Portuguese comment inside a `SwedishPlural` solution (`:63-66`), which - reaches neither the student nor the English code-comment rule. `Logic/PL` is - where it is first met and so where the explanation belongs. -- **`trivial`** — two term-level uses in `Sets.lean:517`, not presented +- **`trivial`** — two term-level uses on `Sets.lean:507`, not presented anywhere. It is listed in the table under types rather than tactics, since that is what it is here. Give it a line or replace it when that chapter is revised. -- **`funext`, `show`, `omega`, `decide` in `IntroL`** — all four appear only - inside the `twice` exercise's `solution!(…)` blocks (`:1136-1138`, `:1141`), - so the student and `terse` variants never show them, but the `solutions` and - `grading` variants do, and nothing presents them before `Logic/Proof`. This - is the cost of moving every proof tactic out of `IntroL`: the chapter is now - deliberately pre-proof, so presenting them here would undo that. Either move - the exercise's tests to `Logic/Proof`, or weaken them to what `rfl` closes. - `decide` → `rfl` is known to work for `twice_test2`. (`funext` is discussed - in the prose at `:807`, but as the principle of function extensionality, not - as a tactic the reader is being handed.) +- **`omega` in `Logic/FOL`** — first used at `FOL.lean:593`, in the `Fin` + examples (`⟨0, by omega⟩`). The prose there presents `Fin` and `Fin.mk` and + says nothing about `omega`, so the reader meets the tactic in passing. It + returns in `fol-infinite`. One line of presentation next to the `Fin` + examples covers both places. +- **`refine` with `?_` and `induction … generalizing` in `Logic/FOL`** — they + appear in `Formula.eval_iff_denote`, `le_foldr_max` and `no_list_lists_Nat`, + which are shown with their proofs as exposition. No exercise asks the reader + to reproduce any of them, so the question is whether a proof the reader only + *reads* counts as handing them a tactic. If it does, a few short lines of + presentation are owed; if it does not, these rows are evidence rather than a + gap. Author's call, and the cheaper fix is the lines. +- **`<;>` in `Logic/FOL`** — first used at `FOL.lean:525`. The prose describes + what happens ("a tática `decide` é combinada com `cases v`, que abre um caso + por construtor") without naming the combinator or saying what `<;>` means. + Naming it costs half a sentence. +- **The `simp` family in `Logic/PL`** — `simp`, `simp only [...]`, + `all_goals`, `simpa … using`, the `at … ⊢` locations and `rw [← …]` all + arrive unannounced in the `pl-to-prop` metatheorems. `Logic/Proof` promises + that `omega` and `simp` "serão explicadas à medida que se fizerem + necessárias"; the promise is never kept. This is the largest gap in the + ledger, and it lands on proofs the reader is expected to read closely. +- **`abbrev`** — `PL.lean:341`, no presentation; it is introduced by use. + Docstring syntax `/-- … -/`, first used in the same chapter, is in the same + state, and is cheap to leave alone. +- **Features that only the answer shows** — `rcases` (`Proof.lean:420`), + `Or.inl`/`Or.inr` (`Proof.lean:196`), `|>` (`PL.lean:120`), `match e₁, e₂ + with` (`FOL.lean:614`), `show … by …` (`Sets.lean:643`), and dependent + `if h : … then … else` and `▸` (`SeaBattle.lean:307` and `315`) all appear + first inside `solution!`, so a student working the exercise is expected to + produce syntax the book never showed them. Two of them surface later in + ordinary code — `|>` at `FOL.lean:369` and `match e₁, e₂ with` at + `Morphology/Phonemes.lean:227`. `mapM` is the same shape: first used inside + a solution (`Phonemes.lean:309`) and visible only much later, at + `InfEngine.lean:439`. The rest never surface at all. `IntroCS` is the constraint's one accepted exception: it uses Lean that `IntroL` only presents later, deliberately, and the chapter says so where its @@ -247,6 +276,12 @@ Prose can be routed to a variant: 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. +- `:::details "summary"` — a collapsible aside, for material that supports the + narrative without belonging to it (an extra proof, a digression). The + positional summary string is the teaser shown while the block is closed, and + is optional. In the generated `.lean` the contents are inlined, bracketed by + `THE FOLLOWING DETAILS CAN BE SKIPPED` / `END DETAILS` markers — nothing is + hidden from the reader of the code, only from the reader of the page. - `:::diagramWithAlt` — a diagram with its textual alternative, for accessibility. diff --git a/STYLE-WRITING.md b/STYLE-WRITING.md index 5dd3f3a..9b5d6a1 100644 --- a/STYLE-WRITING.md +++ b/STYLE-WRITING.md @@ -134,6 +134,10 @@ 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. +Avoid **fragmented sentences** like "A P ↔ Q é a conjunção das duas +implicações, e as regras seguem disso." This is a bad style for +writing pedagogical material. + ### Punctuation and typography - Em dashes for parenthetical breaks, spaced as the surrounding prose does.