J'utilisais Isabelle, notamment parce qu'il me semblait le plus avancé en ce qui concerne son interface, ses outils (sledgehammer) et ses bibliothèques (notamment l'intégration, puisque mon but était de calculer une intégrale, même si je ne suis pas arrivé jusque là).
Bien évidemment, j'utilisais les tactiques de preuves tout le temps, et surtout sledgehammer pour trouver les bonnes combinaisons de tactiques. En relisant de plus près mon code, je me rends compte qu'en fait parfois, ce que je fais en 5-10 lignes pouvait se faire en une ligne que sledgehammer trouvait, sauf que cette ligne pouvait prendre entre 100ms et 1s (et était illisible). Je crois que j'ai essayé de faire quelque chose qui ne mettait pas plusieurs minutes à compiler à chaque fois que j'ouvrais isabelle. Mais même si j'avais utilisé tout le temps les résultats de sledgehammer, aussi illisibles et lents qu'ils aient été, mon fichier aurait quand même fait plusieurs centaines de lignes.
En détail j'avais une fonction \alpha_{\sigma} définie de la manière suivante:
- soit \theta une fonction 2\pi périodique qui vaut 1 sur (-\pi,0) et -1 sur (0,\pi)
- soit q(a,b,a',b') = 3aa' -ab' -a'b -bb'
- soit \alpha_{\sigma}(t_1,t_2) = q(\theta(t_1-\sigma),\theta(t_2-\sigma),\theta(t_1),\theta(t_2)).
Le but final était de calculer la fonction F(t,s_1,s_2) = \int_{\Omega_{t-\max(s_1,s_2)}} \phi'(t+t_1-\max(s_1,s_2)) \alpha_{|s_1-s_2|}(t_1,t_2) dt_1dt_2, où \Omega_\tau est un domaine qui dépend du paramètre \tau et \phi une fonction quelconque. Mais comme je l'ai dit, je ne suis pas arrivé jusque là en isabelle.
Mais sur \alpha_\sigma, voici le genre de choses que je voulais : si 0 <\sigma <\pi et (t_1,t_2) \in (\sigma,\pi)\times(-\pi,0), alors \alpha_\sigma(t_1,t_2) = 4. Pour un humain, c'est facile : regarder ce que valent chacun des \theta(t_1-\sigma), etc., et remplacer leur valeurs dans la définition de q.
Mais en isabelle, ça a donné: définition de theta (plusieurs lignes parce que j'ai défini un "real_mod x y = y*(x/y - floor(x/y))" pour ce faire), démontrer que c'est 2-pi périodique (une bonne cinquantaine de lignes parce qu'il a bien fallu gérer ce real_mod), démontrer que ça vaut bien -1 sur (0,pi) (-2pi,-pi), etc. et 1 sur les autres intervalles, puis définir alpha (ça ne pose pas de problème), et enfin démontrer que ça vaut bien ce que ça vaut sur (\sigma,\pi)\times(-\pi,0). Et puis sur une vingtaine d'autres rectangles. Et avec moi qui ne voulais pas des lignes à rallonge (en nombre de caractère et en temps d’exécution) que proposait sledgehammer, ça donne 800 lignes.
[^] # Re: Typos, erreurs et preuves
Posté par danarmk . En réponse à la dépêche Sortie du Frido pour les Matheux. Évalué à 5. Dernière modification le 20 septembre 2023 à 11:15.
J'utilisais Isabelle, notamment parce qu'il me semblait le plus avancé en ce qui concerne son interface, ses outils (sledgehammer) et ses bibliothèques (notamment l'intégration, puisque mon but était de calculer une intégrale, même si je ne suis pas arrivé jusque là).
Bien évidemment, j'utilisais les tactiques de preuves tout le temps, et surtout sledgehammer pour trouver les bonnes combinaisons de tactiques. En relisant de plus près mon code, je me rends compte qu'en fait parfois, ce que je fais en 5-10 lignes pouvait se faire en une ligne que sledgehammer trouvait, sauf que cette ligne pouvait prendre entre 100ms et 1s (et était illisible). Je crois que j'ai essayé de faire quelque chose qui ne mettait pas plusieurs minutes à compiler à chaque fois que j'ouvrais isabelle. Mais même si j'avais utilisé tout le temps les résultats de sledgehammer, aussi illisibles et lents qu'ils aient été, mon fichier aurait quand même fait plusieurs centaines de lignes.
En détail j'avais une fonction \alpha_{\sigma} définie de la manière suivante:
- soit \theta une fonction 2\pi périodique qui vaut 1 sur (-\pi,0) et -1 sur (0,\pi)
- soit q(a,b,a',b') = 3aa' -ab' -a'b -bb'
- soit \alpha_{\sigma}(t_1,t_2) = q(\theta(t_1-\sigma),\theta(t_2-\sigma),\theta(t_1),\theta(t_2)).
Le but final était de calculer la fonction F(t,s_1,s_2) = \int_{\Omega_{t-\max(s_1,s_2)}} \phi'(t+t_1-\max(s_1,s_2)) \alpha_{|s_1-s_2|}(t_1,t_2) dt_1dt_2, où \Omega_\tau est un domaine qui dépend du paramètre \tau et \phi une fonction quelconque. Mais comme je l'ai dit, je ne suis pas arrivé jusque là en isabelle.
Mais sur \alpha_\sigma, voici le genre de choses que je voulais : si 0 <\sigma <\pi et (t_1,t_2) \in (\sigma,\pi)\times(-\pi,0), alors \alpha_\sigma(t_1,t_2) = 4. Pour un humain, c'est facile : regarder ce que valent chacun des \theta(t_1-\sigma), etc., et remplacer leur valeurs dans la définition de q.
Mais en isabelle, ça a donné: définition de theta (plusieurs lignes parce que j'ai défini un "real_mod x y = y*(x/y - floor(x/y))" pour ce faire), démontrer que c'est 2-pi périodique (une bonne cinquantaine de lignes parce qu'il a bien fallu gérer ce real_mod), démontrer que ça vaut bien -1 sur (0,pi) (-2pi,-pi), etc. et 1 sur les autres intervalles, puis définir alpha (ça ne pose pas de problème), et enfin démontrer que ça vaut bien ce que ça vaut sur (\sigma,\pi)\times(-\pi,0). Et puis sur une vingtaine d'autres rectangles. Et avec moi qui ne voulais pas des lignes à rallonge (en nombre de caractère et en temps d’exécution) que proposait sledgehammer, ça donne 800 lignes.