Home

Assistants de preuve

1. 2 4 2 Logique de Hoare 2 4 3 Preuve de programmes Java 2 4 4 Plongement superficiel ou profond 3 Types inductifs Bek G n ralit ss 2 ives eo Riven DA DA MS AM Be Soe RER Sa LE RAR TRS Lib 3 11 Forme g n rale 2 se aida pee ha du beh eee ee eee ete 3 1 2 Forme abstraite 1 24 gite doa a dos Ghose amp 4 ApS A Std LE chee A 3 2 Les d clarations non r cursives 3 2 1 Les d clarations de base 3 2 2 R gles de formation et d introduction 3 2 3 Schemas d limination 24 244 4 una ne dus 4 do REG Ba 3 2 4 Types inductifs et sortes 2 aa e 3 3 Les types inductifs r cursifs Broil Exemples Lines CE sei gece whee Shien a me Rasa BAe ae ce ae ae LE N 3 3 2 Condition de positivit 3 3 3 Sch ma d limination r cursif primitif 3 3 4 Condition de garde 3 3 5 R currence structurelle versus r currence bien fond e 3 3 6 D finitions mutuellement inductives SA EXT NSIONS Aes ob ek Me a a tous Rag nee EU et ee eee UM dus 341 Structures infinies ie e ete a ed us ee de ee eR Re Se 3 4 2 Structures quotients 3 4 3 R ductions g n ralis es
2. Types coinductifs dans Coq AT Introduction aae pouness ma a AR ge a Me te Re du Res EPS dial 411 Ey pesiConerets orenian Sane ho eee ten Malte es is ae et 4 1 2 Types r cursifs positifs 4 2 Exemple des listes infinies 4 2 1 Principe de destructivit 4 2 2 Principe de co it ration 4 2 3 Principe de co r cursion 4 2 4 D finitions par points fixes 43 D finition des types co inductifs dans Coq 4 3 1 Types de donn es infinis 4 3 2 Conditions de gardes oiie 4 444 Lu 8 de 8 4e a a ii t ABB R du tionssi eth ee nd oN pclae ANA aed AR ee BR ARE AMIE Be 4 3 4 Familles coinductives AA Applications s s rs 0 cen ee Bae ae ee as M i ae ew RCE RES MU 4 4 1 Calcul de processus 4 4 2 Logique temporelle 4 4 3 Autres applications 33 34 34 34 34 39 36 36 36 37 37 37 38 39 44 46 46 A7 48 49 50 51 52 52 53 53 7 f vrier 2014 5 Architecture des assistants 4 la d monstration b 1 Architecture de Coq 2 2 5 ds ow ce ake BR ee Ee be qi UE ns 5 2 Crit res de classification bis Autres SySt
3. La d claration vide Zero arit s pas de constructeur La d claration unitaire Un arit s un constructeur de type Un Les types sommes aussi appel s Z type Ua A B arit s un constructeur de type V x A B gt Sa A B Les sommes disjointes A B arit s deux constructeurs de type A A B et B A B galit x 4 y un param tre x A arit A s un constructeur de type x 4 x Si on suppose que l on a un X type Ua A B avec deux projections m Na A B gt A et 72 p 2x A B B x m p alors il est ais de d finir une somme n aire Z x1 A1 En An avec un constructeur de type V x1 A En An Z x1 A1 Ln An et n projections Ty Vp er Aie An Ak 21 k 1 m D Cr Dh On notera a1 an P l ment de U x A1 Ln An d fini l aide du constructeur Cette somme se d finit par 7 f vrier 2014 38 r currence sur n On pose X Un X x A A et E x Ajay A1 Xn An Ua A X z Are tq n De m me on peut d finir une disjonction n aire A1 An comme tant Zero si n 0 A si n 1 et dans le cas n gt 1 A Ai An A Ai An partir de ces constructions de base on peut trouver un quivalent toute d finition induc tive non r cursive En reprenant les notations donn es en 3 1 1 et en introduisant la notation XA pour ar A1 an An avec A Va A1 an An s Var
4. Case w b f g Y b 7 f vrier 2014 42 Ces fonctions sortent du cadre de ce qui peut tre typ dans un langage la ML elles sont pourtant tr s utiles dans les techniques de preuve base de r flexion pour interpr ter les objets d un type concret de proposition vers des propri t s Coq Nous verrons dans la partie 3 2 4 que l limination forte ne peut tre autoris e pour tous les types inductifs sans risque de rendre le syst me incoh rent Types d pendants Les d finitions inductives permettent de d finir des familles de type I V ai A1 an An s Par exemple on peut d finir une relation neq sur les bool ens par Inductive neq bool bool Prop neq neq true false neq neq false true Le sch ma d limination permet de montrer des propri t s de la forme V x1 T2 bool neq x1 2 gt P x1 x2 Il est trangement plus complexe de construire une preuve de neq b b2 P lorsque b et b sont des termes et plus seulement des variables distinctes C est le cas par exemple si on veut montrer neq true true gt L ou b bool neq b b gt L En fait pour pouvoir utiliser le sch ma d limination il faut pouvoir g n raliser la propri t a montrer en V x1 2 bool neq x 2 Q z x2 puis l appliquer b et b2 Les exemples ci dessus montrent qu une g n ralisation na ve ne fonctionne pas en g n ral Une mani re syst matique de r sou
5. Empty gt Coq lt false Coq lt Node 1 y r gt match compare x y with Coq lt Lt gt mem x 1 Coq lt Eq gt true Coq lt Gt gt mem x r Coq lt end Coq lt end La preuve de correction de cette fonction n cessite de d finir la notion d arbre binaire de re cherche sous la forme du pr dicat inductif bst suivant Coq lt Inductive bst tree gt Prop Coq lt bst_empty Coq lt bst Empty Coq lt bst_node Coq lt forall x l r tree Coq lt bst 1 gt bst r gt Coq lt forall y In y 1 gt y lt x gt Coq lt forall y In y r gt x lt y gt bst Node 1 x r 7 f vrier 2014 88 La correction de la fonction mem peut alors s crire ainsi Coq lt Theorem mem_correct Coq lt forall x s bst s gt mem x s true lt gt In x s On voit sur cet exemple que la sp cification S prend la forme P x gt Q x f x P est ce que l on appelle une pr condition et Q une postcondition Modularit Si l on cherche faire la preuve de mem_correct on commence par induction s simpl pour suivre la d finition de mem Le premier cas Empty est trivial Avec le second Node s1 z s2 on tombe alors sur un terme de la forme match compare x z with qui ne permet pas d aller plus avant En effet on ne sait rien de la fonction compare utilis e ici par la fonction mem Il nous faut la sp cifier par exemple sous la forme d un axiome Coq lt H
6. seront du m me type list n et on pourra remplacer l par l Cette galit vite de passer par un codage de paires assez lourd 3 2 4 Types inductifs et sortes Nous n avons pour l instant pas pr ciser les sortes pour lesquelles l limination d une d finition inductive tait possible Les types de donn es pr dicatifs Les types de donn es pr dicatifs sont ceux pour lesquels les types des arguments des construc teurs sont dans la m me sorte que l inductif C est forc ment le cas si le type inductif est dans Type ou bien dans Set dans le cas o cette sorte est aussi pr dicative Les types de donn es impr dicatifs Un type de donn es est impr dicatif s il est d fini dans Prop ou aussi dans Set si on se place dans la version de Coq avec Set impr dicatif et si au moins un des types d argument est dans la sorte Type C est le cas de la d finition Inductive prop Prop in Prop prop Si on autorisait pour cette d finition une limination forte alors on pourrait d finir out p prop Prop match p with in P P end On v rifie de plus que out in P P On a donc prop Prop qui est isomorphe a Prop Type ce qui introduit deux niveaux d impr dicativit et donne un syst me incoh rent 7 f vrier 2014 45 Une possibilit est d interdire les d finitions impr dicatives celles ci peuvent tre repr sent es par un codage l ordre sup rieur Dans Coq de telles d fi
7. une disjonction dans Prop un tiers exclu pour le pr dicat eq alors que dans le pr c dent on a une disjonction dans Set c est dire un programme d cidant de l galit L extraction de sumbool est un type isomorphe bool Coq lt Extraction sumbool type sumbool Left Right En pratique on peut indiquer l extraction de Coq d utiliser directement les bool ens de ML au lieu de Left et Right permet notamment d utiliser if then else dans le code extrait Variante sumor I existe une variante sumbool o les sortes ne sont pas les m mes gauche et droite Coq lt Inductive sumor A Set B Prop Set Coq lt inleft A gt A B Coq lt inright B gt A B Cet inductif permet de sp cifier une fonction ML qui retourne une valeur du type a option le constructeur inright repr sente le cas None et lui associe la propri t B et le constructeur inleft repr sente le cas Some et lui associe la sp cification A De fait l extraction de sumor est isomorphe au type option de ML 1 C est le cas de le dire 7 f vrier 2014 97 Coq lt Extraction sumor type a sumor Inleft of a Inright On peut ainsi combiner sumor et sig pour sp cifier la fonction min_elt de la mani re sui vante Coq lt Definition min_elt Coq lt forall s bst s gt Coq lt m Z In ms forall x In x s gt m lt x s Empty Il s agit l d
8. v m F Ci Ca o m mt Eptrue mF Cio m mt Ep false mF Com mbt if E then Ci else Cop m mb if E then Ci else Cop m mbt Eptrue mkC gt m1 mit while E do Cem mt Ep false mt while E do C gt m mt while E doCpm FIGURE 2 6 S mantique des commandes 7 f vrier 2014 24 2 2 3 S mantique axiomatique Il s agit d interpr ter les commandes comme des transformations de pr dicats ces pr dicats sp cifiant des propri t s de la m moire Si P et Q sont deux tels pr dicats et C une commande alors on d finit une relation P C Q dont l interpr tation est l ex cution de C partir d une m moire v rifiant P conduit une m moire v rifiant Q Nous aurons besoin de transformateurs de pr dicats particuliers La conjonction et l implica tion de deux pr dicats seront not s par PAQ et P Q si x est une variable et E une expression alors P x E repr sente le pr dicat qui toute m moire m associe P m x v o v est la valeur telle que m F Ebv Si w est une valeur alors E w repr sente le pr dicat qui tout m associe la propri t v w o v est la valeur telle que m F Eb vw La d finition de cette relation est donn e par les r gles d inf rence de la figure 2 7 PIC P P1 C2 Q P C1 C2 Q PA E true C1 Q PA E faise C2 Q P if E then C else C2 Q P A E true C P P while E do C PA E false PP Pj C Qi Q gt Q P C Q FIGURE 2 7 S mantique axiomatique des commande
9. 78 Springer Verlag 1994 Coq94bl Thierry Coquand A new paradox in type theory In 9th International Conference on Logic Methodology and Philosophy of Science pages 555 570 1994 Coq07 The Coq Development Team The Coq Proof Assistant Reference Manual INRIA 2007 Version 8 1 available at http coq inria fr doc main html Cou90 Patrick Cousot Methods and logics for proving programs In J van Leeuwen edi tor Handbook of Theoretical Computer Science volume B pages 841 993 North Holland 1990 CPM90 Thierry Coquand and Christine Paulin Mohring Inductively defined types In P Martin L f and G Mints editors Proceedings of Colog 88 Springer Verlag 1990 LNCS 417 Dia75 Radu Diaconescu Axiom of choice and complementation In Proceedings of AMS volume 51 pages 176 178 1975 Dij76 Edsger W Dijkstra A discipline of programming Series in Automatic Computa tion Prentice Hall Int 1976 DP98 Ferrucio Damiani and Fr d ric Prost Detecting and removing dead code using rank 2 intersection In Proceedings TYPES 96 LNCS 1998 Fil99 Jean Christophe Filli tre Preuve de programmes imp ratifs en th orie des types Th se de doctorat Universit Paris Sud July 1999 Fi102 Jean Christophe Filli tre The why verification tool 2002 http why lri fr Fil03a Jean Christophe Filli tre Verification of Non Functional Programs using Inter pretations in Type Theory Journal of Functional Prog
10. 9 S mantique du Calcul des Constructions Inductives 9 1 Le Calcul des Constructions pur COLLE 240s 34 BE eke eee oS 9 1 1 Puissance logique 9 1 2 Puissance calculatoire 9 1 3 Extensions incoh rentes du Calcul des Constructions 9 2 Le Calcul des Constructions avec univers CCy 9 2 1 Encodage de l arithm tique 9 2 2 Encodage de la th orie des ensembles de Zermelo 9 2 3 Puissance logique 9 3 Extensions coh rentes et incoh rentes du Calcul des Constructions Inductives 112 112 112 113 114 114 115 115 115 116 Chapitre 1 Introduction au Calcul des Constructions Inductives 1 1 Motivations Ce cours traite de la preuve formelle comme discipline de l informatique Il prolonge donc le cours de tronc commun Fondements des syst mes de preuves mais en mettant l accent sur la construction effective de preuves formelles et de leur v rification sur ordinateur Si la logique math matique c est dire la formalisation compl te du raisonnement est une discipline d j relativement ancienne elle a t relativement boulevers e par l arriv e de lor dinateur la capacit de la machine manipuler rapidement de grosses expressions symboliques permet de formaliser enti rement des raisonnements non triviaux La question que se pose le logi cie
11. Let03b Pierre Letouzey Programmation fonctionnelle certifi e en Cog PhD thesis Uni versit Paris Sud 2003 To be defended Luo90 Zhaohui Luo An Extended Calculus of Constructions PhD thesis University of Edinburgh 1990 LW99 Samuel Lacas and Benjamin Werner Which choices imply the excluded middle manuscript 1999 McB99 Conor McBride Dependently Typed Functional Programs and their Proofs Phd thesis Universit d Edimbourg 1999 Miq01 Alexandre Miquel Le calcul des constructions implicite syntaxe et s mantique PhD thesis Universit Paris 7 December 2001 MPMU04 Claude March Christine Paulin Mohring and Xavier Urbain The KRAKATOA tool for certification of JAVA JAVACARD programs annotated in JML Journal of Logic and Algebraic Programming 58 1 2 89 106 2004 http krakatoa lri fr MW98 Paul Andr Melli s and Benjamin Werner A generic normalisation proof for pure type systems In Eduardo Gim nez and Christine Paulin Mohring editors Types for Proofs and Programs International Workshop TYPES 96 Aussois France December 15 19 1996 Selected Papers volume 1512 of Lecture Notes in Computer Science pages 254 276 Springer 1998 MW03 Alexandre Miquel and Benjamin Werner The not so simple proof irrelevant mo del of cc In Herman Geuvers and Freek Wiedijk editors Types for Proofs and Programs Second International Workshop TYPES 2002 Berg en Dal The Ne therlands April 24 28 2
12. cumulativit ne passe pas sous les produits ainsi si f est une variable de type A Type1 alors on a Ac A f x Type2 mais pas f A gt Type2 La version de CC avec univers d crite ici est due Luo Luo90 dont le Calcul des Constructions Etendu ECC correspond l extension de CC avec une construction primitive pour les types existentiels Z types La terminologie CC quant elle remonte Miquel Miq01 5 En fait les d pendances en les preuves ne sont pas n cessaires pour encoder l arithm tique Ainsi Fu avec un niveau suppl mentaire convient tout aussi bien 6 Comme pour l encodage de l arithm tique Fu avec deux niveaux suppl mentaires ce qui se note F 3 suffit pour encoder la th orie des ensembles de Zermelo 7 En th orie des ensembles un niveau suppl mentaire d imbrication des ensembles correspond une applica tion de l axiome des parties On d marre de l ensemble vide dont la profondeur est nulle Le passage la limite se fait avec l axiome de l union 7 f vrier 2014 116 9 3 Extensions coh rentes et incoh rentes du Calcul des Construc tions Inductives On consid re le Calcul des Constructions Inductives avec Set et Prop Dans le cas o Set est impr dicatif il n existe pas de mod le complet du CCI Les deux approximations les plus proches sont le mod le de B Werner qui ne prend en compte ni Prop ni la hi rarchie d univers Wer94 le mod le d
13. des preuves s exprime par VA Prop Vp q A p q Ind pendant dans CC non prouvable pas de preuve close valid par le mod le bool en Incoh rent dans CCI en rempla ant Prop par Set car 0 1 dans Set Logique classique La logique classique peut tre exprim e par exemple par le tiers exclu VA Prop A V A Ind pendant dans CC et ECC non prouvable pas de preuve close valid par le mod le bool en Incoh rent dans CCI si la disjonction est dans Set de part la d rivabilit de l axiome du choix somme forte limination d pendante et de true 4 false dans Set on peut injecter Prop dans bool une r traction puis encoder le syst me U et d river l absurde Remarque VA Set A V AA est suppos coh rent Ce qui permet vraiment de montrer une incoh rence c est que la disjonction soit dans Set Dans CCI la logique classique entra ne l indiscernabilit des preuves la preuve n cessite l limination d pendante des inductifs de Prop et l impr dicativit cf Barbanera et Berardi BB96 7 f vrier 2014 117 Extensionnalit propositionnelle et compl tude propositionnelle La compl tude propositionnelle VA Prop A TrueV A False est quivalente dans CC a la conjonction de la logique classique et de l extensionnalit propositionnelle VA B Prop A B A B Dans CCI l extensionnalit propositionnelle entra ne l indiscernabilit des preuves la preuve n ce
14. tude de la propri t de normalisation et renverra pour l instant au cours de tronc commun Retenons pour l instant que Toutes les fonctions r cursives accept es par le syst me doivent terminer Pour pouvoir d finir des r gles de typage il importe donc d isoler une classe de fonctions r cur sives terminantes Pour ce faire on g n ralise la classe des fonctions d finissables dans le syst me T de G del D finition 1 On consid re un terme de type nat de la forme S n Sont consid r s comme structurellement plus petit que S n les termes suivants n tout terme structurellement plus petit que n Une fonction est structurellement r cursive si l on peut distinguer l un de ses arguments qui d croit structurellement chaque appel r cursif En Coq seules des fonctions structurellement r cursives peuvent tre d finies par Fixpoint Les fonctions plus et mult d finies ci dessus sont structurellement r cursives par rapport leur premier argument Bien s r la fonction non_sens est rejet e par le syst me Voici une d finition alternative de l addition qui d croit par rapport son second argument Coq lt Fixpoint plus n m nat struct m nat Coq lt match m with Coq lt 0 gt n Coq lt S p gt S plus n p Coq lt end Fonctions plus complexes Dans le syst me T seul n est consid r comme structurellement plus petit que S n La d finition ci de
15. 4n P n qui d voile un terme t tel que F P t La r alisation de l axiome du choix Vz A Jy B P x y gt 3f Vx P x f x pose probl me en pr sence de la logique classique consid rer par exemple la preuve clas sique de Vx 1b b true P x R aliser par une fonction calculable faisant intervenir call cc entra ne que le domaine de quantification B soit d g n r Reste alors la r ali sation par une fonction non calculable c d par un oracle d cidant la v rit a priori de toute proposition ce qui pousse refuser un contenu calculatoire aux l ments du domaine de quantification et donc aux V et J On peut alors r aliser l axiome du choix par l identit de P x y dans P x f x pour un certain f non calculatoire c est une voie tr s diff rente de celle suivie dans la suite de ce chapitre Preuves intuitionnistes et r cursivit Un avantage de la logique intuitionniste est qu elle permet de parler de la d cidabilit de propri t s de mani re implicite sans faire appel une th orie de la r cursivit Pour montrer qu un pr dicat est d cidable ou qu une relation fonctionnelle est r cursive il suffit d exhiber une preuve d une formule disjonctive ou existentielle Cependant on ne capture pas ainsi toutes les fonctions r cursives en effet il existe des relations fonctionnelles correspondant des fonctions r cursives et pour lesquelles la formule disant que la relatio
16. Coq lt forall a A 1 Stream P Cons a 1 gt forall s Stream P s D un point de vue plus op rationnel si toute valeur de type Stream peut tre r duite vers un terme construit avec Cons alors on peut utiliser un op rateur de d finition par filtrage Coq lt Variable C Set Coq lt Variable f A gt Stream gt C Coq lt Check fun s Stream gt match s with Coq lt Cons al fal Coq lt end fun s Stream gt match s with Cons a 1 gt fa 1 end Stream gt C et on a la r duction suivante Coq lt Eval compute in Coq lt fun b A s Stream gt match Cons b s with Coq lt Cons al fal Coq lt end fun b A s Stream gt f b s A gt Stream gt C Ceci permet de d finir les fonctions d acc s au premier l ment de la liste ainsi qu sa queue Coq lt Definition head x Stream match x with Coq lt Cons a_ gt a Coq lt end Coq lt Definition tail x Stream match x with Coq lt Cons _ s gt s Coq lt end En combinant ces deux fonctions et par r currence structurelle sur n il est possible de d finir la fonction d acc s au n me l ment d une liste 7 f vrier 2014 56 Coq lt Fixpoint nth n nat s Stream struct n A Coq lt match n with Coq lt 0 gt head s Coq lt S m gt nth m tail s Coq lt end 4 2 2 Principe de co it ration Tout comme les branchements infinis taient en fa
17. In x s gt min_elt s lt x L nonc garde la pr condition s Empty sans quoi il ne serait pas possible de montrer Vappartenance de min_elt sas Note La fonction de division sur les entiers relatifs Zdiv est ainsi d finie comme une fonction totale mais ces propri t s ne sont tablies que sous l hypoth se que le diviseur est non nul Note Une autre fa on de rendre totale la fonction min_elt plus g n rale e t t de lui faire retourner un r sultat de type option Z c est dire None lorsque l ensemble est vide et Some m lorsqu il existe un plus petit l ment m Mais on change alors l g rement le code ML sous jacent et l nonc du th or me de correction 7 1 2 Cas des fonctions non structurellement r cursives Le probl me de la d finition et de l utilisation d une fonction partielle se retrouve galement lorsque l on cherche d finir et prouver une fonction r cursive mais dont la r currence n est pas structurelle En effet une solution pour d finir une telle fonction consiste utiliser un principe de r cur rence bien fond e tel que well_founded_induction Coq lt well_founded_induction Coq lt forall A Set R A gt A gt Prop Coq lt well_founded R gt Coq lt forall P A gt Set Coq lt forall x A forall y A Ry x gt P y gt P x gt Coq lt forall a A Pa Mais alors la d finition n cessite de construire des preuv
18. Ordinaux pe Se AN A ie ee gate bead Abe EAA da i 1 6 2 Arbres arbitrairement branchants 1 7 a Pr dicatsindu ctifs u Haas hrs Sette Sth ee SAR REG 2 Ft Haters pairs Su st mi oe tas LE E ea SOS en ee A NE EE 1 7 2 L ordre sur les entiers 1 7 3 Un exemple dangereux Exemple de d veloppement Gallina S mantique d un mini langage 2 11 Introductions tes der peal ee eA A I a Ph ae NE ah te le dore UE de 2 2 Pr sentation du probl me 2 2 1 S mantique statique 2 2 2 S mantique op rationnelle 2 2 3 S mantique axiomatique 2 2 4 Quelques propri t s 2 3 Sp cincation Gallifa ses Sesa aa E e Par ae RAA han a dns 2 3 1 Les expressions 2 3 2 V rification du type et valuation constructive 2 3 3 Les Commandes 24 paaa eiea a u EE A older ee eee 2 3 4 Mise jour de la m moire 2 3 5 S mantique op rationnelle o O I 11 12 12 14 15 15 16 16 16 17 18 18 18 19 19 19 20 7 f vrier 2014 2 3 6 S mantique axiomatique 2A Pourvien Savoir plus aok cm aah A dE bagues BE ek De Be DES Le a 2 4 1 S mantique des langages et compilateurs
19. X u y t nil list nat 7 f vrier 2014 71 interp sigma norm Plus Plus Zero Var 0 Plus Var 1 Var 2 Coq lt simpl interp simpl norm clear sigma 1 subgoal x nat y nat t nat u nat P x u y t Id alement le travail consistant trouver s tel que s t devrait tre automatis Cela peut se faire en ML ou en utilisant le langage de tactique Un exemple plus consistant de tactique par r flexion disponible dans Coq est la tactique Ring Un model checker utilisant des BDDs a galement t construit selon ce mod le VGLPAKO0 Il n est pas toujours commode ni tr s efficace de programmer dans le langage de Coq des proc dures de recherche de preuve complexes Les outils de preuve automatique peuvent souvent tre adapt s pour produire une trace de preuve On peut alors simplement internaliser dans Coq la notion de trace et la preuve de correction de cette trace A nsi la preuve v rifi e par Coq effectue un calcul sur la trace et sa taille est proportionnelle cette taille Cette approche a t utilis e pour construire une interface entre Coq et le syst me de r criture Elan ou dans une version r flexive de la tactique de preuve en arithm tique Omega Chapitre 6 Extraction de programmes et r alisabilit Introduction Dans ce cours nous tudions le caract re constructif de la logique sous jacente au calcul des constructions inductives Nous montrons comment constr
20. arit A s dans laquelle s est la sorte des d finitions inductives On remplace dans les types de constructeur chaque mention une des d finitions mutuellement in ductives Jj a1 aq par la r f rence l instance appropri e de J c est dire 1 ing a1 amp Le sch ma d limination mutuellement r cursif des d finitions I peut galement se d duire du sch ma g n ral pour T Exemple 4 Inductive arbre A Set Set node A foret A arbre A with foret A Set Set vide foret A add arbre A foret A foret A est quivalent 7 f vrier 2014 52 Inductive arbre_foret A Set bool Set node A arbre_foret A false arbre_foret A true vide arbre_foret A false add arbre_foret A true arbre_foret A false arbre_foret A false Definition arbre A Set arbre_foret A true Definition foret A Set arbre_foret A false Dans le cas de d finitions mutuellement r cursives Coq engendre automatiquement un principe d limination r cursive pour chaque type qui ne tient pas compte des appels aux autres inductifs de la famille Par contre la commande Scheme permet d engendrer automatiquement les sch mas d limination mutuellement r cursifs dans le cas de positivit non imbriqu e Ces sch mas peuvent ensuite tre utilis s par la tactique Elim term using theorem with instances en instanciant de mani re appropri e
21. c t est de type I Soit une fonction f de type I gt I d finie par f cx f xl ct On pourrait penser que l appel r cursif qui se fait sur un sous terme x de c x est bien fond Ce n est pas le cas En effet f c t se r duit en f t I c t qui se r duit en f c t et donc se terme ne se normalise pas 3 3 5 R currence structurelle versus r currence bien fond e La d finition primitive par point fixe permet de capturer certaines fonctions r cursives mais videmment toutes les fonctions ne suivent pas ce crit re de d croissance structurel Un exemple classique est la fonction quicksort sur les listes qui s appelle r cursivement sur deux sous listes qui sont de longueur plus petite videmment on sait ramener cette d croissance un point fixe structurel sur un argument suppl mentaire repr sentant la longueur de la liste Mais on voudrait galement pouvoir justifier la d finition par point fixe en utilisant uniquement un argument de bonne fondation de la relation avoir une longueur strictement plus petite Ceci est possible en Coq en utilisant notre d finition d tre bien fond On suppose que l on dispose d une fonction split A gt list list x list qui s pare une liste l suivant un pivot a en deux listes l et 2 telle que la longueur de l est inf rieure ou gale la longueur de l On notera la longueur de l qui v rifie les propri t s ill 0 cons a l S l On peut alors d
22. est x u yxt Construction de la structure abstraite repr sentant les expressions construites partir de et 0 On prendra les entiers naturels eux m mes pour d noter les variables 7 f vrier 2014 Coq lt Definition index nat Coq lt Inductive expr Set Coq lt Plus expr gt expr gt expr Coq lt Zero expr Coq lt Var index gt expr Construction de la fonction d interpr tation 69 Coq lt Require Import List Coq lt Require Import Plus Coq lt Valeur par d faut de nth si la substitution n tait pas de bonne longueur Coq lt Definition default 0 Coq lt Fonction d interpr tation Coq lt Fixpoint interp s list nat e expr struct e nat Coq lt match e with Coq lt Plus e1 e2 gt interp s el interp s e2 Coq lt Zero gt 0 Coq lt Var i gt nth i s default Coq lt end Construction de la fonction de simplification Coq lt Fixpoint insere e1 e expr struct e1 expr Coq lt match e1 with Coq lt Plus e1 e2 gt insere e1 insere e2 e Coq lt Zero gt e Coq lt Var i gt Plus e1 e Coq lt end Coq lt Fixpoint norm e expr expr Coq lt match e with Coq lt Plus ei Zero gt norm el Coq lt Plus e1 e2 gt insere e1 norm e2 Coq lt x gt x Coq lt end Construction de la preuve de correction de la simplification Coq lt Lemma validite_insere Coq lt
23. finir une fonction de tri quick VY l list n nat lt n list de mani re structurelle sur n La d finition de quick suit le sch ma suivant quick nil n h nil lt n nil quick cons a l 0 Ah cons a l lt 0 absurd ho quick cons a l S n Ah cons a l lt S n let l1 l2 split a l in append quick l n h cons a quick l n h2 7 f vrier 2014 51 Avec ho hy et ho des preuves de L l lt n et l2 lt n Pour obtenir une fonction de tri de type list list il suffit de prendre une valeur initiale de n gale la longueur de l Cependant d un point de vue calculatoire l argument entier n qui a t ajout appara t superflu L alternative consiste utiliser une preuve du fait que la relation R Al m list l lt m est bien fond e Le programme se construit alors comme un terme quickwf de type Vl list wf list R l gt list Cette preuve suit le sch ma suivant quickwf nil X hiwt list R nil gt nil quickwf cons al A h wf list R cons a l let l1 l2 split a l in append quickwf l h cons a quickwf lz h2 Avec h et hg des preuves de wf list R l et wf list R l2 qui sont structurellement plus petites que h Ces preuves sont construites de la mani re suivante Il est possible de d finir wf_inv de type V A Set R A A gt Prop x A wf A Rz gt Vy A Ryxowf ARy par wf_inv A R z wf_intro A Rz h h On remarque que
24. forall b expr c d com Coq lt exprcorrect Sbool b gt Coq lt comcorrect c gt comcorrect d gt comcorrect cond b c d Coq lt corwhile Coq lt forall b expr c com Coq lt exprcorrect Sbool b gt comcorrect c gt comcorrect while b c 2 3 4 Mise jour de la m moire Nous d finissons maintenant la fonction d criture dans la m moire Elle utilise la d cida bilit de l galit sur les variables qui vient de la d cidabilit de l galit sur les noms prise comme axiome puisque l ensemble des noms n est pas sp cifi et de celle sur les sortes qui peut explicitement tre construite Pour montrer la d cidabilit de l galit sur un ensemble A on peut construire une fonction bool enne f de type A A bool et d montrer que c est la fonction caract ristique de l galit f x y true amp x y On choisit une autre solution qui est de construire un terme fdec de type Vx y A x y A x y qui tous x et y associe soit un objet left h avec h une preuve de x y soit un objet right h avec h une preuve de x y Une expression if a b then p else q s crira dans Coq match fdec a b with left _ gt p right _ gt q end Ou de mani re quivalente ifdec fdec a b pq On oublie information de preuve pour construire l expression mais celle ci pourra tre facilement utilis e lorsqu il s agira de montrer des propri t s de cette expression
25. sans avoir repr senter une notion de calculabilit Coq lt Theorem expr_val_check_proof forall E expr Coq lt v semval exprval E v amp exprcorrect sort_val v E exprerr E Si on ne s int resse qu la partie calcul de cette preuve alors on a une fonction eval_prog qui toute expression associe une valeur ou rien du tout Cette fonction peut galement se repr senter dans Gallina en utilisant le type option de Coq Coq lt Print option Inductive option A Type Type Some A gt option A None option A 7 f vrier 2014 30 For Some Argument A is implicit For None Argument A is implicit and maximally inserted For option Argument scope is type_scope For Some Argument scopes are type_scope _ For None Argument scope is type_scope Coq lt Implicit Arguments Some A Warning Implicit Arguments is deprecated use Arguments instead La fonction eval_prog se calcule par point fixe structurel sur l expression Coq lt Fixpoint eval_prog e expr option semval Coq lt match e with Coq lt Var n s gt Some memstate n s Coq lt Tr gt Some Bool true Coq lt Fa gt Some Bool false Coq lt Xor f g gt Coq lt match eval_prog f eval_prog g with Coq lt Some Bool bf Some Bool bg gt Some Bool boolxor bf bg Coq lt _ _ gt None A semval Coq lt end Coq lt Num n gt Some Nat n Coq lt Null f gt Coq lt ma
26. toute structure de don n es complexes ce qui permet de traiter des vrais langages comme Java ou C pour ceux ci la structure de la m moire est mod lis e avec les op rations logiques abstraites et des axiomes L outil Krakatoa MPMU04 suit ce principe et permet de traduire automatiquement un pro gramme Java en un programme Why avec une telle mod lisation L outil Caduceus en cours de d veloppement fait de m me avec les programmes C Remarquons aussi que cette approche pour mod liser les structures de donn es complexes peut tre aussi utilis e pour traiter les entiers born s il suffit d interpr ter les op rations arith m tiques comme l addition par une autre fonction logique On a m me le choix de permettre les d bordements et faire des calculs modulo 2 ou bien imposer le non d bordement en introdui sant une fonction d addition sur les entiers non born s mais avec pr condition de la forme parameter bounded_add x int gt y int gt 2 31 lt x y lt 2731 int result x y Chapitre 9 S mantique du Calcul des Constructions Inductives 9 1 Le Calcul des Constructions pur CC La th orie du Calcul des Constructions pur se ram ne essentiellement celle du syst me Fy par effacement des d pendances en les preuves dans les types cf chapitre sur l extraction Tous deux correspondent une logique tr s faible puisqu en interpr tant Prop de mani re bool enne toute formule adm
27. x x tree Coq 1t plus cardinal_tree y cardinal_tree y Coq plus cardinal_tree x cardinal_tree x gt Py y Coq gt P x x gt lt lt lt lt Coq lt forall y y tree lt lt lt Coq lt forall x x tree P x x La preuve est facile on se ram ne a un principe de r currence bien fond e sur le type nat fourni dans la biblioth que de Coq savoir well_founded_induction_type_2 et l on prouve ais ment que la relation est bien fond e car elle est de la forme 1t f y y f x x et que 1t est une relation bien fond e sur nat autre r sultat fourni par la biblioth que Coq lt Proof Coq lt intros P H x x Coq lt apply well_founded_induction_type_2 Coq lt with R fun yy xx tree tree gt Coq lt 1t plus cardinal_tree fst yy cardinal_tree snd yy Coq lt plus cardinal_tree fst xx cardinal_tree snd xx Coq lt auto Coq lt apply Wf_nat well_founded_ltof _ Coq lt fun xx tree tree gt Coq lt plus cardinal_tree fst xx cardinal_tree snd xx Coq lt Save On peut alors d finir la fonction subset par une d finition preuve utilisant la tactique refine Coq lt Definition subset tree gt tree gt bool Coq lt Proof 7 f vrier 2014 93 On commence par appliquer le principe de r currence cardinal_rec2 Coq lt intros s1 s2 pattern si s2 apply ca
28. A Set et E C E J C est le cas en particulier des conjonctions sur des objets dans Prop ou bien de l galit Dans ces cas l on peut justifier l quivalence pour la r alisabilit de la d finition inductive de I A ou de I A o A est obtenu en rempla ant Set par Prop la fin de l arit A En pratique on traite ce cas en autorisant la construction par cas d objets de type Set m me si t I Prop On tend la notion d extraction pour que l extraction de match t with c z1 p p end soit simplement l extraction de p ce qui est possible car p a le bon type les x logiques n appa raissent pas dans P Limitations La notion d extraction et de r alisabilit s tend mal au cas des univers et de V limination forte sur les types inductifs En effet la propri t d oubli des d pendances ne s ap plique plus D autre part les inclusions Prop lt Type et Set lt Type qui sont essentielles pour un d veloppement harmonieux sont incompatibles avec une extraction incr mentale car il existe alors des types B Type n p ex U Type 1 U U dont des instances sont dans Type et d autres sont dans Type Il faut conna tre le d veloppement complet avant de d cider si l on doit extraire ou cacher les objets de B Le m canisme d extraction de Coq a partir de la version 7 s loigne d ailleurs du sch ma pr sent ici La distinction Typep et Type est abandonn e et c est une a
29. C nom P gt gt C nom P gt P ay ay Com AGC ye Enn C2 PA Ci nom P Jn Cn nom P gt fm Bik Enn Case A P A a A1 a Ay x nom ay az f Ci nom P fn Cn nom P gt P fi fn On v rifie que les objets introduits sont bien typ s du type attendu sauf dans le cas du sch ma d limination Case o le type est plus faible que celui que nous avons propos pr c demment En effet on int gre dans le sch ma le fait que dans chaque branche a1 ar est gal t1 t mais pas le fait que x lui m me est gal com x x On appelle le sch ma ainsi obtenu le sch ma it ratif Dans le cas non r cursif ce sch ma est le m me que le sch ma non d pendant On remarque galement que le sch ma d limination que nous avons cod a une sorte d limination qui est la m me que la sorte de la d finition inductive Cette repr sentation impr dicative a l avantage de ne pas n cessiter d extension de la th orie et donc de ne pas poser de probl me th orique suppl mentaire Cependant la faiblesse du sch ma 7 f vrier 2014 41 d limination fait que certaines propri t s logiquement tr s fortes et pourtant attendues ne sont pas prouvables On peut construire le type des bool ens bool VC Set C C C avec true A C Set t f C t et false A C Set t f C gt f mais il n est pas possible de prouver true
30. Coq Ce m canisme extrait le contenu informatif d un terme Coq sous la forme d un programme ML Les parties logiques dis paraissent ou ne subsistent que sous la forme d une valeur d g n r e sans aucun calcul associ Les fondements th oriques de l extraction ont t expos s au chapitre pr c dent 7 1 M thode directe La fa on la plus simple de certifier un programme purement fonctionnel consiste l crire comme une fonction dans Coq puis prouver des propri t s de cette fonction C est ce qui a t fait par exemple d s le d but de ce cours avec la plus sur les entiers de Peano Un grand nombre de programmes ML purement fonctionnels peuvent tre crits directement dans le Calcul des Constructions D une mani re g n rale on commence par d finir dans Coq une fonction pure c est dire avec un type la ML un type du syst me F purement informatif Supposons ici une fonction prenant un seul argument fo nn On montre alors que cette fonction r alise une certaine sp cification S 7 T2 Prop par un th or me de la forme Va ox Cf amp La preuve de ce th or me se fait en suivant la d finition de f Exemple On souhaite d velopper et certifier formellement une biblioth que d ensembles finis cod s l aide d arbres binaires de recherche On se donne un type d arbres binaires contenant des entiers Coq lt Inductive tree Set Coq lt Empty Coq lt N
31. On peut plonger Prop dans un sous ensemble de Set en faisant correspondre A Prop un ensemble il suffit de prendre C Set A gt C gt C qui a au plus un l ment et qui est habit lorsque A est v rifi On pourra montrer A La partie A gt A peut se justifier dans CC par la r alisabilit On peut galement int grer cet aspect directement dans le calcul par exemple par l interm diaire du sous typage Prop lt Set Cacher le contenu calculatoire des preuves R ciproquement tant donn un type A Set on peut cacher le contenu calculatoire des preuves de en construisant Prop tel que A gt Aet C Prop A C gt C il suffit de prendre C Prop A gt C gt C On n a videmment pas A mais A et A sont quivalents d s lors qu il s agit de montrer des propri t s logiques de type Prop Types inductifs Dans Coq les r gles d limination des types inductifs permettent de faire la distinction entre Prop et Set Lorsque c I avec I instance d une d finition inductive alors sit I Set il est possible par la construction match t de construire la fois des objets dans Prop et dans Set si I Prop il est seulement possible de faire une construction match t pour construire des objets dans Prop 7 f vrier 2014 84 Quelques cas sp ciaux On traite de mani re un peu particuli re les types J A un seul constructeur c C tel que si on avait A Type alors on aurait E
32. b tel que dec b soit v rifi si b true et Va U P x est prouvable ou bien si b false et dr U P x est prouvable On peut bien s r introduire dec comme AU Set P U Prop b bool gt Va U P x Ab true Gx U P x Ab false Mais on peut galement introduire une d finition inductive avec U et P comme param tres Inductive dec U Set P U Prop bool Prop isTrue V x U P x dec U P true isFalse V x U P x dec U P false 3 2 2 R gles de formation et d introduction Une d claration inductive va introduire de nouveaux objets dans la th orie Dans un cadre de d duction naturelle on va trouver des r gles d introduction une par constructeur et des r gles d limination Il faut ajouter une r gle de bonne formation pour la d finition elle m me R gle de formation En reprenant les notations de 3 1 1 la r gle de formation donne le typage de la d finition in ductive La condition est que chaque type de constructeur soit bien form dans un environnement 7 f vrier 2014 39 comportant les param tres T nom AF Cm s mEl p s sorte de l arit A TH nom A Cette r gle impose un lien entre la sorte de l inductif et celles des types d argument de construc teur dans le cas o la sorte s est pr dicative Exemple 3 On peut introduire ZX Prop X de type Prop qui repr sente la propri t 3X X quantification existentielle du second ordre
33. celui de la logique de Hoare classique mais adapt e au langage Why 7 f vrier 2014 107 Voici un extrait des formules de calcul de WP les r gles compl tes sont dans le manuel de Why Fil02 et dans F1199 WP x Q Qiresult zx WP Ix Q Qlresult x WP x e Q WP e Q result tt x result r x WP e15e2 Q WP e WP e2 Q W P if e1 then eg else e3 Q WP e1 if result then W P e2 Q else WP e3 Q WP let x e1 in e2 Q WP e WP e2 Q x result La r gle pour l application est l une des plus complexe WP f ET st en Q WP e1 WP e2 WP en P Yw we result Qf Q n result x1 result si f a le type avec effets annot x t1 En tn gt Pf t R W Q et les expressions 1 n sont pures c d ne modifient aucune variable Cette derni re condition fait qu il peut arriver que l outil Why peut parfois ne pas parvenir g n rer les obligations de preuves auquel cas il faut simplifier l application concern e en introduisant des let in Exercice 3 Annoter le code de crediter 8 2 4 Traduction fonctionnelle Il s agit maintenant du c ur m me de la m thode Why Nous en donnons ici un aper u les d tails tant dans Fil99 Fil03a Le but est d engendrer un programme fonctionnel Coq quivalent au programme Why com pl tement annot Ce programme comportera des trous pour les preuves des annotations logiques les obligations de preuv
34. cifi par la donn e d un ensemble fini de constructeurs qui sont des constantes dont le type a pour conclusion une instance de T On attend d un type concret la propri t suivante tout terme clos de ce type se r duit en un terme commen ant par un constructeur 4 1 2 Types r cursifs positifs Lorsque le type J apparait dans un type d un argument d un constructeur alors le type est dit r cursif Si de plus les occurrences de I sont positives dans les arguments des constructeurs alors on dira que le type concret est positif Un mod le de ces types est donn par des arbres dont les n uds sont indic s par les construc teurs et dont certaines branches peuvent tre des fonctions renvoyant des familles d arbres de m me nature ce qui permet de repr senter par un terme fini un branchement infini C est le cas par exemple des notations ordinales introduites dans le paragraphe 3 3 1 On peut vouloir se restreindre aux structures dont chaque branche est finie m me si du fait des branchements infinis la structure elle m me n est pas finie On parlera alors d objet bien fond dans le type positif Lorsqu on se restreint 4 ces objets bien fond s on peut disposer de principes de r currence pour le type soit sous la forme d une r currence structurelle g n ralis e soit en disant que l ordre sous terme est bien fond Mais il peut tre int ressant de disposer aussi d un type qui pourrait contenir des arbres
35. construire des objets concrets Le m canisme de d finitions induc tives permet galement la d finition d objets plus logiques et en particulier de pr dicats En particulier ce sera en g n ral la mani re la plus commode d isoler une partie des l ments d un type inductif 1 7 1 Entiers pairs En th orie des ensembles une d finition possible de l ensemble des entiers pairs est de dire que c est le plus petit ensemble tel que Oest pair pour tout entier n si n est pair alors n 2 est pair La m me d finition est possible dans CCI Le pr dicat even tre pair tant un objet de type nat Prop Les deux clauses de la d finition ci dessus correspondant aux deux construc teurs du pr dicat inductif En Coq Coq lt Inductive even nat gt Prop Coq lt evenD even 0 Coq lt evenS forall n nat even n gt even S S n On voit bien que la structure d une preuve de parit est r cursive l image de la structure d un terme de type nat Ceci est refl t dans le sch ma de r currence qui permet de prouver des propri t s d entiers pairs Coq lt Check even_ind even_ind forall P nat gt Prop PO gt forall n nat even n gt Pn gt P S S n gt forall n nat even n gt Pn 1 7 2 L ordre sur les entiers Un exemple essentiel est l ordre sur les entiers Coq lt Inductive le n nat nat gt Prop Coq lt len lenn Coq
36. de r duction de point fixe est si n41 Commence par un constructeur alors Fix f n T t a1 an41 or Hf Fix f n T t a1 Gat La r gle de r duction est galement gard e par la condition que l argument de d croissance commence par un constructeur Ceci permet d viter de poursuivre la r duction du point fixe l int rieur du terme ce qui violerait la terminaison forte 7 f vrier 2014 50 On d finit ais ment l aide du point fixe la fonction qui calcule le minimum de deux entiers Fix min 0 nat nat gt nat An m Case nat n 0 An Case nat m 0 Am S min n m Par contre la fonction d Ackermann sp cifi e par les quations ack 0 m Sm ack S n 0 ackn S0 ack S n S m ack n ack S n m n cessite l utilisation de deux points fixes imbriqu s Fix ack 0 nat nat gt nat An Case nat n S An Fix ackn 0 nat nat Am Case nat m ack n S 0 Am ack n ackn m L exigence que l argument de d croissance soit de type inductif est essentielle En effet du fait de la pr sence d impr dicativit on peut construire des types pour lesquels certains sous arbres sont plus grands que l objet initial Ainsi si on introduit un type I avec un constructeur non r cursif c de type VA Set A A gt I On introduit l objet t A Set x A gt x de type VA Set A gt A L objet
37. de types d pendants 7 2 1 Type sous ensemble sig 1 2 2 Variantes desig os acad eri amis ohne LUS Alle ease 7 2 3 Sp cification d une fonction bool enne sumbool 7 2 4 Sp cification dans les types de donn es 7 3 Modules et foncteurs Preuve de programmes imp ratifs 8 1 Logique de Hoare classique 8 1 1 S mantique op rationnelle 8 1 2 Logique de Hoare 8 1 3 Compl tude et calcul de plus faible pr condition 81 47 Difficult s es ans M sante ME de Bo eee SA DS en DE we Li 8 2 Transformation fonctionnelle la m thode Why 8 2 1 Le langage Why 2 3 5 24 44 66 2 bo se ee DG AR BA ann hae ee 8 2 2 Typage avec effets 8 2 3 Calcul de plus faible pr condition 8 2 4 Traduction fonctionnelle 8 3 Traitement des structures donn es complexes et application d autres langages de programmation 24 ismdir vue ge Soe tl dents ok put a RAR eu fe oe 8 3 1 Exemple d un programme avec un tableau le drapeau hollandais 8 3 2 Programmes Java et C 65 65 65 67 67 68 68 68 72 72 72 74 75 76 76 77 79 79 80 84 85 7 f vrier 2014
38. dit s il existe un terme de type V a A1 a A I a1 a J ai alors on peut construire un terme de type C gt C I J Cette condition de monotonicit suffit garantir l existence d un plus petit point fixe qui peut tre cod de mani re impr dicative Par contre cette positivit au sens large ne convient pas lorsqu il s agit de d finir un type inductif au niveau pr dicatif Type Th Coquand CPM90 a montr que accepter la d finition inductive suivante conduisait un paradoxe Inductive X Type in X Prop Prop X En effet pour tout Y il existe une application de Y dans Y Prop qui y Y associe le pr dicat Ay gt y y On en d duit une application de X Prop dans X qui P de type X Prop associe in AP P P On v rifie que est une injection P P gt P P Il suffit alors de consid rer le pr dicat Po Av dP P x A P x et de prendre zo Po On v rifie alors ais ment que Po zo est equivalent P zo d o une incoh rence 7 f vrier 2014 48 Positivit stricte Les d finitions inductives de Coq ne permettent pas de la positivit large c est dire une occurrence de la d finition inductive la gauche d au moins un produit Le sch ma g n ral est que si la d finition inductive J appara t dans un type d argument d un constructeur alors ce type d argument la forme Varie
39. divers syst mes de d veloppe ments de d monstration ACL2 PVS HOL Isabelle MetaPrl anciennement NuPrl Mizar et Coq travers ces crit res Le crit re de de Bruijn Le crit re de de Bruijn caract rise les syst mes dont la part d di e la certification de la correction des preuves est petite et bien d limit e Chacun des syst mes HOL Isabelle et Coq a un noyau consacr la certification des preuves et en ce sens v rifie le crit re de de Bruijn Toutefois autant les noyaux de HOL et Isabelle restent assez petits autant celui de Coq est assez cons quent en particulier en raison de la gestion des types inductifs et de la r duction En revanche ni Mizar ni PVS n ont une notion de noyau bien d limit En particulier de nouvelles m thodes de preuves peuvent tre ajout es ces syst mes et la correction des preuves nouvellement obtenues ne d pendra que de la correction de implantation de la nouvelle m thode pas d un noyau stable et pr alablement bien circonscrit Logique ou m ta logique Le choix des syst mes Isabelle et MetaPrl est de fournir non pas une logique mais une m ta logique logical framework permettant de d clarer les signatures et r gles d inf rences de logiques arbitraires Dans la pratique compte tenu du d veloppement d une biblioth que minimale n cessaire toute formalisation cons quente seules peu de logiques sont effectivement implant es dans u
40. es par _ et donnant lieu des sous buts Ainsi on peut red finir la fonction min_elt de la fa on suivante Coq lt Definition min_elt forall s s Empty gt Z Coq lt refine Coq lt fix min s tree h s Empty struct s Z Coq lt match s return s Empty gt Z with Coq lt Empty gt Coq lt fun h gt _ Coq lt Node 1 x _ gt Coq lt fun h gt match 1 as a return a l gt Z with Coq lt Empty gt fun _ gt x Coq lt _ gt fun h gt min_elt 1 _ Coq lt end _ Coq lt end h On obtient alors deux sous buts qu il est ais de prouver On remarque tout de m me que l on n chappe pas un filtrage d pendant Enfin une derni re solution consiste rendre la fonction totale en la compl tant de mani re arbitraire en dehors de son domaine de d finition Ici on peut choisir de retourner la valeur 0 lorsque l ensemble est vide On vite ainsi l argument logique ns Empty et ses f cheuses cons quences Le type de min_elt redevient tree Z et sa d finition est tr s simple 7 f vrier 2014 91 Coq lt Fixpoint min_elt s tree Z match s with Coq lt Empty gt 0 Coq lt Node Empty z _ gt z Coq lt Node 1 _ _ gt min_elt 1 Coq lt end Le th or me de correction reste le m me en revanche Coq lt Theorem min_elt_correct Coq lt forall s s Empty gt bst s gt Coq lt In min_elt s s Coq lt forall x
41. false gt W P i2 Q W P while e doi Q pas de formule simple Exemple 7 WP z x y x 2y x y 2y Proposition 2 L ensemble des r gles de logique de Hoare est relativement complet Tout triplet valide P i Q est d rivable en particulier on peut trouver des invariants pour les boucles while de i Preuve le relativement exprime ici une hypoth se qui est que la logique dans laquelle on exprime les annotations est suffisamment expressive en particulier pour exprimer les invariants de boucle n cessaires l aide de point fixe Cou90 7 f vrier 2014 103 let isqrt fun n int gt n gt 0 pr condition begin let count ref O in let sum ref 1 in begin while sum lt n do invariant count gt O and n gt count count and sum count 1 x count 1 variant n sum invariant et variant de boucle count count 1 sum sum 2 count 1 done count end end result gt 0 and result result lt n and n lt result 1 result 1 post condition FIGURE 8 1 Calcul de la racine carr e en Why 8 1 4 Difficult s De nombreux travaux ont fait suite la logique de Hoare originale Cou90 pour tendre le formalisme et r soudre des difficult s par exemple R f rer dans une post condition Q de P i Q la valeur d une variable avant l ex cu tion de i Avoir des effets de bord dans les expressions Traiter l appel de
42. false et il n est pas possible de montrer Vb bool b true V b false Il devient alors difficile de raisonner sur les bool ens sauf ajouter ces propri t s comme axiome cependant on perd alors la correspondance entre le calcul et le raisonnement Une autre difficult du codage impr dicatif est qu il y a plus de termes normaux clos dans le codage du type inductif que ceux construits partir des constructeurs L exemple le plus simple illustrant ce ph nom ne consiste prendre le type inductif J des singletons avec un seul constructeur c Un Un I Le codage impr dicatif donne Un VC Set C gt C I VC Set Un gt Un gt C gt C f Un gt Un C Set h Un Un gt C h f Il n est pas difficile de construire un terme normal clos de type J qui ne peut s crire sous la forme c f avec f un terme normal clos de type Un Un On distingue une classe de types appel s types de donn es qui correspondent des codages de d finitions inductives dans lesquelles tous les types d arguments des constructeurs sont eux m mes r cursivement des types de donn es il est surtout essentiel qu il n y ait pas de quantification d ordre sup rieur en position n gative Pour les types de donn es il est possible d tablir un th or me de repr sentation savoir que tous les termes clos normaux sont B quivalent un constructeur appliqu des argumen
43. forall s list nat e1 e2 expr Coq lt interp s insere e1 e2 interp s Plus e1 e2 Coq lt Proof Coq lt induction e1 intro e2 simpl auto Coq lt rewrite plus_assoc_reverse Coq lt change interp s e1_2 interp s e2 with interp s Plus e1_2 e2 Coq lt rewrite lt IHe1_2 Coq lt rewrite IHel_1 trivial Coq lt Qed 7 f vrier 2014 70 Coq lt Theorem validite Coq lt forall s list nat e expr interp s norm e interp s e Coq lt Proof Coq lt induction e simpl auto Coq lt destruct e2 as e e0 il Coq lt rewrite validite_insere Coq lt rewrite lt IHe2 trivial Coq lt simpl interp rewrite IHel auto Coq lt rewrite validite_insere Coq lt rewrite lt IHe2 trivial Coq lt Qed Apr s ce travail pr alable chaque application de la m thode de simplification se d roule comme suit Coq lt Variable P nat gt Prop Coq lt Lemma exemple forall x y t u nat P 0 x u y t Coq lt intros 1 subgoal x nat y nat t nat u nat PCO xe Gp toy t Coq lt pose sigma x u y t nil Coq lt change P interp sigma Plus Plus Zero Var 0 Plus Var 1 Var 2 1 subgoal x nat y nat t nat u nat sigma X u y t nil list nat P interp sigma Plus Plus Zero Var 0 Plus Var 1 Var 2 Coq lt rewrite lt validite 1 subgoal x nat y nat t nat u nat sigma
44. i e une preuve de false d autre part on voit que les arguments logiques li s la pr condition qui compliquaient la d finition ont disparu dans le code extrait ils taient dans la sorte Prop Une autre solution consiste d finir la fonction min_elt par une preuve plut t que par une d finition Il est alors facile de construire les termes de preuve on est dans l diteur de preuves Ici la d finition preuve est relativement simple Coq lt Definition min_elt forall s s Empty gt Z Coq lt Proof Coq lt induction s intro h Coq lt elim h auto Coq lt destruct s1 Coq lt exact z Coq lt apply IHsi discriminate Coq lt Defined Mais il est plus difficile de se persuader que l on construit la bonne fonction tant que l on n a pas montr la correction de cette fonction Il faut en particulier prendre bien soin de ne pas utiliser tort de tactiques automatiques telles que auto qui pourraient avoir pour effet de construire une fonction autre que celle que l on a en t te sur cet exemple auto n est utilis que sur un but logique Empty Empty Une fa on de se persuader que le code sous jacent est bien le bon consiste examiner le code extrait Ici on retrouve exactement le m me que pr c demment La tactique refine aide a la d finition de fonction partielle mais pas seulement Elle permet de donner partiellement un terme de preuve certaines parties tant omises d not
45. l introduction d une notion de r alisabilit dans le Calcul des Constructions a pour but l obtention de programmes plus efficaces ne conservant que la partie de la preuve utile pour le calcul des t moins Elle sert galement justifier certaines propri t s qui ne sont pas d montrables 6 3 1 Oubli des types d pendants On consid re le Calcul des Constructions pur sans univers et sans limination forte sur les types inductifs que nous noterons CC On peut montrer que tout A terme pur typable dans CC est galement typable dans le syst me Fy avec types inductifs Cette propri t est simple montrer On associe chaque terme t ou type de CC un terme ou un type E t dans F en oubliant les d pendances des types par rapport aux preuves et on montre que si Fcc t P alors Fe E t E P La d finition de la fonction d oubli E _ est donn e dans la figure 6 3 Cette traduction permet de montrer que 0 1 n est pas prouvable dans CC En effet 0 4 1 est une abr viation pour P nat gt Set P 0 gt P 1 gt C Set C S il existait un terme de ce type il y aurait galement un terme de F de type E 0 1 c est a dire P Set P gt P gt C Set C Mais comme il existe un terme de type P Set P P on aboutit l existence d un terme de type C Set C ce qui est absurde 7 f vrier 2014 80 Set Set X SA X A Type z e x A Set x A B E A gt E B A B Set X
46. la correction et la compl tude ce qui n est pas vident d s que le langage comporte des constructions avanc es comme des appels de proc dure 2 4 3 Preuve de programmes Java Un domaine actif de recherche est actuellement l tude des propri t s de s curit des pro grammes Java qu ils soient utilis s sur l internet ou les cartes puce Pour garantir de telles propri t s il est essentiel d avoir une description pr cise de la s mantique de ce langage au niveau du code source ou du byte code que ce soit la s mantique statique dynamique ou axiomatique Le projet Bali http isabelle in tum de Balihttp isabelle in tum de Bali l universit 7 f vrier 2014 35 de Munich formalise ces notions dans l outil Isabelle HOL Des d veloppements analogues sont r alis s l aide de Coq en France dans le projet Lemme l INRIA Sophia Antipolis dans le projet Lande IRISA ou par la soci t Trusted Logic Les d finitions inductives sont utilis es de mani re intensive dans ces d veloppements 2 4 4 Plongement superficiel ou profond Lorsqu on veut tudier les programmes d un langage X on peut proc der de deux mani res La premi re appel e plongement profond deep embedding en anglais consiste introduire un type concret dans Coq pour repr senter les arbres de syntaxe abstraite du langage X La seconde appel e plongement superficiel shallow embedding en anglais consiste repr senter directemen
47. les s ries math matiques ou les expressions de processus Il est possible d utiliser des fonctions pour repr senter de tels objets mais on aimerait une repr sentation plus proche de la 7 f vrier 2014 53 structure concr te de ces objets Les d finitions co inductives ont une structure duale des d fi nitions inductives Elles ont t ajout es au Calcul des Constructions Inductives et int gr es a Coq par Eduardo Gim nez L approche suivie avait t sugg r e par Th Coquand Les d fini tions co inductives admettent comme sch ma d limination la d finition par cas et comme r gle d introduction en compl ment des constructeurs des d finitions par point fixe 3 4 2 Structures quotients Les d finitions co inductives sont des structures libres il est donc possible de prouver que deux constructeurs d un type inductif dans Set ou Type ont des images disjointes Supposer qu une quation entre constructeurs est satisfaite conduit une th orie inconsistante Pourtant les structures quotients sont tr s utilis es repr sentation des rationnels des r els ou des lambda termes Plusieurs solutions ont t propos es pour ajouter des types quotients une th orie des types en particulier par R Backhouse M Hofmann S Boutin G Barthe et plus r cemment par P Courtieu A part NuPrl les assistants de preuve ne proposent pas de type inductif quotient C est l utilisateur de g rer la main une galit
48. lt le_S forall m nat le n m gt le n S m Son principe de r currence Coq lt Check le_ind le_ind forall n nat P nat gt Prop P n gt forall m nat le n m gt P m gt P S m gt forall nO nat le n nO gt P nO Exercice Prouver forall n m nat le n m gt le S n S m forall n nat le 0 n forall n m nat le n m gt le m p gt le n p 7 f vrier 2014 20 1 7 3 Un exemple dangereux Voici un exemple pour illustrer les subtilit s propres aux math matiques formelles On peut proposer une d finition alternative a le Coq lt Inductive le_a nat gt nat gt Prop Coq lt le_aO forall n nat le_a O n Coq lt le_aS forall n m nat le_a n m gt le_a S n S m Or cette d finition qui semble raisonnable et est math matiquement saine est peu prati cable telle quelle En particulier la preuve de la transitivit est tr s p nible on peut utiliser cette d finition mais pour certaines propri t s il vaut mieux commencer par prouver d abord l quivalence avec la d finition pr c dente L on risque sinon de s ensabler rapidement Chapitre 2 Exemple de d veloppement Gallina S mantique d un mini langage Le but de ce cours est d illustrer sur un exemple les fonctionnalit s du langage de sp cifi cation Gallina associ au Calcul des Constructions Inductives et implant dans l assistant la d monstration Coq L exemple choisi
49. m p signifie que la fonction r cursive de code n s ex cute sur l entr e de code m pour effectuer un calcul de code p C est un r sultat bien connu que le pr dicat P n 3p T n n p n est pas r cursif car sinon P n le serait aussi et donc il existerait une fonction r cursive de code q qui converge exactement lorsque P n est v rifi e c est dire pour tout n 3p T q n p amp 7A p T n n p Il suffit de prendre n q pour aboutir une contradiction Maintenant en prenant pour A la formule P x 3p T x x p si P x V P x est montrable il en est de m me de Vx P x V P x et on aurait la d cidabilit de P x qui est contradictoire 6 1 2 Constructivit du Calcul des Constructions Inductives Pour montrer le caract re constructif de la logique de Coq on s appuie sur l isomorphisme de Curry Howard qui permet de repr senter les preuves par des termes fortement normalisables et la propri t syntaxique suivante qui caract rise les objets normaux clos dans les types inductifs Propri t Un terme normal clos dont le type est une instance d une d finition inductive est forc ment de la forme c t tn avec c un des constructeurs du type inductif et t des termes clos normaux Preuve En effet tout terme t s crit de mani re unique c t tn avec c qui n est pas une application c peut donc tre soit une abstraction soit une variable soit un constructeur soit une so
50. mantique axiomatique Une assertion est une propri t de la m moire repr sent e par un pr dicat unaire En logique de Hoare ce pr dicat unaire sera d fini concr tement par une formule logique utilisant les variables du programme pour repr senter les valeurs correspondantes de la m moire Coq lt Definition Assertion memory gt Prop Transformations de pr dicats On tend les op rations usuelles de la logique des transformations d assertion Coq lt Definition Istrue E expr Assertion Coq lt fun m memory gt exprval m E Bool true Coq lt Definition Isfalse E expr Assertion Coq lt fun m memory gt exprval m E Bool false Coq lt Inductive AndAss P Q Assertion m memory Prop Coq lt Conjass P m gt Q m gt AndAss P Q m Coq lt Definition ImplAss P Q Assertion Prop forall m memory P m gt Q m Le transformateur suivant correspond ce que nous avons not P X E Le terme memupdate x E P repr sente le pr dicat qui est vrai en m si P m X v est v rifi avec v la valeur de l expression E dans la m moire m Coq lt Definition memupdate x name e expr P Assertion Assertion Coq lt fun m memory gt forall v semval exprval m e v gt P update x v m D finition de P c Q On d finit le pr dicat trueform P c Q correspondant a P C Q telle qu il est d crit dans la figure 2 7 Coq lt Inductive trueform Assertion gt co
51. ou plusieurs style de bonne preuve tout comme il existe de bons styles de programmation pour un probl me et un langage de programmation donn Nous nous attacherons particuli rement la mod lisation et la formalisation de probl mes informatiques o la s ret est importante et la preuve de correction de programmes 7 f vrier 2014 7 Architecture des syst mes Enfin nous chercherons d crire les grands principes d un logiciel d assistant la d monstra tion Poursuivant encore l analogie avec la programmation ceci correspondrait la description d un compilateur Nous nous int resserons principalement au syst me de preuves Coq 1 2 Quelques rappels sur les th ories de types Aujourd hui on d signe g n ralement par th orie des types un formalisme logique dont les objets sont des A termes typ s Il existe plusieurs formalismes rentrant dans cette cat gorie et ils se distinguent essentiellement par le syst me de types plus ou moins riche des objets ainsi que par la logique pour parler de ces objets On peut citer en particulier la logique d ordre sup rieur de Church la Th orie des Types de Martin L f la logique du syst me PVS et le Calcul des Constructions Inductives CCI dont les variantes implant es par Coq seront l objet et le support premier de ce cours Les objets de la logique d ordre sup rieur de Church sont les termes simplement typ s Les trois autres formalismes utilisen
52. petit que limit f Voici une d finition l gale de fonction sur ce type des ordinaux Cette vision de la r cursion structurelle est galement refl t e dans l nonc du sch ma de r currence du type Coq lt Check Ord_ind Ord_ind forall P Ord gt Prop P Qo gt forall o Ord P o gt P So o gt forall o nat gt Ord forall n nat P o n gt P lim o gt forall o Ord P o C est a dire que pour appliquer le sch ma sp cialis un pr dicat P il faut v rifier que si tant donn e f de type nat ord telle que pour tout entier n f n v rifie P alors lim f v rifie galement P 1 6 2 Arbres arbitrairement branchants On peut utiliser l id e pr c dente pour d finir un type d arbre tr s g n ral en utilisant le polymorphisme on s autorise indexer les fils de chaque n ud par un type arbitraire Coq lt Inductive Inf_tree Type Coq lt Node forall A Set A gt Inf_tree gt Inf_tree Inf_tree is defined Inf_tree_rect is defined Inf_tree_ind is defined Inf_tree_rec is defined Ce type est tr s peu intuitif Il utilise et combine toutes les ressources du formalismes et permet ainsi la construction de tr s nombreux l ments De fait le logicien anglais Peter Aczel a prouv qu il tait possible d encoder les l ments de la th orie des ensembles dans ce type 7 f vrier 2014 19 1 7 Pr dicats inductifs Nous avons vu comment
53. point fixe est appel e une d finition inductive La syntaxe en Coq d une telle d finition est Coq lt Inductive nat Set Coq lt 0 nat Coq lt S nat gt nat Cette commande ajoute l environnement du syst me les objets suivants le type nat Set les deux objets O nat et S nat gt nat appel s constructeurs de nat En g n ral cette d finition ainsi que la plupart de celles qui suivent sont d j pr sentes dans l environnement du syst me au lancement Coq lt Print nat Inductive nat Set 0 nat S nat gt nat Coq lt Check nat nat Set Coq lt Check 0 0 nat Coq lt Check S S nat gt nat Remarque Informellemment le plus petit type ainsi d fini est celui dont les habitants sont 0 S 0 S S Q etc On a donc bien une repr sentation de la notion math matique d entier naturel Remarque La vision informatique est que cette d finition est la version Coq du type concret ML bien connu type nat 0 S of nat On peut remarquer au passage qu en Coq le constructeur S est fonctionnel et peut donc exister sans son argument Il s agit l d un point syntaxique d importance marginale Remarque D un point de vue ensembliste les entiers naturels sont le plus petit point fixe de Vop rateur suivant F X 0 U S x x X 7 f vrier 2014 12 Cet op rateur est monotone et admet donc un plus petit point fixe En effet l
54. preuve partielle peut comporter plusieurs points d interrogations c est dire que l on peut avoir plusieurs sous buts simultan ment chacun avec son contexte local La tactique apply correspond l application Coq lt apply c 1 subgoal Prop Prop On est alors pass au terme de preuve partiel fun c A gt B gt C b B gt c 71 o le but courant est maintenant A gt C On finit donc la preuve par Coq lt intros a 1 subgoal A Prop B Prop C Prop c A gt B gt C b a Coq lt exact b No more subgoals La commande Qed ou Save permet alors d ajouter l environnement global le terme exemp1 ainsi cr e Coq lt Qed intros c b apply c intros a exact b exemp1 is defined Coq lt Print exemp1 exemp1 fun c A gt B gt C b B gt c fun A gt B gt C gt B gt C A gt b 7 f vrier 2014 11 Rassurons enfin le lecteur une preuve aussi simple peut heureusement galement tre trou v e automatiquement par les tactiques de preuve plus volu es dont dispose le syst me Plus g n ralement ce document n est d ailleurs pas un manuel d utilisateur ni un cours de Coq Nous renvoyons pour cela la documentation standard de Coq Coq07 1 4 Les Entiers Naturels dans CCI 1 4 1 D finition Le type des entiers naturels est le plus petit type contenant 0 et clos par le successeur S une telle d finition par plus petit
55. qu une fonction attend un entier positif et retourne un entier premier f n Z n gt 0 p Z premier p Nous allons montrer comment 7 2 1 Type sous ensemble sig La notation Coq x A P d signe le sous type de A des valeurs v rifiant la propri t P ou dans un vocabulaire plus th orie des ensembles le sous ensemble de A des l ments v rifiant P La notation x A P d signe l application sig A fun x gt P o sig est Vinductif suivant Coq lt Inductive sig A Set P A gt Prop Set Coq lt exist forall x A P x gt sig P Cet inductif est identique l existentielle ex si ce n est sa sorte Set au lieu de Prop on souhaite d finir une fonction et donc que ses arguments et r sultats soient informatifs En pratique on souhaite lier l argument au r sultat par une postcondition Q et on pr f re donc la forme plus g n rale suivante fiV i Pis ym Q z y Si l on reprend l exemple de la fonction min_elt sa sp cification peut tre la suivante Coq lt Definition min_elt Coq lt forall s s Empty gt bst s gt Coq lt m Z In m s forall x In x s gt m lt x 7 f vrier 2014 95 On a toujours les difficult s de d finition directe mentionn es dans la section pr c dente et l on pr f re donc en g n ral la d finition par preuve avec toujours la m me mise en garde vis vis des m thodes automatiques Note Le d p
56. s agit de la m me d finition mais param tr e par le type A Cette abstraction est possible grace aux types fonctionnels Coq lt Check list list Set gt Set Coq lt Check nil nil forall A Set list A Coq lt Check cons cons forall Set A gt list A gt list A A titre d exemple on crira ainsi l quivalent de l objet ML 1 2 3 Coq lt Check cons nat 1 cons nat 2 cons nat 3 nil nat cons nat 1 cons nat 2 cons nat 3 nil nat list nat A condition de recourir la d finition d finie dans le module List de la biblioth que standard de Coq on peut aussi utiliser la notation suivante Coq lt Require Import List Coq lt Check 1 2 3 nil 1 2 3 Datatypes nil Datatypes list nat Le sch ma de r currence structurelle sur les listes est Coq lt Check list_ind Datatypes list_ind forall A Type P Datatypes list gt Prop P Datatypes nil gt forall a A 1 Datatypes list A P 1 gt P a 1 gt forall 1 Datatypes list A P 1 On reconna t la m me structure que pour les entiers avec toutefois l argument suppl mentaire de cons et la param trisation par rapport A 1 5 3 Types somme et produit Un exemple courant de type param tr est le type somme Coq lt Inductive sum A B Set Set Coq lt inl A gt sum AB Coq lt inr B gt sum A B Son sch ma d limination est plus simple pu
57. simuler le syst me U Si Set est pr dicatif il reste coh rent avec la logique classique la r traction s interpr te comme un oracle qui d cide la validit de toute proposition On peut aussi s int resser aux interactions avec la logique classique calculatoire c est dire bas e sur une r alisation par l op rateur call cc de Scheme ou SML ou l op rateur u de Parigot Une telle interpr tation calculatoire de la logique classique est incompatible avec l axiome de description m me avec Set pr dicatif Her05 Le principe de description ind finie op rateur de Hilbert Le principe de description ind finie affirme l existence a priori d un t moin canonique dans tout pr dicat non vide sur un domaine non vide On peut l exprimer en Coq par la proposition Anon vide gt Xa A 3x A P x gt P x Ce principe est quivalent se donner pour tout A non vide un op rateur A Prop gt A tel que dr A P x P e P op rateur e de Hilbert De mani re vidente le principe de description ind finie entra ne l axiome du choix 7 f vrier 2014 118 Le principe de description ind finie version constructive Le principe de description ind finie dans sa version constructive exprime que si une pro position est prouvablement habit e alors il existe un terme qui d note un habitant de cette proposition Ce principe peut tre exprim dans le CCI par la formule dx A P
58. traite de la s mantique d un mini langage de programmation imp ratif ty page valuation et s mantique axiomatique Plusieurs solutions la mod lisation des diff rentes notions sont propos es Les diff rentes constructions utilis es dans ce chapitre seront expliqu es plus en d tail dans les prochains cours 2 1 Introduction Gallina est le nom donn au langage de sp cification de l assistant Coq I permet de d finir des types de donn es structur s des fonctions qui peuvent tre r cursives sur la structure des donn es des relations sp cifi es inductivement par un ensemble de propri t s de fermeture des formules du calcul des pr dicats d ordre sup rieur Ces caract ristiques du langage le rendent particuli rement adapt la formalisation des math matiques et notamment de l informatique th orique On pourra notamment se faire une opinion sur ce slogan en consultant sur la page de Coq la liste des d veloppements r alis s par les utilisateurs Les d finitions intervenant en s mantique des langages se repr sentent particuli rement bien en Gallina les arbres de syntaxe abstraite se codent naturellement comme des types de donn es structur s l ordre sup rieur permettra de manipuler ais ment les m moires qui pourront tre repr sent es par des fonctions ou bien les assertions qui sont des pr dicats sur la m moire les d finitions s mantiques telles q
59. v et la notation 7 d signe le vecteur de variables obtenus en ajoutant surchargeant les variables de aux variables de Z t t ref alors e est une variable r et E A o Ap P o let 1 f q2 e Zo 1 in let 9 v q f r 24 2 in 41 E3 v 23 o 1 P x 2 P x0 Ti et 3 Q X0 di P v Remarques les interpr tations de l application valuent les arguments de l application de droite gauche L interpr tation des boucles while Fil99 Fil03a utilise we11_founded_induction tel qu expliqu au chapitre 7 Exemple 8 La validation trous de crediter est Definition crediter fun s Z montant Z Pre s gt 0 gt let resulti Post exist fun result Z gt result s montant montant s P01 s montant Pre x result Z result s montant 7 f vrier 2014 109 in exist_2 fun montanti Z result0O unit gt montanti s montant resulti tt Post x resulti Z result2 unit resulti s montant ou PO1 s Z montant Z Pre s gt 0 montant s s montant Proposition 3 Correction Fil99 Fil03a Pour toute expression e typ e avec effets anno t e si les obligations de preuve de sont prouvables alors e v rifie sa sp cification c d que sa post condition est valide quand sa pr condition est satisfaite Pour la preuve de cette proposition il faut d finir formellement la s mantique de Why Fi
60. v sval s mem memory1 Coq lt Definition update forall m nat s sort sval s Le simple fait de savoir que s s ne suffit pas assurer que le terme v de type sval s est aussi de type sval s Il faudra utiliser une analyse par cas suivant les valeurs de s et s Une telle analyse n aurait pas t possible si l ensemble des sortes tait rest param trique 7 f vrier 2014 29 De mani re g n rale en pr sence de types d pendants l usage de l galit devient d licat Il n est pas possible par exemple d crire v v avec v sval s et v sval s sauf lorsque s et s sont convertibles la pr sence d une hypoth se s s est insuffisante Il faudra utiliser des notions plus complexes d galit 2 3 2 V rification du type et valuation constructive On pourrait d finir le fait qu une expression e est mal form e comme la propri t Vs sort exprcorrect s e En fait il est plus ais de manipuler des d finitions positives et donc de d finir une notion constructive d expression erron e en num rant les cas d chec possibles Si on s int resse l interpr tation constructive des preuves que nous verrons plus tard on remarque qu une preuve que l expression erron e permet de retrouver exactement la nature de l erreur savoir dans quel sous terme un op rateur a t appliqu une expression d une sorte non adapt e Coq lt Inductive exprerr e
61. voir l une source de confusion rappelons simplement que l informatique est sans doute la science de la bureaucratie et d une vision un peu tyrannique de l ordre et particuli rement du renommage 1 3 2 V rification et inf rence de types A partir de l nous pouvons taper nos premi res commandes pour utiliser le v rificateur de type En syntaxe Coq l identit polymorphe est donc not e fun A Type a A gt a On demande au syst me de v rifier la bonne formation d un objet par la commande Check les commandes Coq tant toujours termin es par un point cela donne Coq lt Check fun A Type a A gt a fun A Type a A gt a forall Type gt A Toutes les op rations de typage de Coq ont lieu dans un environnement global Cet environ nement correspond au contexte I des jugements de typage IT F t T Il est donc possible de pousser de nouvelles variables dans l environnement Coq lt Variable A Prop is assumed Coq lt Variable a A a is assumed 7 f vrier 2014 9 De plus l environnement de Coq peut galement contenir des constantes ou abr viations Pour cela on associe un terme un nom de plus l environnement m morise aussi un des types du corps de la constante Coq lt Definition Id B Type b B b Id is defined Coq lt Check Id Id forall B Type B gt B Coq lt Print Id Id fun B Type b B gt b forall B Type B g
62. wf_inv A R x H est structurellement plus petit que H car obtenu en prenant un sous terme structurel de H Pour obtenir une fonction de type list 1list il suffit d utiliser une preuve que R est bien fond e c est dire d une preuve de VI list wf list R 1 L avantage de cette d finition est que la propri t wf peut tre d finie dans la sorte Prop Donc le comportement calculatoire de la fonction quickwf l extraction est le comportement attendu Par contre il est compliqu de r duire la fonction quickwf dans Coq car cette r duction ne peut avoir lieu que si la preuve h de wf list R l commence par un constructeur Pour raisonner sur de telles fonctions il est pr f rable d tablir des quations de point fixe Cependant ces quations ne sont pas imm diates tablir Ce probl me a t tudi en d tail dans la th se de Antonia Baala Bal02 Des th or mes dans la biblioth que Init Wf permettent de faciliter les constructions de fonctions par point fixe 3 3 6 D finitions mutuellement inductives Coq accepte de mani re primitive les d finitions mutuellement r cursives En fait de telles d finitions peuvent simplement tre cod es en faisant de la d finition inductive une famille de d finitions inductives On introduit un type A qui fait la somme disjointe des arit s des diff rentes d finitions inductives Les d finitions mutuellement inductives J seront remplac es par une famille inductive d
63. x 2y Exemple 6 Sur le programme ISQRT on souhaiterait montrer la validit du triplet n gt O ISQRT count x count lt n An lt count 1 count 1 Logique de Hoare ensemble de r gles de d duction sur les triplets PAec true ii Q PAe false i2 Q P skip P Phif e then i else i2 Q TAe true i l Pla e l a e P I while e do i I Ae false P h Q Q i R PR PP Q Q PF t2 R PHQ Proposition 1 Cet ensemble de r gles est correct tout triplet d rivable est valide Preuve pas de difficult cf chapitre 2 Difficult prouver un triplet partir de ces r gles demande de deviner les bonnes anno tations interm diaires par exemple pour la s quence mais aussi pour la r gle d affaiblissement Ainsi on ne peut pas prouver le programme de la racine carr e sans r fl chir il faut en parti culier trouver un invariant de boucle ad quat L quivalent du point de vue th orique de cette difficult est a t on compl tude de la logique de Hoare c d peut on prouver tous les triplets valides 8 1 3 Compl tude et calcul de plus faible pr condition Pour 7 et Q fix s l ensemble des P tels que P i Q est valide s il est non vide poss de t il un l ment minimal P au sens o pour tout P tels que P i Q est valide P implique Pp Calcul de WP WP xz e Q Q x lt e WP it i2 Q WP i1 WP i2 Q WP if e then i else i2 Q e true gt WP i1 Q A e
64. x gt Sa A P x Notons que le principe de description ind finie est d rivable si A est d nombrable et P d cidable En effet on peut alors construire un programme qui teste successivement si chacun des l ments de A dans l ordre v rifie P Ce programme est calculable par d cidabilit de P et terminant par existence d un habitant dans P On en d duit le principe de description cf theories Logic ConstructiveEpsilon v Le principe de description d finie op rateur de Church Le principe de description d finie restreint le principe de description ind finie au cas des pr dicats habit s par un objet unique Le t moin a priori de la non vacuit du pr dicat ne v rifie le pr dicat que si ce terme est prouvablement unique Le principe de description d finie peut tre exprim dans le CCI par la formule Anon vide gt ha A Ala P x gt P x Ce principe est quivalent se donner pour tout A non vide un op rateur amp A Prop gt A tel que 2 x A P x P u P op rateur 1 de Church Ce sch ma n entra ne pas l axiome du choix mais il entra ne l axiome du choix unique Le principe de description d finie version constructive Dans sa version constructive le principe de description d finie ne pr suppose pas l existence a priori de t moins le t moin d un pr dicat n aura une d notation que si le pr dicat est effec tivement habit de mani re unique Ce princi
65. 002 Selected Papers volume 2646 of Lecture Notes in Computer Science pages 240 258 Springer 2003 7 f vrier 2014 124 PM89a Christine Paulin Mohring Extracting F s programs from proofs in the Calculus of Constructions In Association for Computing Machinery editor Sixteenth Annual ACM Symposium on Principles of Programming Languages Austin January 1989 PMS89b Christine Paulin Mohring Extraction de programmes dans le Calcul des Construc tions PhD thesis Universit Paris 7 January 1989 Poi02 Henri Poincar La Science et l Hypoth se Flammarion 1902 Pol Randy Pollack The LEGO proof assistant http www dcs ed ac uk home lego PS Frank Pfenning and Carsten Schtirmann The Twelf project http www 2 cs cmu edu twelf Raf Christophe Raffalli The PhoX proof assistant http www lama univ savoie fr sitelama Membres pages_web RAFFALLI af2 html Sch97 Thomas Schreiber Auxiliary variables and recursive procedures In TA PSOFT 97 volume 1214 of LNCS pages 697 711 1997 SG95 Milena Stefanova and Herman Geuvers A simple model construction for the calculus of constructions In TYPES volume 1158 of Lecture Notes in Computer Science pages 249 264 Springer 1995 Tak91 Yukihide Takayama Extraction of redundancy free programs from constructive natural deduction proofs Journal of Symbolic Computation 12 29 69 1991 Ter92 Delphine Terrasse Traduction de TYPOL en COQ Application M
66. 14 100 Note Le langage Objective Caml fournit une biblioth que d ensembles finis cod s par des arbres binaires de recherche quilibr s des AVL AVL62 sous la forme d un foncteur prenant en argument un type ordonn e Cette biblioth que implante toutes les op rations habituelles sur les ensembles union intersection diff rence cardinal plus petit l ment etc des it rateurs map fold iter et galement une fonction d ordre total sur les ensembles permettant d obtenir des ensembles d ensembles par une seconde application du m me foncteur et ainsi de suite Cette biblioth que a t certifi e l aide de Coq par Pierre Letouzey et Jean Christophe Filli tre FL04 Cette preuve a permis de d couvrir un bug dans le r quilibrage des arbres effectu par certaines fonctions le code a t corrig dans la derni re version d ocaml 3 07 Chapitre 8 Preuve de programmes imp ratifs 8 1 Logique de Hoare classique On consid re un langage PASCAL tr s simplifi avec des variables globales enti res des expressions enti res et bool ennes et les instructions d affectation de test et de boucle while e n xz eope op 1 l4l lt l gt ls 2 and or i skip x e i i if e then i else i while e do i done Exemple 5 Appelons ISQRT le programme suivant sur trois variables n count et sum count 0 sum 1 while sum lt n do count count 1 sum sum 2 count 1 d
67. A Miquel qui distingue une sorte Prop interpr t e classiquement et une sorte Set interpr t e par r alisabilit mais qui ne prend pas en compte les types inductifs Miq01 Dans le cas d un Set pr dicatif il n existe pas non plus explicitement de mod le mais il est commun ment admis que le mod le bool en avec Set interpr t comme Type fonctionne Axiome K de Streicher L axiome K de Streicher nonce que toute preuve de la r flexivit de l galit peut tre remplac e dans tout contexte par la preuve canonique de r flexivit VA Set Va A Vp a a VP a a gt Prop P refl_equal a gt P x Cet nonc est quivalent l existence d une unique preuve de r flexivit de l galit VA Set Va A Vp a a p refl equal a Il existe plusieurs autres formulations quivalentes l axiome K D une d elle est particuli rement int ressante en pratique elle exprime que deux objets dans des types d pendants sont gaux d s lors qu ils sont dans la m me instance d pendante VA Set VB Set Va A Vb b B a a b a b gt b b Notons que l axiome K est d rivable si l galit sur A est d cidable ce qui est le cas en parti culier en admettant la logique classique Notons par ailleurs que l axiome K est une cons quence directe de l indiscernabilit des preuves ind pendamment alors de la logique classique Indiscernabilit des preuves L indiscernabilit
68. A B X E A E B A Type B Set x A B E B A Set B Type X A B E A gt E B A B Type x Alt z E AJE t t B Set ou A Type Alt E t t B Type et Set t A Set ou u B Type t A Type et u B Set SS RS t u E t E u tu E t Ce BNO ied Reese my t i FIGURE 6 3 Traduction de CC vers Fy R alisabilit modifi e Une notion de r alisabilit modifi e naturelle est de demander de r aliser toute formule de P du Calcul des Constructions par un terme t de type E P qui satisfait de plus une certaine propri t x r P d finie par r currence sur P dans la figure 6 4 On commence par d finir la formule x r P pour P Set on aura galement besoin de d finir X r A lorsque A Type ce qui est fait dans la figure 6 5 Dans le cas A Type X r A sera galement une arit de type Type qui repr sente le type des pr dicats de r alisabilit pour les objets d arit A Comme une proposition peut tre form e par abstraction et application nous d finissons galement dans la figure 6 6 une transformation R P qui s applique tous les objets P A avec Type et qui coincide avec la d finition du pr dicat x x r A quand A est Set en particulier R A a alors le type E A gt Prop xr P R P x P Set et P n est pas un produit fr z A B E A zrA fz rB A B Set fr X A B X E A X Xr A f X r B A Type B Set FIGURE 6 4 R alisabilit dans CC x r P pou
69. D1 2m Dm A u1 u et I n appara t ni dans les D ni dans les u On v rifiera que toutes les d finitions inductives donn es en exemple satisfont cette condition de positivit R cursivit emboit e La positivit stricte n interdit pas a priori que l argument r cursif se trouve comme param tre d une autre d finition inductive De fait si un type de constructeur de la d finition inductive J a pour type Ax1 I ou Ax est la d finition inductive pour le produit de A et de J alors I est quivalente une d finition J o le type de constructeur serait A gt J gt J et donc strictement positif De m me si le constructeur est A J I alors on peut le remplacer par deux constructeurs strictement positifs de type A gt J et J gt J Cela fonctionne m me si la d finition imbriqu e est r cursive il faut alors d finir deux types mutuellement r cursifs Si le type de constructeur est list J I on remplace J par une d finition J d finie de mani re mutuellement r cursive avec L qui repr sente list J Le constructeur de type list I gt I devient un constructeur de type L J les constructeurs de L sont ceux de list T soit nilz L et cons J gt L gt L Cette transformation nous montre qu il est possible d autoriser une occurrence r cursive de Vinductif I comme param tre d une autre d finition inductive J Cependant certaines conditions doivent tre v rifi e L occurrence de J do
70. E 6 8 R alisabilit tendue Prop x r P avec P Set Exemple Pour comprendre les interactions entre Prop et Set dans la r alisabilit on peut prendre l exemple de la d finition impr dicative d une famille list de listes d objets de type A v rifiant un pr dicat P La famille list a pour type A Set A Prop Set et est d finie par list A Set P A Prop X Set X gt a A Pa 9 X gt X gt X 7 f vrier 2014 82 Fr x A B FrB B Type et A Prop Fr X A B X L A F rP B Type et A Typep FIGURE 6 9 R alisabilit tendue Prop x r P pour P Type R P t R P P B Type et t A Prop R PT R P L T P B Typeet T A Typep R x AJP R P P B Type et A Prop R X AJP X L A R P P B Type et A Typep FIGURE 6 10 R alisabilit tendue Prop R P pour P B Type L Prop Prop L X X variable de type B Typep ou B Prop L x A B a E A L B B Type ou B Prop et A Set L X A B X E A X X r A L B B Typep ou B Prop et A Type L x A B a L A L B B Typep ou B Prop et A Typep L x A B a L A L B B Typep ou B Prop et A Prop L P t L P E t P B Typep ett A Set L PT L P E T R T P B Typep et T A Type L PT L P L T P B Typep ou P B Prop et T A Typep L PT L P L T P B Typep ou P B Prop et T A Prop L x AJP z
71. E A JL P P B Typep et A Set L X AJP X E A X X r AJL P P B Typep et A Type L X AJP X L A L P P B Typep ou P B Prop et A Typep L X AJP X L A L P P B Typep ou P B Prop et A Prop FIGURE 6 11 R alisabilit tendue Prop L P 7 f vrier 2014 83 Le terme extrait de list est juste la d finition usuelle des listes polymorphes La propri t R list a pour type A Set A A Prop A Prop Prop et est d finie par R list A Set A A Prop P A Prop l E 1ist X Set X X Prop iXX r gt f A X gt X a A A a gt P a gt x X X x gt X f a x X UX x f On aurait pu choisir une autre notion d extraction du contenu logique L A d une proposition A Par exemple on aurait pu compl tement ignorer les d pendances par rapport aux preuves logiques en modifiant la d finition comme suit L x A B L B B Typep et A Prop L Pt L P P B Typebett A Prop L z AJP L P P B Typep et A Prop Dans un tel mod le la propri t PI A Prop p q A P A gt Prop P p gt P q qui dit que deux preuves dans un m me type Prop sont gales aurait t vraie c est dire que L PI qui se r duit a A Prop p q A P Prop P gt P est d montrable Prop est inclus dans Set Les r les de Prop et Set sont dissym triques du fait de l interpr ta tion de r alisabilit
72. MES an gegen e Boe koa te HEE dde dd us oe oi Roa de 5 4 Preuves par r flexion 5 4 1 Utilisation de preuves de d cidabilit 5 4 2 Utilisation d une structure abstraite 5 4 3 Un exemple en Coq l associativit de l addition sur les entiers naturels Extraction de programmes et r alisabilit 6 1 Interpr tation constructive des preuves 6 1 1 Logique classique versus logique intuitionniste 6 1 2 Constructivit du Calcul des Constructions Inductives 6 1 3 Les limites de l isomorphisme de Curry Howard 6 2 R alisabilit msia Lo met ds a fe Le ut a iQ Un BEM 6 2 1 Principes g n raux 6 2 2 Diff rentes notions de r alisabilit 6 3 R alisabilit dans le Calcul des Constructions 6 3 1 Oubli des types d pendants 6 3 2 Distinction entre Prop et Set 6 3 3 Autres m thodes d analyse 6 4 L extraction en pratique Preuve de programmes fonctionnels hl M thode directe s r ia paie wia we de de ef ek ee dr eo ee er 7 1 1 Cas des fonctions partielles 7 1 2 Cas des fonctions non structurellement r cursives 7 2 Utilisation
73. Master Parisien de Recherche en Informatique 2009 10 cours 2 7 2 Assistants de preuve Christine Paulin Mohring Benjamin Werner Bruno Barras Hugo Herbelin Jean Christophe Filli tre Claude March Table des mati res 1 2 Introduction au Calcul des Constructions Inductives LL Motivations 22 0 5 3 en wen pu ee be num ee ee ae a sun 1 2 Quelques rappels sur les th ories de types 1 3 Un premier contact avec Coq Curry Howard en action 1 3 1 Syntaxe de base du formalisme 1 3 2 V rification et inf rence de types 1 3 3 Deux tactiques de base 1 4 Les Entiers Naturels dans CCI LA D finition oo eins te ay te Dates a Matte Ae So SA en de nn Bat 1 4 2 Syntaxe alternative 1 4 3 Fonctions sur les entiers 1 44 Calculer pour raisonner 1 4 5 Le sch ma de r currence des entiers naturels 1 4 6 Une preuve par r currence 1 5 D autres types de donn es courants 1 5 1 Listes d nti rs 444 28 e nra eb Be ka ae OE eR Ba end 1 5 2 Listes param tr es s 1 5 3 Types somme et produit 1 6 Types inductifs plus complexes LOT
74. Nous commen ons par poser en axiome la d cidabilit de l galit sur l ensemble des noms et nous prouvons la d cidabilit de l galit sur l ensemble des sortes Coq lt Parameter eq_name_dec forall n m name n m n lt gt m Coq lt Lemma eq_sort_dec forall s s sort s s s lt gt s Coq lt decide equality Coq lt Defined 7 f vrier 2014 32 Nous pouvons d finir maintenant l op ration update de mise jour de la m moire qui se fait dans une section introduisant le nom de la variable x la valeur affecter cette variable v et la m moire m La sorte de la valeur est localement nomm e s Coq lt Section Update Coq lt Variable x name Coq lt Variable v semval Coq lt Variable mem memory Coq lt Let s sort_val v Coq lt Definition update memory Coq lt fun m name s sort gt Coq lt ifdec eq_sort_dec s s ifdec eq_name_dec x m v mem m s Coq lt mem m s On montre ensuite les propri t s de base de cette fonction Coq lt Theorem update_eq v update x s Coq lt Theorem update_diff_name Coq lt forall m name s sort x lt gt m gt mem m s update m gs Coq lt Theorem update_diff_sort Coq lt forall m name s sort s lt gt s gt mem m s update ms Apr s avoir prouv les lemmes la section peut tre referm e les constructions sont alors para m tr es par z v
75. Par contre ZX Type X repr sente le type des types non vides et sera bien typ de type Type Finalement dans un syst me avec Set pr dicatif le type XX Set X est forc ment de type Type alors qu il peut tre de type Set si cette sorte est impr dicative R gle d introduction Il y a une r gle d introduction par constructeur donc pas de r gle d introduction pour le type inductif sans constructeur la pr condition est juste la bonne formation des types de construc teurs T nom AF Cm s mMEl p s sorte de l arit A Pic n Cys 3 2 3 Sch mas d limination Les r gles d introduction nous disent comment former des objets dans une d finition inductive Les r gles d limination indiquent comment utiliser un objet x nom w1 w Il y a plusieurs mani res d exprimer cette propri t Le sch ma d limination minimal L interpr tation usuelle des d finitions inductives est que les valeurs objets clos normaux dans une instance de la d finition inductive sont exactement ceux form s partir des construc teurs Donc si on a un objet x dans la d finition inductive nom w1 u et que l on veut montrer une propri t il suffit de regarder les cas o co T1 Zn avec x quelconque du type appropri Il suffit donc de montrer pour chaque m V x CJ re Ce u1 u tl ltl Com zt z C Cependant faire intervenir des n uplets et l galit qui ne sont pas des notions prim
76. T sinon La r gle de conversion est remplac e en cons quence par CEST TET is TCA Pet 3 Typiquement il suffit de prendre Univ VA Type A A Prop A Prop 7 f vrier 2014 115 CC correspond la partie sans inductifs et sans Set du Calcul des Constructions Inductives 4 9 2 1 Encodage de l arithm tique Dans CC on peut d finir l ensemble des entiers naturels au niveau Type Nat Type VX Type X gt X gt X X 0 Nat AX fa a s Nat gt Nat nX fa nX f fa puis on peut d finir le pr dicat caract ristique des entiers naturels par IsNat An Nat VP Nat gt Prop P 0 gt Vm Nat P m gt P s m gt P n On peut alors prouver que 0 4 s n et que s est injectif sur tout entier de ZsNat ce qui donne Varithm tique de Peano Ainsi CC avec juste un niveau suppl mentaire de Type contient l arithm tique 9 2 2 Encodage de la th orie des ensembles de Zermelo En utilisant un codage des ensembles sous forme de graphe point Miquel Miq01 a pu plonger la th orie des ensembles de Zermelo qui est beaucoup plus faible que ZF dans CC avec trois niveaux de Type 9 2 3 Puissance logique Nous allons faire une analyse de la force logique de CC en termes ensemblistes c est dire en termes de profondeur d imbrication des ensembles que l on peut construire dans ECC On vient de voir que Type contient l ensemble des entiers naturels w ce qui c
77. _introl A gt or AB or_intror B gt or A B En normalisant cette preuve on obtient soit un terme or_introl a avec a clos de type A et donc A est prouvable soit or_intror b avec b clos de type B et donc B est prouvable De m me la d finition inductive de 3x A P x est Inductive ex A Set P A gt Set Set ex_intro forall x A P x gt ex AP Une preuve normale close de ex A P est de la forme ex_intro t p avec t terme clos de type A et p une preuve de P t Si on a une preuve close de Va A dy B P x y alors il existe un terme F du type correspondant Pour tout terme clos a de type A on peut appliquer F a ce qui nous donne un terme clos de type Jy B P a y que l on peut normaliser ce qui nous donne un terme de la forme ex_intro t p avec t terme clos de type B et p une preuve de P at Ily a donc une fonction r cursive f qui transforme a en t et telle que P a f a est montrable pour tout a Cependant cette m thode ne nous dit pas si f peut tre repr sent e dans le langage du syst me ni si la formule Vx A P x f x est d montrable Le m me raisonnement s applique montrer que s il existe une preuve de Va A P x V P z alors il existe un pr dicat r cursif p tel que p a true si et seulement si P a est d montrable et p a false si et seulement si P a est d montrable 6 1 3 Les limites de l isomorphisme de Curry Howard L isomorphisme de Curry Ho
78. a liste M me si on le souhaite les m thodes reposant sur la r alisabilit ne permettent pas ais ment de supprimer cette composante Pour r gler ce probl me on peut d placer les marques des arit s vers les quantifications On introduit une quantification logique Vx A B avec E Vz A B E B et frVr AB Vr AfrB De tels syst mes ont t tudi s par Takayama Tak91 Hayashi Une autre possibilit explor e plus r cemment est de s appuyer sur des m thodes d analyse de code mort Ces techniques ont t tudi es par Berardi Ber96 Boerio BB95 Damiani et Prost DP98 7 f vrier 2014 85 L extraction a lieu a posteriori le terme initial et le terme dans lequel on a retir des parties de code mort sont prouvablement gaux pour une galit extensionnelle Berardi utilise une propri t g n rale qui dit que si deux termes du calcul simplement typ ont le m me type et que l un est obtenu par lagage de certains sous termes de l autre alors les deux termes sont extensionnellement gaux Une des difficult s est qu une m me constante peut appara tre plusieurs endroits avec des contenus calculatoires diff rents d o l id e d utiliser du sous typage ou des types conjonctifs pour prendre en compte ce polymorphisme 6 4 L extraction en pratique Le m canisme d extraction de Coq implante la fonction d extraction E _ Il se pr sente sous la forme d une commande Extraction qu
79. a r alisabilit modifi e d crite dans la figure 6 2 Simplement la condition pour qu un programme t r alise une formule P est simplement que t r P et ne comporte plus de condition de bon typage de t Pour assurer la terminaison il sera n cessaire que la formule montrer explicite cette condi tion de terminaison Par exemple l interpr tation du pr dicat de base x nat pourra tre telle que l existence d une preuve de t nat assure que t est normalisable Une telle notion de r alisabilit est utilis e dans le syst me AF de J L Krivine Les formules utilis es pour garantir la terminaison des programmes ne permettent de garantir le calcul des valeurs que dans une strat gie paresseuse R alisabilit et ordre sup rieur Lorsque la logique manipule des variables du second ordre on ne sait pas a priori par quelle formule cette variable sera instanci e On r alise donc cette variable par un pr dicat unaire arbitraire xrVX A VPx xr A EEX Pia Formules auto r alis es Les formules auto r alis es sont des formules pour lesquelles on conna t a priori une r alisation Plus formellement une formule P est auto r alis e s il existe un objet t tel que si P est r alisable alors t r P est v rifi Les formules de Harrop sont des formules auto r alis es 6 3 R alisabilit dans le Calcul des Constructions Par rapport l interpr tation des preuves comme programmes par l isomorphisme de Curry Howard
80. ad hoc et des conditions de compatibilit 3 4 3 R ductions g n ralis es Les types inductifs de Coq permettent de d finir ais ment une addition sur les entiers qui v rifie les axiomes de Peano 0 x x et S y a S x y comme des r gles de conversion Par contre la propri t x 0 x ou l associativit de l addition sont prouvables mais ne sont pas des conversions et doivent donc tre trait s manuellement alors que les syst mes de r criture savent parfaitement traiter ses galit s de mani re automatique Pour pallier cette difficult on tudie depuis quelques ann es des syst mes qui combinent la r criture et le lambda calcul typ Une difficult est de garantir la confluence et terminaison du syst me r sultant Pour cela il faut bien entendu restreindre la forme des r critures applicables Les travaux r cents de F Blanqui dans la lign e de ceux de J P Jouannaud et M Okada proposent un cadre qui capture un tr s large sous ensemble des d finitions inductives de Coq et permet de d finir des fonctions par des syst mes de r criture v rifiant un certain sch ma De mani re alternative J P Jouannaud A Rubio et D Walukiewicz Chrzaszcz proposent un ordre RPO applicable aux termes du Calcul des Constructions qui garantit la pr servation par ajout de r gles de r criture Chapitre 4 Types coinductifs dans Coq 4 1 Introduction 4 1 1 Types concrets On appellera type concret un type I sp
81. al Opn o f g Nat semop o nf ng On peut maintenant noncer le th or me qui dit que toute expression correctement typ e admet une valeur Coq lt Theorem expr_val_cor forall E expr s sort Coq lt exprcorrect s E gt exists v semval exprval E v La preuve par r currence n cessite un lemme plus fort qui dit que la valeur calcul e est compatible avec la sorte de l expression Coq lt Lemma expr_val_cor_dom forall E expr s sort Coq lt exprcorrect s E gt exists2 v semval compat s v amp exprval E v 7 f vrier 2014 28 Repr sentation de la m moire l aide de types d pendants Le traitement de la relation entre la sorte de l expression et le domaine de la valeur s mantique est lourd On peut profiter de l expressivit du langage de sp cification de Coq pour utiliser d autres formalisations On construit une famille d pendante sval dont le type est sort Set qui la sorte Sbool associe le type bool et Snat associe le type nat Le domaine s mantique semval pourrait tre repr sent par un couple form d une sorte s et d un objet de type sval s ceci revient juste coder une somme disjointe explicitement l aide d un s lecteur s et d un champ dont le type varie suivant le s lecteur On peut tirer partie de cette repr sentation pour simplifier la formalisation en rendant im plicite dans la d finition de la m moire la notion de compatibilit Coq lt Definit
82. al du langage et la paresse de l valuation pour construire des structures infinies En reprenant les quations d finissant les propri t s des streams d finies par coit ration ou cor cursion on voit que ces streams auraient pu tre directement d finies par les quations r cursives 4 1 ou 4 2 Cependant dans notre approche nous avons suppos priori que toute liste tait infinie et en particulier poss dait un objet de t te Il ne sera donc pas possible d accepter n importe quelle d finition de point fixe L exemple classique de liste probl matique est la fonction qui filtre une liste infinie en ne gardant que les objets qui v rifient une condition P Dans un langage de programmation on crirait comme corps de la d finition de filtre P s Cases s of Cons al if P a then Cons a filtre P l else filtre P end Cette d finition n est pas correcte sans information suppl mentaire en effet si la liste ne pos s de plus partir d un certain rang d l ments qui v rifie P alors la liste filtre P s n est pas infinie Renvoyer le r sultat dans le type des listes finies ou infinies ne solutionne pas le probl me puisqu on ne sais pas d cider si la liste s arr te ou pas en ayant examin un fragment initial Le m me probl me se pose d ailleurs si les listes infinies sont repr sent es par des fonctions totales Pour contourner cette difficult on peut adopter plusieurs approches comme par exemple int
83. alement fournir quelques propri t s sur eq relation d quivalence et 1t relation d ordre incompatible avec eq sans lesquelles les fonctions sur les arbres binaires de recherche ne peuvent tre correctes Coq lt Axiom eq_refl forall x eq x x Coq lt Axiom eq_sym forall x y eq x y gt eq y x Coq lt Axiom eq_trans forall x y z eq x y gt eq y z gt eq x z Coq lt Coq lt Axiom lt_trans forall x y z 1t x y gt lt y z gt lt x 2 Coq lt Axiom 1t_not_eq forall x y lt x y gt eq x y Enfin on peut ajouter la signature des commandes Hint pour la tactique auto et elles seront ainsi disponibles automatiquement dans le corps du foncteur Coq lt Hint Immediate eq_sym Coq lt Hint Resolve eq_refl eq_trans lt_not_eq lt_trans Coq lt End OrderedType On peut alors crire notre biblioth que d ensembles sous la forme d un foncteur prenant un argument X de type OrderedType Module ABR X OrderedType Inductive tree Set Empty Node tree gt X t gt tree gt tree Fixpoint mem x X t s tree struct s bool Inductive In x X t tree gt Prop Hint Constructors In Inductive bst tree gt Prop bst_empty bst Empty bst_node forall x l r tree bst 1 gt bst r gt forall y In y 1 gt X 1t y x gt forall y In y r gt X lt x y gt bst Node 1 x r etc 7 f vrier 20
84. ans modifier la th orie de base en particulier sans risque de la rendre incoh rente Par contre elle introduit une distance entre ce que l utilisateur crit et ce que la machine prouve Techniquement cela complexifie l interaction avec l utilisateur affichage d tection des erreurs Un second aspect de l architecture de Coq est le m canisme de construction de preuves qui se fait l aide de tactiques Partant d une propri t montrer on cherche construire une preuve dans le cas de Coq un terme de ce type Cela se fait l aide de tactiques qui travaillent sur un arbre de preuve dont la racine correspond la propri t P tablir et les feuilles un ensemble de propri t s suffisantes pour prouver P Les tactiques peuvent implanter des proc dures arbitrairement complexes Dans Coq lorsque l arbre n a plus de feuilles un terme de preuve est reconstruit puis v rifi par le noyau On peut imaginer diff rents langages pour exprimer les tapes de preuve 5 2 Crit res de classification Il est d usage de classer les syst mes d aide ou assistants la d monstration selon les crit res suivants Bar81 Wieb Wieal Crit re de de Bruijn Logique ou m ta logique Principe de Poincar 65 7 f vrier 2014 66 La repr sentation des preuves D veloppement interactif des preuves Degr d automatisation Dans la suite on d crira ces diff rents crit res et on analysera
85. apport Technique 0221 INRIA May 1998 7 f vrier 2014 123 Gir72 Jean Yves Girard Interpr tation fonctionnelle et limination des coupures de Varithm tique d ordre sup rieur 1972 Gro Computer Assisted Reasoning Group The PLASTIC proof assistant http www dur ac uk CARG plastic html Her05 Hugo Herbelin On the degeneracy of sigma types in presence of computatio nal classical logic In Pawel Urzyczyn editor Seventh International Conference TLCA 05 Nara Japan April 2005 Proceedings volume 3461 of LNCS pages 209 220 Springer 2005 HS98 Martin Hofmann and Thomas Streicher The groupoid interpretation of type theory In Proceedings of the meeting Twenty five years of constructive type theory Oxford University Press 1998 Kle45 Stephen C Kleene On the interpretation of intuitionistic number theory The Journal of Symbolic Logic 10 109 124 1945 Kle98 Thomas Kleymann Hoare Logic and VDM Machine Checked Soundness and Completeness Proofs PhD thesis Edinburgh LFCS Technical Report ECS LFCS 98 392 1998 Ler00 Xavier Leroy A modular module system Journal of Functional Programming 10 3 269 303 2000 Let03a Pierre Letouzey A New Extraction for Coq In Herman Geuvers and Freek Wiedijk editors Types for Proofs and Programs Second International Workshop TYPES 2002 Berg en Dal The Netherlands April 24 28 2002 volume 2646 of Lecture Notes in Computer Science Springer Verlag 2003
86. ariable de type t A ct A nat xr z 0AA A atomique t AAB t A xt B rrAAB fst x r A A snd x r B t A B t 4 t B fr A B Vz t A xr A f x r B ct dy 0 B o xt B xr Jy o B snd x r Bly fst x t Vy 0 B o gt t B f rYz o B Vic f x r B FIGURE 6 2 R alisabilit modifi e Une formule A est r alisable s il existe un terme t de type t A tel que t r A soit prouvable Une mani re alternative de pr senter la r alisabilit modifi e est de prendre des suites finies de programmes pour les r alisations on vite ainsi l utilisation de produits on peut de plus liminer les r alisations des formules de Harrop Ind pendance des pr misses La r alisabilit modifi e sert justifier le principe d ind pen dance des pr misses A Jz o P x gt Jx o mA gt P x Principe de Markov La r alisabilit modifi e sert justifier que le principe de Markov n est pas d montrable en logique intuitionniste Vz nat P x V PO ditnat PE gt Jx nat P x valuation Dans le cas de la r alisabilit modifi e les r alisations sont des programmes typ s fortement normalisables 7 f vrier 2014 79 R alisabilit modifi e non typ e La r alisabilit modifi e non typ e se place dans une logique o la quantification porte sur tous les objets qu ils repr sentent ou non des programmes qui terminent La d finition est identique celle de l
87. ase est trivial Coq lt induction n 2 subgoals 0 0 0 subgoal 2 is Sn Sn 0 Coq lt reflexivity 1 subgoal n nat 7 f vrier 2014 16 Pour le cas par r currence on peut proc der une tape de r duction Coq lt simpl 1 subgoal Il suffit alors d utiliser Vhypoth se de r currence pour remplacer dans le but courant p 0 par p cela peut se faire par Coq lt rewrite lt IHn 1 subgoal Coq lt reflexivity No more subgoals 1 5 D autres types de donn es courants Comme en ML le principe de d finitions inductives permet la construction de types de donn es plus complexes que les entiers Suivent quelques exemples courants 1 5 1 Listes d entiers Il est sans doute inutile de rappeler la structure des listes avec leurs deux constructeurs nil et cons La commande d finissant les listes d entiers naturels est bien s r Coq lt Inductive list Set Coq lt nil list Coq lt cons nat gt list gt list Une premi re remarque marginale est que contrairement ML les constructeurs peuvent avoir plusieurs arguments ici cons est curryfi 1 5 2 Listes param tr es Il est pr f rable de remplacer la d finition pr c dente par une autre o le type des l ments des listes est un param tre La bonne d finition des listes est Coq lt Inductive list A Set Set Coq lt nil list A Coq lt cons A gt list A gt list A 7 f vrier 2014 17 Il
88. atch m with Coq lt 0 gt ack n S 0 Coq lt S m gt ack n aux m Coq lt end Coq lt end 1 4 4 Calculer pour raisonner Donnons un exemple simple et classique d utilisation de la r gle de conversion il s agit de prouver 2 2 4 o est la notation infixe de Coq pour plus et 2 et 4 les repr sentations de S S 0 et S S S S O Ici cette proposition s nonce Coq lt Lemma deux_et_deux 2 2 4 1 subgoal Il suffit d observer que le terme correspondant 2 2 se r duit effectivement vers 4 et donc que la proposition est logiquement identifi e 4 4 Coq lt simpl 1 subgoal Coq lt reflexivity No more subgoals Remarquons que la tactique simpl qui proc de donc la 6 normalisation du but courant ne construit pas de terme preuve Cela est d la forme de la r gle de conversion qui rappelons le est Trt A TRB s A B Conv Trt B On voit bien que les termes preuves de la conclusion et de la pr misse principale sont identiques En cons quence l on pourrait dans l exemple pr c dent se passer compl tement de simpl et utiliser juste reflexivity qui construit la preuve correspondant la r flexivit de l galit La d finition exacte du pr dicat d galit sera d taill e plus tard 7 f vrier 2014 15 Exercice 1 Prouver partir de l la commutativit de l addition 1 4 5 Le sch ma de r currence des entiers naturels Le fait qu
89. cas les param tres 21 Pj z Pk sont plus sp cifiquement appel es param tres de famille On verra aussi certains locuteurs utiliser les termes arguments contraintes ou param tres r els pour les variables a A1 ag Aj Co1 co sont les noms des p constructeurs de la d claration on peut avoir p 0 On notera Cm V x Cl x m Cm nom z1 zp th t et ce terme est appel le type du m me constructeur de la d claration nom On appellera type d argument de constructeur les types C7 On appelle arit du constructeur le nombre Nnm d arguments du constructeur Dans une application nom u1 Uk sex i les termes u1 Uz sont appel s arguments de famille et les termes t t sont appel s soit index soit arguments de pr dicat D claration r cursive On dira que la d claration est r cursive si nom appara t dans l un des types d argument de constructeur Cp On dira qu elle est non r cursive sinon 36 7 f vrier 2014 37 3 1 2 Forme abstraite Une d claration inductive dans Coq introduit de nouveaux noms Sur le plan th orique il est parfois plus commode d avoir une repr sentation abstraite des d finitions inductives On ne garde alors que les l ments essentiels l arit A de la d claration inductive et les types des constructeurs Cm Dans le cas o il n y a pas de param tre une notation possible pour la d finition inductive est Ind nom A C1 Cp
90. cessaire pour notre analyse Autrement dit on se restreint un mod le ayant le grain du mod le bool en de Fi 2 qui sont incidemment aussi des objets du niveau Type 112 7 f vrier 2014 113 La r gle de conversion est valid e par le mod le et on a F t A qui implique A true d o la coh rence du CC puisque VA Prop A false Le mod le est localement fini et A true est d cidable puisque les quantifications ne portent que sur des espaces fonctionnels engendr s partir de B qui est fini et d un nombre fini de construction par produit En particulier la coh rence de CC est prouvable dans l arithm tique Dans ce mod le tous les entiers dans le type VA A A A A sont identifi s On ne peut donc prouver 0 1 Les axiomes de Peano ne sont donc pas d rivables en accord avec l existence d une preuve de coh rence dans l arithm tique Question ouverte compl tion de Fi et plus g n ralement de CC dans son mod le bool en standard vis vis du mod le bool en Quels axiomes ajouter pour obtenir A true H A candidats VA Prop A True V A False compl tude propositionnelle et Vf g Va T U Vu T fu uu gu f g extensionnalit Remarque 1 l indiscernabilit des preuves proof irrelevance la compl tude proposition nelle et le tiers exclu sont tous les trois valid s par le mod le bool en Remarque 2 on peut typiquement repr senter false e
91. claire dans l impl mentation Une articulation entre calcul et d duction qui permet des preuves particuli rement concises dans certains cas depuis l exemple 2 2 4 ci apr s aux preuves par r flexion comme la tactique ring 1 3 Un premier contact avec Coq Curry Howard en action Le syst me Coq est un syst me de traitement de preuves pour une version pr dicative du Calcul des Constructions Inductives Les composantes essentielles du syst me Coq sont un noyau de v rification de types et de construction d environnements bien typ s un langage de d veloppement de th ories math matiques Gallina un outillage d aide la construction interactive de preuves par des tactiques de preuve 7 f vrier 2014 8 1 3 1 Syntaxe de base du formalisme Le formalisme implant par Coq sera donc couramment appel CCI Il s agit pour l essentiel d une extension du Calcul de Constructions CC trait en tronc commun Il nous faut d s maintenant signaler quelques diff rences de notations avec la syntaxe employ e jusqu ici Tout d abord Coq est con u pour pouvoir tre utilis par une interface en mode texte ASCII ou Unicode Les notations de Coq pour Ax A t et Ilx A B sont La abstraction est not e fun x A gt t Cela d signe la fonction qui un objet x de type A associe l objet t La quantification universelle est not e forall x A B Cet objet est le type des fonctions qui un ob
92. classique C est l origine un r sultat de Diaconescu pour la th orie des ensembles qui a t adapt la th orie des types par Lacas et Werner Dia75 LW99 Extensionnalit fonctionnelle L extensionnalit des fonctions exprime pour deux types A et B ou plus g n ralement pour un produit fonctionnel Vz A B x que deux fonctions ayant le m me graphe d entr es sorties sont gales Vf g Vx A B x Va A f x g x gt f g Typiquement l extensionnalit fonctionnelle implique que l addition sur les entiers d finie par r currence sur son premier argument est gale l addition d finie par r currence sur son se cond argument L extensionnalit n est pas prouvable elle n est pas valid e par le mod le de r alisabilit qui est intentionnel par ailleurs une inspection des formes normales possibles d une ventuelle preuve devraient permettre d affirmer l absence d une telle preuve Un mod le ensembliste validerait l extensionnalit fonctionnelle Donner un mod le ensem bliste du Calcul des Constructions Inductives avec Set pr dicatif est faisable la condition de retirer la r gle de sous typage Prop C Type En pr sence de Prop C Type il est vraisemblable que le mod le ensembliste fonctionne mais il reste des obstacles techniques Une question ouverte reste donc la compatibilit de l extension nalit fonctionnelle avec le sous typage Prop C Type Condition de gar
93. construites interactivement par des tactiques Pour les constructions par point fixe une tactique t Cofix existe Elle introduit dans le but une hypo th se identique la propri t prouver mais qui ne pourra tre utilis e que de mani re gard e V rifier que la condition de garde est toujours satisfaite apr s chaque application de tactique est trop coutetix aussi cette v rification n est faite qu au moment de la sauvegarde de la preuve finale ou bien la demande explicite de l utilisateur Exemples de preuves par point fixe Nou pouvons montrer que l galite sur les streams est r flexive sym trique et transitive Coq lt Lemma EqStreamRefl forall x Stream EqStream x x Coq lt cofix constructor trivial No more subgoals Coq lt Lemma EqStreamSym forall x y Stream A EqStream x y gt EqStream y x Coq lt cofix intros 1 subgoal EqStreamSym forall x y Stream A EqStream x y gt EqStream y x x Stream A y Stream A H EqStream x y EqStream y x Coq lt inversion_clear H constructor auto No more subgoals Coq lt Lemma EqStreamTrans Coq lt forall x y z Stream A EqStream x y gt EqStream y z gt EqStream x z Coq lt cofix intros 1 subgoal EqStreamTrans forall x y z Stream A EqStream x y gt EqStream y z gt EqStream x z x Stream A y Stream A Z Stream A H EqStream x y HO EqStream y z 7 f vrier 2014 63 EqStream x z Coq lt inv
94. de Sans condition de garde on peut directement d river l absurde Fixpoint Paradox u unit False Paradox u Condition de positivit Sans condition de positivit on peut facilement d river l absurde Inductive Prop intro A gt False gt A Definition Paradox False fun H A gt False gt H intro H limination forte sur un ensemble large Sans restriction de l limination forte sur un inductif large on pourrait encapsuler le type des propositions un type large comme une proposition un petit type et le red capsuler volont sans perte d information Inductive prop Prop down Prop gt prop Definition up p prop Prop let A p in A Theorem iso forall A Prop up down A A Proof reflexivity Qed La quantification impr dicative dans Type du syst me U deviendrait ainsi simulable dans le CCI par une simple quantification impr dicative dans Prop rendant possible la d rivation d un paradoxe dans le CCI 7 f vrier 2014 120 Condition de positivit stricte La positivit large n est pas suffisante pour garantir l absence de paradoxe De fait autoriser le type non strictement positif suivant Inductive T Type I T gt Prop gt Prop gt T conduit un paradoxe L id e extraite de Coquand Paulin Mohring CPM90 est la suivante Tout objet de type peut s interpr ter comme un ensemble singleton de type Prop en posant s4
95. de ne pas perdre la normalisation forte Un point fixe est une forme normale Coq lt Eval compute in zeros cofix zeros Stream nat Cons 0 zeros Stream nat Coq lt Eval compute in from 0 cofix from n nat Stream nat Cons n from S n 0 Stream nat Si f est d finie comme le co fixpoint de la fonctionnelle F par f Ax gt F f x alors la r duction f x gt F f x ne se produira que si f se trouve en position de t te dans une d finition par cas La r duction a donc pour forme match f x with end match F f x with end La preuve de normalisation forte peut se trouver dans Gim96b Cette propri t de r duction est suffisante pour calculer n importe quelle valeur d une stream Coq lt Eval compute in head from 0 0 nat Coq lt Eval compute in tail from 1 cofix from n nat Stream nat Cons n from S n 2 Stream nat Coq lt Eval compute in nth 6 from 0 6 nat En pratique il est possible de faire une preuve de f x F f x dans laquelle l galit est celle de Leibniz alors que f x et F f x ne sont pas directement convertibles Pour cela il faut passer par une tape interm diaire analogue une 7 expansion que nous allons expliquer maintenant 7 f vrier 2014 61 Soit J un type inductif avec n constructeurs c1 cn Il est facile de montrer par cas sur x la propri t suivante que nous appelerons 7 x matc
96. des s mantiques statiques op rationnelles naturelles et axiomatiques pour ce langage Toutes sont repr sent es en s mantique naturelle par la d finition d une relation entre un programme et des valeurs Cette relation sera d crite l aide des r gles d inf rence 2 2 1 S mantique statique Il s agit de d terminer de mani re statique sans l ex cuter qu un programme est bien form Ici il faut v rifier que dans les expressions conditionnelles ou de boucle les tests sont faits sur des expressions bool ennes Cela nous am ne d finir une relation de typage sur les expressions Les deux valeurs seront les deux sortes nat et bool La relation de typage E s est d finie par les axiomes et r gles de la figure 2 3 X s true bool false bool n nat E bool E bool E nat Ei nat E gt nat E xor E bool null E bool Ey op E gt nat FIGURE 2 3 S mantique statique des expressions Pour les commandes on d finit la relation ok par les r gles de la figure 2 4 7 f vrier 2014 23 skip wok E s Ci ok C2 ok X E ok Ci C2 ok E bool Ci ok C2 ok E bool C ok if E then C else Cy ok while E do C ok FIGURE 2 4 S mantique statique des commandes 2 2 2 S mantique op rationnelle La s mantique op rationnelle d finit le programme comme une transformation de l tat de la m moire Cette m moire associe chaque variable et sorte une valeur qui sera une constante ent
97. dont les branches sont potentiellement infinies I ne s agit pas alors de se donner un principe de r currence pour raisonner sur ces objets mais au contraire des op rateurs pour construire de tels objets infinis en effet l application des seuls constructeurs ne construira que des objets finis 4 2 Exemple des listes infinies L exemple de base qui est donn pour de tels types infinis est celui des listes Coq lt Variable Set 1 on pourra trouver la d finition de Streams dans la biblioth que theories Lists 54 7 f vrier 2014 55 Coq lt CoInductive ListI Set Nill ListI ConsI A gt ListI gt ListI Coq lt CoInductive Stream Set Cons A gt Stream gt Stream Dans le cas de ListI les listes peuvent tre finies ou infinies dans le cas de Stream il n y a que des listes infinies dans ce type Exercice Montrer que si on d finit le type Stream de mani re inductive et pas coinductive alors ce type est vide c est dire que l on a une preuve de Stream False 4 2 1 Principe de destructivit Il faut garder l esprit que l on cherche pr server la propri t des types concrets que chaque terme clos se r duira vers un terme qui commence par un constructeur Dans le cas des streams cela revient dire que tout terme de type Stream est gal Cons a l pour un certain a et l Stream ce qui peut s crire Coq lt Lemma Stream_destr forall P Stream gt Set
98. dre ce probl me est de renforcer la propri t prouver en Viti 2 bool neq 2 z2 gt ay b gt T2 b2 gt P puis d utiliser l limination standard et de simplifier les galit s Certaines correspondent des hypoth ses absurdes d autres vont donner lieu des simplifications on obtiendra de nouvelles galit s qui pourront tre propag es Tactiques d inversion Le travail d crit ci dessus est partiellement automatis par les tac tiques d inversion Cependant la preuve engendr e est loin d tre atomique Il faut donc viter autant que possible d avoir recours aux sch mas d inversion Pour cela il est utile de mettre ex plicitement en param tre tout argument qui n est pas instanci dans les constructeurs juste une variable li e L ordre dans lequel on r alise les liminations et des g n ralisations appropri es permettent parfois d viter l utilisation de l inversion Finalement il peut tre utile d engendrer des principes d limination ad hoc pour certaines instances de d finition inductive ce qui permet d viter l utilisation multiple de l inversion galit On suppose fix un type Set L galit inductive est d finie par Inductive eq x A Prop refl eq x x On note x y le terme eq x y Le sch ma d limination exprime que toute preuve de x y est de la forme ref1 x il a la forme suivante e x y P Vy A x y s p P
99. duit dans la logique On pourrait ainsi imaginer d tendre la r gle de conversion un quotient relativement une valuation non d terministe des programmes C est ce que se propose de faire les extensions du calcul des constructions avec des r gles de r criture Toutefois il existe une mani re de ramener toute proc dure de simplification d cidable une application de la r gle de conversion et une tape de r criture C est le m canisme de r flexion La repr sentation des preuves Un syst me de preuve peut soit valider une preuve sans garder aucune trace de la v rification autre que le source de la preuve C est le cas de PVS et ACL2 Ceci est forc ment le cas lorsqu aucun noyau ne v rifie les preuves Toutefois un syst me peut v rifier le crit re de de Bruijn et ne pas garder de trace des preuves C est le cas de 7 f vrier 2014 67 HOL qui d duit de nouveaux th or mes partir de r gles d inf rence bien d finies sans garder de trace de quelles r gles ont t appliqu es pour valider tel ou tel th or me Un syst me peut valider les preuves sous la forme d un terme de preuve C est le cas de Coq et Isabelle Le d veloppement interactif des preuves Tous les syst mes n offrent pas un m canisme de d veloppement interactif de preuves Par exemple Mizar et ACL2 ne peuvent que v rifier une preuve dans sa globalit En cas de non validation l utilisateur doit apporter des modifica
100. e velopment Texts in Theoretical Computer Science An EATCS Series Springer Verlag 2004 http www labri fr Perso casteran CogArt index html Michael J Beeson Foundations of Constructive Mathematics Metamathematical Studies Springer Verlag 1985 Stefano Berardi Pruning simply typed lambda terms Journal of Logic and Com putation 6 5 663 681 1996 Yves Bertot A certified compiler for an imperative language Rapport de Re cherche RR 34 88 INRIA 1998 Dominique Cl ment Jo lle Despeyroux Thierry Despeyroux and Gilles Kahn A simple applicative language Mini ML Rapport de Recherche 529 INRIA May 1986 Jacek Chrzaszcz Implementing modules in the system Coq In 16th International Conference on Theorem Proving in Higher Order Logics University of Rome III September 2003 Jacek Chrzaszcz Modules in Type Theory with generative definitions PhD thesis Warsaw University and Universit Paris Sud 2003 To be defended Catarina Coquand Agda http www cs chalmers se catarina agda Thierry Coquand Une Th orie des Constructions PhD thesis Universit Paris 7 January 1985 Thierry Coquand An analysis of girard s paradox In Symposium on Logic in Computer Science Cambridge MA 1986 IEEE Computer Society Press 121 7 f vrier 2014 122 Coq94a Thierry Coquand Infinite objects in type theory In Henk Barendregt and Tobias Nipkow editors Types for Proofs and Programs volume 806 of LNCS pages 62
101. e Celle ci peuvent naturellement tre prouv es dans Coq pour obtenir alors un programme fonctionnel Coq certifi quivalent au programme de d part que Von appelle la validation Why Interpr tation fonctionnelle des types avec effets Tout type avec effets annot T P t F w Q est interpr t en un type Coq T VE P amp gt Ay 3r Q z Y r La notation P g d signe la formule P o les occurrences des variables lues 7 sont substitu es par les 7 et la notation Q y r d signe la formule Q o pour chaque variable v de w les occurrences de v sont remplac es par le y correspondant les v par le x correspondant pour chaque variable v de Fr qui n est pas dans w chaque occurrence de v est remplac e par le x correspondant et enfin result est remplac par r Il s agit l d exprimer le fait que les x d signent les anciennes valeurs des variables modifiables alors que les y d signent les nouvelles valeurs En pratique le 4 est utilis est celui dans Set not avec des accolades Par exemple le type avec effet de crediter s int gt s gt 0 unit montant montant montant s montant 0 est interpr t par le type Coq forall s Z forall montant Z forall H s gt 0 montant0 Z result unit montantO s montant Notons galement que les types de base int bool et float sont interpr t s par leurs re pr sentations math matiques Coq Z bool e
102. e la forme com x x avec com un constructeur et x une variable On peut utiliser la notation A ay Ai a A x nom ay a gt match x with co at 2 fi x1 x cop 1 P gt fm t x end Elimination non d pendante Un cas particulier souvent utilis de l limination est celui o le pr dicat P ne d pend pas de l objet limin On parle alors d limination non d pendante La r gle devient Tr a2 moma a TH P V a Ai a Aj 8 Eppes Vie CL ee Ce P tl th ce 1p T F Case P x fi fp P a1 a Codage impr dicatif Les d finitions inductives peuvent tre vues comme de nouveaux objets ajout s la th orie ou bien on peut essayer de les coder c est dire tant donn une th orie fix e et une d claration inductive de la forme 3 1 1 peut on trouver des termes nom COm et Case qui ont les types appropri s et satisfont les r gles de r duction Un des attraits des logiques d ordre sup rieur est qu elles sont assez puissantes pour coder les d finitions inductives C est d ailleurs ce qui est fait dans les syst mes HOL o les d fini tions inductives sont juste des packages plus ou moins puissants automatisant la d finition de propri t s Dans le Calcul des Constructions Pures il est possible de coder les d finitions inductives On introduit les d finitions suivantes nom A a A1 a gt VP A
103. e la version correspondant une fonction ML rendue totale avec un type option On peut de m me combiner sumor et sumbool pour sp cifier notre fonction de comparaison ternaire Coq lt Hypothesis compare forall x y x lt y x y x gt y On note que maintenant cette seule hypoth se remplace elle seule l inductif order et les deux hypoth ses compare et compare_spec Reprenons l exemple de la fonction de test d appartenance dans un arbre binaire de recherche mem On peut maintenant la sp cifier l aide d un type d pendant Coq lt Definition mem Coq lt forall x s bst s gt In x s In x s La d finition preuve commence par une induction sur s Coq lt Proof Coq lt induction s intros Coq lt s Empty Coq lt right intro h inversion_clear h Le cas s Empty est trivial Dans le cas s Node s1 z s2 il s agit de proc der par cas sur le r sultat de compare x z C est maintenant plus simple qu avec la m thode pr c dente plus besoin de faire appel au lemme compare_spec car compare x z contient sa sp cification dans son type Coq lt s Node s1 z s2 Coq lt case compare x z intro De m me chaque hypoth se de r currence sur s1 et s2 est une fonction contenant sa sp cifi cation On Vutilise le cas ch ant en lui appliquant la tactique case Le reste de la preuve est ais Note Il est possible de retrouver la fonction pure comme projecti
104. e nat est bien le plus petit type clos par ses deux constructeurs est exprim par le sch ma de r currence Il s agit d une propri t logique qui s nonce ainsi soit P un pr dicat sur les entiers pour que la proposition P n soit vraie pour tout entier n il suffit que les deux conditions suffisantes soient v rifi es P 0 est vrai pour tout entier n si P n est vraie alors P S n l est aussi Dans une logique d ordre sup rieur ce sch ma peut tre exprim comme une proposition En syntaxe Coq forall P nat gt Prop P 0 gt forall m nat P m gt P S m gt forall n nat P n De fait la d finition d un type inductif g n re automatiquement une preuve du sch ma de r currence correspondant Si le type inductif est nomm I la preuve du sch ma de r currence s appellera I_ind par exemple Coq lt Check nat_ind nat_ind forall P nat gt Prop P 0 gt forall n nat P n gt P S n gt forall n nat Pn L utilisation du sch ma de r currence en Coq se fait gr ce aux tactiques elim et induction 1 4 6 Une preuve par r currence Voici un autre exemple simple combinant le calcul et le raisonnement par r currence Il s agit de prouver une premi re tape vers la commutativit de l addition savoir Coq lt Lemma comm_0 forall n nat n n 0 1 subgoal forall n nat n n 0O Cette preuve se fait bien s r par r currence sur n le cas de b
105. e nature a t effectu e par Samuel Boutin Il s agissait du sch ma de compilation d un mini ml vers la CAM Categorical Abstract Machine tel qu il tait d crit dans l article CDDK86 Yves Bertot a tudi la preuve du compilateur d un langage imp ratif vers un langage assembleur Ber98 Des preuves de compilateurs plus cons quents ont ensuite t entreprises Delphine Ter rasse Ter92 a bauch la preuve d un compilateur Esterel Pablo Argon Arg98 a extrait le noyau du compilateur du langage Electre exprim comme l ex cution des r gles de la s man tique des quipes de recherche de Dassault et A rospatiale ont tudi la formalisation d un compilateur pour le langage Lustre tel qu il est implant dans l outil Scade une partie de ces d veloppements est disponible domme contribution au syst me Coq On trouvera galement dans les contributions des formalisations de plusieurs calculs de processus en particulier le a calcul ainsi que des mod lisations de logique temporelle 2 4 2 Logique de Hoare La formalisation de la logique de Hoare a t effectu e par Thomas Kleymann Schreiber Sch97 Kle98 dans l assistant LEGO dont le langage s apparente au Calcul des Constructions Induc tives Une formalisation dans l outil HOL a galement t r alis e par Peter Homeier l objectif principal de ces d veloppements est de justifier les propri t s fondamentales de la s mantique axiomatique comme
106. e que 7 f vrier 2014 104 programmes annot s A Coq PVS HOL light Mizar Simplify haRVey Obligations de preuves FIGURE 8 2 Approche multi prouveur de Why Le langage Why est un langage proche de Caml En particulier il n y a pas de distinction entre instruction et expression Les triplets la Hoare s applique sur des expressions et dans une post condition on peut utiliser le mot cl result pour parler du r sultat de l expression L ajout d un variant pour garantir la terminaison Le travail de l outil Why consiste produire partir d un programme annot des obligations de preuves dont la validit assure la correction du programme Avec Why ces obligations de preuves sont des formules en logique du premier ordre exprimable dans la syntaxe de diff rents d monstrateurs existants aussi bien des d monstrateurs interactifs comme Coq PVS HOL light ou Mizar que des d monstrateurs automatiques comme Simplify ou haRVey N anmoins la sortie pour Coq poss de une particularit suppl mentaire la validation qui est un programme fonctionnel Coq quivalent au programme de d part Il s agit l de l id e directrice de l approche Why un programme imp ratif peut tre traduit en un programme fonctionnel par ajout de param tre Sur l exemple de ISQRT on crirait quelque chose comme isqrt n isqrt2 n 0 1 isqrt2 n count sum if sum lt n then isqrt2 n count 1 sum 2 coun
107. e repr sentant une r alisation Une formule P dont l interpr tation est non vide sera dite r alisable L id e de base des d finitions est la suivante l absurde est interpr t par l ensemble vide A B est interpr t comme l ensemble des r alisations repr sentant des fonctions des r alisations de dans les r alisations de B AAB est interpr t comme l ensemble des r alisations repr sentant des couples form s d une r alisation de et d une r alisation de B Jx P x sera interpr t comme l ensemble des r alisations repr sentant des couples form s d un objet t et d une r alisation de P t Une fois l interpr tation d finie on montre que si une formule est prouvable alors son interpr tation est non vide et que de plus il est possible de construire par r currence sur la structure de la preuve une r alisation particuli re L int r t de cette m thode est qu elle s tend aux preuves sous contextes c est dire que si une formule est prouvable sous hypoth ses et que chaque hypoth se a une interpr tation non vide alors il en est de m me de la conclusion Une cons quence de cette propri t est que toute 7 f vrier 2014 77 formule dont l interpr tation est non vide est coh rente avec la th orie En effet si on pouvait d river l absurde partir de cette proposition alors l interpr tation de l absurde serait non vide La r alisabilit peut se
108. e utilis es pour repr senter des suites infinies par exemple des suites de rationnels permettant de repr senter des entiers Chapitre 5 Architecture des assistants a la d monstration 5 1 Architecture de Coq Le syst me Coq repose sur un noyau de v rification du Calcul des Constructions Inductives Les op rations de base de ce noyau consistent 4 ajouter une d claration variable d finition d claration inductive module dans l environnement Cela n cessite d effectuer le typage des termes en particulier de contr ler des contraintes d univers et de pouvoir tester la convertibilit de deux termes ce qui passe par des tapes de r duction Au dessus de ce noyau est construit un langage de description de haut niveau qui est compil vers le CCI Ce langage permet de laisser certaines informations implicites par exemple d uti liser des coercions entre diff rents types de donn es d utiliser les d pendances entre types pour omettre certains arguments de fonction qui seront calcul s par unification Le m canisme de d fi nition par filtrage est galement compil vers le filtrage atomique du CCI On pourrait avoir des m canismes de d finition r cursive de fonctions proches des langages de programmation et crire des termes incomplets qui n cessitent des preuves compl mentaires par exemple pour traiter agr ablement des fonctions partielles La distinction de ces deux niveaux permet une souplesse d expression s
109. ect par rapport n importe quelle d finition inductive Le second cas est plus int ressant Nous appelons type singleton un type qui n a qu un constructeur dont tous les types d arguments sont de type Prop L limination ne comporte donc qu une seule branche et on montre ais ment que si la propri t est v rifi e alors le programme extrait de cette branche est correct par rapport la propri t de la conclusion L extraction de la d finition par cas est alors d finie comme l extraction de l unique branche l l ment sur lequel se fait le Case n intervient donc pas dans le calcul On peut montrer que pour de tels types d s que l on a l limination vers Set et que ces types sont pr dicatifs alors l limination vers Type peut galement tre simul e et est donc valide 7 f vrier 2014 46 Les types conjonctions de propri t s logiques sont des types singletons bien que d finis dans Prop ils admettent une limination pour toutes les sortes il en est de m me du pr dicat d galit que nous avons d fini plus haut La condition que tous les types d arguments de constructeur sont de nature purement pro positionnelle est essentielle Un exemple de type un seul constructeur qui ne v rifie pas cette condition est un type I avec un seul constructeur c avec un argument de type bool La r gle d limination x I P I Set f Vb bool P cb Case P x f P x Sur le plan calculatoire la preuve x est ess
110. el on n introduit pas la syntaxe des formules Cette repr sentation peut permettre de raisonner rapidement sur les propri t s de pro grammes particuliers Par contre elle ne permet pas de construire des programmes ou de faire des preuves par r currence sur la structure des programmes Elle n est donc pas adapt e l tude m ta th orique des propri t s du langage Chapitre 3 Types inductifs Ce chapitre d crit la th orie des types inductifs Dans une premi re partie nous nous int ressons aux d finitions non r cursives puis nous aborderons les d finitions r cursives Dans ce document pour simplifier les notations les symboles V et A seront utilis s la place des mots cl de Coq forall et fun 3 1 G n ralit s 3 1 1 Forme g n rale Une d claration inductive dans Coq a la forme suivante Inductive nom 21 Pi zp Pk V ai A1 a Ay 8 co1 V x CE x OP nom z1 2s zp tE tl cop IV Ce Cp nom z1 Zk te Vocabulaire On introduit les notations suivantes On appelle param tres les variables 21 P1 2p Pr On notera V ai Ai a Aj s ce type est appel l arit de la d finition inductive et s est la sorte de la d finition inductive La terminologie pour les variables a Aj a A n est pas stable dans certains contextes on les appelle index dans d autres on les appelle param tres de pr dicat auquel
111. entielle pour d cider l instance de la branche choisir f true ou bien f false 3 3 Les types inductifs r cursifs 3 3 1 Exemples La d finition inductive r cursive de base est bien entendu celle des entiers Inductive nat Set 0 nat S nat nat peine plus compliqu e est celle des listes qui peut tre param tr e par le type des l ments Inductive list A Set Set nil list A cons A list A gt list On construit ais ment sur le m me mod le le type des arbres ou de mani re plus g n rale de toute structure de terme alg brique Un exemple un peu plus sophistiqu est celui des notations ordinales du second ordre Il se construit comme le type des entiers mais on ajoute un constructeur de limite qui correspond un branchement infini param tr par des entiers Cette structure infinie se repr sente de mani re finie par une fonction des entiers vers les ordinaux Inductive ord Set 0 ord S ord ord lim nat ord ord En suivant le m me mod le on peut d finir un type g n rique d arbre o les branchements sont indic s par un premier type de donn es A il y a autant de type de branchements possibles que d l ments dans A et o l arit de chaque branchement est donn e par un type B qui d pend de l indice du branchement Ce type a t initialement introduit par Per Martin L f et est traditionnellement crit W Il se d finit en Coq pa
112. eption Le langage complet est d crit dans le manuel utilisateur En Why toute expression e peut tre annot e avec la notation des triplets de Hoare pre e post Les boucles while doivent tre annot e par while e do invariant inv variant var e done pour sp cifier un invariant de boucle ainsi qu un variant une expression cens e d croitre chaque it ration de la boucle assurant ainsi la terminaison Les annotations pre post et inv sont des formules de logique du premier ordre leur variables sont les variables du programme De plus dans les post on peut utiliser le mot cl result pour r f rer la valeur r sultat de l expression et v pour d signer la valeur de v avant l ex cution de l expression 8 2 2 Typage avec effets Comme un langage de programmation classique le langage Why poss de des r gles de typage et un programme doit tre correctement typ pour que la g n ration des obligations de preuves puissent se faire Comme ce langage est proche de Caml le type en est assez proche aussi mais on lui ajoute une sp cificit qui est le typage des effets qui consiste pr ciser quelles sont les r f rences qui sont lues et celles qui sont crites Voici un exemple de programme tr s simple qui va nous servir pour illustrer les m canismes de Why parameter montant int ref let crediter fun s int gt s gt 0 montant montant s montant s montant En tant que program
113. ersion_clear H inversion_clear HO constructor 2 subgoals EqStreamTrans forall x y z Stream A EqStream x y gt EqStream y z gt EqStream x z x Stream A y Stream A z Stream A Hi head x head y H2 EqStream tail x tail y H head y head z H3 EqStream tail y tail z head x head z subgoal 2 is EqStream tail x tail z Coq lt transitivity head y auto 1 subgoal EqStreamTrans forall x y Zz Stream A EqStream x y gt EqStream y z gt EqStream x z x Stream A y Stream A z Stream A Hi head x head y H2 EqStream tail x tail y H head y head z H3 EqStream tail y tail z EqStream tail x tail z Coq lt apply EqStreamTrans with tail y trivial No more subgoals On peut galement montrer que l galit ainsi d finie est bien la plus grande relation R qui v rifie R s s2 gt head s1 head s2 A R tail s tail s2 Il suffit de montrer que si R est une telle relation alors R s s2 gt EqStream s s2 Cette preuve se fait ais ment en utilisant un point fixe est est laiss e en exercice 4 4 Applications 4 4 1 Calcul de processus Les d finitions co inductives sont utiles la mod lisation de processus parall les En effet une d finition co inductive d une alg bre de processus permet de pouvoir d finir des processus r cursifs sans avoir explicitement manipuler un op rateur de r cursion D autres part les d fi nit
114. es PTS tout PTS se plonge dans Type Type Ces trois syst mes sont incoh rents Une des mani res de d river une incoh rence est de construire dans U et donc aussi dans les 2 autres syst mes un type Univ Type et une injection i VA Type A Prop gt A gt Prop gt Univ En sp cialisant Univ on peut plonger dans Univ toute relation R Univ Univ Prop d finie sur un domaine D Univ Prop Par ce fait on peut d river le paradoxe de Burali Forti cf Girard Gir72 Coq86 le paradoxe de Reynolds Coquand cf Coquand Coq94b ou plus g n ralement encoder la th orie na ve des ensembles de Cantor et en particulier le paradoxe de Russell cf Miquel Miq01 9 2 Le Calcul des Constructions avec univers CC Le Calcul des Constructions avec univers CC tend le CC avec une hi rarchie d nom brable d univers Type Types Types on identifie alors le niveau Type de CC avec Type Les produits sur cette hi rarchie sont pr dicatifs si T Type et U X Type alors IIX T U X TYPemaz i j La sorte Prop reste impr dicative si T Type et U X Prop alors IIX T U X Prop De plus CC introduit une relation de sous typage v rifiant Prop C Type C Type C Types Concr tement la relation de conversion est remplac e par une relation de sous typage d finie par Type C Type ssiz lt 7 Prop C Type IX TU X c HIX T U X ssi T T et U X c U X T cT siT
115. es de R y x pour chaque appel r cursif sur y on retrouve les difficult s mais aussi les solutions mentionn es dans la section pr c dente Supposons que l on souhaite crire une fonction subset qui teste l inclusion sur nos ensembles comme arbres binaires de recherche Un code ML possible est le suivant let rec subset si s2 match si s2 with Empty _ gt true _ Empty gt false Node 11 vi ri Node 12 v2 r2 as t2 gt let c compare vi v2 in 7 f vrier 2014 92 if c 0 then subset 11 12 amp amp subset ri r2 else if c lt 0 then subset Node 11 vi Empty 12 amp amp subset ri t2 else subset Node Empty vi r1 r2 amp amp subset 11 t2 On voit que les appels r cursifs se font sur des arbres qui ne sont pas toujours des sous termes des arguments initiaux sans compter la difficult suppl mentaire d une r currence simultan e sur les deux arguments Il existe cependant un crit re simple de terminaison savoir le nombre total d l ments dans les deux arbres On commence donc par tablir un principe de r currence bien fond e sur deux arbres bas sur la somme de leur nombre d l ments Coq lt Fixpoint cardinal_tree s tree nat match s with Coq lt Empty gt 0 Coq lt Node 1 _ r gt S plus cardinal _ tree 1 cardinal _ tree r Coq lt end Coq Coq lt Lemma cardinal_rec2 Coq forall P tree gt tree gt Set Coq forall
116. es puissances successives den 1 n n nf des deux mani res suivantes en prenant dans les deux cas un registre de type entier Pour tran la fonction successeur tran k k 1 pour out la fonction out k n et pour valeur initiale 0 Pour fonction tran la fonction tran k k xn pour out la fonction identit out k k et pour valeur initiale 1 S il faut calculer un segment de cette suite alors la seconde m thode sera plus efficace En g n ral si on se donne une fonction f nat A alors celle ci peut tre implant e par une stream de registre entier initialis e 0 de fonction out gale f et de fonction tran gale la fonction successeur Si cette stream permet de calculer toutes les valeurs successives de f elle ne tient pas compte des calculs pr c dents pour le faire Les streams d finies par co it ration peuvent v ritablement se voir comme des petits circuits s quentiels 4 2 3 Principe de co r cursion Dans le principe de co it ration le processus fournit des valeurs successives en mettant jour le registre mais ne modifie jamais sa structure interne type du registre ou fonctions de sortie ou de transition Ce n est pas th oriquement un probl me En effet supposons que l on veuille faire voluer un processus X1 out tran 1 vers un processus X2 out tran2 x2 il suffit de le pr voir en avance et d appliquer le principe de coit ration un registre de type la somme dis
117. est possible d extraire un programme Les r gles de typage permettent d assurer qu aucun objet logique de sorte Prop ne sera utilis pour la construction d un objet calculatoire dans la sorte Set Ceci permet de retirer de mani re coh rente tout sous terme logique d un terme calculatoire en pr servant le r sultat du calcul D un point de vue technique il faut tendre les notions d extraction et de r alisabilit pr c demment d finies La fonction d extraction ne s applique toujours qu des objets de type Set ou Type Elle est d finie dans la figure 6 7 La fonction de r alisabilit f r P s applique tous les objets de Set et Type et est d finie figures 6 8 6 9 et 6 10 On dira que A Type lorsque A est une suite de produits se terminant par Prop La d finition de la r alisabilit passe par la d finition d une transformation L P sur les objets de Prop ou Typep qui est d finie figure 6 11 Le r le de cette transformation est d ajuster les types des objets de Set ou Type apparaissant dans P en y appliquant la fonction d extraction E B En particulier si A est dans Prop L A est aussi dans Prop E x A B E B A Prop ou A Typep E x Ajt E t A Prop ou A Typep E t u E t u B Propouu B Typep FIGURE 6 7 Extraction tendue Prop fr x A B x L A fr B A Prop ou A Typep et B Set fr x A B x L A fr B A Propet B Type fr z A B x L A f r B A Typep et B Type FIGUR
118. et m Coq lt End Update 2 3 5 S mantique op rationnelle La d claration suivante impl mente la relation d crivant la s mantique op rationnelle du langage de commande telle qu elle est d crite dans la figure 2 6 Coq lt Inductive semcom memory gt com gt memory gt Prop Coq lt semskip forall m memory semcom m skip m Coq lt semaff Coq lt forall m memory n name v semval e expr Coq lt exprval m e v gt semcom m aff n e update n v m Coq lt semseq Coq lt forall m mi m memory c d com Coq lt semcom m c mi gt semcom mi d m gt semcom m seq c d m Coq lt semcondtr Coq lt forall m m memory e expr c d com Coq lt exprval m e Bool true gt Coq lt semcom m c m gt semcom m cond e c d m Coq lt semcondfa Coq lt forall m m memory e expr c d com Coq lt exprval m e Bool false gt Coq lt semcom m d m gt semcom m cond e c d m Coq lt semwhiletr Coq lt forall m m memory e expr c com 7 f vrier 2014 33 Coq lt exprval m e Bool true gt Coq lt forall mi memory Coq lt semcom m c mi gt Coq lt semcom mi while e c m gt semcom m while e c m Coq lt semwhilefa Coq lt forall m memory e expr c com Coq lt exprval m e Bool false gt semcom m while e c m 2 3 6 S mantique axiomatique Nous nous int ressons finalement la s
119. et pour le k me constructeur Constr k Ind nom A C Cp nom peut tre vu comme un lieur dans la d claration de l inductif ce qui permet d identifier des d clarations inductives isomorphes m me arit m me nombre de constructeurs avec les m mes types d argument Dans cette approche si toutes les occurrences de nom dans les types d arguments sont appli qu es aux param tres z1 2 alors les param tres peuvent tre vus comme des abstractions On construit de nouveaux types de constructeur Ci en rempla ant dans chaque type de constructeur Cp le terme nom 21 z par le nouvel identificateur nom et on retrouve la d finition inductive g n rale l aide des d finitions suivantes nom A z1 Py 2x Py Ind nom A C Cp co A z Pi 2k Pk gt Constr k Ind nom A C C Une d claration inductive avec param tres peut se voir comme une famille de d finitions induc tives 3 2 Les d clarations non r cursives Beaucoup des difficult s concernant les d finitions inductives apparaissent d j au niveau des d finitions non r cursives que nous tudions en premier Dans un premier temps nous ne pr cisons pas la sorte de d claration de la d finition inductive Nous consid rons galement des d finitions inductives sans param tres car ceux ci ne jouent pas de r le essentiel 3 2 1 Les d clarations de base Les d finitions de base non r cursives sont
120. et un mod le fini En revanche tous deux correspondent un langage de fonctions tr s riche puisqu ils contiennent toutes les fonctions prouvablement totales dans l arithm tique d ordre sup rieur 9 1 1 Puissance logique Le mod le bool en preuve unique mod le proof irrelevant Le CC admet un mod le bool en dans lequel Prop est interpr t par l ensemble a deux l ment B true false L impr dicativit se r sume alors une quantification finie sur B Les types de Type sont construits r cursivement partir de B et le produit fonctionnel Dans le cas d un produit A T avec A une proposition et T un type l interpr tation est celle L interpr tation s applique tous les jugements qui ne sont pas des jugements de preuve on note X P Q et T U pour les objets et types du niveau Type et x t u et B pour les objets et types du niveau Prop Prop true false Va A U U VX T U T gt U VX T B true ssi B x y true pour tout V T Vz A B true ssi A false ou B true VX T B true ssi B x y true pour tout V T Az A P P AX T P V T gt Plx Pal P PQ P1 101 X p X 1 Le mod le bool en standard de CC diff rencie selon que A est prouvable ou pas cf par exemple MW03 de T Ce raffinement qui force 4 consid rer des interpr tations partiellement d finies n est pas n
121. eur s mantique il faudra de plus supposer que cette valeur est compatible avec la sorte Coq lt Definition memory name gt sort gt semval Valeur d une expression Pour construire la relation entre une expression et sa valeur on peut se donner une m moire comme param tre dans une Section lorsque la section est ferm e les notions introduites seront automatiquement abstraites par rapport aux param tres dont elles d pendent Coq lt Section Valexpr Coq lt Variable memstate memory Coq lt Hypothesis memstate_correct Coq lt forall n name s sort compat s memstate n s La d finition exprval formalise la s mantique des expressions telle qu elle est pr sent e a la figure 2 5 Coq lt Inductive exprval expr gt semval gt Prop Coq lt valvar forall n name s sort exprval Var n s memstate n s Coq lt valtr exprval Tr Bool true Coq lt valfa exprval Fa Bool false Coq lt valxor Coq lt forall f g expr bf bg bool Coq lt exprval f Bool bf gt Coq lt exprval g Bool bg gt exprval Xor f g Bool boolxor bf bg Coq lt valnum forall n nat exprval Num n Nat n Coq lt valtzero Coq lt forall f expr nf nat Coq lt exprval f Nat nf gt exprval Null f Bool iszero nf Coq lt valopn Coq lt forall o op f g expr nf ng nat Coq lt exprval f Nat nf gt Coq lt exprval g Nat ng gt exprv
122. fl Ageirs xr Jy B snd x r B y fst x fives Vi f x Viet B FIGURE 6 1 R alisabilit r cursive On montre que si une formule A est d montrable alors on peut trouver un terme t tel que t Atr A soit d montrable 7 f vrier 2014 78 Principe de Markov La r alisabilit r cursive sert justifier par exemple le principe de Markov Va nat P x V P x 774 a nat P x 2x nat P x Ind pendance des pr misses La r alisabilit r cursive sert justifier que le principe d in d pendance des pr misses n est pas d montrable en logique intuitionniste A gt 3xz P x gt 3xz A gt P x Evaluation Tous les objets interm diaires manipul s dans le programme ont une valeur ce qui permet d assurer qu un programme t qui r alise une formule pourra se calculer par une strat gie d appel par valeur mais sans valuer les termes sous les abstractions R alisabilit modifi e La r alisabilit modifi e typ e a t introduite par Kreisel Il s agit d assurer la terminaison des interpr tations par une condition de bon typage Les objets mani pul s par la logique sont des termes typ s dans un A calcul avec des types simples un produit et des entiers On notera explicitement le type des variables apparaissant dans les quantificateurs Jy o P ou Vy o P A chaque formule A est associ le type t A de ses r alisations Dans la formule x r A x repr sente une v
123. h x with c1 Z gt c1 Z Cn T gt cn Z end On proc de ensuite de la mani re suivante fx match fx with c Z c Z cn T Cn Z end n match F f x with c1 2 gt c1 Z Cn Z cn end F f zx n Cas des Streams Dans le cas des streams le lemme de 7 expansion aura la forme suivante Coq lt Lemma Stream_eta forall A Set x Stream A Coq lt x match x with Cons a 1 gt Cons a 1 end Coq lt destruct x trivial Coq lt Qed Coq lt Hint Resolve Stream_eta On montre ensuite les propri t s attendues Coq lt Lemma puis_eq forall k nat puis k Cons k puis k n Coq lt intros transitivity Stream_eta puis k simpl in Coq lt trivial 4 3 4 Familles coinductives Le sch ma de d finition de familles inductives suit le sch ma de d finition des types inductifs Il en est de m me pour les d finitions de familles co inductives Une famille d finie co inductivement est une propri t dont les preuves peuvent tre des objets infinis Supposons que l on veuille justifier que de streams potentiellement infinies sont extension nellement gales c est dire que les valeurs de leurs diff rents l ments sont les m mes On pourrait le faire en utilisant un entier n et l acc s la n me valeur d une stream Cependant si le type co inductif devient plus compliqu alors l acc s aux composantes va n cessiter l int
124. i re n ou bool enne b Les deux op rations utiles sur la m moire sont la lecture et la mise jour si x est une variable et s une sorte alors m x s repr sente la valeur de la m moire pour la variable x et la sorte s si v est une valeur alors m x v repr sente la m moire o la variable x a t mise jour par la valeur v On a choisi de ne pas indiquer explicitement la sorte de la variable affect e celle ci sera d duite de la sorte de la valeur v S mantique des expressions On a besoin de la relation qui associe chaque m moire m et expression une valeur v repr sentant le r sultat de l valuation de E dans la m moire m On note cette relation m F Epuv On utilisera des constantes et des fonctions sur le domaine des valeurs r alisant les op rations bool ennes et arithm tiques Elles seront not es en italique en utilisant le m me identificateur que dans la syntaxe ainsi la construction syntaxique xor correspond la fonction s mantique zor mk X pm X s mF truetrue mt falsep false mbrnon mbt Ey eb mt Eee be mbe Epn mk Eini mt Bop ne mb E xor Ea gt b zor bz m F null Ep null n mt E1 op E2 gt nz op no FIGURE 2 5 S mantique des expressions S mantique des commandes La relation m C gt m exprime que la commande C s value dans une m moire m qu elle transforme en une m moire m On la d finit par les r gles d inf rence de la figure 2 6 PE mbt Epv m Ovom m F Com mk X Epm X
125. i produit du code pour plusieurs langages de programmation fonctionnels Ocaml Haskell et Scheme Cette commande peut tre utilis e directement dans la boucle d interaction de Coq pour afficher le code extrait Coq lt Extraction plus val plus nat gt nat gt nat let rec plus n m match n with 0 gt m S p gt S plus p m La commande Recursive Extraction aura pour effet d extraire r cursivement tout ce qui est n cessaire On peut galement utiliser la commande Extraction pour crire dans un fichier tout le code correspondant un ensemble d objets Coq le caract re r cursif est alors implicite Coq lt Extraction arith ml plus mult Dans le cas d Ocaml une interface est galement cr e fichier mli Chapitre 7 Preuve de programmes fonctionnels Dans ce cours nous nous int ressons la sp cification et la preuve de programmes purement fonctionnels Nous montrons comment Coq peut tre utilis pour produire du code ML certifi Ce chapitre est illustr par des programmes manipulant des arbres binaires de recherche qui sont repr sentatifs des programmes purement fonctionnels la fois complexes et tr s utiles en pratique Dans la suite nous d nommons informatif tout ce qui se trouve dans la sorte Set et logique tout ce qui se trouve dans la sorte Prop Cette distinction de sorte est exploit e par le m ca nisme d extraction PM89a PM89b Let03a Let03b fourni par
126. ini ML Rapport de dea IARFA September 1992 Tro73 Anne S Troelstra editor Metamathematical Investigation of Intuitionistic Arith metic and Analysis LNM 344 Springer Verlag 1973 TvD88 Anne S Troelstra and Dirk van Dalen Constructivism in Mathematics an intro duction Studies in Logic and the foundations of Mathematics volumes 121 and 123 North Holland 1988 VGLPAK00 Kumar Neeraj Verma Jean Goubault Larrecq Sanjiva Prasad and S Arun Kumar Reflecting BDDs in Coq In ASIAN 2000 volume 1961 of LNCS pages 162 181 2000 Wer94 Benjamin Werner Une th orie des constructions inductives Th se de doctorat Universit Paris 7 1994 Wieal Freek Wiedijk Comparing mathematical provers http www cs kun nl freek comparison index html Wieb Freek Wiedijk The fifteen provers of the world http www cs kun nl freek comparison index html
127. ion sval s sort Set Coq lt match s with Coq lt Sbool gt bool Coq lt Snat gt nat Coq lt end Coq lt Definition memoryi name gt forall s sort sval s On d finit alors Coq lt Parameter memstatel memoryi Coq lt Inductive exprvall expr gt forall s sort sval s gt Prop Coq lt valvari Coq lt forall n name s sort exprvali Var n s s memstatei n s Coq lt valtri exprvali Tr Sbool true Coq lt valfal exprvali Fa Sbool false Coq lt valxori Coq lt forall f g expr bf bg bool Coq lt exprvali f Sbool bf gt Coq lt exprvall g Sbool bg gt exprvali Xor f g Sbool boolxor bf bg Coq lt valnumi forall n nat exprvali Num n Snat n Coq lt valtzerol Coq lt forall f expr nf nat Coq lt exprvali f Snat nf gt exprvali Null f Sbool iszero nf Coq lt valopni Coq lt forall o op f g expr nf ng nat Coq lt exprvali f Snat nf gt Coq lt exprvali g Snat ng gt exprvali Opn o f g Snat semop o nf ng Le lemme de correction de l valuation s nonce alors simplement Coq lt Theorem expr_val_cor1 forall E expr s sort Coq lt exprcorrect s E gt exists v sval s exprvali Es v La formalisation et la preuve sont plus simples cependant l usage de types d pendants rendra la formalisation de la fonction d criture sur la m moire plus complexe en effet on doit avoir avec n name s sort
128. ions de bisimulation entre processus sont naturellement des d finitions co inductives Dans les contributions du syst me Coq on trouvera des mod lisations de plusieurs alg bres de processus CCS CBS ainsi que du z calcul 7 f vrier 2014 64 4 4 2 Logique temporelle Les d finitions co inductives permettent galement de d finir naturellement certains op ra teurs de la logique temporelle Si on suppose donn e un syst me de transitions R sur des tats de type X Les formules de la logique temporelle ont pour interpr tation in ensemble d tats On peut d finir les propri t s de la logique temporelle en les repr sentant directement par leur semantique Il sera alors tr s simple de d finir de mani re co inductive les op rateurs All et Ex sur les formules La s mantique de A11 resp Ex est que soit P une formule et x un tat pour tout chemin resp pour un chemin issu de la formule P est v rifi e Coq lt Section Logique_temporelle Coq lt Variable X Set Coq lt Variable R X gt X gt Prop Coq lt Variable P X gt Prop Coq lt CoInductive All X gt Prop Coq lt All_intro forall x X P x gt forall y X R x y gt All y gt All x Coq lt CoInductive Ex X gt Prop Coq lt Ex_intro forall x X P x gt exists y X R x y Ex y gt Ex x Coq lt End Logique_temporelle 4 4 3 Autres applications Les d finitions co inductives peuvent galement tr
129. ique En 7 f vrier 2014 114 particulier le mod le par r alisabilit montre la coh rence de CC 0 A n 1 injectivit du successeur induction c est dire de CC les axiomes de Peano Tous les programmes prouvablement terminant dans l arithm tique d ordre sup rieur sont d rivables dans Fy et donc dans le CC Gir72 Sch matiquement le mod le par r alisabilit interpr te les propositions comme des ensembles de A termes clos par 6 expansion avec la propri t que t A gt B ssi tu B pour tout u A propri t dite de r ductibilit L interpr tation des types de Type est alors la m me que pour le mod le bool en standard du CC le produit du CC est interpr t comme le produit ensembliste ceci pr s que le domaine de base Prop est maintenant un ensemble de parties de A termes 9 1 3 Extensions incoh rentes du Calcul des Constructions Syst mes U U et Type Type Les syst mes U et U dus J Y Girard Gir72 sont en fait des extensions du syst me Fw Alors que la couche Type de F correspond un calcul simplement typ bati sur la constante Prop la couche Type des syst mes U et U correspond un calcul polymorphe le syst me F incluant Prop comme type de base Le syst me Type Type nonc par P Martin L f est le syst me o Prop et Type sont confondus et o tous les produits sont permis En particulier Type Type est un objet terminal de la cat gorie d
130. isque le type est non r cursif il s agit juste d ex primer que tout l ment de sum A B ne peut tre construit qu partir de l un des deux constructeurs Coq lt Check sum_ind sum_ind forall A B Set P sum A B gt Prop forall a A P inl A B a gt forall b B P inr A B b gt forall s sum AB Ps 7 f vrier 2014 18 1 6 Types inductifs plus complexes Dans tous les exemples de types r cursifs vus jusqu ici l ordre correspondant la r cursion et la r currence structurelle se confondait avec la relation de sous terme Le m canisme des types inductifs autorise toutefois des constructions plus g n rales 1 6 1 Ordinaux La d finition qui suit est souvent appel type des ordinaux par abus de langage Il s agit en fait d une notation ordinale qui ne permet que la repr sentation d un fragment des ordinaux constructible dans CCI Il s agit d une copie du type des entiers naturels tendue par un nouveau constructeur correspondant la limite ordinale Coq lt Inductive Ord Set Coq lt Oo Ord Coq lt So Ord gt Ord Coq lt lim nat gt Ord gt Ord On remarque que le constructeur lim est r cursif mais que son argument est une suite enti re d ordinaux L ordre de la r cursion structurelle est alors g n ralis de la mani re suivante quel que soit les termes n de type nat et f de type nat ord f n est structurellement plus
131. it de la d finition inductive nom al Ai a Ay gt WO en CF1 a1 01 x eat FAAR GOT PSC so 5A CR Exemple 1 Le type des bool ens est quivalent Un Un Op rateurs primitifs vs sch ma g n ral On peut choisir d introduire dans un formalisme les constructions de base c est le cas d un syst me comme NuPrl ou dans des pr sentations ca t goriques ou bien introduire un sch ma g n ral de d finition inductive Le second choix permet d utiliser l uniformit des principes d introduction et d limination des diff rents op rateurs Il permet galement de repr senter de mani re concise des propri t s qui n cessiteraient une imbri cation profonde de connecteurs L introduction ou l limination de ces propri t s peuvent alors se faire en une seule tape ce qui permet d avoir des preuves plus directes Par contre la g n ralit du sch ma complique les raisonnements par cas sur la forme des d finitions inductives on ne peut pas juste traiter les cas Zero Un X type somme disjointe et galit il faut raisonner sur la structure interne des d finitions inductives et traiter de mani re g n rale des suites finies de termes ou de types cela introduit une lourdeur la fois au niveau de la programmation et de la pr sentation th orique Exemple 2 On suppose donn un type U Set et un pr dicat P U Prop On se propose de d finir une relation dec portant sur un bool en
132. it appara tre strictement positivement en position de param tre de la d finition inductive J et ce param tre doit lui m me appara tre strictement positivement dans les types d arguments de J On peut donc avoir un type de constructeur de I de la forme list A 7 I par contre si on introduit Inductive neg X Prop Prop in X False neg X Alors d finir un inductif J dont un type de constructeur est neg I I est non valide 3 3 3 Sch ma d limination r cursif primitif Supposons que l on d finisse un inductif r cursif qui v rifie la condition de stricte positivit sans imbrication Alors le sch ma d limination peut tre renforc pour prendre en compte le fait que la propri t que l on cherche montrer est r cursivement satisfaite pour les sous termes du type appropri On peut donc renforcer le sch ma d limination en prenant sa forme r cursive Tha nomai aq TEF P V a A a Az nom az aj gt 8 m l p Ci Cin types d arguments r cursifs TH fn Val Ch am Cm CH P 24 gt Fo P atm P tl t com at m TE Rec P x fi fp P a1 a Si C est un type d argument r cursif strictement positif et sans imbrication alors il est de la forme Ver D1 2n Dn nom u1 u 7 f vrier 2014 49 si x C on d finit C P x Y z1 Di 2n Dn P u1 u z1 2n On voit que ce sch ma d
133. it repr sent s par des fonctions qui sont une notation finie pour repr senter une infinit de valeurs les branches infinies seront repr sent es intentionnellement par des programmes permettant de les d velopper aussi loin que n cessaire Le principe dit de co it ration a le type suivant Coq lt Definition Stream_coiter forall X Set X gt A gt X gt X gt X gt Stream Le principe de base pour repr senter un liste infinie par un objet fini est de se donner un type X quelconque une fonction out de type X A une fonction tran de type X X et un objet x de type X Ces composantes permettent de construire un processus dont l tat est compos d un registre de type X dont la valeur initiale est x et des deux fonctions out et tran On obtient alors une stream Stream_coiter out tran x que l on notera galement X out tran x On peut interpr ter cette stream comme un processus A chaque tape ce processus a une valeur x dans son registre il peut mettre une valeur de type A donn e par out x et transformer son registre en la valeur tran x Si on appelle p la fonction qui prend en entr e la valeur z du registre et renvoie la stream X out tran x alors ona p x Cons out x p tran x 4 1 Tout comme il existe plusieurs algorithmes qui implantent la m me fonction la m me liste infinie pourra tre engendr e par des processus tr s diff rents Par exemple on peut engendrer la suite d
134. itives para t peu intuitif il faudrait commencer par pr ciser les r gles pour ces deux types inductifs Pour viter cela on peut int grer le raisonnement galitaire dans le sch ma d limination On suppose que l on a une propri t P de type Y a A1 a Aj nom ay aj gt 8 Pour prouver V ai Ai aj Aq x nom a1 amp P ay amp x il suffit de montrer pour chaque constructeur com la propri t y x CL a OR P th th Com ct On obtient donc le sch ma d limination suivant qui est param tr par la sorte s de la propri t prouver TF nomu w TF P V ay A a A nom ai aj 8 FE fee Vee CL 2 Cnm PU at conn 2 m E 1 p TF Case P x fi fp P u1 u x O Case est un nouveau constructeur de terme 7 f vrier 2014 40 R duction Comme toute r gle d limination celle ci se combine avec les r gles d introduction pour former une r duction Si la fonction d limination est appliqu e au m i me constructeur alors elle se r duit en la m me branche instanci e par les arguments du constructeur On v rifie que le type est pr serv Cette r duction est appel e la r duction et s crit Case P com eee Haka re nes fm 1 2 On remarque que cette construction est analogue une d claration par filtrage dans laquelle on examine dans l ordre les constructeurs et on n a que des motifs d
135. jet x de type A associent un objet de type B Comme en tronc commun on utilisera la fl che pour simplifier l criture de ce type lorsque x n appara tra pas dans B En ASCII cela donne A gt B Par ailleurs essentiellement pour des raisons historiques les sortes portent d autres noms en Coq que dans le cours de tronc commun Rappelons que les sortes sont des constantes particu li res qui sont les types des types Dans le cours de tronc commun on utilisait une sorte Type qui est le type des types et une sorte Kind qui tait le type de Type Cette derni re servant essentiellement noncer les r gles correspondant au polymorphisme Dans les versions de Coq ant rieures la version 8 0 Type est remplac e par deux sortes ju melles Prop et Set Intuitivement Set contient les types de donn es objets calculatoires qui sont pris en compte par le processus d extraction de programmes de Coq cf le chapitre consacr et Prop les nonc s logiques qui sont oubli s par le processus d extraction Depuis la version 8 0 de Coq Prop garde le r le jou par Type dans le Calcul des Constructions trait dans le cours de tronc commun Il reste une sorte nomm e Set mais qui est une version pr dicative de Type Typiquement le type forall A Set A gt A ne peut pas s appliquer lui m me en Coq version 8 0 Pour ne rien arranger la sorte Kind se trouve renomm e Type dans Coq Au lecteur qui serait tent de
136. jointe X1 X2 7 f vrier 2014 57 de X et X2 la fonction de sortie qui utilise out lorsque le registre est dans l tat X et outo lorsque le registre est dans l tat X2 quant la fonction de transition elle peut choisir de laisser le processus dans l tat X ou X ou au contraire d effectuer une transition d un tat X dans un tat X ou inversement Il y a une mani re syst matique de capturer cette possibilit de transformation dans l im plantation d une stream c est le principe de co r cursion Coq lt Definition Stream_corec Coq lt forall X Set X gt A gt X gt X Stream gt X gt Stream La fonction de transition peut soit choisir de renvoyer un processus de m me implantation soit choisir de transformer le processus en un nouvel objet de type Stream pouvant avoir une implantation compl tement diff rente Exercice Montrer que la propri t de cor cursion Stream_corec se d duit de la coit ration Stream_coiter La propri t attendue pour l op rateur de co r cursion est la suivante p x Cons out x Cases tran x of inl x gt p 2 inr s gt s end 4 2 4 2 4 D finitions par points fixes Dans les langages de programmation fonctionnels qui manipulent des structures infinies par exemple les langages de la famille ML paresseux tels que Haskell il n est pas question d op rateur de co it ration on utilise simplement le point fixe g n r
137. l99 Fil03a 8 3 Traitement des structures donn es complexes et application d autres langages de programmation Why ne g re pas explicitement de structures de donn es complexes N anmoins il a une approche modulaire dans le sens o de m me qu il accepte des programmes en param tre avec uniquement leurs sp cifications il accepte des types abstraits et des pr dicats et fonctions lo giques abstraites sur ces types 8 3 1 Exemple d un programme avec un tableau le drapeau hollandais Il s agit d un exemple c l bre un programme de tri lin aire quand il n y a que trois valeurs comme les couleurs du drapeau hollandais d Dijkstra Dij76 On introduit un type abstrait Why avec des axiomes parameter BLUE WHITE RED color logic iscolor color gt prop axiom color_elim forall c color iscolor c gt c BLUE or c WHITE or c RED puis un premier programme Why uniquement sp cifi pour le test d galit des couleurs parameter eq_color ci color gt c2 color gt bool if result then ci c2 else ci lt gt c2 On introduit ensuite une axiomatisation des tableaux on les repr sente en logique comme des tableaux fonctionnels c c o la mise jour d une case de tableau retourne un nouveau tableau logic acc colorarray int gt color acc t i represente t i logic length colorarray gt int longueur d un tableau logic update colorarray int colo
138. lacement de la propri t bst s vers la pr condition n est pas n cessaire c est juste plus naturel Note L extraction de sig Q oublie l annotation logique Q et se r duit donc l extraction du type A Dit autrement le type sig peut dispara tre l extraction de fait on a Coq lt Extraction sig type a sig a singleton inductive whose constructor was exist 7 2 2 Variantes de sig On peut d finir d autres types similaires sig Ainsi si l on souhaite crire une fonction retournant deux entiers telle que par exemple une division euclidienne on envie d embo ter deux utilisation de sig de la m me mani re que l on peut le faire pour deux existentielles ex div Va b b gt 0 gt q r a bq rA0 lt r lt b Mais la seconde utilisation de sig a pour sorte Set et non Prop ce qui rend cette criture incorrecte Coq introduit pour cela une variante de sig sigs Coq lt Inductive sigS A Set P A gt Set Set Coq lt existS forall x A P x gt sig P o la seule diff rence est la sorte de P Set au lieu de Prop sigs A fun x gt P se note x A amp P ce qui permet d crire div Va b b gt 0 gt q amp r a bq rA0 lt r lt b L extraction de sigS est naturellement une paire Coq lt Extraction sigs type a p sigS ExistS of a p De m me si l on souhaite une sp cification de la forme x A PxAQ x il existe
139. le remplace ment de e 0 0 par ref1 0 ne peut se faire En effet il faut utiliser le sch ma d limination qui demande de g n raliser le but sous la forme d un pr dicat de type Vy nat 0 y Prop or les d pendances nous emp chent de g n raliser comme on le souhaiterait A y nat e 0 y gt Case list e nil nil n est pas un terme bien typ Cette pathologie a t mise en vidence par Thierry Coquand Thomas Streicher et Martin Hofmann HS98 ont exhib des mod les de la th orie des types pour lesquels il y a des preuves de x x qui ne sont pas convertibles refl x Cependant s il existe une galit d cidable sur A ce qui est le cas de tous les types de donn es usuels alors cette propri t est d montrable mais la construction est complexe l id e originale est due Michael Hedberg elle a t cod e dans LEGO par Thomas Kleymann et reprise dans Coq par Bruno Barras cf le fichier theories Logic Eqdep_dec v L axiome K de Streicher Thomas Streicher a propos d ajouter un principe d limination plus puissant pour l galit qui capture exactement que toute preuve de x x est une preuve par r flexivit e x x P x xr gt s p P refl zx Caseg P e p P e Ce nouvel op rateur satisfait une r gle de r duction Casex P ref1 x p p 7 f vrier 2014 44 Il existe de nombreuses formes quivalentes de cet axiome La th orie EqDep de Coq int
140. les propri t s montrer pour les types auxiliaires Dans le cas de l exemple des arbres et des for ts la commande Inductive introduit en parti culier le sch ma suivant qui n utilise pas la structure r cursive de foret arbre_ind V A Set P arbre A Prop V a A f foret A P node A a f Va arbre A Pa Pour d finir arbre_foret_ind qui permet de prouver une propri t P sur les arbres en utilisant une propri t Q sur les for ts prouv e de mani re mutuellement r cursive on utilise Scheme arbre_foret_rec Induction for arbre Sort Prop with foret_arbre_rec Induction for foret Sort Prop On obtient alors arbre_foret_ind V A Set P arbre A Prop Q foret A Prop V a A foret A Q f P node A a f PO vide A Va arbre A P a Vf foret A Q f Q add A a f Va arbre A Pa 3 4 Extensions Les d finitions inductives du Calcul des Constructions Inductives permettent une repr sen tation directe des types de donn es concrets et des relations inductives d finies comme les plus petites propri t s satisfaisant un ensemble de conditions de stabilit Cependant cette notion est insuffisante pour repr senter certaines structures qui apparaissent naturellement dans les d veloppements math matiques et informatiques 3 4 1 Structures infinies Il s agit en particulier des structures potentiellement infinies comme les streams suites in finies
141. leur double n gation telle que Fco AS A et si Fc A alors A Les formules Vn dm Q n m avec Q sans quantificateur formules dites IIS sont d mon trables de mani re intuitionniste si et seulement elles sont d montrables de mani re clas sique Ho Vn dm Q n m si et seulement si Fy Vn 3m Q n m Les propri t s sp cifiques des preuves intuitionnistes Les preuves intuitionnistes v rifient les propri t s de la disjonction et du t moin si Fz AV B alors ou B si Hz 3x P x alors il existe t tel que Fz P t Les preuves intuitionnistes v rifient l axiome du choix si Hz Vx P x V P x alors il existe f fonction r cursive telle que Fy f x true P x si Fz Vx dy P x y alors il existe f fonction r cursive telle que Hz P x f x Les propri t s sp cifiques des preuves classiques Les preuves classiques peuvent donner des r sultats non conformes l intuition de la v rit tel que le c l bre th or me des buveurs Dans chaque bar il y a une personne telle que si cette personne boit alors tout le monde boit Les preuves classiques ont un contenu calculatoire le sch ma A gt B gt A A loi de Peirce a pour contenu calculatoire l op rateur de contr le call cc l op rateur call with current continuation que l on peut trouver dans Scheme et SML Toute preuve classique de H 2n P n avec P n atomique s value en une preuve intui tionniste de
142. limination est plus g n ral que le sch ma non r cursif pr alablement introduit Il implique en particulier que l ordre structurel sur le type inductif est bien fond Nos objets dans le type inductif ne repr sentent que des structures qui peuvent tre infinies mais dont toutes les branches r cursives sont finies Les sch mas d limination r cursive sont engendr s automatiquement par Coq au moment de la d finition inductive Dans le cas d une d finition de sorte Prop le sch ma d clar correspond une limination non d pendante Les sch mas d pendants peuvent tre introduits l aide de la commande de vernaculaire Scheme Dans le cas de d finition inductive imbriqu e la forme du sch ma d limination r cursive nest pas aussi simple formuler Coq ne fournit pas de facilit pour les introduire c est l utilisateur de concevoir un sch ma adapt et de le d montrer l aide de l limination r cursive et des constructions par point fixe que nous allons maintenant introduire 3 3 4 Condition de garde Le sch ma d limination r cursive tait propos par P Martin L f comme la construction d limination de base des d finitions inductives Il permet de capturer la notion de fonctionnelle d finie de mani re primitive r cursive ainsi que la notion de preuve par r currence structurelle Cependant Th Coquand a sugg r une approche alternative o comme dans les langages de programmation fonctio
143. m gt Assertion gt Prop Coq lt trueskip forall P Assertion trueform P skip P Coq lt trueaff Coq lt forall P Assertion n name e expr Coq lt trueform memupdate n e P aff ne P Coq lt trueseq Coq lt forall P Q R Assertion c d com Coq lt trueform P c R gt trueform R d Q gt trueform P seq c d Q Coq lt truecond Coq lt forall P Q Assertion e expr c d com Coq lt trueform AndAss P Istrue e c Q gt 7 f vrier 2014 34 Coq lt trueform AndAss P Isfalse e d Q gt trueform P cond e c d Q Coq lt truewhile Coq lt forall P Assertion e expr c com Coq lt trueform AndAss P Istrue e c P gt Coq lt trueform P while e c AndAss P Isfalse e Coq lt truecons Coq lt forall P P1 Q Qi Assertion c com Coq lt ImplAss P Pi gt Coq lt trueform P1 c Q1 gt ImplAss Q1 Q gt trueform P c Q Lemme de correction Le th or me suivant nonce la correction de la relation donn e P c Q par rapport la s mantique Coq lt Theorem truecorrect forall P Q Assertion c com Coq lt trueform P c Q gt forall mi m2 memory semcom mi c m2 gt P mi gt Q m2 2 4 Pour en savoir plus 2 4 1 S mantique des langages et compilateurs Les logiques d ordre sup rieur comme le Calcul des Constructions Inductives se pr tent bien aux formalisations de notions s mantiques et logiques Une des premi res preuves de cett
144. me Caml on sait tr s bien inf rer que crediter ale type int gt unit Ce qu on va faire en plus c est de calculer ses effets pour d terminer dans cet exemple que la r f rence montant est la fois lue et crite Un type avec effet est un triplet type variables lues variables crites Voici un extrait des r gles de typage de Why cf Fil03a pour le reste x iter t non ref x tref er yt t 0 0 Pele t 0 Tre t2 gt t1 R W Ri W1 TH e t2 Ro W2 t non ref TH e1 e2 t1 R U Rg U R Wi U W2 U W T z tHe t R W TH fun z t gt e t t R W 0 9 x tref er Tre R W Phew e gt unit fo U R x U W 7 f vrier 2014 106 La r gle de typage de l application ci dessus interdit d appliquer une fonction une r f rence Une r gle sp ciale existe dans ce cas THe t2 ref gt t1 R W Ri W1 Ter t2 ref R2 W2 r t1 R W TE e1 r tilz r RU RU Rfrx r W1 U W2 U Wfe rl Il est fondamental de remarquer que cette r gle interdit les alias c d de r f rencer la m me chose avec deux noms diff rents C est une condition essentielle pour garantir la correction de la m thode Why Voici un exemple typique let incr2 fun x int ref y int ref gt true begin x x 1 y y 1 end x x 1 and y y 1 parameter t int ref let test true incr2 t t t t 0 1 Why signale une erreur de typage su
145. n programme les preuves sont des termes qui sont saisis interactivement via une interface graphique Ces syst mes sont d velopp s l universit de Chalmers en Su de PhoX Raf est un syst me bas sur l arithm tique d ordre 2 manipulant des programmes ML avec inf rence de type polymorphe la Milner Son utilisation est importante en milieu enseignant Il est d velopp par C Raffali l universit de Savoie Twelf PS est une m ta logique dot e d un m canisme d unification d ordre sup rieur Twelf est utilis pour mod liser la s mantique de langages de programmation Ce syst me est d velopp Carnegie Mellon University dans l quipe de Frank Pfenning 5 4 Preuves par r flexion La r flexion est une technique permettant de remplacer les tapes de preuves associ es une proc dure de simplification ou de d cision en la combinaison d une unique tape de preuve et du calcul En ce sens la technique de r flexion suit le principe de Poincar qui consiste sortir du langage de preuve les m thodes de preuves qui se ram nent un simple calcul 7 f vrier 2014 68 5 4 1 Utilisation de preuves de d cidabilit Supposons qu une propri t A sur un ensemble U soit d cidable On a alors une preuve dec de la propri t Vz U A x A x On en d duit ais ment une fonction de d cision bool enne dec_bool U bool et sa propri t de correction correct Vx U dec_bool
146. n est 7 f vrier 2014 74 fonctionnelle n est pas prouvable Par exemple il est possible de coder les termes du calcul comme des entiers et de d finir la relation de r duction sur les termes La preuve de totalit de la fonction de normalisation permet de montrer la coh rence logique du syst me et ne peut donc du fait des th or mes d incompl tude de G del tre montr e dans le syst me lui m me Exemple 1 La propri t suivante qui dit que toute fonction sur les entiers admet un minimum est vraie de mani re classique mais pas de mani re intuitionniste m me si on se limite aux fonctions r cursives Vf dn Vm f m gt f n En effet il n existe pas de fonction r cursive qui pour une fonction quelconque calcule son mi nimum Sinon on pourrait d cider pour toute fonction si elle prend la valeur nulle et donc on pourrait d cider du probl me de l arr t Exemple 2 On peut montrer de mani re classique l existence de deux nombre x et y irrationnels tels que z soit rationnel On suppose tabli que V2 est irrationnel si fx est rationnel alors on prend x y V2 si 2 est irrationnel alors on prend x s n y V2 ona r VON Ve V est rationnel Cette d monstration ne permet pas d exhiber une solution Exemple 3 Les r sultats pr c dents permettent d tablir que AV A n est pas d montrable en g n ral En effet supposons que ce soit le cas On utilise le pr dicat T de Kleene T n
147. n n est alors plus tant existe t il une formalisation de tel raisonnement que de construire et d exhiber cette formalisation C est avec cette observation l esprit que nous chercherons traiter des points suivants Formalismes Le choix du formalisme est important pour la pratique des math matiques formelles Non seulement il doit tre capable d exprimer la preuve con ue par le math maticien mais il doit permettre de le faire de la mani re la plus facile et la plus intuitive possible De fait les volutions r centes du Calcul des Constructions Inductives ont presque toujours t motiv es par la pratique et sont donc post rieures aux premi res impl mentations de CoC puis Coq Mod lisation Plus encore qu en math matiques usuelles savoir bien noncer les propositions que l on esp re prouver est essentiel si l on veut ultimement aboutir une preuve formelle Si l on fait l analogie entre les activit s de prouver et programmer alors le choix de la mod lisation correspond celui de la structure de repr sentation des donn es avec les cons quences imm diates et videntes sur l architecture du logiciel obtenu Plus g n ralement il nous semble que les analogies entre les activit s de preuves et de pro grammation sont nombreuses et s il existe un art de la bonne programmation il en va de m me pour les preuves formelles De plus chaque couple formalisme probl me correspond un
148. n syst me bas sur une m ta logique Ainsi Isabelle par exemple offre essentiellement des biblioth ques pour la logique d ordre sup rieur de Church HOL et la th orie des ensembles de Zermelo Fraenkel ZF Le principe de Poincar Le principe de Poincar Poi02 caract rise les syst mes qui dis tinguent entre simples v rifications calculatoires et tapes de preuve Poincar prend l exemple de la propri t 2 2 4 qui ne se justifie pas par une preuve mais plut t par une v rification par calcul Des syst mes comme Coq Isabelle MetaPrl PVS et HOL utilisent une r gle de conver sion qui identifie des propri t s quivalentes modulo certaines r gles de calcul Dans HOL cette r gle de conversion ne prend en compte que la B r duction dans un lambda calcul simplement typ alors que dans Coq on identifie les termes modulo la amp r duction qui permet de calculer une grande classe de fonctions r cursives Mizar par contre n int gre pas de notion de calcul Le principe de Poincar peut tre implant des degr s tr s divers Par exemple dans le Calcul des Constructions Inductives une preuve de 0 n n rel ve de la simple v rification c est la r gle de conversion tandis qu une preuve de n 0 n n cessite une tape d induction et des tapes de r criture Autrement dit dans le Calcul des Constructions Inductives seul un quotient relativement une valuation s quentielle des programmes est intro
149. n th orie des ensembles par l ensemble vide et true par un ensemble singleton typiquement l ensemble dont l unique l ment est l ensemble vide en ce cas VX T B s exprime comme Nyeprj P x v Le mod le bool en sur le calcul pur mod le bool en non proof irrelevant Il existe une variante du mod le bool en qui pr serve le contenu calculatoire des preuves Ce mod le non exprimable dans l arithm tique permet par exemple de montrer la non prouvabilit de l induction de Peano Geu01 SG95 La diff rence par rapport au mod le bool en preuve unique est que les propositions vraies sont interpr t es par l ensemble de tous les termes purs L interpr tation est donc la suivante Prop A Va AU U VX T U T gt U Ve A B t Alpour tout u A tu B VX T B a Wer B x v Az A P P AX T P V T gt Phx PE Pa P PQ P X p X x p x AX Ti ltl Av At y E PI El tu 1 lul et on montre que F t A implique ft A DOUT Y frais 9 1 2 Puissance calculatoire Le CC admet aussi un mod le par r alisabilit qui respecte le contenu intensionnel des fonc tions et des preuves Un tel type de mod le permet de prouver la normalisation forte de CC et Fu donc la coh rence de l arithm tique d ordre sup rieur et a fortiori de l arithm t
150. nalyse ult rieure sur le programme qui permet de s affranchir localement des occurrences de b B Type qui s av rent purement logique Int r t s mantique la distinction entre Prop et Set La distinction entre Prop et Set est utile sur le plan s mantique En effet certaines extensions logique classique extensionnalit interagissent mal avec les aspects constructifs du Calcul des Constructions Inductives Les prendre en compte simplement sur la sorte Prop permet de ne pas d truire la coh rence du syst me 6 3 3 Autres m thodes d analyse Tous les assistants de preuves permettant de manipuler des programmes int grent une certaine notion d objets logiques Dans le syst me Nuprl on utilise un op rateur pour cacher le contenu calculatoire des preuves analogue notre construction D autres syst mes privil gient la notion de sous ensemble ou bien donnent un statut logique des propri t s particuli res comme l galit Toutes ses m thodes sont h rit es de la notion logique de formule non calculatoire Le d faut de cette m thode est qu elle ne permet pas de supprimer du programme certains arguments inutiles C est le cas des listes de longueur n le constructeur cons aura pour type n nat A gt list n gt list S n ce qui laisse un terme extrait de type nat A list gt list dans lequel chaque constructeur est appliqu un argument de type entier repr sentant la longueur de l
151. nition en ML let rec plus nm match n with 0 gt m S p gt S plus p m et l quivalent en syntaxe Coq Coq lt Fixpoint plus n m nat struct n nat Coq lt match n with Coq lt O0 gt m Coq lt S p gt S plus p m Coq lt end Et voici de m me une d finition de la multiplication Coq lt Fixpoint mult n m nat struct n nat Coq lt match n with Coq lt O gt 0 Coq lt S p gt plus m mult p m Coq lt end La notion de r cursion structurelle On comprend bien que la construction Fixpoint correspond la d finition d une fonction r cursive au m me titre que le let rec de ML On note en revanche que le premier des deux arguments de chacune des deux fonctions est syntaxiquement distingu par l emploi du mot cl 7 f vrier 2014 13 struct La raison en est simple lorsque la th orie des types comme ici est utilis e en tant que formalisme logique la coh rence du formalisme est essentiellement assur e par la propri t de normalisation c est a dire de la terminaison des calculs Une sommaire justification informelle pourrait tre donn e ainsi supposons qu il soit possible de d finir la fonction suivante Coq lt Fixpoint non_sens n nat nat non_sens n Il est alors clair que l objet non_sens 0 ne correspond math matiquement pas un entier naturel et ne saurait tre accept dans le formalisme On reviendra par la suite l
152. nitions sont autoris es on peut utiliser le sch ma d limination usuel sur la sorte impr dicative de la d finition inductive par contre l limination forte sur un pr dicat dont la sorte est Type ne peut pas leur tre appliqu e De telles d finitions inductives sont utiles pour coder des existentielles du second ordre qui servent elle m me coder des types abstraits on sait qu il existe un type avec certaines op ra tions sur ce type mais on ne peut pas acc der l implantation de ce type Un exemple de telle utilisation est la d finition nu dans contribs Lyon GFP v qui code un plus grand point fixe d un op rateur monotone sur les types La distinction entre Prop et Set Les sortes Prop et Set sont toutes les deux de type Type Leur interpr tation diff re vis vis de l extraction de programmes partir de preuves Un terme de preuve est dit logique s il est de type P Prop le typage garantit qu il ne servira pas de mani re calculatoire pour construire un terme de preuve calculatoire de type S Set Ceci permet d liminer les termes de preuve logique qui sont toujours en position de code mort dans les termes calculatoires Si un type inductif est de type Prop alors on ne peut pas en g n ral autoriser une limination sur la sorte Set En effet la r gle d limination est Tha noma a TFP Y a A a Ar nom ai ay gt 5 Pipettes CL 2m Cle PEL at Com 274278 m E 1 p TF Case P
153. nnelle les notions primitives sont l limination non r cursive qui cor respond l analyse par cas et les d finitions par point fixe videmment on ne peut autoriser n importe quel point fixe sous peine de construire des termes non normalisables et d aboutir une incoh rence Une condition syntaxique de garde permet d accepter les d finitions qui suivent un sch ma primitif r cursif et de pr server la terminaison Pour cela une fonction f peut tre d finie par point fixe si un de ses arguments x a pour type une d finition inductive et si dans le corps de f tous les appels r cursifs f se font avec en place de x un terme t que l on reconna t syntaxiquement comme tant plus petit que x La r gle principale pour tre structurellement plus petit que x est d apparaitre dans une branche d un Case sur x et d tre l un des sous termes de x Mais cette d finition peut tre tendue Par exemple un Case est reconnu plus petit que x si chacune de ses branches est plus petite que x en particulier s il n y a aucune branche dans le cas de l limination d une condition absurde De m me tre plus petit est une op ration transitive Les points fixes de Coq sont repr sent s de mani re anonyme par un terme Fix f n T t dans lequel f est une variable li e et n est un entier positif ou nul La r gle de typage est TrT f THt T_ f est gard e dans t par le n 1 me argument TE Fix f n T t T La r gle
154. ode tree gt Z gt tree gt tree 86 7 f vrier 2014 87 et une relation d appartenance In indiquant qu un l ment apparait dans un arbre ind pendam ment de tout choix de rangement des l ments dans les arbres Coq lt Inductive In x Z tree gt Prop Coq lt In_left forall 1 r y In x 1 gt In x Node 1 y r Coq lt In_right forall 1 r y In x r gt In x Node 1 y r Coq lt Is_root forall 1 r In x Node 1 x r Une fonction de test de l ensemble vide peut alors s crire Coq lt Definition is_empty s tree bool match s with Coq lt Empty gt true Coq lt _ gt false end et sa preuve de correction s nonce ainsi Coq lt Theorem is_empty_correct Coq lt forall s is_empty s true lt gt forall x In x s La preuve suit la d finition de is_empty et tient en trois lignes Coq lt Proof Coq lt destruct s simpl intuition Coq lt inversion_clear HO Coq lt elim H with z auto Coq lt Qed Venons en au test d occurrence dans un arbre binaire de recherche On commence par se donner une relation d ordre ternaire sur les entiers relatifs Coq lt Inductive order Set Lt Eq Gt Coq lt Hypothesis compare Z gt Z gt order Puis on d finit une fonction mem de recherche dans un arbre suppos tre un arbre de recherche Coq lt Fixpoint mem x Z s tree struct s bool match s with Coq lt
155. ogic monochrome colorarray int int color gt prop axiom moni forall t colorarray forall i int forall j int forall c color monochrome t i j c gt forall k int i lt k lt j gt acc t k c axiom mon2 forall t colorarray forall i int forall j int forall c color forall k int i lt k lt j gt acc t k c gt monochrome t i j c 7 f vrier 2014 111 et le programme principal est alors let flag fun t colorarray ref gt forall k int 0 lt k lt length t gt iscolor acc t k begin let b ref O in let i ref O in let r ref length_ t in while i lt r do invariant forall k int 0 lt k lt length t gt iscolor acc t k and 0 lt b and b lt i and i lt r and r lt length t and monochrome t 0 b BLUE and monochrome t b i WHITE and monochrome t r length t RED variant r i let c acc_ t i in if eq_color c BLUE then begin swap t b i b b 1 i i 1 end else if eq_color c WHITE then i li 1 else begin r r 1 swap t r i end done end exists r int exists b int monochrome t 0 b BLUE and monochrome t b r WHITE and monochrome t r length t RED Notons que les onze obligations de preuves engendr es pour ces deux programmes swap et flag sont prouv es enti rement automatiquement par Simplify 8 3 2 Programmes Java et C L approche ci dessus pour les tableaux simples peut tre tendue
156. on de la fonction sp cifi e l aide d un type d pendant Coq lt Definition mem_bool x s h bst s match mem x s h with Coq lt left _ gt true Coq lt right _ gt false Coq lt end 7 f vrier 2014 98 Il est alors ais de montrer la correction de cette fonction pure car la preuve est contenue dans le type de la fonction d origine Coq lt Theorem mem_bool_correct Coq lt forall x s forall h bst s Coq lt mem_bool x s h true lt gt In xs Coq lt Proof Coq lt intros Coq lt unfold mem_bool simpl case mem x s h intuition Coq lt discriminate H Coq lt Qed Mais cette projection a peu d int r t en pratique Note Il est important de noter que chaque fonction se voit maintenant donner sa sp cification d s sa d finition il n est plus aussi facile de montrer plusieurs propri t s d une m me fonction que dans le cas d une fonction pure 7 2 4 Sp cification dans les types de donn es L ajout de sp cification dans les types ML peut galement s appliquer aux types r cursifs Ainsi on peut introduire le type d pendant des arbres ayant la propri t d tre des arbres binaires de recherche Coq lt Inductive bst_tree Set Coq lt Bst_tree forall t bst t gt bst_tree Il s agit l d un couple d pendant constitu d un arbre t dans la sorte Set et d une preuve de bst t dans la sorte Prop Un tel inductif a un constructeu
157. one Affirmation la fin de l ex cution de ce programme count est la racine carr de n arrondie l entier inf rieur 8 1 1 S mantique op rationnelle Un tat d un programme est une table d association E qui chaque variable x du programme associe sa valeur courante E x La valeur d une expression bien typ e e dans un tat E est d finie par E n n E x E x E e op e2 E e1 op E e2 La s mantique op rationnelle de ce langage est d finie par les r gles de transition sur toute instruction bien typ e E E z E e z e E E3 si Ey r et E Es 21522 12 Ey E si Ei e j true et Ey re if e then iz else i2 i FE E gt si Ei e false et Ey Fu Eo if e then iz else i2 E gt Ez si E e true Ey et Bp gt while e do i i while e do i E E si E e false 101 7 f vrier 2014 102 8 1 2 Logique de Hoare Un triplet de Hoare est un triplet not P i Q ot P et Q sont des assertions logiques et i une instruction Ces assertions logiques sont des formules du premier ordre avec comme formules atomiques les expressions de notre langage Remarque importante il y a ainsi identification entre les variables du programme et les variables de la logique On dit qu un triplet de Hoare P i Q est valide si pour tous tats E1 et E gt tels que FE E gt et P est vraie dans E Q est vraie dans Fo v Exemples de triplets valides x 1 x x 2 x 3 x y x x y
158. orrespond en th orie des ensembles un ensemble de profondeur w Par ailleurs la construction de chaque Type permet au plus d it rer w fois le produit fonctionnel partir de Type Les fonctions tant repr sent es en th orie des ensembles par des relations une fonction de type B correspond en th orie des ensembles une partie de l ensemble produit A x B et plus g n ralement une fonction de type Ilx A B x est une partie de A x Urea B x Ainsi l ensemble de fonctions IIx A B x se construit en ajoutant un niveau d imbrication au maximum des niveaux de A et des B x Les types de Type ont donc un nombre fini de niveaux d imbrication en plus du niveau d imbrication de Type En passant la limite le type Type lui m me a donc w niveaux d imbrication en plus que Type On arrive de la sorte tablir que Type contient des ensembles de niveaux d imbrication ensemblistes w i En passant la limite une nouvelle fois on tablit que ECC doit contenir des ensembles de niveau d imbrication au moins w Par ailleurs P A Melli s et B Werner MW98 ont exhib un mod le de cette cardinalit montrant que la force ordinale de ECC tait bien w it ration w des parties 4 Une premi re version de CC avec univers appara t dans la th se de T Coquand Coq85 sous le nom de Calcul des Constructions G n ralis GCC c est une version sans la r gle Prop C Type et dont le sous typage appel
159. orter une information servant au calcul du t moin y Par exemple si on prouve Vn m n lt m gt 2p n p m par induction sur la preuve de n lt m alors le calcul de la diff rence entre n et m d pendra de cette preuve Elle ne pourra plus tre consid r e comme non calculatoire et devra tre donn e en argument au programme On s int ressera caract riser certaines formules P x dont les preuves ne contiennent pas d information calculatoire int ressante C est le cas par exemple des formules de Harrop qui sont des formules n ayant pas de disjonction ou de quantificateur existentiel en partie strictement positive par exemple toutes les formules P Nous allons nous int resser maintenant des m thodes pour obtenir partir d une preuve in tuitionniste de Vx P x gt 4y Q x y effectivement un programme f et une preuve de correction Va P x gt Q x f x 6 2 R alisabilit 6 2 1 Principes g n raux La r alisabilit a t introduite par Kleene en 1945 C est une interpr tation s mantique des propositions en logique intuitionniste On se donne un ensemble de r alisations qui repr sentent des programmes Chaque proposition P est interpr t e comme un ensemble de r alisations qui est d fini en g n ral par r currence sur la structure de la formule P Cet ensemble est d fini intentionnellement par une propri t de r alisabilit x r P dans lequel x est une nouvelle variable libr
160. par le pr dicat valnat Coq lt Inductive valbool semval gt Prop Coq lt valbool_intro forall b bool valbool Bool b Coq lt Inductive valnat semval gt Prop Coq lt valnat_intro forall n nat valnat Nat n Coq lt Definition compat s sort v semval Prop lt Coq lt match s with Coq lt Sbool gt valbool v Coq lt Snat gt valnat v lt Coq end On remarque que le d finition inductive de valbool est un codage inductif direct de la propo sition fun x semval gt exists b bool x Bool b On peut ais ment montrer la correspon dance entre compat et sort_val Coq lt Theorem compat_sort_val Coq lt forall s sort v semval compat s v gt s sort_val v Une alternative est de repr senter la notion de compatibilit par un pr dicat inductif Coq lt Inductive compati sort gt semval gt Prop Coq lt compat_bool forall b bool compati Sbool Bool b Coq lt compat_nat forall n nat compati Snat Nat n Les deux d finitions sont quivalentes remarquons que dans le second cas la propri t compati Snat v gt dn nat v Nat n n cessite une inversion du pr dicat inductif alors que dans le cas de compat c est une simple cons quence du calcul de l expression Cases et de la d finition de valnat 7 f vrier 2014 27 La m moire La m moire est repr sent e comme une fonction qui 4 toute variable et sorte associe une val
161. pe s exprime dans le CCI par la formule lg A P x gt Sa A P x Tout comme le principe de description ind finie dans sa version constructive la description d finie est d rivable dans sa version constructive si A est d nombrable et P d cidable Axiome du choix relationnel L axiome du choix sous sa forme relationnelle s exprime par Va Ab B P a b 2P Va Ab B P a b A P a b AW B P a b gt b b L axiome du choix relationnel l axiome de choix unique est quivalent l axiome du choix fonctionnel Dans les conflits entre logique classique axiome du choix et impr dicativit de Set c est la composante choix unique qui pose probl me En effet cette derni re en pr sence de la logique classique peuple le monde des fonctions d objets non calculables ce qui est incompatible avec la vision du monde requise par l impr dicativit vision pour laquelle seules existent les fonctions qui sont calculables Ainsi l axiome du choix avec sa r elle capacit ordonner les domaines non d nombrables n a semble t il rien d incompatible avec logique classique et impr dicativit si l on se restreint sa formulation relationnelle 7 f vrier 2014 119 Extensionnalit des pr dicats et axiome du choix L extensionnalit des pr dicats l axiome du choix m me sous une forme relationnelle qui n implique pas l axiome de description entra ne la logique
162. r Inductive W A Set B A Set Set node Vx A B x WA B gt WAB Ce type est suffisant pour coder les autres d finitions inductives Par exemple pour repr senter les entiers on remarque qu il nous faut deux types de branchement lun pour 0 qui est d arit nulle et l autre pour S qui est d arit un Il suffit donc de prendre A bool et B d finie par B true False et B false True On pose alors nat W A B On peut alors introduire 0 node true At False gt Case nat t et S An nat node false At True gt n dont on v rifie qu ils ont le bon type Un autre type r cursif int ressant est la d finition d un l ment bien fond x A pour une relation R A A Prop On dit que x est bien fond si tous les l ments en relation avec x sont eux m mes bien fond s Cela s crit Inductive wf A Set R A A Prop A Prop wf_intro Vr A Vy A R y z gt wf AR y gt wi AR x 7 f vrier 2014 47 3 3 2 Condition de positivit Positivit large Un type inductif qui comporterait une occurrence r cursive n gative permet de construire des objets qui bouclent sans utiliser de r cursivit Supposons que l on puisse d finir Inductive L Set lam L gt L gt L et que l limination sur la sorte Set soit permise Ce type est habit puisqu il contient au moins le terme lam x L On peut galement d finir Defini
163. r Coq lt Xor expr gt expr gt expr Coq lt Num nat gt expr Coq lt Null expr gt expr Coq lt Opn op gt expr gt expr gt expr Expressions correctes Le pr dicat exprcorrect traduit la relation d crite dans la figure 2 3 Chaque r gle d inf rence d finissant la relation est traduite en un constructeur de la d finition inductive Les variables libres des d finitions deviennent des variables quantifi es universellement dans les constructeurs Coq lt Inductive exprcorrect sort gt expr gt Prop Coq lt corvar forall n name s sort exprcorrect s Var n s Coq lt cortr exprcorrect Sbool Tr Coq lt corfa exprcorrect Sbool Fa Coq lt corxor Coq lt forall b c expr Coq lt exprcorrect Sbool b gt Coq lt exprcorrect Sbool c gt exprcorrect Sbool Xor b c Coq lt cornum forall n nat exprcorrect Snat Num n Coq lt cornull Coq lt forall e expr exprcorrect Snat e gt exprcorrect Sbool Null e Coq lt corop Coq lt forall o op e f expr Coq lt exprcorrect Snat e gt Coq lt exprcorrect Snat f gt exprcorrect Snat Opn o e f Domaines s mantiques Il s agit de repr senter le domaine s mantique des variables chaque sorte de variable cor respond un ensemble au sens math matique qui sera repr sent par un type de donn es Coq ici le type des bool ens ou des entiers Le domaine s mantique des valeurs
164. r gt colorarray mise jour t i c axiom length_pos forall t colorarray 0 lt length t axiom length_up forall t colorarray forall i int forall v color length update t i v length t 7 f vrier 2014 110 axiom acc_up_eq forall t colorarray forall i int forall v color acc update t i v i v axiom acc_up_neq forall t colorarray forall i int forall j int forall v color i lt gt j gt acc update t i v j acc t j et on a les programme WHY suivant sur les tableaux parameter length_ t colorarray gt int result length t parameter acc_ t colorarray gt i int gt 0 lt i lt length t color result acc t i parameter update_ t colorarray ref gt i int gt v color gt 0 lt i lt length t unit reads t writes t t update t i v noter les pr conditions sur les bornes des tableaux utilis s On peut maintenant commencer par un petit programme qui echange deux l ments d un tableau let swap fun t colorarray ref i int j int gt 0 lt i lt length t and 0 lt j lt length t let ti acc_ t i in let tj acc_ t j in begin update_ t i tj update_ t j ti end length t length t and acc t i acc t j and acc t j acc t i and forall k int i lt gt k and j lt gt k gt acc t k acc t k Pour crire le programme de tri de Dijkstra on introduit un predicat monochrome l
165. r P Set X r Set X Prop Fr x A B x E A Fr B A Set B Type Fr x A B X E A X X r A F X rB A B Type FIGURE 6 5 R alisabilit dans CC x r P pour P Type Exercice A quelle condition un terme p r alise t il une preuve de l galit d finie avec A Set par P A gt Set P t gt P u 6 3 2 Distinction entre Prop et Set L oubli des types d pendants n est pas suffisant il est important de pouvoir liminer les parties de la preuve qui ne servent pas au calcul du r sultat La notion de formule de Harrop nest pas naturelle dans un cadre d ordre sup rieur o il n y a pas de formule atomique autre que les variables de pr dicats 7 f vrier 2014 81 R X Xe X variable de pr dicat R P t R P E t t A Set R PT R P E T R Z T A Type R x AJP z E A R P Set R X AJP X E A X X r A R P A Type R P jx E P z r P si P est un produit FIGURE 6 6 R alisabilit dans CC R P pour P B Type Pour rem dier cela Coq propose une distinction entre deux sortes Prop et Set Les deux sortes sont impr dicatives ce qui justifie les bonnes propri t s du syst me il suffit d identifier Prop et Set pour retrouver le calcul initial L interpr tation de t A lorsque A Prop est que A est v rifi e et que la preuve t de A ne sert pas au calcul L interpr tation de t A lorsque Set est que t est une preuve calculatoire de A dont il
166. r est un record type enregistrement Coq lt Record bst_tree Set Coq lt t gt tree Coq lt bst_t bst t Coq lt Note La notation gt introduit une coercion du type bst_tree vers le type tree la premi re projection Ceci permet par exemple d appliquer directement le pr dicat In a une valeur du type bst_tree 7 3 Modules et foncteurs L ad quation de Coq comme formalisme de sp cification et de preuve de programmes ML purement fonctionnels s tend jusqu au syst me de modules En effet Coq est depuis peu quip d un syst me de modules inspir de celui d Objective Caml Ler00 Chr03a Chr03b De m me que les types de fonction Coq peuvent enrichir ceux de ML par des annotations logiques les modules de Coq peuvent enrichir ceux de ML Ainsi si l on souhaite crire notre biblioth que d ensembles finis sous la forme d un foncteur prenant en argument un type quelconque et non plus Z comme jusqu pr sent quip d un ordre total on commence par d finir une signature pour cet argument On y met un type t une galit eq et une relation d ordre 1t sur ce type 7 f vrier 2014 99 Coq lt Module Type OrderedType Coq lt Parameter t Set Coq lt Parameter eq t gt t gt Prop Coq lt Parameter lt t gt t gt Prop ainsi qu un r sultat de d cidabilit de 1t et eq Coq lt Parameter compare forall x y lt x y eq x y 1t y x Il faut g
167. r l application incr2 t t Si c tait accept alors au vu de la post condition de incr2 la post condition t t 1 serait prouvable or elle est fausse Cest t t 2 qui est vrai Exercice 2 D river le jugement de typage montant int ref crediter int unit montant montant 0 0 On peut utiliser cette approche de typage avec effets pour d finir des programmes Why de fa on modulaire un programme peut tr s faire appel une autre fonction dont le code n est pas donn cette fonction doit seulement tre sp cifi e par son type avec effets ainsi qu avec un pr et une post condition Par exemple on peut crire parameter montant int ref parameter crediter s int gt s gt 0 unit reads montant writes montant montant s montant let test fun tt unit gt true begin crediter 50 crediter 80 end montant montant 130 8 2 3 Calcul de plus faible pr condition Avec l inf rence de type avec effets on est capable d associer chaque sous expression d un programme un type avec effets L tape suivante consiste leur associer aussi une pr et une post condition de deux choses l une soit l expression consid r e est d j annot e une boucle while un identificateur de fonction ou une expression explicitement annot e par l utilisateur soit on lui d termine une annotation par calcul de plus faible pr condition d une mani re tr s similaire
168. ramming 13 4 709 745 July 2003 Fil03b Jean Christophe Filli tre Why a multi language multi prover verification tool Research Report 1366 LRI Universit Paris Sud March 2003 http www lri fr filliatr ftp publis why tool ps gz FL04 Jean Christophe Filli tre and Pierre Letouzey Functors for Proofs and Programs In Proceedings of The European Symposium on Programming Barcelona Spain March 29 April 2 2004 Voir aussi http www lri fr filliatr fsets Geu01 Herman Geuvers Induction is not derivable in second order dependent type theory In TLCA pages 166 181 2001 Gim95 Eduardo Gim nez Codifying guarded definitions with recursive schemes In P Dybjer B Nordstr m and J Smith editors Types for Proofs and Programs TYPES 94 volume 996 of LNCS pages 39 59 Springer Verlag 1995 Gim96a Eduardo Gim nez An application of co inductive types in Coq Verification of the alternating bit protocol In Stefano Berardi and Mario Coppo editors Types for Proofs and Programs TYPES 95 volume 1158 of LNCS 1996 Gim96b Eduardo Gim nez Un Calcul de Constructions Infinies et son application la v rification de syst mes communicants Th se d universit Ecole Normale Sup rieure de Lyon December 1996 Gim97 Eduardo Gim nez A certification of Petersson s algorithm for managing mutual exclusion Coq s Contributions 1997 Gim98 Eduardo Gim nez A tutorial on recursive types in coq R
169. rdinal_rec2 Puis on filtre sur x et x les deux cas Empty tant triviaux Coq lt destruct x Coq lt x Empty Coq lt intros exact true Coq lt x Node x1 z x2 Coq lt destruct x Coq lt x Empty Coq lt intros exact false On proc de ensuite par cas sur le r sultat de compare z z0 Coq lt x Node x 1 z0 x 2 Coq lt intros case compare z z0 Dans chacun des trois cas les appels r cursifs hypoth se H se font l aide de la tactique refine on alors une obligation de montrer la d croissance du nombre d l ments ce qui est automatiquement prouv par simpl omega simpl est n cessaire pour d plier la d finition de cardinal _tree Coq lt z lt 20 Coq lt refine andb H Node x1 z Empty x 2 _ Coq lt H x2 Node x 1 z0 x 2 _ simpl omega Coq lt z z0 Coq lt refine andb H x1 x 1 _ H x2 x 2 _ simpl omega Coq lt z gt z0 Coq lt refine andb H Node Empty z x2 x 2 _ Coq lt H x1 Node x 1 z0 x 2 _ simpl omega Coq lt Defined Note On aurait pu galement faire une d finition l aide d un unique refine Note I est int ressant d examiner le code extrait d une fonction d finie l aide d un r curseur tel que well_founded_induction On peut commencer par regarder directement le code extrait pour well_founded_induction et l on reconna t un op rateur de poin
170. reprenant naturellement celle de la fonction hypoth se h et ajoutant bst s La pr sence de h est m me n cessaire pour pouvoir appliquer la fonction min_elt On voit que l utilisation d une fonction partielle en Coq n est pas simple il faut passer en argument des termes de preuve souvent difficiles construire La d finition m me d une fonction partielle est souvent d licate Ecrivons une fonction min_elt ayant le type 7 1 Le code ML que l on a en t te est le suivant let rec min_elt function Empty gt assert false Node Empty x _ gt x Node 1 _ _ gt min_elt 1 Malheureusement la d finition en Coq est plus difficile D une part l assert false dans le pre mier cas de filtrage correspond un cas absurde on a suppos l arbre non vide La d finition en Coq exprime cette absurdit l aide du r curseur False_rec appliqu une preuve de l absurde Il faut donc construire une telle preuve partir de la pr condition De m me le troisi me cas de filtrage fait un appel r cursif min_elt et pour cela on doit construire une preuve que l argument 1 n est pas vide C est ici une cons quence du filtrage qui a limin le cas o 1 est Empty Dans ces deux cas la n cessit de construire ces termes de preuve complique le filtrage qui doit tre d pendant On obtient la d finition suivante Coq lt Fixpoint min_elt s tree h s Empty struct s Z Coq lt match
171. roduc tion de types de donn es assez complexes Il est plus naturel d utiliser une d finitions structurelle de l galit Deux objets co inductifs sont gaux si ils commencent par le m me constructeur et que les composantes sont gales videmment dans le cas d objets infinis on ne peut utiliser une d finition inductive de l galit Il faut avoir recours une d finition co inductive pour capturer l galit d objets infinis Dans le cas des streams cela donne Coq lt Parameter A Set A is assumed Coq lt CoInductive EqStream Stream A gt Stream A gt Prop Coq lt EqStream_intro forall si s2 Stream A head si head s2 gt Coq lt EqStream tail s1 tail s2 gt EqStream s1 s2 EqStream is defined Une variante quivalente est 7 f vrier 2014 62 Coq lt CoInductive EqStream2 Stream A gt Stream A gt Prop Coq lt EqStream2_intro forall a A si s2 Stream A Coq lt EqStream2 si s2 gt EqStream2 Cons a s1 Cons a s2 EqStream2 is defined Les preuves de d finitions de relations co inductives suivent les m me r gles que les types coin ductifs On peut leur appliquer des analyses par cas des inversions ou bien construire des preuves par co it ration co r cursion ou plus g n ralement par point fixe gard Cette derni re m thode s av re la plus souple Cependant sa manipulation pour la construction de preuves peut tre parfois d licate En effet les preuves sont
172. roduire un constructeur silencieux pour les listes r sultats qui sera introduit dans le cas o l l ment ne v rifie pas P On peut aussi ajouter un l ment de preuve qui va garantir que P est vrai infiniment souvent dans s 4 3 D finition des types co inductifs dans Coq Nous montrons maintenant les diff rentes constructions disponibles dans Coq pour manipuler les structures infinies 7 f vrier 2014 58 4 3 1 Types de donn es infinis Ceux ci se sp cifient l aide d une construction analogue celle des d finitions inductives mais utilisant le mot cl CoInductive On a vu la d finition du type des listes L op ateur de destruction par filtrage Cases traite de la m me mani re les d finitions induc tives et coinductives Il exprime juste qu une valeur dans le type concret est form partir de l un des constructeurs du type 4 3 2 Conditions de gardes Les d finitions d objets infinis se font l aide d un point fixe gard par des constructeurs il n y a pas besoin de sp cifier d argument de d croissance comme dans le cas de d finition inductive Exemples de streams sur les entiers Coq lt CoFixpoint zeros Stream nat Cons 0 zeros zeros is corecursively defined Coq lt CoFixpoint from n nat Stream nat Cons n from S n from is corecursively defined Coq lt Parameter n nat n is assumed Coq lt CoFixpoint puis nk nat Stream nat Cons nk puis nk n pui
173. roduit un axiome qui dit que Vie x x p P x Case P e p p qui ne dit pas que e est gal refl x mais qu il se comporte calculatoirement de mani re identique galit de John Major C McBride McB99 a introduit une galit qui permet de comparer deux objets dans des types quelconques De mani re inductive cette galit se d finit par Inductive eq A Set x A YB Set B Prop refl eq A A x x On peut facilement prouver que cette galit est r flexive sym trique et transitive en utilisant le sch ma g n ral des d finitions inductives Par contre ce sch ma impose une g n ralisation du but sous la forme d un pr dicat de type VB Set B Prop ce qui est en g n ral malais C McBride propose d introduire un sch ma d limination renforc analogue et prouvable ment quivalent axiome K de Streicher Ce sch ma d limination dit que si deux objets de m me type sont gaux selon l galit de John Major alors on peut remplacer l un par l autre autrement dit ils sont gaux au sens de l galit de Leibniz P A s e eqAxAy q P x Case P e q P y Cette galit est commode car si on a n nat et l list n ainsi que n nat et l list n on pourra simplement crire eq nat n nat n et eq list n List n l Comme n et n sont du m me type on pourra remplacer n par n en particulier dans le type de l ensuite et l
174. rte soit un produit soit un Case soit un point fixe On proc de par r currence sur la structure du terme et on examine chaque cas cne peut pas tre une abstraction car t est normal et dans le cas n 0 le type de t serait un produit cne peut pas tre une variable car t est clos cne peut pas tre une sorte ou un produit car on aurait n 0 et le type de t serait une sorte 7 f vrier 2014 75 cne peut pas tre un Case car l argument principal du Case est un terme clos dans un type inductif et donc par hypoth se de r currence commencerait par un constructeur et t ne serait pas normal de m me c ne peut pas tre un point fixe en effet un point fixe a pour type x Aj p Ap B avec x l argument de d croissance dont le type est inductif c serait au moins appliqu p arguments sinon le type est un produit donc p lt n et tp clos et normal commencerait par un constructeur et t ne serait pas normal donc c est un constructeur dont le type est x A1 p Ap J avec I une instance d un type inductif On a p n car c ne peut tre appliqu au plus qu p arguments et doit au moins tre appliqu 4 p arguments pour que son type soit un type inductif Justification de la constructivit Si AV B est prouvable sans hypoth se alors il existe une preuve de V B donc un terme clos de type A V B qui est un type inductif deux constructeurs Inductive or A B Set Set or
175. rvir galement montrer que certaines formules ne sont pas d mon trables comme cons quence du fait qu elles ne sont pas r alisables 6 2 2 Diff rentes notions de r alisabilit Il y a de tr s nombreuses notions de r alisabilit adapt es aux propri t s que l on cherche montrer Elles se distinguent par la nature du langage de r alisation on peut en effet prendre des entiers repr sentant des codes de fonction ou bien un lambda calcul pur ou typ ou tout autre langage Ensuite on peut mettre diff rents ingr dients dans les formules de r alisabilit Par exemple f appartient l interpr tation de A B peut tre d fini comme pour tout a dans l interpr tation de A f a termine et est dans l interpr tation de B ou bien on peut de plus demander que B soit d montrable etc Les preuves de normalisation par les m thodes de candidat de r ductibilit peuvent se voir comme des cas particuliers de m thode de r alisabilit On peut d finir la r alisabilit de mani re s mantique ou au contraire de mani re syntaxique on parle de r alisabilit abstraite la propri t x r P qui dit qu une r alisation x est dans l interpr tation d une formule P est d finie comme une formule du syst me logique lui m me d finie en g n ral dans un fragment plus faible on limine les connecteurs intuitionnistes 4 et V Plus d information sur la r alisabilit peut se trouver dans les livres de Troelstra Tro73 Troel
176. s P skip P PIX El X E P On remarque que toutes ces d finitions font intervenir des notions d finies dans le m ta langage telles que la m moire les domaines s mantiques les op rations sur ces domaines 2 2 4 Quelques propri t s Parmi les propri t s int ressantes montrer on a D cidabilit de la correction par rapport la s mantique statique algorithme de typage Toute expression correctement typ e admet une valeur Correction de la s mantique axiomatique Si P C Q est v rifi alors toute valuation de C dans une m moire qui v rifie P conduit une m moire qui v rifie Q 2 3 Sp cification Gallina Nous montrons comment repr senter la th orie pr c dente en Gallina 2 3 1 Les expressions D finitions On choisit de repr senter les variables et les op rateurs binaires par des ensembles param triques qui pourront tre instanci s dans un second temps Par contre les fonctions bool ennes sont repr sent es de mani re concr te par un constructeur du type de donn es Ce choix permet d illustrer deux traitements possibles des op rations du langage que l on cherche mod liser Coq lt Parameter name Set Coq lt Inductive sort Set 7 f vrier 2014 25 Coq lt Sbool sort Coq lt Snat sort Coq lt Parameter op Set Coq lt Inductive expr Set Coq lt Var name gt sort gt expr Coq lt Tr expr Coq lt Fa exp
177. s is corecursively defined D finitions des op rateurs de co it ration et co r cursion Coq lt Variables X Set A is assumed X is assumed Coq lt Variable out X gt A out is assumed Coq lt Variable tran X gt X tran is assumed Coq lt CoFixpoint Stream_coiter x X Stream A Coq lt Cons out x Stream_coiter tran x Stream_coiter is corecursively defined Coq lt Variable tran_rec X gt X Stream A tran_rec is assumed Coq lt CoFixpoint Stream_corec x X Stream A Coq lt Cons out x Coq lt match tran_rec x with Coq lt inl x gt Stream_corec x Coq lt inr s gt s Coq lt end Stream_corec is corecursively defined 7 f vrier 2014 59 La condition de garde stipule qu un appel r cursif ne peut avoir lieu que sous au moins un constructeur et il doit alors tre en position d argument r cursif et sous uniquement des constructeurs en particulier un appel r cursif ne doit pas se trouver en position d argument d un symbole de fonction ou dans la partie principale d un filtrage par contre il peut tre dans la branche d une d finition par cas Par exemple pour d finir la fonction map sur les streams Coq lt Variable B Set B is assumed Coq lt Variable f A gt B f is assumed Coq lt CoFixpoint map s Stream A Stream B Coq lt match s with Coq lt Cons a 1 gt Cons f a map 1 Coq lt end map is corecursi
178. s return s Empty gt Z with Coq lt Empty gt Coq lt fun h gt False rec _ h refl_equal Empty Coq lt Node 1 x _ gt Coq lt fun h gt match 1 as a return a l gt Z with Coq lt Empty gt fun _ gt x Coq lt _ gt fun h gt min_elt 1 Coq lt Node_not_empty _ _ _ _ h Coq lt end refl_equal 1 Coq lt endh La premi re preuve argument de False_rec est construite directement La seconde fait appel au lemme suivant Coq lt Lemma Node_not_empty forall 1 x r s Node 1 x r s gt s Empty On peut alors prouver la correction de cette fonction Coq lt Theorem min_elt_correct Coq lt forall s h s Empty bst s gt Coq lt In min_elt s h s Coq lt forall x In x s gt min_elt s h lt x L encore la preuve se fait en suivant la d finition de la fonction et ne pose pas de probl me On peut v rifier que le code extrait est bien celui que l on avait en t te Extraction min_elt donne en effet let rec min_elt function Empty gt assert false absurd case Node 1 x t gt match 1 with Empty gt x Node t0 z0 t1 gt min_elt 1 7 f vrier 2014 90 Plusieurs points sont noter d une part l utilisation de False_rec est extraite en assert false ce qui est exactement le comportement souhait on a fait une preuve que ce point de programme est inatteignable il est donc l gitime de dire qu arriver l est absurde
179. semval est repr sent par la somme disjointe des deux types Coq lt Inductive semval Set Coq lt Bool bool gt semval Coq lt Nat nat gt semval Interpr tation des fonctions Les fonctions s mantiques correspondant aux op rateurs concrets peuvent tre explicitement programm es Par contre la s mantique des op rations arithm tiques qui sont vues de mani re param trique doit tre fournie comme un param tre 7 f vrier 2014 26 Coq lt Definition boolxor b1 b2 bool bool Coq lt if b1 then if b2 then false else true else b2 Coq lt Definition iszero n nat bool Coq lt match n with Coq lt 0 gt true Coq lt S n gt false Coq lt end Coq lt Parameter semop op gt nat gt nat gt nat Compatibilit entre sortes et valeurs I nous faudra relier la sorte des expressions et le type de leur interpr tation s mantique Pour cela on d finit sort_val une fonction des domaines s mantiques dans les sortes qui chaque valeur s mantique associe la sorte correspondante Coq lt Definition sort_val v semval sort Coq lt match v with Coq lt Bool b gt Sbool Coq lt Nat n gt Snat Coq lt end On utilisera galement une relation compat entre les valeurs et les sortes telle que compat Sbool v soit quivalent 4b bool v Bool b d fini par le pr dicat valbool et compat Snat v soit quivalent dn nat v Nat n d fini
180. sous programmes Prouver la terminaison des programmes terminaison des boucles while Supporter les break continue les exceptions Avoir des structures de donn es complexes tableaux structures pointeurs objets etc Travailler sur des entiers born s et v rifier le non d bordement des op rations sur les entiers 8 2 Transformation fonctionnelle la m thode Why Objectif g n ral tablir la validit d un triplet de Hoare non pas avec les r gles de d duction pr c dente mais avec une technique fond e sur le calcul des constructions inductives Cet objectif a t d velopp par Jean Christophe Filli tre Fil03a et implant e dans un outil logiciel appel e Why Fil03b Les programmes trait s par Why ne sont pas en PASCAL ni en C ou autre langage de programmation existant mais dans une syntaxe sp cifique qui a t con ue pour la preuve de ces programmes En Why toutes les difficult s mentionn es ci dessus sont trait es except s la possibilit d avoir des structures de donn es complexes et les entiers born s Dans la section suivante nous verrons la fois comment traiter les structures de donn es complexes et comment faire des preuves sur des programmes crits dans des langages de programmation imp ratifs standards Java ou C en l occurrence La figure 8 1 donne de nouveau le programme qui calcule la racine carr e crit cette fois sous forme d une fonction Why On remarqu
181. ssite l limination d pendante des inductifs de Prop Axiome du choix L axiome du choix forme fonctionnelle est d rivable si l existentielle not e alors comme un X type est dans Set ou dans Type Va X Xy Y P lt y gt Uf X gt YVx X P x fx Si l existentielle est dans Prop et Y dans Set l axiome est incoh rent en pr sence de la logique classique dans Prop car alors on peut injecter Prop dans bool et encoder le syst me U VX Type VA Set Vx X Ja A P x y gt 3f X gt ANVa X P x fx En fait une forme beaucoup plus faible de l axiome du choix bien que plus compliqu e expri mer savoir l axiome de description suffit obtenir cette contradiction Remarque Si Y est dans Type du fait du sous typage Set C Type la contradiction avec la logique classique persiste L axiome du choix unique Contrairement ce que son nom sugg re l axiome de choix unique ne choisit pas Ce qu ex prime l axiome du choix unique c est que toute relation fonctionnelle peut tre r ifi e en une fonction Va A d b B P a b gt 3f A gt BVa A P a fa Si l existentielle est dans Set ou Type l axiome est d rivable Dans Prop et avec B dans Set ou Type il entra ne l existence d une r traction de Prop vers bool Set Ainsi l axiome est incoh rent avec la logique classique dans Prop pour le CCI avec Set impr dicatif car alors on peut
182. ssus est plus souple par exemple voici une d finition possible en Coq du quotient de la division enti re par deux Coq lt Fixpoint div2 n nat nat Coq lt match n with Coq lt 0 gt 0 Coq lt 1 gt 0 Coq lt S S p gt S div2 p Coq lt end Il faut noter que cette fonction pourrait galement tre d finie dans le syst me T mais de mani re un peu plus lourde Il s agit donc l d un am nagement du formalisme qui n tend pas Vexpressivit du formalisme mais juste son confort d utilisation Dans un registre diff rent le m canisme de r cursion structurelle permet la d finition de fonctions logiquement complexes c est dire qui croissent tr s vite L exemple le plus connu est la fonction due Ackermann dont voici la d finition ML 7 f vrier 2014 14 let rec ack function O m gt S m S n 0 gt ack n S 0 S n S m gt ack n ack S n m La terminaison de cette d finition est assur e par une d croissance de la paire d arguments vis a vis de l ordre lexicographique En terme de r cursion structurelle ceci est cod par l utilisation de deux r cursions emboit es En Coq la syntaxe est alors un peu plus complexe la commande fix jouant le r le d un let rec in Coq lt Fixpoint ack n nat nat gt nat Coq lt match n with Coq lt 0 gt fun m nat gt S m Cog lt S n gt Coq lt fix aux m nat nat Coq lt m
183. stra et van Dalen TvD88 et Beeson Bee85 Nous d crivons trois notions de r alisabilit abstraite Pour cela nous nous plagons dans une arithm tique fonctionnelle du premier ordre qui est l arithm tique que l on tend de mani re pouvoir parler d objets fonctionnels repr sent s par des termes on consid re galement la possibilit de former la paire de deux objets Les objets de base sont les entiers Un pr dicat particulier z nat permet de distinguer les objets entiers De mani re usuelle on crira Vx nat P pour Vx x nat P et dx nat P pour 2x x nat A P La disjonction A V B est d finie comme Jb nat b 0 gt A A b40 gt B R alisabilit r cursive La r alisabilit r cursive a t introduite par Kleene Kle45 L en semble des r alisations est l ensemble des fonctions r cursives partielles Une r alisation est for c ment un objet qui a une valeur soit un entier qui peut repr senter le code d une fonction r cursive dans le cas de l arithm tique du premier ordre soit un entier ou une abstraction dans le cas de l arithm tique fonctionnelle On distingue un pr dicat t qui est vrai lorsque le terme t a une valeur Les quantifications portent implicitement sur les termes qui ont une valeur La d finition de la r alisabilit r cursive est d crite dans la figure 6 1 xr x 0AA A atomique zr AAB fst x r A snd x r B frA gt B Vr xr A gt
184. t Ax A x t Pour tant T Prop on en d duit l existence d un plongement o P I S7_ prop t de T Prop vers T Ce plongement est injectif par injectivit de I On pose alors P z T 3P x SOP ASP Par injectivit de on montre que Po Po est quivalent P Po Contradiction Bibliographie Arg98 AVL62 Balo2 Bar81 BB95 BB96 BC04 Bee85 Ber96 Ber98 CDDKS86 Chr03a Chr03b Coq Coq85 Coq86 Pablo Argon Etude sur l application de m thodes formelles la compilation et la validation de programmes ELECTRE Th se de doctorat cole Centrale de Nantes 1998 G M Adel son Vel skii and E M Landis An algorithm for the organization of information Soviet Mathematics Doklady 3 5 1259 1263 September 1962 Antonia Balaa Fonctions r cursives g n rales dans le calcul des constructions Th se de doctorat Universit de Nice Sophia Antipolis November 2002 Henk P Barendregt The Lambda Calculus its Syntax and Semantics North Holland 1981 Stefano Berardi and Luca Boerio Using subtyping in program optimization In Typed Lambda Calculus and Applications 1995 Franco Barbanera and Stefano Berardi Proof irrelevance out of excluded middle and choice in the calculus of constructions Journal of Functional Programming 6 3 519 525 1996 Yves Bertot and Pierre Cast ran Interactive Theorem Proving and Program D
185. t B Argument scopes are type_scope _ 1 3 3 Deux tactiques de base Construire une preuve revient dans notre formalisme exhiber un terme du type attendu L utilisateur dispose pour cela d un mode de preuve interactif Les commandes de ce mode interactif sont appel es tactiques de preuve Voici une illustration sommaire de leur principe sur un exemple simple on se donne trois variables propositionnelles A B et C puis l on cherche prouver la tautologie suivante Coq lt Variables B C Prop is assumed B is assumed C is assumed Coq lt Lemma exempt A gt B gt C gt B gt C 1 subgoal A Prop B Prop C Prop A gt B gt C gt B gt C On a alors le lemme comme seul but courant sous la double barre On peut commencer construire la preuve Coq lt intros c b 1 subgoal A Prop B Prop C Prop c A gt B gt C b 1 Rappelons qu en raison de la r gle de conversion un terme bien form peut avoir plusieurs types dans CC ou CCI 7 f vrier 2014 10 On voit que A gt B gt C et B ont t pouss es comme hypoth ses dans le contexte local au dessus de la double barre Elles ont t nomm es comme demand Du point de vue de la construction de la preuve cette tactique correspond la abstraction comme on peut le voir en affichant la preuve partielle construite Coq lt Show Proof fun c A gt B gt C b B gt 7 3 Une
186. t 1 1 else count On est ramen alors la preuve d un programme fonctionnel Il s agit l d une instance de l ap proche par plongement superficiel shallow embedding en anglais oppos plongement profond deep embedding tel qu expliqu dans le chapitre 2 8 2 1 Le langage Why C est un langage fonctionnel auquel sont rajout s quelques traits imp ratifs Les types de base sont int bool float et unit habit par la constante void Comme d habitude avec les langages fonctionnels il n y a pas de distinction syntaxiques entre expressions et instructions les instructions sont les expressions de type unit Le noyau fonctionnel est constitu des expressions suivantes les constantes enti res bool ennes flottantes et void les variables l application not e sous forme curryfi e e e1 en les op rations primitives unaires et binaires etc les d finitions locales let v e in e2 les conditionnelles if e1 then eg else e3 l abstraction not e fun z1 t1 Zn tn gt e Les traits imp ratifs sont introduits par les d finitions de r f rences locales let v ref eq in e2 7 f vrier 2014 105 la d r f renciation v l affectation v e la s quence e1 n la boucle while e do eg done Remarque pour simplifier on ne traite pas les d finitions r cursives ici ni la lev e et le rattrapage d exc
187. t R et donc en particulier les entiers ne sont pas born s 7 f vrier 2014 108 Interpr tation fonctionnelle des programmes On donne maintenant des r gles de traduction d une expression e de type avec effets T Ph t ri re wi wi Q dans un environnement T en un terme Coq trous de type T dans l environnement T obtenu en enlevant toutes les variables de type ref sie q variable Ax Ap P x 0 x 71 o 1 Q x0 0 2 sie r Xi Ap P io 0 toi 21 o zo est la variable correspondant x et 1 Q x6 0 xo si e z 1 o e ale type Pi t1 ri wi Qi E Ax Ap P x0 let di v q1 ex do 21 in ti x v tt 22 o 1 Pi et 2 Q x 41 D x v tt o di x v d signe le vecteur de variables 1 o la variable x correspondant x est remplac e par v si e fun x t gt e1 et t n est pas un type ref Ax Ap P x0 0 Av 7 71 o 1 Q o 0 Are sie e2 e1 alors e2 a un type avec effets annot de la forme P x t gt P t R W Q Ro W2 Q2 on distingue deux cas suivant e1 t non ref ei a le type Pi t1 Ri Wi Qi E AX Ap P let x1 a q1 Lo 1 in let gt f q2 0 P 1 2 in let 3 v q f a t 41 P 2 73 in Z D 22 B 3 v 24 o 1 Pi to 2 Po o di 3 P 20 21 T2 et 24 Q x9 di Lo 3
188. t essentiellement des variantes ou plut t des fragments du langage de programmation ML Ils se distinguent par leur logique PVS utilise un calcul des pr dicats classique sous forme de calcul des s quents ses objets sont un fragment fortement terminant de ML enrichi par une notion de sous type Les preuves en revanche ne sont pas un objet du formalisme La th orie des types de Martin L f est une logique pr dicative Les preuves sont elles m mes des A termes et l accent est mis sur la constructivit Le Calcul des Constructions Inductives est lui une extension de la logique d ordre sup rieur et autorise la quantification impr dicative sur toutes les propositions Sur tous ces points nous renvoyons bien s r au cours de tronc commun La plupart seront par ailleurs illustr s tout au long du cours Un point commun essentiel de CCI et de la th orie de Martin L f est bien s r qu ils sont construits sur la correspondance de Curry Howard Rappelons que cela signifie que les preuves sont des objets les propositions sont des types une preuve d une proposition P est un objet p de type P En simplifiant on peut dire que les avantages informatiques de cette approche sont Une plus grande homog n it preuves objets qui simplifie impl mentation du syst me de preuves Un statut bien compris des preuves comme objets du formalisme en cons quence elles ont galement une repr sentation
189. t fixe let rec well_founded_induction x a x a fun y _ gt well_founded_induction x y En d pliant cet op rateur et deux autres constantes Coq lt Extraction NoInline andb Coq lt Extraction Inline cardinal_rec2 Acc_iter_2 well_founded_induction_type_2 Coq lt Extraction subset on obtient exactement le code ML souhait 7 f vrier 2014 94 let rec subset x x match x with Empty gt True Node x1 z0 x2 gt match x with Empty gt False Node x 1 zi x 2 gt match compare z0 z1 with Lt gt andb subset Node x1 z0 Empty x 2 subset x2 Node x 1 zi x 2 Eq gt andb subset x1 x 1 subset x2 x 2 Gt gt andb subset Node Empty z0 x2 x 2 subset x1 Node x 1 zi x 2 De nombreuses autres techniques pour d finir des fonctions r cursives non structurelles dans Coq sont d crites dans le chapitre 15 de l ouvrage Interactive Theorem Proving and Program Development BC04 7 2 Utilisation de types d pendants Une autre approche de la preuve de programmes fonctionnels dans Coq consiste utiliser la richesse du syst me de types du Calcul des Constructions Inductives pour exprimer la sp cifi cation de la fonction dans son type m me En fait un type est une sp cification Dans le cas de ML c est juste une sp cification tr s pauvre une fonction attend un entier et retourne un entier mais dans Coq on peut exprimer
190. t un programme de X par sa s mantique exprim e dans le langage math matique du syst me Coq Plongement profond Dans le plongement profond on dispose d un type concret Y qui repr sente les arbres de syntaxe abstraite du langage X On peut ensuite construire des fonctions et des relations sur ce type On pourra ainsi parler des expressions bien form es construire des al gorithmes de typage repr senter la s mantique du langage Un programme crit dans le langage X pourra tre repr sent par un objet Coq de type Y les propri t s de cet objet seront tablies en utilisant diff rentes s mantiques Dans notre exemple les programmes sont repr sent s par un plongement profond Plongement superficiel Dans le plongement superficiel un programme est directement tra duit en sa s mantique Par exemple on pourrait commencer par introduire une notion de m moire et identifier un programme une fonction de transformation des m moires La s quence de deux programmes pourrait tre d finie comme la composition des m moires les repr sentant Les re lations sur les programmes comme les s mantiques op rationnelle ou axiomatique peuvent tre d finies en faisant r f rence la s mantique des programmes Les r gles d inf rence deviennent alors des th or mes qui peuvent tre utilis s pour prouver des propri t s de programmes La repr sentation des propri t s dans la s mantique axiomatique utilise un plongement superfici
191. tch eval_prog f with Coq lt Some Nat nf gt Some Bool iszero nf Coq lt _ gt None A semval Coq lt end Coq lt Opn o f g gt Coq lt match eval_prog f eval_prog g with Coq lt Some Nat nf Some Nat ng gt Some Nat semop o nf ng Coq lt _ _ gt None A semval Coq lt end Coq lt end La section Valexpr ouverte page 27 est alors ferm e ce qui a pour effet d abstraire les d finitions effectu es dans la section par rapport memstate et l hypoth se memstate_correct lorsqu elle est utilis e Coq lt End Valexpr Coq lt Check eval_prog eval_prog memory gt expr gt option semval 2 3 3 Les commandes La repr sentation de la syntaxe et de la s mantique statique des commandes suit les d finitions des figures 2 1 et 2 4 Syntaxe Coq lt Inductive com Set Coq lt skip com Coq lt aff name gt expr gt com 7 f vrier 2014 31 Coq lt seq com gt com gt com Coq lt cond expr gt com gt com gt com Coq lt while expr gt com gt com S mantique statique Coq lt Inductive comcorrect com gt Prop Coq lt corskip comcorrect skip Coq lt coraff Coq lt forall n name e expr s sort Coq lt exprcorrect s e gt comcorrect aff n e Coq lt corseq Coq lt forall c d com Coq lt comcorrect c gt comcorrect d gt comcorrect seq c d Coq lt corcond Coq lt
192. tion app l l2 L L match l with lam f f l2 end La r duction suivante est satisfaite app lam f D f 1 On construit alors Definition 6 L lam x L gt app x x On v rifie alors que le terme app 6 6 se r duit en une tape de r duction vers lui m me et donc que ce terme n est pas normalisable Cet exemple peut tre ais ment cod en ML Par contre il explique pourquoi les d finitions inductives doivent imposer une condition de positivit Une d finition inductive I est positive si les seules occurrences de J dans des types d argu ments de constructeur se font de mani re positive c est dire la gauche d un nombre pair ventuellement nul de produits avec la d finition suivante Dans le terme Vz A B le terme B est gauche de 0 produit un sous terme C de B qui est gauche de n produits dans B est galement gauche de n produits dans Vx A B Le terme A est gauche d un produit dans Va A B et un sous terme C de A qui est gauche de n produits dans A est galement gauche de n 1 produits dans Vx A B Des exemples de type de constructeur positif pour J sont A I avec I qui n apparait pas dans A I gt A gt B avec I qui n apparait pas dans A mais peut appara tre positivement dans B Un type d argument C qui d pend de 1 de mani re positive satisfait une condition de mono tonicit c est dire que si J C J autrement
193. tions globales la preuve De l autre c t les syst mes HOL Coq Isabelle et PVS h ritent tous de la notion de tac tique introduite dans le syst me LCF et offrent ainsi la possibilit de d veloppement de preuve interactifs Le degr d automatisation Le degr d automatisation est un facteur cl dans la diffusion des assistants de preuve en dehors du milieu des logiciens Souvent l automatisation car elle applique des m thodes de force brute s oppose au souci de lisibilit des preuves un nonc m me simple aura facilement une preuve complexe et en tout cas non directe Une r ponse ce souci est une nouvelle fois le m canisme de preuve par r flexion qui isole la m thode de preuve en une tape l mentaire l chelle humaine de d monstration PVS et ACL2 sont actuellement les syst mes les plus automatis s parmi ceux mentionn s ci dessus Viennent ensuite Isabelle puis HOL et Coq 5 3 Autres syst mes On peut mentionner de nombreux autres syst mes dont les biblioth ques et la base d utilisa teur sont moins d velopp es Lego Pol est une impl mentation du Calcul des Constructions enrichie par des d clarations de types inductifs Le syst me Plastic Gro est une continuation de Lego exp rimentant divers m canismes de coercions Ces syst mes sont d velopp s Edimbourg et Durham au Royaume Uni Alfa Agda Coq est un syst me exp rimental de d veloppement de preuve comme u
194. ts clos du bon type Cependant m me pour les types de donn es le sch ma qui dit que les seuls objets dans le type sont ceux obtenus via les constructeurs n est pas d montrable D finition de types par cas Elimination forte On appelle sch ma d limination forte le sch ma d limination d un inductif d une sorte impr dicative par exemple Prop mais aussi Set dans le calcul des constructions avec Set impr dicatif vers des pr dicats de sorte Type Si on reprend l exemple des bool ens le sch ma d limination forte a la forme suivante b bool P bool Type f P true g P false Case P b f g Pb On peut en particulier instancier ce sch ma avec P Ab bool gt Prop on obtient f Prop g Prop Ab bool Case P b f g bool Prop En prenant pour f la propri t toujours vrai True et pour g la propri t toujours fausse False on obtient une propri t de type bool Prop telle que true est quivalent True et false quivalent 4 False Cette propri t P nous permet de r futer le fait que true false On peut galement prendre P Ab bool gt Set f nat et g bool on pourra alors d finir un type de type bool Set tel que true est quivalent nat et d false quivalent false Pour construire un objet dans ce type il est encore n cessaire d utiliser le sch ma d limination de bool en prenant cette fois ci P f nat et g bool On a alors
195. u true gt A u Supposons que l on veuille prouver la propri t A u pour un terme u clos Le terme dec_bool u est clos et de type bool il doit s valuer vers la valeur true Une preuve pos sible de A u est donc correct u refl true La v rification que ce terme est de type A u n cessite de typer u puis de typer refl true de type dec_bool u true ce qui revient r duire dec_bool u en true ce qui peut n cessiter un calcul complexe 5 4 2 Utilisation d une structure abstraite En g n ral on souhaite montrer des propri t s sur des termes qui ne sont pas forc ment clos et sur lesquels il n est pas forc ment simple de construire des proc dures de d cision On introduit alors une structure abstraite interm diaire qui va repr senter la syntaxe des expressions manipuler et qui va permettre des manipulations symboliques On a alors besoin d une fonction d interpr tation de la syntaxe vers les propri t s montrer La technique de r flexion proc de comme suit D finition d une structure abstraite S pour le type de probl me auquel s adresse la m thode de d cision ou de simplification consid r e D finition d une fonction d interpr tation x S x des objets de cette structure abs traite S en une expression concr te un terme ou une formule du syst me logique D finition de la fonction de d cision ou de simplification par calcul sur les objets de la struct
196. ue le typage ou l valuation lorsqu elles sont pr sen t es par un ensemble de r gles d inf rence se traduisent imm diatement en d finitions inductives Nous d taillons ici la formalisation de la s mantique d un petit langage de programmation dans le style imp ratif Ce genre de formalisation aussi appel plongement profond constitue une alternative la preuve de programme imp ratif Une autre alternative est le plongement simple aussi appel plongement superficiel qui simule les propri t s des programmes imp ratifs partir de leur 21 7 f vrier 2014 22 interpr tation dans un langage purement fonctionnel La s mantique est alors implicite dans la traduction Cette question sera voqu e dans le chapitre traitant de la preuve de programmes imp ratifs 2 2 Pr sentation du probl me Notre langage comprend les commandes suivantes 4 partir d un ensemble de variables X C skip X E Ci C2 if E then Ci else C2 while E do C FIGURE 2 1 Syntaxe des commandes Les expressions sont form es de constructions enti res et bool ennes simples et sont donn es par la syntaxe de la figure 2 2 B X5 Variables sort es true false Constantes bool ennes Fy xor Ey Ou exclusif n Constantes enti res null E Teste si un entier est nul Fy op E2 Op ration binaire sur les entiers s nat bool op x FIGURE 2 2 Syntaxe des expressions On cherche d finir
197. uire partir d une preuve un pro gramme qui r alise la propri t montr e Nous expliquerons la distinction entre les sortes Prop et Set dans le syst me Coq 6 1 Interpr tation constructive des preuves 6 1 1 Logique classique versus logique intuitionniste La logique de Coq est intuitionniste aucun axiome ne permet de d river A V A ou bien gt A pour une formule arbitraire Est ce emb tant On se place par exemple dans l arithm tique du premier ordre ou d ordre sup rieur On notera Hc lorsque est prouvable de mani re classique et Fy A lorsque A est prouvable de mani re intuitionniste Il existe de nombreux r sultats sur les liens entre les preuves classiques et intuitionnistes Une propri t vraie de mani re intuitionniste l est aussi de mani re classique si IT Hz alors T Fc Une propri t vraie de mani re classique peut tre prouv e de mani re intuitionniste en ajoutant le sch ma d axiome du tiers exclu si I Fe alors C V C T Fr A En logique classique kcAVB amp AA B Fo An nat P n amp Vn P n En logique intuitionniste l quivalence ne peut tre prouv e que dans un seul sens FAVB AAAAB Fran nat P n gt Vis P n 72 7 f vrier 2014 73 Toute formule A peut tre transform e en une formule Ax classiquement quivalente par exemple en liminant les 4 et V et en rempla ant les formules atomiques par
198. un inductif sur mesure sig2 d fini par Coq lt Inductive sig2 A Set P A gt Prop Q A gt Prop Set Coq lt exist2 forall x A P x gt Q x gt sig2 PQ Son extraction est identique celle de sig 7 f vrier 2014 96 7 2 3 Sp cification d une fonction bool enne sumbool Un type de sp cification qui revient tr s souvent est celui de la sp cification d une fonction bool enne Dans ce cas on souhaite exprimer quelles sont les deux propri t s tablies lorsque la fonction retourne false et true respectivement Coq introduit un type inductif pour cela sumbool d fini par Coq lt Inductive sumbool A Prop B Prop Set Coq lt left gt sumbool B Coq lt right B gt sumbool A B C est un type semblable au type bool mais dont chaque constructeur contient une preuve de A et de B respectivement sumbool A B se note A B Une fonction de test de l ensemble vide pourra se sp cifier ainsi is_ empty Vs s Empty s Empty Un cas plus g n ral et tr s fr quent est celui d une galit d cidable En effet si un type A est muni d une galit eq Prop on peut sp cifier une fonction de test de cette galit sous la forme A_eq dec Vr y eq x y eq x y C est presque la m me chose que donner une preuve de Va y eq x y V eq x y si ce n est que la sorte n est pas la m me Dans ce dernier cas on
199. univers des ensembles est un treillis complet par rapport l ordre d inclusion Cette possibilit de voir la d finition comme un plus petit point fixe sera commune toutes les d finitions inductives Par ailleurs on verra plus tard comment ces points fixes apparaissent galement dans la s mantique de la th orie Dans ce chapitre nous n expliciterons pas les r gles de typage qui sous tendent les d finitions inductives Elles seront explicit es en partie lors du cours 3 1 4 2 Syntaxe alternative Par d faut les entiers de nat sont repr sent s en Coq via la notation standard en base 10 Par exemple la notation 3 d signe l entier naturel S S S 0 Qu il soit clair que ces deux critures d signent le m me terme et sont repr sent es de mani re identique dans le syst me On verra plus loin que les symboles infixes lt d signent aussi par d faut en Coq les op rations arithm tiques sur nat tout moment lors d une session Coq on peut d sactiver les notations volu es telles que 3 lt en utilisant la commande Set Printing All 1 4 3 Fonctions sur les entiers Deux exemples simples Les entiers sont l arch type du type de donn es r cursif Tout comme en ML l on calcule sur ces entiers gr ce des fonctions d finies par deux m canismes fondamentaux le filtrage la r cursion Le premier exemple d une telle fonction est en g n ral l addition Voici sa d fi
200. ure abstraite Preuve que la m thode est valide c est dire que Vs S s s pour une proc dure de simplification sur les termes Vs S s p s pour une proc dure de simplification sur les propositions sachant qu une proc dure de d cision peut tre vue comme une proc dure de simplification renvoyant soit la proposition vraie soit la proposition fausse Ces bases tant pos es la simplification d un nonc de la forme w t en l nonc t o t a t simplifi proc de par une simple application du lemme de validit de En effet par applicabilit de la m thode de d cision il existe un s S tel que s est convertible avec t qui par le lemme de validit est gal s qui lui m me est convertible en la forme simplifi e de t En fait plus g n ralement on consid re des structures abstraites avec des variables et des fonctions d interpr tation param tr es par une substitution de ces variables par des sous termes non traitables par la m thode de simplification On a alors un lemme de validit qui a la forme Vs 5 Vo Var gt Term s g s s 5 4 3 Un exemple en Coq l associativit de l addition sur les entiers naturels On consid re des expressions construites partir de l addition plus not e sur les entiers naturels que l on souhaite normaliser sous une forme associative droite en supprimant les z ros par exemple la normalisation de x u y t 0
201. vely defined Exemples de d finitions mal form es On v rifie que la fonction filter n est pas accept e Coq lt Parameter P A gt bool P is assumed Coq lt CoFixpoint filtre s Stream A Stream A Coq lt match s with Coq lt Cons a 1 gt if P a then Cons a filtre 1 else filtre 1 Coq lt end Error Recursive definition of filtre is ill formed In environment A Set X Set out X gt A tran X gt X tran_rec X gt X Stream A B Set f A gt B filtre Stream A gt Stream A s Stream A a 1 Stream A Unguarded recursive call in filtre 1 Recursive definition is fun s Stream gt match s with Cons a 1 gt if P a then Cons a filtre 1 else filtre 1 end Cependant certaines d finitions qui sont s mantiquement productives ne sont pas accept es par ce crit re essentiellement syntaxique Coq lt CoFixpoint bad Stream nat Cons O map S bad Error 7 f vrier 2014 60 Recursive definition of bad is ill formed In environment bad Stream nat Unguarded recursive call in cofix map s Stream nat Stream nat match s with Cons a 1 gt Cons S a map 1 end Recursive definition is Cons 0 map S bad D autres syst mes Gim97 permettent une tol rance plus grande vis vis de ces d finitions 4 3 3 R duction Comme dans le cas des d finitions co inductives il est n cessaire de garder galement la r duction afin
202. ward permet de montrer la constructivit de la logique intuition niste Cependant il ne permet pas de justifier certains principes comme celui de l ind pendance des pr misses Information logique Soit une preuve du th or me de division euclidienne Va b b gt 0 qgdra bxqtrAr lt b Pour calculer effectivement le quotient et le reste il faut fournir les entr es a et b mais aussi une justification de b gt 0 et le programme calculera le quotient et le reste mais aussi une preuve de correction On voit que d une part on doit fournir une information qui n est pas utile pour le calcul 7 f vrier 2014 76 mais pour la terminaison et la correction du programme d autre part on calcule effectivement la preuve de correction du r sultat ce qui est a priori inutile La m thode propos e est donc inefficace Remarque L isomorphisme de Curry Howard n est pas satisfaisant lorsqu il s agit de mettre en vidence les fonctions r cursives sous jacentes aux preuves En effet il ne permet pas de traiter le cas des preuves sous axiome car alors les preuves ne sont plus closes et le calcul peut d pendre de mani re essentielle de l hypoth se Le probl me est donc de savoir si tant donn e une preuve de Vx P x gt 2y Q x y il est possible de construire un programme f tel que Vx P x gt Q x f x Ce n est en g n ral pas vrai pour toutes les propri t s P x En effet la preuve de P x peut transp
203. x fi fp P a1 a x Si x est logique il doit dispara tre l extraction par contre si s est de type Set on doit tre en mesure de fournir une r alisation de P a1 a x On a beau pouvoir extraire chaque branche fi en l absence de x il est difficile de les combiner On aboutit la r gle suivante un inductif de sorte Prop ne peut s liminer sur un pr dicat de sorte Set Il ne peut pas non plus s liminer sur un pr dicat de sorte Type car tout objet dans Set est galement un objet de la sorte Type donc l limination sur Type implique l limination sur Set De plus l limination sur Type permet de montrer qu il existe une propri t A Prop et a b A tel que a b est prouvable par analogie avec la preuve de true false Or du fait de notre interpr tation non calculatoire des propositions logiques supposer que toutes les preuves d une m me proposition logique sont gales est parfois utile C est galement une propri t que l on d rive partir d autres axiomes tel que celui de la logique classique VA Prop V A ou de l extensionnalit VA B Prop A amp B A B Les types singletons Il existe deux cas particuliers d inductif d finis dans Prop pour lesquels l limination sur la sorte Set ne pose pas de difficult Il s agit tout d abord de la d finition induc tive vide Dans une situation ou l absurde est prouvable n importe quel objet est un programme corr
204. xpr gt Prop Coq lt errxorl forall b c expr exprcorrect Snat b gt exprerr Xor b c Coq lt errxorr forall b c expr exprcorrect Snat c gt exprerr Xor b c Coq lt errtzero forall b expr exprcorrect Sbool b gt exprerr Null b Coq lt erropl Coq lt forall op op b c expr Coq lt exprcorrect Sbool b gt exprerr Opn op b c Coq lt erropr Coq lt forall op op b c expr Coq lt exprcorrect Sbool c gt exprerr Opn op b c Coq lt errcongxorl forall b c expr exprerr b gt exprerr Xor b c Coq lt errcongxorr forall b c expr exprerr c gt exprerr Xor b c Coq lt errcongtzero forall b expr exprerr b gt exprerr Null b Coq lt errcongopl Coq lt forall op op b c expr exprerr b gt exprerr Opn op b c Coq lt errcongopr Coq lt forall op op b c expr exprerr c gt exprerr Opn op b c Le th or me exprimant la d cidabilit du typage et de l valuation est juste une preuve du fait que pour toute expression E soit il est possible de construire une valeur v de l expression dont la sorte est la sorte de l expression soit il est possible de prouver que l expression est mal form e Le fait d utiliser une interpr tation constructive de la disjonction et de lexistentielle assure l existence d un algorithme permettant de d cider dans quel cas on est et de calculer effectivement la valeur On tablit un r sultat de d cidabilit
205. ypothesis compare_spec Coq lt forall x y match compare x y with Coq lt Lt gt x lt y Coq lt Eq gt x y Coq lt Gt gt x gt y Coq lt end On peut alors utiliser cette sp cification de la mani re suivante Coq lt generalize compare_spec x z destruct compare x z La preuve se poursuit alors sans difficult Note Pour des fonctions purement informatives telles que is_empty ou mem le programme extrait est identique au terme Coq Ainsi la commande Extraction mem donne t elle le code ocaml let rec mem x function Empty gt false Node 1 y r gt match compare x y with Lt gt mem x 1 Eq gt true Gt gt mem x r 7 1 1 Cas des fonctions partielles Une premi re difficult appara t lorsque la fonction est partielle i e a un type de la forme f Vz n Pr n Le cas typique est celui d une fonction de division qui attend un diviseur non nul Dans notre exemple on peut souhaiter d finir une fonction min_elt retournant le plus petit l ment d un ensemble suppos non vide c est dire l l ment rang le plus gauche dans l arbre binaire de recherche On peut donner cette fonction le type suivant min _elt Vs tree 4s Empty gt Z 7 1 o appara t la pr condition s Empty La sp cification de min_elt peut alors s crire Vs Vh s Empty bst s gt In min elt sh sAVx Ing s min eltsh lt x 7 f vrier 2014 89 avec une pr condition
206. zx reflzx Case P e p P y e 7 f vrier 2014 43 Il v rifie la r gle de r duction Case P refl x p p Cette galit permet de comparer deux objets du m me type Cependant on est parfois amen s devoir comparer des objets dans des types diff rents Un exemple est la d finition du type r cursif des listes de longueur n Inductive list nat Prop nil list 0 cons Vn nat A gt list n gt list S n Une propri t attendue est Vl list 0 nil Pour la montrer en utilisant la g n ralisation pour l inversion on voudrait se ramener montrer V n nat l list n n 0 gt l nil Malheureusement cette propri t ne peut tre nonc e car la propri t l nil est mal form e puisque l list n et nil list 0 sont de type diff rents non convertibles Le fait qu il existe une preuve e de n 0 dans le contexte permet juste d appliquer une transformation l pour en faire un objet de type list 0 Mais l nonc devient V n nat l list n e n 0 Case list e nil On peut ensuite faire une preuve par cas sur l cependant on se retrouve devoir montrer V e 0 0 Case list e nil nil On souhaiterait alors utiliser le fait que toute preuve de 0 0 est de la forme ref1 0 en rempla ant e par cette valeur on doit montrer Case list refl 0 nil nil En utilisant la amp r duction on aboutit la trivialit nil nil Malheureusement

Assistants de preuve

Contents

Download Pdf Manuals

Related Search

Related Contents