Each language version is independently generated for its own context, not a direct translation.
Imaginez que vous êtes un architecte qui doit construire une maison (une preuve mathématique) avec un logiciel très puissant appelé Isabelle/HOL.
Dans ce monde, il existe deux façons de construire :
- La méthode "Apply" (le style procédural) : C'est comme donner des ordres à un robot de construction en mode "pilote automatique". Vous dites : "Prends ce mur, pose-le ici, puis enlève cette brique, puis vérifie si le toit tient". C'est rapide, on peut tester plein d'idées différentes très vite, mais c'est un peu comme une recette de cuisine écrite en code binaire : si vous changez un ingrédient au début, tout le reste peut s'effondrer sans que vous sachiez pourquoi. C'est fragile et difficile à lire pour un humain.
- La méthode "Isar" (le style déclaratif) : C'est comme écrire un plan d'architecte magnifique et clair. Vous dites : "Voici le mur, il repose sur ces fondations. Voici le toit, il s'appuie sur ce mur". C'est beau, logique, et si vous changez une fondation, vous voyez immédiatement quel mur tremble. C'est robuste et facile à comprendre, mais c'est plus long et plus difficile à écrire au début.
Le Problème
Beaucoup d'utilisateurs commencent par la méthode rapide (Apply) pour explorer les idées, mais ils se retrouvent avec des "plans" illisibles et fragiles. Ils aimeraient pouvoir transformer ces instructions robotiques en plans d'architecte clairs, mais le faire à la main est un travail épuisant et fastidieux.
La Solution : Apply2Isar
C'est là qu'intervient Apply2Isar, l'outil présenté dans cet article.
Imaginez Apply2Isar comme un traducteur automatique ultra-puissant ou un chef cuisinier qui transforme un plat préparé industriel en recette de grand-mère.
Comment ça marche ?
L'outil regarde votre script "Apply" (la liste d'ordres robotiques). Il le rejoue étape par étape, comme un film en accéléré, pour voir exactement ce qui se passe à chaque moment. Ensuite, il écrit le script "Isar" (le plan clair) en inversant le temps : il part du résultat final et explique comment on y est arrivé, en nommant chaque étape intermédiaire.L'analogie du film à l'envers :
Si votre preuve Apply dit : "Enlève la brique A, puis pose la brique B, puis vérifie le toit", Apply2Isar va écrire : "Pour vérifier le toit, nous avons besoin de la brique B. Pour avoir la brique B, nous avons dû enlever la brique A."
Le résultat est un texte qui ressemble à un raisonnement mathématique humain, même si le processus de création était purement mécanique.
Les Défis (Les Pièges du Traducteur)
Traduire n'est pas toujours simple, comme essayer de traduire un poème en gardant le même rythme. Les auteurs ont dû résoudre plusieurs énigmes :
- Les "Briques" multiples : Parfois, une seule commande Apply touche dix murs en même temps. Apply2Isar doit décider s'il faut écrire dix phrases séparées (ce qui serait long) ou grouper les actions intelligemment pour que ce soit lisible.
- Les "Sous-chantiers" (Subgoals) : Parfois, on doit construire une aile de la maison avant de continuer le reste. L'outil doit savoir déplacer ces sous-chantiers au début du plan pour que tout soit cohérent, comme si on construisait d'abord les fondations avant de montrer le plan du rez-de-chaussée.
- Les noms qui se trompent : Parfois, on utilise le même nom pour deux choses différentes (comme appeler deux chats "Minou"). L'outil doit être assez malin pour renommer les chats afin qu'on ne les confonde pas dans le plan final.
- Les "Inconnus" (Variables schématiques) : Parfois, la preuve utilise des variables mystères ("X") qu'on ne connaît pas encore. L'outil ne peut pas toujours deviner la solution, donc il laisse parfois de petits bouts de code "Apply" au milieu du plan Isar, comme une note manuscrite disant "À vérifier plus tard".
Le Résultat
Les auteurs ont testé leur outil sur des milliers de preuves réelles (des milliers de pages de mathématiques).
- Le succès : Dans 95 % à 99 % des cas, l'outil a réussi à transformer le code robotique illisible en un plan d'architecte clair et robuste.
- L'avantage : Même si le résultat ressemble parfois un peu trop à une machine (il manque un peu de "poésie" humaine), il est infiniment plus facile à lire, à corriger et à maintenir que le code original.
En Résumé
Apply2Isar est un pont entre la vitesse de l'exploration (le style Apply) et la clarté de la communication (le style Isar). C'est un outil qui permet aux mathématiciens et aux informaticiens de ne plus avoir à choisir entre "aller vite" et "être clair". Ils peuvent aller vite, puis laisser l'outil transformer leur brouillon en un chef-d'œuvre lisible pour tout le monde.
C'est comme si vous pouviez griffonner des idées en vitesse sur un coin de table, et qu'un assistant intelligent les transcrivait instantanément dans un livre de mathématiques parfaitement structuré.