6. Aula 6: Programação Funcional
A Aula 3 introduziu os tipos indutivos por exemplo, reconstruindo ℕ e List e definindo funções sobre eles por casamento de padrões. Esta aula retoma esse material e apresenta o mecanismo geral, seguindo o capítulo 5 do Hitchhiker's Guide to Logical Verification.A. Baanen, A. Bentkamp, J. Blanchette, J. Hölzl, J. Limperg, The Hitchhiker's Guide to Logical Verification, edição de 2026, capítulo 5. Ela lê uma definição indutiva como uma lista de construtores e nomeia o que o núcleo deriva deles, define funções totais por recursão estrutural e explica por que Lean exige a terminação, empacota dados em estruturas e explica as classes de tipos, o mecanismo que a Aula 2 usou para Membership e a Aula 4 usou para a associatividade e a comutatividade que ac_rfl consulta.
O curso passa duas semanas neste capítulo. Esta aula é o lado dos programas, definindo dados e funções. A Aula 7 é o lado das provas, derivando o princípio de indução estrutural e provando as propriedades desses programas. Assim, esta aula enuncia as leis das suas funções e prova apenas aquelas que a computação ou uma única análise de casos resolve, e adia para a Aula 7 toda prova que precisa de indução, exatamente como a Aula 5 adiou a teoria geral da indução estrutural.
Esta aula também está disponível como slides de apresentação.