Introdução
Certa noite, você encontrou um caderno antigo cheio de rabiscos enigmáticos, como se alguém estivesse perseguindo uma ideia de forma obsessiva.
Em uma das páginas, uma única pergunta se destacava: Todo número consegue encontrar o caminho até 1?
Ela estava ligada a algo chamado Conjectura de Collatz, um enigma que confunde pensadores há décadas.
As regras eram enganosamente simples.
Escolha qualquer número inteiro positivo.
- Se for par, divida por 2.
- Se for ímpar, multiplique por 3 e some 1.
Depois, repita esses passos com o resultado, continuando indefinidamente.
A curiosidade venceu: você escolheu o número 12 para testar e começou a jornada:
12 ➜ 6 ➜ 3 ➜ 10 ➜ 5 ➜ 16 ➜ 8 ➜ 4 ➜ 2 ➜ 1
Contando a partir do segundo número (6), foram 9 passos até chegar a 1, e a cada vez que as regras se repetiam, o número continuava mudando.
No início, a sequência parecia imprevisível: subia, descia e pulava de um lado para o outro.
Ainda assim, a conjectura afirma que, não importa o número inicial, sempre vamos terminar em 1.
Era fascinante, mas também intrigante.
Por que isso parece sempre funcionar?
Será que existe um número em que o processo se quebra, repetindo para sempre ou escapando para o infinito?
O caderno sugeria que resolver isso poderia revelar algo profundo. E, com isso, fama, fortuna e um lugar na história esperam por quem conseguisse desvendar seus segredos.
Instruções
Dado um número inteiro positivo, retorne o número de passos necessários para chegar a 1 de acordo com as regras da Conjectura de Collatz.
Subtipos
Este exercício define um Subtipo chamado Positive, para todos os números naturais maiores que 0.
Um Subtipo pode ser pensado como um par ⟨x, h⟩, onde x é o valor e h é a prova de sua validade.
O valor dentro de um Subtipo (x, neste caso) pode ser acessado usando .val, por exemplo, x.val.
Sua prova pode ser acessada usando .property, por exemplo, x.property.
Os dois também podem ser acessados por casamento de padrões, como de costume.
Para construir um valor para um Subtipo, é preciso provar sua validade, neste caso, que o número é maior que 0.
Existem vários lemas e teoremas em Lean que podem servir de ponto de partida para essa prova.
Por exemplo, Nat.zero_lt_succ é um lema que afirma que, para qualquer número natural n: 0 < n + 1.
Uma boa referência para prova de teoremas em Lean pode ser encontrada na documentação principal.
Prova de terminação
Em Lean, funções recursivas precisam provar sua terminação.
Às vezes essa prova é simples e decorre implicitamente da estrutura de uma função.
Em outros casos, ela precisa ser explícita.
Neste exercício, a terminação da função é exatamente a collatz conjecture, que é um problema matemático em aberto.
Considere usar uma das seguintes opções:
- Adicionar 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).
- Construções imperativas permitidas em código monádico, como
while, são implementadas com recursão parcial por baixo dos panos, então podem ser usadas sempre que a terminação não for exigida.
Usar a mônada Id é uma forma conveniente de habilitar essas construções em código que, fora isso, 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.
