Instruções
A tua tarefa é provar a igualdade entre uma função personalizada de inversão de listas e o List.reverse integrado.
Devido à natureza deste exercício, em vez de depender de testes de execução tradicionais, a prova é verificada por um teorema check.
Podes considerar que o teste passa se este teorema passar na verificação de tipos.
Se trabalhares localmente ou no playground online do Lean, recebes feedback imediato sobre se um teorema tem sucesso ou falha, e porque falha, através do Lean InfoView.
É uma ferramenta inestimável, capaz de mostrar todos os valores locais usados pela tua prova e o teu objetivo atual.
A tática sorry faz com que qualquer prova pareça estar correta.
Por este motivo, o teorema check pode parecer passar automaticamente na verificação de tipos antes de qualquer prova ser realmente escrita.
Assim que removeres o sorry da tua prova, o Lean InfoView mostrará o feedback correto.
Provar teoremas em Lean
A prova de teoremas é uma parte integrante do Lean.
Permite aos programadores provar propriedades dos seus programas, raciocinar sobre o seu comportamento e codificar restrições e especificações ao nível dos tipos.
Este capítulo é uma boa introdução à prova de teoremas em Lean.
Para um estudo mais aprofundado, este livro está listado como recurso oficial no site do Lean.
O Lean oferece muitas táticas que conseguem automatizar provas, ou partes delas.
Podes querer consultar uma referência da linguagem.
Podemos usar o atributo do compilador csimp num teorema que prova a igualdade entre duas definições.
Este atributo indica ao compilador que use a segunda definição em vez da primeira:
@[csimp]
theorem custom_reverse_eq_spec_reverse : @Extra.custom_reverse = @List.reverse := by
... -- proof here
-- now any occurrence of `Extra.custom_reverse` may now compile to `List.reverse`.
É particularmente útil em situações em que uma implementação é mais eficiente, mas menos clara.
Podemos escrever uma especificação simples e fazer com que o código compilado use a implementação mais eficiente.
Muitas funções de List e Array usam este padrão.
