Introduction
Un soir, tu es tombé sur un vieux carnet rempli de gribouillages énigmatiques, comme si quelqu'un avait poursuivi une idée avec obsession.
Sur une page, une seule question attirait l'attention : tout nombre peut-il trouver son chemin jusqu'à 1 ?
Elle était liée à ce qu'on appelle la conjecture de Collatz, une énigme qui déroute les penseurs depuis des décennies.
Les règles étaient d'une simplicité trompeuse.
Choisis un entier positif quelconque.
- S'il est pair, divise-le par 2.
- S'il est impair, multiplie-le par 3 et ajoute 1.
Répète ensuite ces étapes avec le résultat, indéfiniment.
Curieux, tu as choisi le nombre 12 pour tester et tu as commencé le voyage :
12 ➜ 6 ➜ 3 ➜ 10 ➜ 5 ➜ 16 ➜ 8 ➜ 4 ➜ 2 ➜ 1
En partant du deuxième nombre (6), il a fallu 9 étapes pour atteindre 1, et à chaque fois que les règles se répétaient, le nombre changeait sans cesse.
Au début, la séquence semblait imprévisible : elle montait, descendait, partait dans tous les sens.
Pourtant, la conjecture affirme que quel que soit le nombre de départ, on finit toujours par arriver à 1.
C'était fascinant, mais aussi déroutant.
Pourquoi cela semble-t-il toujours fonctionner ?
Existe-t-il un nombre pour lequel le processus s'enraye, tournant en boucle pour toujours ou s'échappant vers l'infini ?
Le carnet laissait entendre que résoudre cette énigme pourrait révéler quelque chose de profond ; et la gloire, la fortune et une place dans l'histoire attendent quiconque parviendrait à en percer les secrets.
Instructions
Étant donné un entier positif, renvoie le nombre d'étapes qu'il faut pour atteindre 1, selon les règles de la conjecture de Collatz.
Sous-types
Cet exercice définit un sous-type appelé Positive, pour tous les entiers naturels supérieurs à 0.
On peut voir un sous-type comme un couple ⟨x, h⟩, où x est la valeur et h la preuve de sa validité.
On peut accéder à la valeur contenue dans un sous-type (x, ici) en utilisant .val, par exemple x.val.
On peut accéder à sa preuve en utilisant .property, par exemple x.property.
On peut aussi accéder aux deux par filtrage de motifs, comme d'habitude.
Pour construire une valeur d'un sous-type, il faut prouver sa validité, ici, que le nombre est supérieur à 0.
Lean contient un certain nombre de lemmes et de théorèmes qui peuvent servir de point de départ à cette preuve.
Par exemple, Nat.zero_lt_succ est un lemme qui affirme que pour tout entier naturel n : 0 < n + 1.
On trouve une bonne référence pour la démonstration de théorèmes en Lean dans la documentation principale.
Preuve de terminaison
En Lean, les fonctions récursives doivent prouver leur terminaison.
Cette preuve est parfois évidente, découlant implicitement de la structure d'une fonction.
Dans d'autres cas, il faut la rendre explicite.
Dans cet exercice, la terminaison de la fonction est précisément la collatz conjecture, qui est un problème mathématique ouvert.
Envisage d'utiliser l'une des options suivantes :
- Ajouter le mot-clé
partial avant la déclaration d'une fonction désactive la vérification de terminaison et autorise des appels récursifs (potentiellement dangereux).
- Les constructions impératives autorisées dans le code monadique, comme
while, sont implémentées en interne à l'aide de la récursion partielle ; on peut donc les utiliser dès lors que la terminaison n'est pas exigée.
Utiliser la monade Id est un moyen commode d'activer ces constructions dans du code qui, sinon, a l'air pur, sans introduire d'effets supplémentaires.
- Définir une fonction auxiliaire avec un paramètre supplémentaire pour le nombre maximal d'appels récursifs garantit la terminaison.
