J’ai commencé (il y a 3 heures) la rédaction d’un article au doux nom
de « Un zeste de mathématiques assistées par ordinateur » et j’ai pour objectif de proposer en validation
un texte aux petits oignons. Je fais donc appel à votre bonté sans
limites pour dénicher le moindre pépin, que ce soit à propos
du fond ou de la forme. Vous pourrez consulter la bêta à votre guise à
l’adresse suivante :
Super contenu et tu as trouvé le bon univers avec des petits théorèmes sympas pour ça. Tu as inversé le rewrite <- sym_n_s. et le rewrite <- rotd_n_o. dans la preuve que tu donnes. La preuve reste correcte bien sûr, c’est juste que tu dis qu’on fait la preuve dans le sens inverse, donc on s’attend à avoir l’ordre inversé par rapport à la preuve informelle.
Une question très naïve après un premier survol de l’article: pourquoi définir tes opérations sur des points comme des variables opaques, au lieu de les définir comme des fonctions (et donc les propriétés seraient des lemmes sur ces fonctions au lieu d’axiomes) ? Est-ce que c’est prévu pour dans un second temps ?
Une question très naïve après un premier survol de l’article: pourquoi définir tes opérations sur des points comme des variables opaques, au lieu de les définir comme des fonctions (et donc les propriétés seraient des lemmes sur ces fonctions au lieu d’axiomes) ? Est-ce que c’est prévu pour dans un second temps ?
C’est un choix. L’idée c’est de faire des maths qui ressemblent aux maths habituelles, en ayant quelques axiomes et en démontrant des propriétés. Je n’ai volontairement pas introduit de fonctions, parce que ça sort de cet objectif. Ce ne sera donc pas non plus dans un second temps (a priori).
Ceci dit on pourrait tout à fait définir exhaustivement les fonctions, mais les démonstrations deviennent moins amusantes, parce qu’en gros il suffirait probablement de destruct et unfold dans tous les sens pour arriver à n’importe quel résultat. Là avec les axiomes, il y a beaucoup d’implicite, et je voulais le garder pour que les démonstrations ne ressemblent pas à de l’exhaustion de cas.
Une variante avec définitions pourrait être un autre petit article qui présente l’extraction de code, mais je n’ai pas prévu d’en écrire un. En fait, avant les choix que j’ai faits, j’avais tenté une petite fonction amusante qui rend une transformation permettant de retrouver le nord depuis n’importe quel point avec seulement les opérations élémentaires. C’était assez artificiel et pas très amusant.
Je viens de mettre à jour la bêta avec une figure pour illustrer.
@gasche : après réflexion, un article sur l’extraction de code serait sûrement intéressant, mais il faudrait prendre une approche plus orientée langage de programmation. Il faudrait un univers un peu plus riche. Je pense par exemple à un optimiseur de parcours qui opérerait sur un damier, et il s’agirait alors de prouver des théorèmes sur les simplifications possibles (par exemple tourner trois fois à droite revient au point de départ).
Je viens de lire un peu en diagonale. Et moi qui ait un a priori plutôt négatif sur Coq (un de mes potes adoraient ça et m’a bien saoûlé avec), tu m’as presque donné envie d’en faire !
Le choix actuel me convient. Par contre je pense que dans ta réponse tu fais un lien un peu trop fort entre "définir des fonctions" et "extraire du code". Même quand on n’essaie pas d’écrire un programme, mais une preuve mathématique, il peut être utile de manipuler des objets au comportement calculatoire (dans le cas de ton article, c’est même "trop utile" puisque comme tu le dis cela trivialise les preuves). D’ailleurs la bibliothèque SSR en Coq, qui a été développée pour faire des maths (et pas de la programmation), tient son nom de "Small Scale Reflection", une technique de preuve qui utilise beaucoup de petits calculs locaux.
Tu as inversé le 
