Instruções
Sua tarefa é provar a igualdade entre uma função personalizada de inversão de listas e a função integrada List.reverse.
Por causa da natureza deste exercício, em vez de contar com testes tradicionais em tempo de execução, a prova é verificada por um teorema check.
Você pode considerar o teste aprovado se esse teorema passar na verificação de tipos.
Se você trabalhar localmente ou no playground online do Lean, receberá feedback instantâneo sobre se qualquer teorema funciona ou falha, e por que falha, pelo Lean InfoView.
É uma ferramenta valiosa, capaz de mostrar todos os valores locais usados pela sua prova e o seu objetivo atual.
A tática sorry faz qualquer prova parecer correta.
Por esse motivo, o teorema check pode parecer passar automaticamente na verificação de tipos antes que qualquer prova seja realmente escrita.
Quando você remover sorry da sua prova, o Lean InfoView mostrará o feedback correto.
Provando teoremas em Lean
A prova de teoremas é parte integrante do Lean.
Ela permite que quem programa prove propriedades sobre seus programas, reflita sobre o comportamento deles e codifique restrições e especificações no nível dos tipos.
Este capítulo oferece uma boa introdução à prova de teoremas em Lean.
Para um mergulho mais profundo, este livro aparece como recurso oficial no site do Lean.
O Lean oferece muitas táticas capazes de automatizar provas, ou partes delas.
Talvez você queira consultar uma referência da linguagem.
Podemos usar o atributo do compilador csimp em um teorema que prova a igualdade entre duas definições.
Esse atributo instrui o compilador a usar a segunda definição no lugar 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`.
Isso é especialmente ú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 esse padrão.
