5. Aula 5: Provas Progressivas
A Aula 4 provou os teoremas da lógica de forma regressiva, partindo do objetivo e reduzindo-o com táticas. Esta aula inverte os mesmos enunciados e os prova de forma progressiva, partindo das hipóteses e derivando novos fatos até alcançar o objetivo, seguindo o capítulo 4 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 4. Ela escreve provas como termos estruturados cuja forma espelha a proposição, introduz provas calculacionais com calc e explica a leitura de Curry–Howard, o princípio de que uma prova é um termo e uma proposição é um tipo. São as duas faces de uma mesma atividade, e ao final as duas aulas se leem como um único argumento visto de ambos os extremos.
Esta aula também está disponível como slides de apresentação.