Introdução
Numa noite, encontraste um caderno antigo cheio de rabiscos enigmáticos, como se alguém perseguisse uma ideia de forma obsessiva.
Numa das páginas, destacava-se uma única pergunta: Será que todos os números conseguem chegar ao 1?
Estava ligada a algo chamado Conjetura de Collatz, um enigma que intriga pensadores há décadas.
As regras eram enganadoramente simples.
Escolhe qualquer número inteiro positivo.
- Se for par, divide-o por 2.
- Se for ímpar, multiplica-o por 3 e soma 1.
Depois, repete estes passos com o resultado e continua assim indefinidamente.
Curioso, escolheste o número 12 para testar e começaste a viagem:
12 ➜ 6 ➜ 3 ➜ 10 ➜ 5 ➜ 16 ➜ 8 ➜ 4 ➜ 2 ➜ 1
A contar desde o segundo número (6), foram precisos 9 passos para chegar ao 1, e a cada repetição das regras o número continuava a mudar.
Ao início, a sequência parecia imprevisível: saltava para cima, para baixo e para todos os lados.
No entanto, a conjetura afirma que, seja qual for o número de partida, acabamos sempre no 1.
Era fascinante, mas também desconcertante.
Porque é que isto parece funcionar sempre?
Será que existe algum número em que o processo se desmorone, entre num ciclo sem fim ou se perca no infinito?
O caderno sugeria que resolver isto poderia revelar algo profundo, e, com isso, a fama, a fortuna e um lugar na história esperam quem conseguir desvendar os seus segredos.
Instruções
Dado um número inteiro positivo, devolve o número de passos necessários para chegar a 1 de acordo com as regras da Conjetura de Collatz.
Subtypes
Este exercício define um Subtype chamado Positive, para todos os números naturais maiores que 0.
Um Subtype pode ser encarado como um par ⟨x, h⟩, em que x é o valor e h é a prova da sua validade.
O valor dentro de um Subtype (x, neste caso) pode ser acedido com .val, por exemplo, x.val.
A sua prova pode ser acedida com .property, por exemplo, x.property.
Ambos podem também ser acedidos por pattern matching, como habitualmente.
Para construir um valor para um Subtype, é necessário provar a sua validade, neste caso, que o número é maior que 0.
Há vários lemas e teoremas em Lean que podem servir de ponto de partida para esta prova.
Por exemplo, Nat.zero_lt_succ é um lema que afirma que, para qualquer número natural n: 0 < n + 1.
Encontras uma boa referência para a prova de teoremas em Lean na documentação principal.
Prova de terminação
Em Lean, as funções recursivas têm de provar a sua terminação.
Esta prova é por vezes imediata, decorrendo implicitamente da estrutura de uma função.
Noutros casos, tem de ser explicitada.
Neste exercício, a terminação da função é precisamente a collatz conjecture, que é um problema matemático em aberto.
Considera usar uma das seguintes opções:
- Acrescentar a palavra-chave
partial antes da declaração de uma função desativa a verificação de terminação e permite chamadas recursivas (potencialmente inseguras).
- As construções imperativas permitidas em código monádico, como
while, são implementadas internamente com recursão parcial, pelo que podem ser usadas sempre que a terminação não seja imposta.
Usar a mónada Id é uma forma cómoda de ativar estas construções em código que, de resto, parece puro, sem introduzir efeitos adicionais.
- Definir uma função auxiliar com um parâmetro extra para o número máximo de chamadas recursivas garante a terminação.
