Apprentissage

Dans l'optique de résoudre des exercices de classe préparatoire, nous avons essayé de concevoir un assistant de preuve automatique.

Intérêt

Plus puissant que les tactiques de type auto, eauto, omega... existant déjà dans coq, notre assistant devra être un assistant intelligent, qui ne se contentera pas d'essayer pleins de tactiques différentes tout en créant un lambda-term horriblement moche.

Fonctionnement

L'idée a été d'écrire un algorithme d'apprentissage qui s'adapte au langage coqueux. Nous fournirons ensuite à cet algorithme un grand ensemble de preuves déjà faites et validées afin qu'il construise un arbre d'apprentissage. Cet arbre permettra ensuite à partir d'un début de preuve (but, sous-buts, hypothèses) de résoudre miraculeusement (dans le meilleur des cas) la preuve de l'utilisateurt désireux de Coquille.

IDE

Le WP IDE s'est donné comme but de construire une interface de programmation en Coq plus orientée vers l'aide à la programmation que l'actuel CoqIde. Quelques listes non exhaustives :

Ce que Coquille fait que CoqIde ne fait pas

Au niveau du code :
  • Les numéros de ligne
  • Le code folding (replier des lignes de code en une seule, pour une preuve par exemple)
  • Des raccourcis plus "classiques", et personnalisables
  • Possibilité de faire "Redo" après des "Undo"
Au niveau du langage :
  • La gestion de Ltac Debug, avec une interface de parcours des résultatsScreenshot
  • Plusieurs instances de Coqtop, une par onglet ouvert
  • Un affichage des résultats au choix : classique ou LaTeX-likeScreenshot
  • L'action "Next/Previous" d'envoi d'une commande est considérée comme une action comme les autres, donc "Undo/Redo" agit dessus
Ce que CoqIde fait que Coquille ne fait pas (encore), et s'il est prévu de l'implémenter
Au niveau du code :
  • Lister les tactiques existantes dans un menuSera fait
  • Lister les actions disponibles par click droit sur une hypothèse / un butSera fait
Au niveau du langage :
  • Le Proof WizardNe sera pas fait
  • La gestion des Write State / Restore StateNe sera pas fait
  • La gestion de l'aideSera fait
  • La gestions de la compilationSera fait
Preuves Toute la documentation générée par coqdoc est disponible ici. Le respect des conventions de nommage permet une consultation facilitée.

Quelques jolis résultats

De nouvelles bibliothèques

Tactiques

Valid XHTML 1.1 CSS Valide !

Nous contacter - Dernières modifications : novembre 2009