Um companheiro magro para “Análise I”

Quase 20 anos atrás, escrevi um livro em análise actual chamado “Análise i“O objetivo foi complementar os muitos livros didáticos de análise disponíveis, concentrando -se mais em questões fundamentais, como a construção de números naturais, números inteiros, números racionais e reais, além de fornecer teoria e lógica suficientes para permitir que os alunos desenvolvam provas em altos níveis de rigor.

Enquanto alguns assistentes de prova como Coq ou AGDA estavam bem estabelecidos quando o livro foi escrito, a verificação formal não estava no meu radar na época. No entanto, agora que tive alguma experiência com esse assunto, percebo que o conteúdo deste livro é de fato muito compatível com esses assistentes de prova; Em specific, a ‘teoria do tipo ingênua’ que eu estava usando implicitamente para fazer coisas como construir os sistemas de números padrão, se encaixa bem com a teoria do tipo dependente da enx (que, entre outras coisas, tem excelente suporte para tipos de quocientes).

Portanto, decidi lançar um Companheiro magro para “Análise I”que é uma “tradução” de muitas das definições, teoremas e exercícios do texto em Lean. Em specific, isso fornece uma maneira alternativa de executar os exercícios no livro, preenchendo os “Sorries” correspondentes no código Lean. (No entanto, não planejo hospedar soluções “oficiais” para os exercícios neste companheiro; em vez disso, sinto -me à vontade para criar garfos do repositório em que essas dor são preenchidas.)

Atualmente, as seguintes seções do texto foram traduzidas para Lean:

A formalização foi deliberadamente projetada para ser separada da biblioteca de matemática enxuta padrão Mathlib Em alguns lugares, mas dependente de outros. Por exemplo, Mathlib já tem uma noção padrão dos números naturais . Na formalização enxuta, primeiro desenvolvo “manualmente” uma construção alternativa Chapter2.Nat dos números naturais (ou apenas Natse alguém estiver trabalhando no Chapter2 espaço para nome), configurando muitos dos resultados básicos sobre esses números naturais alternativos que paralelam lemas semelhantes sobre que já estão em Mathlib (mas com muitos desses lemas definidos como exercícios para o leitor, com as provas atualmente substituídas por “Sorries”). Então, em uma seção de epílogo, os isomorfismos entre esses números naturais alternativos e os números naturais Mathlib são estabelecidos (ou mais precisamente, definidos como exercícios). A partir desse momento, os números naturais do capítulo 2 são preteridos e os números naturais Mathlib são usados. Pretendo continuar esse padrão geral ao longo do livro, de modo que, à medida que alguém avança nos capítulos posteriores, se depende cada vez mais das definições e funções de Mathlib, em vez de se referir diretamente a qualquer contraparte dos capítulos anteriores. Como tal, esse companheiro também pode ser usado como uma introdução ao Lean e Mathlib, bem como à análise actual (um pouco no espírito do “Jogo de números naturais“, Que de fato tem uma sobreposição temática significativa com o capítulo 2 do meu texto).

O código nesse repositório compila em Lean, mas não testei se todas as (numerosas) “dor” no código podem realmente ser preenchidas (ou seja, se todos os exercícios puderem ser realmente resolvidos em Lean). Eu estaria interessado em ter voluntários “Playtest” o companheiro para ver se isso pode realmente ser feito (e se o lemas auxiliar ou “API” fornecidos nos arquivos enxados forem suficientes para preencher as Dorries de maneira conceitualmente direta, sem ter que confiar em técnicas de programação magra mais esotéricas). Qualquer outro suggestions também será bem -vindo.

(Atualização, 31 de maio: moveu o companheiro para um repositório independente.)