Introducción
Una noche, te topaste con un cuaderno viejo lleno de garabatos misteriosos, como si alguien hubiera estado persiguiendo una idea de forma obsesiva.
En una página, una sola pregunta resaltaba: ¿Todo número puede encontrar su camino hacia el 1?
Estaba ligada a algo llamado la Conjetura de Collatz, un rompecabezas que ha desconcertado a los pensadores durante décadas.
Las reglas eran engañosamente simples.
Elige cualquier número entero positivo.
- Si es par, divídelo entre 2.
- Si es impar, multiplícalo por 3 y súmale 1.
Luego, repite estos pasos con el resultado, continuando indefinidamente.
Con curiosidad, elegiste el número 12 para probarlo y comenzaste el viaje:
12 ➜ 6 ➜ 3 ➜ 10 ➜ 5 ➜ 16 ➜ 8 ➜ 4 ➜ 2 ➜ 1
Contando desde el segundo número (6), hizo falta 9 pasos para llegar al 1, y cada vez que las reglas se repetían, el número seguía cambiando.
Al principio, la secuencia parecía impredecible, saltando hacia arriba, hacia abajo y por todos lados.
Sin embargo, la conjetura afirma que sin importar cuál sea el número inicial, siempre terminaremos en el 1.
Era fascinante, pero también desconcertante.
¿Por qué parece funcionar siempre así?
¿Podría existir un número en el que el proceso se rompa, se repita en un bucle infinito o se escape hacia el infinito?
El cuaderno sugería que resolver esto podría revelar algo profundo y, con ello, la fama, la fortuna y un lugar en la historia le esperan a quien logre descifrar sus secretos.
Instrucciones
Dado un entero positivo, devuelve el número de pasos que se necesitan para llegar a 1 según las reglas de la Conjetura de Collatz.
Subtypes
Este ejercicio define un Subtype llamado Positive, para todos los números naturales mayores que 0.
Un Subtype se puede pensar como un par ⟨x, h⟩, donde x es el valor y h es la demostración de su validez.
Se puede acceder al valor dentro de un Subtype (x, en este caso) usando .val; por ejemplo, x.val.
Se puede acceder a su demostración usando .property; por ejemplo, x.property.
También se puede acceder a ambos mediante coincidencia de patrones, como siempre.
Para construir un valor de un Subtype, es necesario demostrar su validez; en este caso, que el número sea mayor que 0.
Hay varios lemas y teoremas en Lean que pueden servir como punto de partida para esta demostración.
Por ejemplo, Nat.zero_lt_succ es un lema que afirma que para cualquier número natural n: 0 < n + 1.
Puedes encontrar una buena referencia para la demostración de teoremas en Lean en la documentación principal.
Demostración de terminación
En Lean, las funciones recursivas deben demostrar su terminación.
A veces esta demostración es sencilla y se deduce implícitamente de la estructura de la función.
En otros casos, hay que hacerla explícita.
En este ejercicio, la terminación de la función es precisamente la collatz conjecture, que es un problema matemático abierto.
Considera usar una de las siguientes opciones:
- Agregar la palabra clave
partial antes de la declaración de una función desactiva la comprobación de terminación y permite llamadas recursivas (potencialmente inseguras).
- Las construcciones imperativas permitidas en código monádico, como
while, se implementan internamente mediante recursión parcial, así que se pueden usar siempre que no se exija la terminación.
Usar la mónada Id es una forma cómoda de habilitar estas construcciones en código que de otro modo parece puro, sin introducir efectos adicionales.
- Definir una función auxiliar con un parámetro extra para el número máximo de llamadas recursivas asegura la terminación.
