Rapport final du projet Coquille
Contents
1. 3 14 L r sultatiactuell cla ee e wk SPER as ee Be wee RENNES 3 4 1 Ce que COQUILLE fait et que CoqIDE ne fait pas 3 4 2 Ce que CoqIDE fait et que COQUILLE ne fait pas encore 3 4 3 Ce que ni l un ni l autre ne font bien 344 Aperctt en couleur aan u e e a cm EE ee a a E de dr Us Jos GES Objects A dings Guen NE ea at gh Nes aol ao col Sar Uh Court Me rar ni el Le WP Apprentissage AT ObjectllSe ces t ee Le GMa he At ONE LE AU see 5 4 8 td 4 2 Les arbr s de d cisions 214 44 bee bee Ree A EE SAAR xx 4 3 Organisation des modules 4 3 1 Fouille sur le net R solution d exercices 4 3 2 Parsing discussion avec Coqtop 43 3 Algorithme d apprentissage 4 34 Traductions ove IA Bee Sk de ea eB alii AA DA RE EMA ce 4 4 Parsing discussion avec coqtop A5 Apprentiss ge m is 2 w aaa he Side eee BAGS ee ere ok BR ene An E 456 Pipeau os due al ae ds dudit 414 408 FD GA eee A GU Sede bed AY R sultats eu eee tac eee hae eee te de eee aah LM AR RS 4 8 Perspectives site me 44 AAA ra EERE REY Ee ea ie aa A A Le WP communication polo Objects se 2 Se foe hie EE Scat at A tin fh ue pe ae 5 2 Mat riels et m thodes 50 R SULTATS ts2. we abstract iv Abort Y Pr c dent Suivant Au d but Tout Jusqu au curseur Nouveau fichier x 1 subgoal reflexivity Qed 2 2 Line 5 Visual column O Text column 0 INSERT FIG 3 6 La fen tre principale Nouveau fichier fal Fichier Edition Naviguer Affichage Aide Dee ee el es A OO Nouveau Ouvrir Enregistrer Toutenregistrer Copier Couper Coller Annuler R tablir t y f a ave abstract vi M Abort x Pr c dent Suivant Au d but Tout Jusqu au curseur 5 soup ER 2 Nouveau fichier X F mine Size Type Documentation 5 E Ratanv 31KB v Fil cs E RFsequence fac 18 KB v Fil 2 1 subgoal JL Go 2 E RFsequence v 1KB v Fil S P Rfunction defv 216 bytes v Fil 5 7 Rfunction_facts v 1KB v Fil 8 E Rintegral_tactic v 1KB v Fil E Rintegral_usual v 2KB vFil M Rintegral v 17KB v Fil E Rmarkov v 9KB v Fil M Rpser_def v 6KB v fil E Rpser_facts v 53KB v Fil E Rsequence_bas 7KB v fil n F Rsequence_cv_f 34 KB v Fil j E Rsequence_fact 3KB v fil E Rsequence_rel_ 30KB v Fil E Rsequence_ring v 1KB v fil Rsequence_sub 7 KB v Fil Rsequence_tact 8KB vFil E Rsequence_usu 15 KB v Fil E Rsequence v 3 KB v Fil B Rseries_facts v 36 KB v Fil Rseries_Rieman 9KB v Fil Rseries v 902 bytes v Fil RStidina 9KB vFill Line 2 Visual column 0 Text
3. OTHER Equal Goal Hyp NO forall Equal Son 0 0 Son 0 1 NO YES YES reflexivity assumption exact H1 4 3 Organisation des modules 4 3 1 Fouille sur le net R solution d exercices Un premier travail est de rassembler un grand nombre de d monstrations dans un m me domaine Nous nous sommes essay s sur deux domaines la logique du premier ordre et les comparaisons d entiers Pour des tactiques compl tes pour ces domaines il faudrait plus de lignes de d monstrations Mais ces collections suffisent tester notre algorithme 4 3 2 Parsing discussion avec Coqtop Les fichiers que l on r colte sont des fichiers coqs normaux Il faut ensuite en extraire les exemples que l on va apprendre et les mettres sous la forme que l algorithme d apprentissage prend en param tre 4 8 3 Algorithme d apprentissage L algorithme d apprentissage transforme ces donn es exp rimentales en un arbre de d cision 4 3 4 Traduction L arbre est transform automatiquement en une tactique qui pourra ensuite tre utilis e telle quelle 24 lt Parsing discussion avec cogtop gt 4 4 Parsing discussion avec coqtop Il faut aussi analyser les fichiers de preuves v pour d terminer les tactiques Cette analyse est sp cifique et on n a pas besoin d analyser les fichiers vernaculaires d une mani re aussi compliqu e que celle de Coq qui utilise un nombre importan
4. 5Comme peu pr s tout stdlib Contenu de la biblioth que Elle d finit des propri t s de base et op re quelques renommages sur les lemmes de stdlib Elle se veut tr s g n raliste sans pour autant assommer l ventuel utilisateur sous des monceaux de r sultats la techX Convergence Nous avons renomm la convergence vers un r el afin de respecter un sch ma plus naturel Nous avons aussi d fini formellement la divergence vers l infini ce qui n existe pas de base dans la biblioth que standard Rsequence contient une quantit assez impressionnante de lemmules sur la compatibilit des op rations avec la limite Ces r sultats sont d ailleurs utilis s par une tactique de d cision de convergence Relations de Landau Grands classiques des propri t s s quentielles qui souffrent pourtant de cruelles absences de stdlib Nous avons donc d fini les relations de Landau petit o grand O et quivalence de suite Nous en avons montr des propri t s importantes quasi ordre quivalence compatibilit s entre elles etc Nous avons en outre montr des compatibilit s avec les propri t s la limite et les op rations usuelles Suites usuelles Afin de rester dans un esprit pratique notre biblioth que d finit des suites appel es tre utilis es un peu partout suites constantes polynomiales exponentielles et factorielles Certains r sultats de comparaison ont t prouv s et nous avons aussi d crit leur co
5. 3 2 1 Le Langage utilis Apr s r flexion il a t d cid d utiliser le C Durant la premi re semaine du Projet deux parties du WP IDE se sont affront es en proposant un mini diteur cod soit en Java avec Swing soit en C avec Qt Au cahier des charges ils devaient proposer l dition de texte avec les menus basiques copier coller etc la coloration syntaxique d sactivable des parenth ses et de certains mots cl s un bouton insertion qui ins re du texte apr s le curseur un bouton pour afficher l int gralit du texte dans une nouvelle fen tre 16 Apr s comparaison sur des crit res pr d finis il en est ressorti que les deux langages sont tr s similaires tant en rapidit de codage ils ont une API pour dessiner les fen tres chacun par exemple en structure et sont assez abordables Les deux mini IDE taient quivalents la diff rence que celui en C tait plus rapide et montrait plus de flexibilit dans la coloration syntaxique Le mini IDE en java utilisait des biblioth ques annexes JLex pour la coloration syntaxique Nous avons donc choisi peu de diff rences le C S ajoutait le fait que parmi nous plus de personnes taient comp tents en C et novices en Java 3 2 2 Les Biblioth ques utilis es Qt Qt nous a s duits pour la gestion des fen tres En effet Qt Creator facilite amplement la cr ation de fen tres le code Qt est tr s clair pro
6. Rapport final du projet COQUILLE M1 Informatique Fondamentale ENS Lyon 4 janvier 2009 Table des mati res 1 Le projet Coquille en g n ral 1 1 Introductions ayn at ele eee Le en Ch OA dan a PRO ROME er enr ee tn Se Wid Pr sentation g n rale concn a a a A 4 2 RARE ele ouh rate ait ee M es ELZ Motivation AA TRE 2 BIOS OY Os brise CCE Se ER mis LT Pubie vise th LL Le A LR RAR ok lil Approches sss soe EMULE es ee MP er A A Dae es Sh Ake it de N 1 1 5 Ressources humaines g 42 4 eee RRA am mas OR ee ee ee a a 2 Le WP preuves DL 4 WOBIG UC LAS Be RE o He gay Sq aaah aaa PY BL AAA ee BOM AE Aer 2 1 1 Ind nombrabilit de R Runcountable 2 1 2 Implications classiques de l axiomatique r elle Rmarkov 22 1 Reels x 65 90 hk De ag ces ra etre de Ded DOG Oo oS Reto GO ee ee 2 2 1 Suites r elles Rsequence 2 2 2 S ries r elles Rseries o oo ee tasat ta ee N 2 2 3 S ries enti res r elles Rpser 2 2 4 Int grales de Riemann r elles Rintegral 2 3 Complexes gon e rte ho MATE LT Line a ii OER Be wis ee ERAS 2 3 1 Propri t s de C et fonctions de base 2 3 2 Propri t s de C Cmet Ctacfield 2 3 3 Des fonctions et d finitions de base 2 3 4 Suites complexes Cse
7. et a motiv la d monstration de nombreux r sultats interm diaires sur les s ries comme la s paration d une somme infinie selon la parit de ses termes Elle a n cessit l introduction des sommes de suites relatives Z R ainsi que les sommes doubles correspondantes parfois priv es de leurs termes diagonaux Une partie non n gligeable de la preuve est consacr e des majorations fines et du calcul 6Pour plus de clart se r f rer Rseq_asymptotic 2 2 3 S ries enti res r elles Rpser Motivations Les s ries enti res sont une partie int grante du programme des classes pr paratoires Elles sont prati quement totalement absentes de la biblioth que standard une notation Pser traduit le fait que la suite des sommes partielles converge mais les rayons de convergence ne sont nullement formalis s Leur forme tr s particuli re permet de plus de d montrer des th or mes puissants sans hypoth ses trop restrictives On pourrait en d duire la d rivabilit et la continuit de certaines fonctions de la biblioth que standard exp cos sin qui sont actuellement prouv es la main et qui utilisent des hypoth ses inutiles D finitions Une partie importante de nos deux premi res semaines de travail a t de trouver les d finitions des concepts nous assurant une manipulation ais e de ceux ci elles ont fait l objet de nombreuses retouches au fur et mesure que nous progressions dans les preuves
8. 1 subgoal Vn nat 3p nat gt 3q nat p A pzq 1 Fic 3 5 L affichage MT X like 3 4 2 Ce que CoqIDE fait et que COQUILLE ne fait pas encore Au niveau du code Lister les actions disponibles par clic droit sur une hypoth se ou un but 19 Au niveau du langage Le Proof Wizard La gestion de la compilation et des exportations CoqIDE permet de compiler exporter un fichier sans passer par ligne de commande 3 4 3 Ce que ni l un ni l autre ne font bien Au niveau du code L auto compl tion Au niveau du langage La gestion de l aide La gestion des Write State Restore State En th orie la commande Write State est cens e sauvegarder l tat de l interpr teur variables commandes envoy es etc tandis que Restore State est cens restaurer cet tat En pratique Restore State ne marche pas dans Coqtop 3 4 4 Aper u en couleur Sur la figure 3 6 on peut voir la fen tre principale sans panneau optionnel La partie gauche est un diteur de document par lequel on dialogue avec Coq Celle de droite contient 2 r cepteurs de texte qui affichent les r ponses de Coq Sur la figure 3 7 on peut voir la fen tre principale avec des panneaux optionnels Le panneau de gauche contient un explorateur de fichiers et un navigateur de documents ouverts Celui de droite est le panneau de documentation Ces panneaux sont bien entendu d placables d autres emplacements autour de l
9. 2 Jaan Se Ae DE CS ee qu a a ir e ee ee te ee du done 6 Annexe 1 documentation de PIDE 23 23 23 24 24 24 24 24 25 27 28 28 29 29 29 29 31 Chapitre 1 Le projet Coquille en g n ral 1 1 Introduction 1 1 1 Pr sentation g n rale L objectif de COQUILLE COQ User Interactive Library Learning Expert est la r alisation d un environ nement de preuve assist e par ordinateur dotant l utilisateur des outils n cessaires l impl mentation de r sultats proches de ceux d montr s dans les classes pr paratoires Il doit tre labor partir de l assistant de preuves Coq L objectif est en somme d largir la port e de Coq aux math matiques de classes pr paratoires et des math maticiens non forc ment experts en calcul des constructions et en th orie des types 1 1 2 Motivation La preuve assist e par ordinateur ouvre de nouvelles perspectives pour les math matiques modernes Le chemin parcouru depuis Automath 3 fin des ann es 60 permet de parler r ellement de preuve interactive l utilisateur n a plus fournir un A terme du bon type mais peut le construire via l utilisation de tactiques et de lemmes d finis dans la biblioth que standard ou par ses soins La principale limite des assistants de preuves n est donc plus la complexit de la th orie sous jacente mais Vabsence de certaines biblioth ques de base une bonne partie du programme des classes pr paratoires n est pas co
10. Kohlenbach An Arithmetical Hierarchy of the Law of Excluded Middle and Related Principles Logic in Computer Science Symposium on 2004 2 Alberto Ciaffaglione and Pietro Di Gianantonio A Tour with Constructive Real Numbers 2000 3 F Dechesne Archives automath http www win tue nl automath 4 Hugo Herbelin Proposed naming conventions for the Coq standard library Technical report INRIA 2009 5 Cezary Kaliszyk and Russell O Connor Computing with Classical Real Numbers Journal of Formalized Reasoning 2008 30 Chapitre 6 Annexe 1 documentation de PIDE
11. column 0 _ IN m gt Fic 3 7 Les panneaux optionnels 21 Nouveau fichier Fichier Edition Naviguer Affichage Aide ee ees a OO oes Nouveau Ouvrir Enregistrer Tout enregistrer Copier Couper Coller Annuler R tablir Documentation ns A Seer a ts toe abstract Go Pr c dent Suivant Au d but Tout Jusqu au curseur Nouveau fichier X 1 subgoal Line 2 Visual column O Text column 0 INSERT Documents Nouveau fichier RFsequence_fac RFsequence v Rfunction_def v 216 bytes Rfunction_facts v 1KB v File Rintegral_tactic v 1KB v File Rintegral_usual v 2KB v File Rintegral v 17 KB v File Rmarkov v 9KB y File Rpser_def v 6 KB v File Rpser_facts v 53 KB v File FIG 3 8 Les panneaux optionnels l ext rieur Date Modified 28 12 09 17 39 28 12 09 17 39 28 12 09 17 39 28 12 09 17 39 28 12 09 17 39 28 12 09 17 39 28 12 09 17 39 28 12 09 17 39 28 12 09 17 39 28 12 09 17 39 Nouveau fichier Fichier dition Naviguer Affichage Aide 33 a hal A D le Nouveau Ouvrir Enregistrer Tout enregistrer Copier Couper Coller Annuler R tablir t F 4 2 ave abstract M Abort y Pr c dent Suivant Au d but Tout Jusqu au curseur 1 Page Raccourcis Pr f rences Pr c dent Meta Ctri Up Default R tablir Ctrl Shift Z Default Jusqu au curseur Meta Ctri Space Default Au d but Meta Ctri PgUp Default Annuler Ctri z De
12. et que nous constations leurs imperfections Nous avons abouti des repr sentations tr s satisfaisantes dont entre autres les suivantes S rie enti re On choisit de repr senter la s rie enti re gt y nz par la suite an ey Les fonctions gt_Pser et gt_abs_Pser sont respectivement de la forme Aa Az An a 1 et Aan AL AN a x et permettent donc de parler ais ment des sommes partielles en n ayant que la suite a y en param tre Rayon de convergence Le rayon de convergence p an est d fini de la mani re suivante p an sup r anar nen est born e On utilise en pratique une version plus faible Cv_radius_weak a r anr y est born e Manipulation des d finitions Quiconque travaill sur la biblioth que des r els peut mesurer quel point les lemmes tr s simples permettant de manipuler les d finitions sont vitaux On se donne donc ici quelques lemmes qui permettront de travailler dans des cas particuliers les d monstrations d ordre g n ral que nous avons faites par la suite ne n cessitaient pas vraiment la pr sence de ce genre de choses Op rations simples On prouve que Cv_radius_weak supporte l affaiblissement et on en d duit que Cv_radius_weak supporte les op rations simples sur les suites oppos somme diff rence pour un r bien choisi Lien entre Pser et convergence de suite On prouve qu il existe un lien entre Pser d finition pr existante no
13. sultats de hi rarchisation des propri t s semi classiques qui nous confortent dans cette supposition D veloppements ventuels L id e de biblioth que r elle auto contenue pourrait tre compl tement impl ment e et cela en expurgeant toutes les r f rences au module Classical de la biblioth que Reals Cependant la t che risque de s av rer longue pour un r sultat l int r t douteux 2 2 R els 2 2 1 Suites r elles Rsequence Motivations Les suites sont parmi les outils de base de l analyse r elle et le moins qu on puisse dire c est que la biblioth que standard de Coq n est ni tr s tendue dans ce domaine ni tr s coh rente Il y a donc une masse de travail non n gligeable Pour ne pas reproduire les d fauts de la biblioth que standard nous nous sommes entendus pour suivre la lettre les conventions de nommages recommand es dans la proposition de Hugo Herbelin 4 m me si cela s av re parfois fastidieux Nous avons galement r parti les lemmes en diff rentes sous biblioth ques th matiques afin de garantir une consultation ais e et de rendre possible une utilisation modulaire 2Nous n avons pas encore trouv de propri t purement analytique sur R qui ait besoin de plus de MP et WLPO pour tre prouv e Evidemment si on accepte l axiome du choix c est une autre affaire 3L axiomatique de Coq suppose explicitement que c est un corps archim dien 4Nous en avons une preuve
14. une commande de base n est pas la m me selon que l on est au sein d une preuve ou non Ensuite certaines commandes sont purement inutiles et ignor es par Coqtop C est le cas de la commande Proof qu il ne faut surtout pas tenter d annuler sous peine d annuler la commande pr c dente Enfin dans certains cas il est tout simplement impossible actuellement d annuler une seule op ration D apr s ces messieurs de l INRIA eux m mes le seul moyen d annuler la commande Qed validant un th or me nomm truc par exemple est d ex cuter Reset truc puis de renvoyer une une les commandes situ es entre la d finition de truc et le fameux Qed Si jamais la preuve est longue ou comporte des calculs longs pour l ordinateur c est compl tement insens Pire encore dans le cas de preuves imbriqu es Reset truc annule toutes les preuves jusqu revenir en mode Galina Une solution envisag e tait d utiliser les commandes Write State et Restore State chaque tape pour pouvoir revenir en arri re plus facilement Seulement Coqtop est tellement surprenant que Write State ne fait pas que sauvegarder l tat il r initialise Coqtop Restore State ne fonctionne pas du tout Nous avons donc contact Vincent Gross INRIA et de cette discussion il ressort que Il n y a l heure actuelle aucune s paration entre Coq et ses interfaces de communication Cogtop CogIDE et que si on a du mal trav
15. On d montre que C est un anneau puis un corps Cela nous permet d obtenir les tactiques ring_simplify ring field_simplify et field qui sont tr s utiles pour r soudre des galit s ces tactiques sont compatibles avec Cpow qui est la puissance enti re 2 3 3 Des fonctions et d finitions de base Motivations Une biblioth que sur les complexes ne peut pas se passer des fonctions de base que ce soit la puissance la norme etc et des lemmes qui permettent leur manipulation compatibilit avec les op rateurs de base in galit s etc Description Cpow est l quivalent de pow pour les nombres complexes Cnorm est la fonction renvoyant la norme d un nombre complexe on a notamment prouv l in galit triangulaire sum_f_CO est la somme finie 2 3 4 Suites complexes Csequence Motivations Il est n cessaire de disposer de r sultats de base sur les suites valeurs complexes pour pouvoir construire une biblioth que traitant des s ries enti res dans C Description Cette biblioth que est la petite s ur de la biblioth que sur les suites valeurs r elles Elle ne fait que transposer les th or mes concernant la convergence des suites et la compatibilit de ces convergences avec les op rateurs de base oppos inverse somme diff rence multiplication 11 2 3 5 S ries enti res complexes Cpser Motivations Les s ries enti res sont la base de la trigonom trie telle qu elle est fai
16. a fen tre et peuvent galement tre extraits comme sur la figure 3 8 Sur la figure 3 9 on peut voir la fen tre de modification des pr f rences L onglet Page contient les pr f rences d affichage des l ments police taille L onglet Raccourcis permet de modifier les raccourcis des actions les plus utilis es L onglet Pr f rences permet de choisir quelques options avanc es d affichage d filement du curseur 3 5 Les objectifs La majorit des objectifs que le WP IDE s taient fix s l origine ont t largement atteints puisqu on dispose d un IDE fonctionnel si on s interdit la gestion de l environnement Write State amp cie qui reprend CoqIDE avec plus de fonctionnalit s et qui est plus pratique utiliser dans l optique du projet Il serait envisageable de continuer le projet si l INRIA finit de d velopper une interface de dialogue avec Coq utilisable En attendant on ne peut que corriger les bugs Au niveau de la distribution nous avons d j mis COQUILLE sous forme de paquets deb amp cie Il nous reste donc principalement distribuer et diffuser COQUILLE dans la communaut Coq et y inclure un petit manuel d utilisation Un manuel programmeur basique est d j mis disposition 20 Fichier dition Naviguer Affichage Aide 0 56 q W LYC e Nouveau Ouvrir Enregistrer Tout enregistrer Copier Couper Coller Annuler R tablir t 3 39
17. ailler de cette mani re c est tout simplement parce que Il n existe aucune API Aucun moyen donc de faire notre propre interface sans faire des choses tr s sales 3 4 Le r sultat actuel 3 4 1 Ce que COQUILLE fait et que CoqIDE ne fait pas Au niveau du code Marquer les num ros de ligne cf Fig 3 1 Le code folding replier des lignes de code en une seule pour am liorer la lisibilit cf Fig 3 2 Des raccourcis clavier plus classiques et personnalisables La possibilit de faire des Redo apr s des Undo cf Fig 3 3 18 Lemma bidon 2 2 10 Variable A Type roe le LS qu Qed Annuler R tablir FIG 3 1 La num rotation des lignes FIG 3 2 Le code folding Fic 3 3 Le Redo Au niveau du langage La gestion de Ltac Debug cf Fig 3 4 C est une interface que nous avons mise au point et qui permet de voir en d tail l ex cution d une tactique en Coq avec une interface de parcours des r sultats G rer plusieurs instances de Coqtop une par onglet ouvert sans annuler tout chaque changement d onglet Un affichage des r sultats en version classique ou MT X like cf Fig 3 5 L action Send Unsend d envoi d une commande est consid r e comme une action comme les autres donc Undo Redo peut agir dessus a yann hourdel dm3 v Cte Fichier Edition Naviguer Affichage Aide AAA TA A A Nouveau Ouvrir Enregistrer Tout enregistrer Copier Coup
18. analyse r elle auto contenue qui ne ferait pas appel des axiomes classiques En effet la plupart des propri t s analytiques sont s quentielles et MP et WLPO permettent de manipuler les suites classiquement Par ailleurs nous avons tent de tirer la quintessentielle moelle classique de l axiomatique r elle Hugo Herbelin pensait que l on pouvait d duire le fait que R tait archim dien des autres axiomes Il nous a communiqu une preuve int ressante qui montrait que l on pouvait d duire le tiers exclu faible WEM dans Type partir de l axiomatique des r els Reals VA Prop A 24 L axiome archim dien et MP sont de fait quivalents Nous avons des indices qui nous laissent penser que cet axiome ne peut pas tre r duit aux autres D abord parce que MP et WLPO sont compl tement orthogonaux en logique intuitionniste Ensuite parce que WEM a beau impliquer WLPO WEM r implique pas non plus MP Or l argument utilis pour prouver WEM l aide de l axiomatique des r els est peu propice la g n ralisation pour MP En effet de quelque bord qu on l attaque la technique employ e ne donne que des r sultats par double n gation ce qui est f cheux pour MP on veut justement liminer cette double n gation videmment nous n avons pas de mod le pour prouver cela mais nous conjecturons que l on ne peut pas se passer de l axiome archim dien On pourra trouver dans 1 une s rie de r
19. e apr s la question Difficult s surmont es Certes nous nous basons sur un algorithme d j connu Mais notre situation est plus compliqu e et il a fallu r soudre un certain nombre de probl mes Multiplicit des r ponses Un m me exemple peut avoir plusieurs r ponses une m me question En effet si il y a plusieurs hypoth ses il y aura plusieurs r ponses la question What Hypothese 7 Renum rotation des hypoth ses Lorsque les exemples arrivent l algorithme d apprentissage la r ponse apply HO sera crite apply i avec 2 l indice de Ho dans la liste des hypoth ses Or ce 7 ne veut rien dire Si l hypoth se Ho avait t un autre endroit on aurait quand m me appel Hp Il acquiert du sens seulement si dans le chemin que l on fait dans l arbre de d cision pour arriver jusqu la r ponse apply HO on pose une question sur une hypoth se et que c est Ho qui y r pond On repr sentera alors apply HO par apply j avec j la profondeur de la question o Ay a r pondu Or il peut y avoir plusieurs hypoth ses r pondant la question on peut se rendre compte plus tard que l une d elles n y r pond pas on peut ne pas encore avoir trouv de question o Ho r pond Grand nombre de r ponses A priori n importe quelle fonction ou constante du langage y compris celles d finies par l utilisateur peuvent tre des r ponses Pour ne pas surcharger l arbre dans le cas o seule
20. e binomial Il n est pas possible de le r utiliser directement pour prouver le r sultat dans les complexes cause de la notation i qui fait appara tre de nouvelles difficult s Existence de racines d un trin me Dans Croot_n nous nous sommes int ress s aux polyn mes Nous avons entre autres prouv l existence d une racine carr e pour tout nombre complexe On a aussi montr que tout polyn me complexe admet 2 racines On a d duit l existence ou non de racines pour un polyn me de degr 2 dans les r els ainsi que la positivit lorsque lt 0 Repr sentation polaire Nous avons d fini les complexes comme des paires de r els Nous ne savions pas a priori qu il existait une repr sentation polaire pour ces complexes Nous l avons donc montr Ce r sultat fait intervenir l arctangente cf Reals Formule d Euler Nous avons d fini l exponentielle complexe comme une somme infinie la m me d finition que l exponen tielle r elle Nous avons donc montr la formule d Euler et cos 6 isin 0 12 Produit de Cauchy complexe Existence de la racine n i me d un nombre complexe Nos r sultats pr c dents nous ont permis de montrer que pour tout nombre complexe z et tout entier n sup rieur 0 il existe un nombre complexe z tel que 27 z 2 4 Topologie 2 4 1 Objets topologiques Topology Motivations L approche standard de d finition des objets math matiques dans Coq est bas e
21. er Coller Annuler R tablir ae voc abstract o a Pr c dent Suivant Au d but Tout Jusqu au curseur Nouveau fichier 3 yann hourdel dm3 v 3 Ltac Debug Pile Pattern rule 0 i TcDebug 1 gt 7 TeDebug 2 gt n bool a b gt induction n brute 3 Conclusion has been matched a amp amp b amp amp true amp amp true amp amp true TeDebug 2 gt a amp amp b amp amp true amp amp true amp amp true Hypothesis b bound to n has been matched bool The goal has been successfully matched TDebug 2 gt TcDebug 3 gt TcDebug 4 gt Let us execute the right hand side part TeDebug 4 gt TDebug 4 gt Goal 1 3 TeDebug 5 gt a bool b bool R Four Sent con TcDebug 6 gt y SSA ivi M pe TeDebug 6 gt a amp amp b amp amp true amp amp true amp amp true a amp amp b amp amp true amp amp true amp amp true Ltac norm assoc rq TcDebug 6 gt Going to execute TcDebug 7 gt 70 Lemma ex1_norm assoc induction n brute a amp amp b amp c 8 d Proof TcDebug 8 gt intros b TcDebug 8 gt norm_assoc b TcDebug 8 gt Die Wed TeDebug 6 gt Line 60 Visual column 15 Text gt TeDebug 7 gt lt Pr c dent s Suivant cancel jx FIG 3 4 Le mode Ltac Debug
22. es classiques d apprentissage nous avons r solu des th or mes en Coq en analysant chaque tape notre raisonnement Nous avons remarqu que nous r flechissions le plus souvent comme des arbres de d cision Nous nous interrogeons sur la structure des hypoth ses et du but commencer par les n uds de l arbre syntaxique de moindre profondeur La racine du but nous donne assez souvent elle seule la tactique utiliser La plupart du temps si le but est T amp U on utilise split si c est forall x TouT gt U on utilise intro D finition des arbres de d cision Un arbre de d cision est d fini par induction comme tant une liste de r ponse une question sur la situation et pour chaque valeur un arbre de d cision Possibilit s pour les questions D apr s ce que nous avons dit plus haut il est logique de poser les questions sur le haut des arbres Donc on s autorise interroger le n ud la racine des arbres syntaxiques des hypoth ses et du but ainsi que les fils des arbres d j interrog s Les questions qu on leur pose sont What addr quel est le token l adresse addr et Equal addri addr2 est ce que les tokens aux adresses addri et addr2 sont les m mes 23 Exemple Ici si le but est de la forme T T on r pondra reflexivity Son i j d signe le j i me fils de l arbre interrog la profondeur 1 Si la valeur ne correspond aucune autre on emprunte la branche 0THER
23. eut d ores et d j la comparer une axiomatique intuitionniste telle que d crite dans 2 D un point de vue logique ceci nous permet de quantifier ce pouvoir expressif ce qui est toujours int ressant D un point de vue pratique cela nous permet de tirer des ponts entre les diff rentes repr sentations des r els qu elles soient constructives ou non Une preuve certaine que cette question poss de un int r t est apport e par le fait qu une partie de notre d monstration a t faite avant nous par des chercheurs il y a quelques mois et sert de base un d veloppement tr s int ressant entre C Corn et Coq 5 1Cependant il en existe une preuve dans C Corn Enonc s L axiomatique r elle nous permet de prouver les deux formules suivantes R_markov VP N B 7 Vn N P n gt In N 7P n MP R_sequence_dec VP N gt B vn N P n Vv Vn N P n WLPO Le premier est le principe de Markov le second est le principe d omniscience limit faible Il est clair que MP n est que l g rement classique m me si crc MP il est constructif au sens algorithmique du terme alors que WLPO est violemment classique il permet de r soudre le probl me de l arr t Contrairement l article voqu pr c demment nous avons montr que le principe de Markov tait enti rement d ductible de l axiomatique r elle Ce r sultat permettrait d crire une biblioth que d
24. fault Tout Meta Ctri PgDown p Default Suivant Meta Ctri Down Default Y apply Cancel Jo Line 1 Visual column O Text column O INSERT Ola FIG 3 9 La fen tre de modification des pr f rences 22 Chapitre 4 Le WP Apprentissage 4 1 Objectifs Lorsque l on prouve des th or mes on a souvent l impression de faire la m me chose on obtient des r flexes dans de nombreuses situations Dans les domaines les plus utilis s il existe maintenant des tactiques r solvant ces op rations r p titives auto de mani re g n rale omega pour les entiers naturels field dans les corps Cependant lorsque l on travaille sur des outils plus rares ou des outils que l on a soi m me d finis il n existe pas de tactiques pr d finies Une solution serait de construire soi m me ses propres tactiques lorsque l on d finit de nouveaux concepts Malheureusement cela est difficile D une part parce que Ltac est assez difficile ma triser d autre part parce qu il est difficile de transformer un savoir faire compos de r flexes en une description de ce savoir faire L objectif de ce groupe de travail est de rem dier ce probl me On cherche donc cr er automatiquement partir de nombreuses d monstrations des tactiques permettant de faire des d monstrations similaires 4 2 Les arbres de d cisions Pourquoi des arbres de d cision Apr s une revue des m thod
25. ficiles ind cidables par exemple il n est bien entendu pas exclu que l ordinateur demande de l aide l utilisateur Rapidit Nous souhaitons proposer l utilisateur un certain nombre de biblioth ques et de tactiques de haut niveau correspondant aux diff rents chapitres du programme des classes pr paratoires L existence de ces outils permettra d impl menter rapidement des preuves complexes en r utilisant des r sultats d j existants Pour parvenir ce r sultat ce projet de recherche s est organis autour de trois axes R sultats math matiques majeurs Les groupes de travail Preuves et Tactiques d veloppent des biblio th ques regroupant les concepts voqu s en classes pr paratoires ainsi que les r sultats majeurs les concer nant D monstrations automatiques Le groupe de travail Apprentissage a pour but de permettre la r solution automatique de r sultats simples via l adaptation d un algorithme d apprentissage classique au contexte d une d monstration en Coq Prise en main facile Le groupe de travail IDE d veloppe une interface intuitive et ergonomique permet tant une utilisation simple de Coq et de l int gralit des r sultats d montr s au sein du projet COQUILLE 1 1 5 Ressources humaines Ce projet est d velopp par 22 l ves du M1 d informatique fondamentale de PENS Lyon Les t ches se sont r parties entre quatre groupes de travail WP dont nous allons d crire les d veloppement
26. lisateur de Coquille les utiliserait et les alimenterait Update la vol e Actuellement si on veut rajouter des exemples il faut refaire enti rement l arbre On pourrait chercher un moyen pour actualiser l arbre de d cision avec les nouveaux exemples m me si on a effac les exemples d avant 28 Chapitre 5 Le WP communication 5 1 Objectifs L objectif de ce groupe de travail est de faciliter la coordination des autres groupes de travail et de promouvoir le projet et ses r sultats aupr s de potentiels utilisateurs 5 2 Mat riels et m thodes Pour atteindre ces objectifs ce groupe de travail a r alis un site Internet une pr sentation du projet notamment de nos r sultats les plus int ressants une page de contacts et la documentation de COQUILLE pour faciliter son utilisation Ce groupe a par ailleurs r alis la r daction des diff rents rapports hebdomadaires et coordonn la r daction du rapport de mi projet Enfin des documents de communications internes et des formations HTML et LTEX ont aussi t r alis es 5 3 R sultats Les principales r alisations de ce groupe de travail sont le site Internet et le pr sent rapport La docu mentation est disponible sur le site Internet pour tenir compte de l avanc e des WP Ce groupe de travail a r alis les diapositives de la d monstration du projet 29 Bibliographie 1 Yohji Akama Stefano Berardi Susumu Hayashi and Ulrich
27. lure directement le code source dans notre programme il nous a donc fallu batailler ferme Ensuite cette biblioth que est un projet entier elle seule et il a t long d apprendre la ma triser car le code quoique tr s bien document reste du code crit par quelqu un d autre ce que tout le monde conna t comme tr s dur relire Un grand merci Hugues Luc Bruant ENSIMAG responsable de cette biblioth que dont les r ponses nos mails taient toujours rapides claires et utiles ce qui nous a sans nul doute sauv de nombreuses mauvaises situations 17 3 3 3 Au niveau du dialogue avec Coq Voici les principaux probl mes ceux qui nous ont pris le plus de temps La discrimination des erreurs Une r ponse de Coqtop qu elle soit bonne ou mauvaise est donn e sur stdout Seul le prompt passe par stderr Et puisque Coqtop ne renvoie aucun autre signal impossible a priori de savoir si une r ponse est une erreur ou pas Les r ponses vides Certaines commandes de Galina ne renvoient absolument rien quand elles fonctionnent et une erreur quand elles chouent Sion attend une r ponse pour pouvoir la discriminer en erreur ou non on peut attendre tr s longtemps Si on choisit un temps maximal d attente rien ne nous dit qu une commande ne va pas prendre exactement 5 secondes de plus que ce laps de temps L annulation Un v ritable casse t te Premi rement la commande d annulation d
28. ment certaines r ponses sont int ressantes on a cr la r ponse 0THER dans laquelle on met les r ponses faisant perdre le moins d entropie Questions non fixes Le fait d interroger une question permet ensuite d interroger ses fils Types complexes Les types des objets sont souvent grands en t moigne le type galinaRoot int id answer list nodeAddress galinaRoot id int galinaTerm list list list list manipul plusieurs endroits du programme Sachant que galinaRoot galinaTerm nodeAddress answer sont encore des types compos s 26 Concepts proches Il est souvent ardu de s y retrouver dans les programmes car il y a beaucoup de structures se ressemblant mais qu il ne faut pas confondre Par exemple on peut consid rer une hypoth se comme un terme de galina un token de galina ou une adresse laquelle on peut poser une question Il y a les arbres de d cision et les arbres syntaxiques Les r ponses un environnement les r ponses aux questions que l on pose sur l environnement Les tactiques l mentaires qui sont les r ponses dans les exemples d apprentissage et la tactique qui r sultera de l arbre de d cision 4 6 Pipeau L apprentissage automatique est souvent accus d tre pipeau Il y a effectivement une part non n gli geable d approximations et de suppositions dans cet algorithme Nous allons les lister ici et voir dans quelle mesure elles sont raisonnables Sup
29. mportement asymptotique Autres Rsequence contient des propri t s inclassables n anmoins fort utiles On peut compter parmi celles l le fait que la convergence et les relations de Landau soient asymptotiques c est dire que tout lemme permettant de prouver une telle propri t peut tre g n ralis en montrant que les hypoth ses ne sont v rifi es qu partir d un certain rang Nous avons aussi quelques r sultats sur les suites partielles 2 2 2 S ries r elles Rseries Contenu de la biblioth que Les s ries sont un prolongement naturel des suites et toutes les d finitions sont donc calqu es sur celles des suites notamment celles de convergence divergence et les relations de Landau En particulier les liens entre convergence divergence et les relations de Landau ont t faits et beaucoup de r sultats concernent les s ries termes positifs puisque beaucoup de probl mes s y ram nent S rie 2 La convergence de la s rie des inverses des carr s des naturels est une propri t connue La somme de cette 2 2 2 ry 2 2 DEN s rie vaut 7 et ce r sultat fait partie des r sultats d analyse r pandus et d montr s de diverses mani res CO Daz n 6 n 1 Cependant les preuves de ce r sultat sont tr s calculatoires ce qui les rend difficiles formaliser La preuve utilis e dans Rzeta2 utilise la d finition de 7 dans la biblioth que standard sous forme d une s rie celle d arctan
30. nce d une preuve et que sa valeur est I Cette d finition est similaire celle donn e pour la convergence des suites et des s ries la valeur de l int grale est un argument et non pas une valeur donn e par une fonction Lien avec les s ries Nous avons fait le lien entre int grales et s ries ce qui a entre autres permis de donner un quivalent de la s rie harmonique Propri t s de base La biblioth que contient les r sultats concernant les propri t s alg briques des int grales somme multi plication par un scalaire ou les manipulations des bornes change des bornes th or me de Chasles int grale sur un sous intervalle Autres r sultats Quelques propri t s d in galit comme Cauchy Schwarz ou l in galit de la moyenne sur les int grales sont maintenant contenues dans la biblioth que tout comme d autres r sultats forts comme la nullit d une fonction continue positive et d int grale nulle ou encore le th or me fondamental de l analyse Ce dernier tait en effet d j d montr dans la biblioth que standard mais ses hypoth ses taient trop fortes en particulier la fonction devait tre C sur R bien que l on ne l int gre que sur un intervalle Ceci a permis de donner la valeur de nombreuses int grales usuelles comme les polyn mes ou les fonctions trigonom triques 2 3 Complexes Motivations L analyse complexe est une importante partie du programme des classes pr parat
31. nt opaque il aurait fallu en comprendre la structure les subtilit s g rer le dialogue avec Coq sans modularit mais en plus cela ne nous semblait pas tr s formateur de reprendre son code On aurait pu certes reprendre CoqIDE et le structurer d avantage mais cela aurait t monstrueusement long Cr er des plugins pour les diteurs classiques Mis part CoqIDE il n y a pas d diteur d di Coq En admettant que l on e t fait un plugin pour un diteur classique NetBeans Code Blocks il aurait t dur de dialoguer avec Coqtop et un plugin ne permet pas de faire un interpr teur Or il nous semble vital d avoir un interpr teur disposition lorsqu on code en Coq Coder un IDE from scratch C est l alternative que nous avons choisie Tout d abord il aura t plus facile de bien structurer le code et de s parer le dialogue avec Coq Cela aura permis galement d int grer facilement la communication avec les fonctionnalit s propos es par l apprentissage De m me g rer des d tails comme la mise en page la coloration le folding de preuves nous para t plus facile si on reprend VIDE z ro Enfin dans le cadre d un tel projet il est plus formateur de coder un diteur partir de rien et de se poser des questions sur la fa on de le coder ou de le structurer dans un but pr cis plut t que de perdre du temps modifier un diteur que nous ne comprenons pas 3 2 Quelques choix faire
32. oires Il est donc ab solument n cessaire de d finir les complexes proprement et de d velopper un tr s grand nombre de lemmes permettant de manipuler les concepts de base Ce sont ces lemmes qui permettent ensuite de d velopper des preuves en vitant de revenir trop souvent aux axiomes ce qui est tr s lourd D finition et notations Les complexes ont t d finis comme une paire de r els Ainsi aucun axiome n a t ajout on se base uniquement sur l axiomatique des r els Nous avons d fini une fonction de R R C afin de pouvoir cr er des complexes Cette fonction s est vu associer la notation i ainsi un complexe peut s crire sous la forme a i b Nous avons aussi permis l utilisation des num rables l aide d une coercion de R dans C Nous avons tent d utiliser des d finitions analogues 4 celles utilis es dans les r els lorsque cela tait possible pour faciliter l utilisation de nos biblioth ques Description Bases D finitions projecteurs et injections des entiers et des r els Fonctions de base Puissance enti re norme et lemmes de manipulation r criture majorations Analyse complexe Continuit et d rivabilit Polyn mes Lemmes sur des polyn mes de degr 2 permettant de r soudre certains probl mes dans les r els Trigonom trie Existence de la repr sentation polaire et formule d Euler Suites Complexes D finition et lemmes sur les suites ainsi q
33. ontre que sur un espace m trique la topologie induite par la distance d finit la m me continuit que la continuit m trique Les espaces vectoriels sont introduits dans Vectors ainsi que la notion de base d un espace La d finition du produit scalaire est dans Inner_product Une importante attention est port e la r utilisation des objets car il s agit typiquement d objets sujets l h ritage Par exemple un espace hermitien est un espace vectoriel sur C de dimension finie et muni d un produit scalaire L utilisation des typeclasses semble incontournable D veloppements futurs Comme Vectors pourra donner naissance des tactiques de manipulation sp cifiques aux espaces vec toriels l h ritage l ajout d un produit scalaire par exemple pourra augmenter le nombre de tactiques et de th or mes disponibles Le but inh rent est d crire et de prouver des th or mes utilisant des objets les plus g n raux possibles pour tendre leur champ d application Pr visions l ordre est indicatif de la priorit suites de Cauchy cas m trique compl tion compacit dimension finie application cas de R o alg bres mesure espace vectoriel topologique axiome du choix quivalents cons quences 13 2 5 Arithm tique 2 5 1 Motivations L arithm tique est une branche difficile des math matiques dont la plupart des preuves reposent soit sur des r
34. oth ses al atoires et la tactique utilis e est apply H Dans l autre moiti les hypoth ses contiennent H True True H 0 1 et des hypoth ses al atoires et la tactique utilis e est inversion H Demander si il y a une hypoth se dont la racine est un ou un n apportera aucune information car tous les exemples ont de telles hypoth ses Donc l algorithme ne posera pas ces questions l Donc il n interrogera jamais les fils droits de H et H qui sont pourtant les seules informations r ellement pertinentes Nous n avons donc aucune borne d approximation pour cette heuristique La seule confiance que nous pouvons lui faire est l intuition notre exemple est quand m me tir par les cheveux lheuristique semble marcher et l exp rience Choix des questions Il arrive que le raisonnement que fait le math maticien ne puisse pas tre traduit dans les termes de l arbre de d cision Consid rons le probl me de l galit de deux conjonctions a amp b amp c amp d amp e b amp a amp d amp c amp e Le math maticien va d abord v rifier que les listes de variables sont les m mes des deux c t s Cette question a un caract re global que l on ne peut pas capturer avec nos questions Equal et What Ca semble la limite la plus s v re notre algorithme Il faudrait rajouter des questions Oui mais lesquelles Si l on autorise un trop grand nombre de questions par rapport au nombre d exemples il
35. position de distribution repr sentative L algorithme n a de sens que si la distribution des tactiques qu il faut utiliser en fonction des r ponses aux questions que l on peut poser sur l environnement est la m me dans les exemples d apprentissage et dans les exemples o va tre utilis l arbre de d cision Les exemples utilis s pour inf rer l arbre et les exemples o l arbre sera utilis sont pris dans le m me domaine Donc d apr s la loi des grands nombres pour un nombre d exemple suffisamment grand la dis tribution dans les exemples sera aussi proche de la distribution r elle que l on veut Le nombre de questions est relativement petit ce qui acc l re la convergence Il y a 2 questions au d part et dans la pratique ce nombre augmente peu Chaque question pos e supprime cette question sauf les questions sur les hypoth ses et rajoute autant de questions qu il y a de fils Les arit s les plus courantes sont 1 et 2 donc le nombre de questions possibles stagne ou augmente de 1 la plupart du temps De plus plus le domaine dans lequel nous g n rons la tactique est restreint plus cette convergence est acc l r e L arbre n est pas minimal Pour d terminer les tactiques en minimisant la taille de l arbre on utilise une heuristique Consid rons un grand nombre d exemples Les buts sont toujours false Dans la moiti des exemples les hypoth ses contiennent H True False H 0 0 et des hyp
36. pre et structur le slots sont g r s proprement en comparaison avec GTK par exemple D autre part la documentation est vraiment tr s abordable de sorte que l on a appris tr s rapidement sur le tas se servir de Qt QCodeEdit Nous avons pass beaucoup de temps chercher une biblioth que d dition de texte fournissant un plugin de code folding Il s est av r qu il en existe peu et QCodeEdit est l une d entre elles Nous nous sommes apercus ensuite que cette biblioth que tr s puissante permet de faire bien d autres choses ce qui nous a beaucoup aid QTermWidget Pour int grer un terminal VIDE ce fut un peu le m me combat que pour trouver QCodeEdit Nous voulions un terminal qui puisse s inclure dans un QWidget et qui soit utilisable exactement comme un terminal UNIX 3 2 3 Le dialogue avec Coq Le choix s est tout simplement restreint Coqtop car nous n en avons pas trouv d autre 3 3 Les probl mes rencontr s 3 3 1 Au niveau du langage Qt et le C n ont pas pos de probl mes majeurs Nous tions d j habitu s coder en C et les documentations de Qt et Qt Designer sont vraiment tr s abordables 3 3 2 Au niveau des biblioth ques Nous avons eu quelques petits probl mes de codage en utilisant la librairie QCodeEdit Premi rement c est une biblioth que plut t destin e tre install e par l utilisateur ind pendamment de toute compilation Nous voulions en inc
37. quence 2 3 5 S ries enti res complexes Cpser 2 3 6 R sultats int ressants o ee o stace a e a e a eaa E a a a a o ZA T polopie es afin a tee ea e a ae RAD a ed A a a ee a 2 4 1 Objets topologiques Topology Zo Arithm tique epa aa BERR RR a AOS rer Oe Be wie oe Late 2 50 MotivatiGns 2 ake aye A bb oe PM ete E E ee Sar a ee eo 2 52 Description Bane it ed 2 5 3 D veloppements futurs 3 Le WP IDE 3 1 Contexte initial ce sa ia ee LENS he Roe ee A nt A din ee ne St eee art CogIDE op ag deg hho E a E ede ante ae A BS Gs anes ae FS 3 1 2 Les besoins du projet COQUILLE ak3 Que faites seo ke eet re t d drames da dus amp ER Bad es 3 2 Quelqu s cholx afaires aba aca eee EE a A ee sages ee 08 US A de 321 Le Langage Utilise z a s ere te eue eg da A lave ane wl bas Vers nn Ve 3 2 2 Les Biblioth ques utilis es 3 2 3 Le dialogue avec Coge e ud ta ke bE a ae Ba memes A els we ie eS 3 3 Les probl mes rencontr s 3 3 1 Au niveau du langage t e e a re dde ses ae du a ee es H Co Co Co Co w en 00 J OO C1 C1 a Et P RRRR MHE ER oe PE RWW NA FO 14 3 3 2 Au niveau des biblioth ques 3 3 3 Au niveau du dialogue avec Coq
38. qui persiste Vimpossibilit de copier coller depuis un autre cadre que celui d dition Vabsence de coloration des d limiteurs ouvrants et fermants correspondants parenth ses etc le cruel manque d outils compl mentaires que tout IDE devrait proposer console biblioth que etc divers bugs de l diteur li s au copier coller des bugs d affichage incompr hensibles sans doutes li s au binding OCaml GTK le manque de personnalisation de l interface On peut en outre constater d autres d fauts de conception plus importants tels qu une gestion des threads catastrophique et ce qui en d coule l impossibilit de valider plusieurs documents la fois Tr s opaque En effet le code de CoqIDE n est pas tr s accessible sa structure pas vidente et il aurait probablement fallu plus de temps le comprendre qu le d velopper Plus exactement il n y a aucune information sur le code part une maigre trame de structure dans la documentation du code source mais cela reste tr s l ger peu modulaire il n y a aucune s paration entre CoqIDE et le noyau de Coq et CoqIDE n a pas de structure propre ind pendante de Coq cf les d tails de la discussion avec Vincent Gross 3 1 2 Les besoins du projet COQUILLE Mise part la n cessit d un IDE pour Coq qui reprenne donc les principales fonctionnalit s de CoqIDE savoir l dition et coloration l en
39. rithme d apprentissage en prenant soin de conserver une forme la plus g n rale et abstraite possible le moins de variables libres possibles pour esp rer de meilleures performances d apprentissage 25 4 5 Apprentissage Entropie On consid re un ensemble x ier On tire au hasard n fois un x x est pris avec la probabilit pj Le meilleur code d crivant la suite des l ments tir s a une esp rance de longueur de n jer pi log pi On d finit alors l entropie du tirage comme gt p log pi soit environ la longueur moyenne du code d crivant quel l ment a t tir En particulier on remarque que si une seule r ponse est possible l entropie est nulle Application de l entropie aux arbres de d cision Nous voulons que chaque feuille de l arbre de d cision l entropie soit minimale C est dire que pour les exemples conduisant une m me feuille la tactique utiliser soit toujours la m me Il faut donc diminuer l entropie chaque tape On veut que l arbre soit de taille minimale donc il faut maximiser la perte d entropie moyenne sur le nombre de n uds total de l arbre de d cision La maximisation exacte n est a priori m me pas dans WP Il para t donc pr ferable d utiliser une heuris tique chaque n ud de l arbre de d cision on cherche maximiser la perte d entropie sur le nombre de fils Pour cela pour toutes les questions possibles on mesure l entropie moyenn
40. s La liste des participants et d coupage des groupes de travail est en annexe Chapitre 2 Le WP preuves 2 1 Logique 2 1 1 Ind nombrabilit de R Runcountable Motivations Le r sultat d ind nombrabilit de R est un r sultat fondamental en th orie des ensembles ce qu il semble il n a toujours pas t d montr en Coq avec l axiomatique classique des r els Quoi qu il n ait pas d int r t en lui m me au sein d une biblioth que d analyse r elle ce th or me m rite clairement de figurer parmi les r sultats de Rlogic Enonc et preuve Ce th or me se pr sente sous deux formes l une plus forte que l autre R_uncountable strong Vf N R Vx lt y fr WneN rHf in a relx yl 0 R_uncountable Vf NOR r Vn EN rF f n 49 La preuve n utilise pas la version g n rale de l argument diagonal de Cantor beaucoup trop dur forma liser en Coq mais utilise la premi re preuve de ce r sultat que Cantor ait fourni Elle repose sur un argument purement topologique 4 savoir la compl tude de R 2 1 2 Implications classiques de l axiomatique r elle Rmarkov Motivations L axiomatique r elle de Coq est classique en ce sens o elle permet de prouver des propri t s que la logique intuitionniste et par l m me Coq dans le contexte vide ne permet pas On ignore encore exactement quelles sont les limites de l expressivit classique conf r e par cette axiomatique mais on p
41. somme On d montre que toute s rie est d rivable donc continue sur son disque de convergence Ce r sultat est obtenu est utilisant le fait que la suite des d riv es des sommes partielles converge uniform ment car normalement sur ce m me disque Etant donn que la d riv e d une s rie enti re est une s rie enti re on a d ailleurs explicit la fonction An_deriv Aa n 1 an41 qui donne la suite associ e la s rie d riv e on vient de prouver que toute s rie enti re est C sur son disque de convergence S ries de Taylor La biblioth que contient galement quelques d veloppements en s rie de Taylor des fonctions usuelles Ces r sultats se trouvent dans le fichier RTaylor 2 2 4 Int grales de Riemann r elles Rintegral Motivations La biblioth que standard contient les bases sur le sujet mais les lemmes et d finitions sont peu maniables et la convention de nommage est loin d tre respect e puisqu il est impossible d inf rer le nom d un lemme et inversement de savoir ce que fait un lemme dont le nom est du type RiemannInt_P42 Nous nous sommes donc attach s fournir des lemmes et des d finitions de plus haut niveau partir des r sulats existants tout en essayant de respecter les conventions de nommage D finitions et notations Nous ne manipulons ici que des int grales r elles d finies sur des intervalles Rint f a b I signifie que la fonction f est int grable entre a et b i e existe
42. sommes et produits finis d finitions et propri t s notamment sur le fait de couper une somme en deux coefficients binomiaux d finitions partir de la relation de Pascal liens avec l expression sous forme de factorielles divisibilit formule du bin me de Newton preuve du th or me de Newton dans le cas o toutes les variables sont des entiers naturels petit th or me de Fermat preuve l mentaire du th or me bas sur la formule du bin me de Newton 2 5 3 D veloppements futurs Il faudrait tendre ces r sultats au cas des entiers relatifs Une autre direction serait de faire une preuve en utilisant des r sultats sur les groupes ou encore de g n raliser le bin me de Newton un anneau commutatif ce serait alors un r sultat d alg bre 14 Chapitre 3 Le WP IDE 3 1 Contexte initial 3 1 1 tat de l art CoqIDE Pas vraiment user friendly CoqIDE poss de de nombreux d fauts mineurs qui n apparaissent pas au premier coup d il mais apr s une utilisation fr quente de ce logiciel On donne ici une liste de tels d tails l impossibilit de fermer une fen tre active il faut s lectionner un autre onglet et effectuer une vali dation de code Vimpossibilit d ouvrir un fichier temporaire il faut obligatoirement sauvegarder le nouveau fichier une gestion calamiteuse de la coloration des fonctions de recherche et de remplacement la coloration
43. sultats difficiles d alg bre soit sur des preuves l mentaires mais dont de nombreux l ments de la preuve sont laiss s au lecteur ou peu formels De plus de nombreux l ments consid r s comme l mentaires en th orie des nombres coefficients binomiaux manipulations de sommes finies r sultats sur la primalit etc demandent un grand effort pour tre formalis s et utilis s Le but de ce d veloppement est de formaliser quelques uns de ces concepts et de les utiliser afin de prouver un r sultat non trivial de th orie des nombres savoir le petit th or me de Fermat 2 5 2 Description Tous les th or mes traitent des entiers naturels nat Bien que la plupart puissent tre tendus au cas des entiers relatifs Z ceux ci ne sont pas n cessaires pour obtenir ces th or mes De plus la plupart des preuves sont bas es sur un raisonnement par induction qui est naturel dans nat et qui l est moins dans Z Les d veloppements sur l arithm tique ont t pens s de fa on modulaire ceux ci regroupent les th ma tiques suivantes induction g n ralisation de la r currence sur nat la r currence n pas fonction puissance d finitions de la mise d un entier la puissance d un autre divisibilit d finition de la divisibilit de la primalit du plus grand diviseur commun du plus petit resp grand diviseur premier d un nombre d cidabilit de la divisibilit
44. sur la d finition construc tive d l ments moins g n raux vers d autres plus g n raux Les principes constructifs justifient cette ap proche Cependant certains objets ne peuvent tre construits par exemple dans Reals le fait que R est un corps n est pas une propri t mais un axiome Ainsi pour faciliter la d finition d objets plus g n raux on peut tenter de d finir les objets les plus g n raux dans un premier temps Un besoin sugg r par la manipulation des suites s ries ou m me des complexes est une homog n isation des tactiques pour simplifier les expressions qui supportent des propri t s de groupe d anneau ou encore d espace vectoriel On cherche g n raliser la notion d espace Description Dans Topology sont d finis les espaces topologiques Il est n cessaire d introduire la notion d union d une famille d ensembles index e par un ensemble quelconque d nombrable ou non On y montre que les topologies discr te V P V et triviale V 0 V sont effectivement des topologies et on d finit la notion de s paration 72 de Hausdorff Dans Metrics on d finit les espaces m triques Notamment il y est prouv qu un espace m trique d finit une topologie dont les ouverts sont les unions de boules ouvertes et que l espace topologique ainsi construit est s par La notion de continuit est introduite dans Continuity dans la version topologique et la version m trique On y m
45. t de fichiers de grammaires Il est important galement de prendre en compte les nombreuses tactiques comme apply H H2 in H3 qui ne sont pas de simples chaines de caract res mono lithiques comme assumption ou constructor 2 et il est pour cela n cessaire de rep rer les identificateurs dans une cha ne de caract res Comme Coq est tr s permissif sur les caract res autoris s dans les identifica teurs il est possible que certains accents ne soient pas pris en compte durant l apprentissage ce qui risque de g n rer un r sultat moins pr cis l apprentissage mais ne g n re pas d erreur bloquante Il est remarquer que la prise en compte dans les tactiques des identificateurs pr sents dans le contexte et plus g n ralement le mode d apprentissage tr s permissif permet d appr hender diff rentes formes ventuellement impr vues du langage de tactique comme ou par exemple Pour les fichiers v on utilise un syst me qui combine galement l analyse ad hoc et les analyseurs ocamllex ocamlyacc pour le sch ma global d un tel fichier mais pas pour les termes utilis s dans les tactiques Finalement apr s avoir combin les contextes avec les tactiques et v rifi leur coh rence num rique le traitement des donn es n cessite la transformation des identificateurs en indices de De Bruijn la mise en une forme un peu plus canonique des termes et des expressions la mise en forme sp cifique l algo
46. te en Coq Le programme de classes pr paratoires se base aussi largement sur ce genre de s rie Il appara t donc essentiel de d finir les s ries enti res en Coq Cpser est une g n ralisation de Rpser et doit tre con u de mani re plus modulaire le but n est plus seulement de faire tomber des r sultats th oriques majeurs mais de fournir galement des lemmes interm diaires r utilisables lorsqu on voudra s int resser des cas particuliers Description Cette biblioth que commence par tablir des liens entre les s ries enti res r elles et les s ries enti res com plexes afin de simplifier les preuves de convergence On utilsera galement un r sultat majeur de Csequence qui prouve que si 2 nen v rifie le crit re de Cauchy alors Im Zn nen et Re Zn nen le v rifient galement et r ciproquement Elle donne ensuite des preuves modulaires des lemmes d Abel et d Alembert la d monstration est d coup e en lemmes interm diaires tr s g n raux qui sont ais ment r utilisables Application Cette biblioth que peut tre utilis e pour d finir des fonctions telles que l exponentielle complexe et les fonctions trigonom triques qui en d coulent Cette approche permet de d montrer automatiquement la d rivabilit des fonctions ainsi d finies 2 3 6 R sultats int ressants D veloppement en sommes finies de a b Ce r sultat semble d j avoir t d montr dans les r els sous le nom d
47. tre biblioth que et la convergence des sommes partielles Th or mes fondamentaux Nous avons choisi de commencer par impl menter les th or mes fondamentaux traitant des s ries enti res lemme d Abel crit re de convergence de d Alembert caract risation du rayon de convergence et d rivabilit de la s rie sur son disque de convergence C est l que se situe la majeure partie du travail sur les s ries enti res la d rivabilit a notamment fait appel des lemmes qu il a fallu d montrer dans RFsequence TLes preuves de d rivabilit de cos et de sin d pendent par exemple de l axiome surnum raire sin 5 T SSi anr cy est born e et que r lt r alors an r y l est galement 9Le min des r des suites en pr sence fonctionne Lemme d Abel Si a r y est born e alors 1 Vx z lt r gt 5 ant admet une limite finie nen Yr UR SS gt a 2 converge normalement sur D 0 7 nEN Et une sorte de r ciproque Si eyn 411 converge alors Cv_radius_weak a x neN Crit re de d Alembert a 1 Si Heti Pog alors vr o lt r lt x gt Cv_radius_weak a r an Caract risation du rayon de convergence On utilise cette fois ci la d finition exacte du rayon de convergence et non la version affaiblie Si gt en ant converge simplement et que gt ey an2 diverge alors x est le rayon de convergence de la s rie enti re D rivabilit de la
48. ue les s ries et s ries enti res 2 3 1 Propri t s de C et fonctions de base Motivations Il para t essentiel si l on veut d finir les complexes de fa on ce qu ils soient utilisables d crire des petits lemmes sur la compatibilit de l addition multiplication division etc Dans la m me optique d utilisabilit de la biblioth que complexe nous avons cr des tactiques permettant d utiliser les choses connues dans les r els 10 Description Dans Cbase on d montre que les op rations d addition et de multiplication que l on a d finies font de C un corps Cela nous donne un d but de biblioth que de lemmes utilisables pour prouver des th or mes dans E Nous avons des tactiques permettant de passer dans les r els CusingR d truit tous les nombres complexes de l environnement et fait auto sur les r els ainsi cr s CusingR_f fait la m me chose que CusingR mais fait field au lieu de auto CusingR_simpl est utilisable sur une galit On passe dans les r els travers Cre et Cim respectivement fonctions d obtention de la partie r elle et complexe 2 3 2 Propri t s de C Cmet Ctacfield Motivations La biblioth que standard propose des r sultats g n raux sur certaines structures Afin d utiliser au mieux ces r sultats on doit videmment prouver que C remplit les conditions n cessaires Description Cmet On d montre que C est un espace m trique Ctacfield
49. uverte la n cessit de d montrer de nombreux sous buts relativement triviaux ainsi que l aust rit des interfaces ce qui peut rebuter les non informaticiens Partant de ces constatations le projet COQUILLE t chera de d velopper des outils permettant de d mon trer simplement des th or mes nonc s en classes pr paratoires 1 1 3 Public vis Nous souhaitons avant tout fournir un outil utilisable dans le contexte des classes pr paratoires mais il serait tr s fortement envisageable de le diffuser dans le monde de l industrie et de la recherche par exemple pour aider confirmer des conjectures ou m me des preuves lourdes en calculs et apporter une surcouche de fiabilit aux chercheurs 1 1 4 Approches Le projet COQUILLE a trois composantes principales et chacune a pour but de combler une partie des limites voqu es pr c demment MI est tout fait possible de d montrer de nombreux th or mes sans comprendre toutes les subtilit s du calcul des construc tions Ergonomie Le logiciel doit tre ergonomique m me si le public vis est assez scientifique pour vouloir prouver un th or me de math matiques il n est pas forc ment informaticien Le projet COQUILLE d velop pera donc une interface intuitive et fonctionnelle pour Coq Simplicit La d monstration de lemmes devra tre la plus simple possible nous t cherons donc d auto matiser au maximum le processus Les probl mes pouvant tre dif
50. voi d instructions Coqtop tape par tape et la r cup ration des r sultats ou messages d erreurs nous sommes rest s l coute des attentes des autres groupes de travail WP 1Ah cette couleur cette couleur 2Coqtop et CoqIDE sont si intimement li s que tout plantage de l un induit un plantage de l autre 15 WP Apprentissage Les besoins principaux concernaient l apprentissage La possibilit pour l utilisateur de donner une preuve type ou classique au programme d ap prentissage qui se chargera de parser le code et d apprendre la preuve En somme cela revient un bouton Apprendre cette preuve qui pourrait s appliquer une s lection de code ou un th or me en particulier Offrir l utilisateur une proposition de preuve ou de tactique par un bouton Propositions par exemple qui s en suivrait par une liste de tactiques disponibles et ad quates On pourrait envisager des retours l apprentissage pour dire que la proposition a t fructueuse ou que au contraire elle est absurde WP Preuves Tactiques Ce groupe a fourni des librairies et des tactiques sous forme de fichiers en langage Coq directement utilisables par des commandes Coq donc il n y avait a priori aucune attente de la part de ce WP 3 1 3 Que faire Tenter de modifier CoqIDE Ce n tait clairement pas envisageable En effet non seulement le code de CoqIDE est compl teme
51. y a de fortes probabilit s pour qu une question soit consid r e comme int ressante alors qu elle ne l est pas 27 4 7 R sultats Nous avons rempli nos objectifs de base l extraction de donn es algorithme d apprentissage et algorithme de parcours d un arbre de d cision partir d un probl me De plus nous avons fait deux des bonus qu on avait pr vus la compr hension des hypoth ses ainsi que la transformation en une tactique Les tactiques g n r es semblent satisfaisantes sur de petits ensembles Malheureusement nous n avons pas eu le temps de l essayer grande chelle et sur des probl mes complexes 4 8 Perspectives Compr hension des termes De m me que l on a r ussi comprendre H dans apply H comme un argument correspondant une hypoth se il faudrait r ussir comprendre cut z 0 Mais ce n est pas aussi simple priori z 0 ne se retrouve nulle part Ou pas enti rement On pourrait voir dans les arbres syntaxiques interrog s lesquels ont le plus grand sous arbre commun avec z 0 Connexion avec VIDE II serait bien que depuis IDE l utilisateur puisse dire quelles preuves il veut rajouter dans les bases d exemples pour quels domaines Les tactiques serait r actualis es r guli rement pour correspondre aux nouveaux exemples Bases d exemples sur Internet Plus il y a de preuves meilleures seront les tactiques On peut imaginer de grandes bases de donn es sur Internet Chaque uti
Download Pdf Manuals
Related Search