Bases: Programmation fonctionnelle en Coq

Introduction

Le style fonctionnel rapproche la programmation des mathématiques : si une procédure ou une méthode n'a pas d'effets de bord, elle est déterminée par les sorties qu'elle associe à chaque entrée --- c'est-à-dire qu'on peut réduire son comportement à une fonction mathématique. C'est une des raisons du choix de l'adjectif «fonctionnel» dans «programmation fonctionnelle». Cette connexion directe entre programmes et des objets mathématiques simples aide à raisonner de manière correcte, même informellement. Elle permet aussi des preuves formelles de correction. L'autre sens dans lequel la programmation fonctionnelle est «fonctionnelle» est qu'elle met en avant l'utilisation des fonctions comme valeurs de première classe -- c'est-à-dire des valeurs qu'on peut passer en arguments à d'autres fonctions, renvoyer comme résultats, mémoriser dans des structures de données, etc. Ce traitement des fonctions comme des données permet de nombreuses tournure de programmation, comme on va le voir. D'autres éléments standard dans les langages fonctionnels sont les types de données algébriques et le filtrage de motifs (pattern matching en anglais), qui facilitent la construction et la manipulation de structures de données riches, ainsi que les systèmes de typage polymorphes, qui encouragent l'abstraction et la réutilisation de code. Coq dispose de tous ces éléments.

Types énumérés

Un aspect inhabituel de Coq est que son ensemble de constructions primitives est extrêmement petit. Par exemple, plutôt que de fournir la palette habituelle des types de données de base (booléens, entiers relatifs, chaînes de caractères, etc.), Coq offre un mécanisme extrêmement puissant pour définir entièrement de nouveaux types de données -- si puissant que ces types bien connus en sont des instances. Bien sûr, la distribution de Coq comprend une riche bibliothèque standard, qui fournit des définitions pour les booléens, les entiers et de nombreuses structures de données habituelles, telles que les listes et les tables de hachage. Il n'y a cependant rien de magique ni de primitif dans ces définitions : elles relèvent du code utilisateur ordinaire. Pour voir cela à l'oeuvre, commençons par un exemple très simple.

Jours de la semaine

La définition suivante déclare à Coq un nouvel ensemble de valeurs un type.

Le type s'appelle jour et ses éléments sont lundi, mardi, etc... Les lignes 2 à 8 de la définition peuvent se lire «lundi est un jour, mardi est un jour, etc.» Ayant défini jour, on peut écrire des fonctions qui agissent dessus.

Une chose à noter est que les types de l'argument et du résultat de cette fonction sont déclarés explicitement. Comme la plupart des langages de programmation fonctionnels, Coq sait souvent deviner ces types, même s'ils ne sont pas donnés explicitement -- c'est-à-dire qu'il fait de l' inférence de types -- mais nous les incluerons toujours pour faciliter la lecture. Ayant défini une fonction, nous devrions commencer par vérifier qu'elle a le comportement attendu sur quelques exemples. Il y a en fait trois moyens différents de le faire en Coq. Premièrement, nous pouvons utiliser la commande Eval simpl pour évaluer une expression composée utilisant jour_ouvre_suivant.

Si vous avez un ordinateur sous la main, c'est le moment de lancer Coq dans votre IDE favori -- soit CoqIde soit Proof General -- et d'essayer vous-même. Ouvrez ce fichier (Basics.v), que vous trouverez dans les sources accompagnant le livre, trouvez l'exemple ci-dessus, soumettez-le à Coq et observez le résultat. Le mot-clef simpl ("simplifier") indique à Coq quelle méthode utiliser pour évaluer l'expression qu'on lui fournit. Pour le moment, simpl est la seule dont on a besoin; plus bas, nous verrons des alternatives qui sont parfois utiles. Deuxièmement, nous pouvons noter ce qu'on s'attend à obtenir comme résultat, sous forme d'un exemple Coq:

Cette déclaration fait deux choses: elle fait une assertion (que le deuxième jour ouvré suivant samedi est mardi) et elle donne un nom à cette assertion, qu'on peut utiliser plus tard pour y faire référence. Ayant fait notre assertion, nous pouvons aussi demander à Coq de la vérifier, comme ceci:

Les détails de cette preuve ne sont pas importants pour l'instant (nous y reviendrons sous peu), mais en gros elle peut se lire: «l'assertion qu'on vient de faire se prouve en observant que les deux membres de l'égalité sont les mêmes après simplification.» Troisièmement, nous pouvons demander à Coq d'«extraire», à partir d'une Definition, un programme écrit dans un autre langage de programmation plus conventionnel (OCaml, Scheme, or Haskell), doté d'un compilateur très efficace. Cette possibilité est très intéressante, parce qu'elle permet la construction de programmes entièrement certifiés dans des langages très répandus. C'est d'ailleurs l'un des usages principaux ayant motivé le développement de Coq. Nous reviendrons sur ce sujet dans des chapitres ultérieurs. On trouve aussi de plus amples informations dans le livre Coq'Art de Bertot et Castéran, ainsi que dans le manuel de référence.

Booléens

D'une manière similaire, nous pouvons définir le type bool des booléens, constitué des éléments true et false (vrai et faux, respectivement).

Nous définissons ici nos propres booléens, pour montrer comment faire à partir de rien. Mais bien sûr, la bibliothèque standard de Coq fournit une implantation par défaut des booléens, ainsi qu'une multitude de fonctions et de lemmes utiles. (Le lecteur intéressé pourra jeter un oeil à Coq.Init.Datatypes dans la documentation de la bibliothèque standard.) Autant que possible, nous nommerons nos définitions et théorèmes pour qu'ils coïncident exactement avec ceux de la bibliothèque standard. On peut définir, comme ci-dessus sur les jours de la semaine, des fonctions sur les booléens:

Les deux dernères illustrent la syntaxe pour les définitions de fonctions à plusieurs arguments. Les «tests unitaires» suivants constituent une spécification complète -- une table de vérité -- de la fonction orb:

(Observons qu'on a omis le simpl dans les preuves. Il n'est pas nécessaire, car reflexivity effectue la même simplification automatiquement. Note sur les notations : on utilise les crochets pour délimiter les fragments de code Coq dans les commentaires des fichiers .v; cette convention, utilisée aussi par l'outil coqdoc de documentation, les sépare visuellement du texte autour. Dans la version html de ces fichiers, ces parties du texte apparaissent dans une police différente. Les valeurs Admitted et admit peuvent servir à combler un trou dans une définition ou une preuve incomplète. Nous les utiliserons dans les exercices suivants. En général, votre travail dans les exercices consiste à remplacer admit ou Admitted par des définitions et preuves complètes.

Exercice : 1 étoile (nandb)

Compléter la définition de la fonction suivante, puis s'assurer que les assertions Example ci-dessous sont toutes validées par Coq. Cette fonction doit renvoyer true si au moins l'un de ses arguments est false.

Remplacer "Admitted." dans chaque preuve par "Proof. reflexivity. Qed."

☐

Exercice : 1 étoile (andb3)

Faire la même chose pour la fonction andb3 ci-dessous. Cette fonction doit renvoyer true quand tous ses arguments sont true et false sinon.

☐

Types fonctionnels

La commande Check fait afficher par Coq le type d'une expression. Par exemple, le type de negb true est bool.

Les fonctions, telles que negb, sont elle-mêmes des valeurs, des données, exactement comme true et false. Leurs types sont appelés types fonctionnels et sont notés avec une flèche. they are written with arrows.

Le type de negb, noté bool -> bool et prononcé «bool flèche bool», se comprend comme: «étant donné un argument de type bool, cette fonction renvoie un résultat de type bool.» De la même manière, le type de andb, noté bool -> bool -> bool, se comprend comme: «étant donnés deux arguments, tous deux de type bool, cette fonction renvoie un résultat de type bool».

Nombres

Digression technique: Coq offre un système de modules plutôt sophistiqué, utile pour organiser les gros développements. Dans ce cours, nous n'utiliserons que peu de ses possibilités, mais une nous servira: si nous entourons une collection de déclarations des marqueurs Module X et End X, alors, dans le reste du fichier après le End, on pourra faire référence à ces définitions par des noms tels que X.truc, plutôt que seulement truc. Ici, nous utilisons cette possibilité pour définir le type nat dans un module, de sorte qu'il ne masque pas le type nat de la bibliothèque standard.

Les types définis jusqu'ici sont des exemples de «types énumérés»: leurs définitions énumèrent explicitement un ensemble fini d'éléments. Une manière plus élaborée de définir un type est de donner une collection de «règles inductives» décrivant ses éléments. Par exemple, on peut définir les entiers naturels comme suit:

Les clauses de cette définition peuvent se comprendre comme:

• O est un entier naturel (observons qu'on utilise la lettre «O», pas le nombre «0»).
• S est un «constructeur» qui prend en argument un entier naturel et en rend un autre -- c'est-à-dire que si n est un entier, alors S n en est un aussi.

Entrons un peu plus dans le détail. Tout ensemble défini inductivement (jour, nat, bool, etc.) est en fait un ensemble d' expressions. La définition de nat dit comment les expressions de l'ensemble nat sont construites:

• l'expression O appartient à l'ensemble nat;
• si n est une expression appartenant à l'ensemble nat, alors S n aussi; et
• les expressions formées de ces deux manières sont les seules appartenant à l'ensemble nat.

Les mêmes règles s'appliquent pour nos définitions de jour et bool. Les annotations utilisées pour leurs constructeurs sont analogues à celle du constructeur O; elles indiquent que ces constructeurs n'attendent pas d'arguments. Ces trois conditions inductives font précisément la force de la déclaration Inductive. Elles impliquent que l'expression O, l'expression S O, l'expression S (S O), l'expression S (S (S O)), et ainsi de suite, appartiennent toutes à l'ensemble nat, contrairement à d'autres expressions comme true, andb true false, ou S (S false). On peut écrire des fonctions simples par cas sur les entiers exactement comme on l'a fait plus haut -- par exemple, la fonction prédécesseur:

La seconde branche peut se comprendre comme «si n est de la forme S n' pour un certain n', alors renvoyer n'».

Les entiers naturels sont utilisés partout, ce qui justifie un soupçon de magie built-in pour les écrire et les afficher: les nombres arabes ordinaires peuvent être utilisés alternativement à la notation unaire définie par les constructeurs S et O. Coq affiche par défaut les entiers en notation arabe:

Le constructeur S a le type nat -> nat, exactement comme les fonctions minutstwo et pred:

On appliquer ces trois valeurs à un entier pour en obtenir un nouveau. Néanmoins, il y a une différence fondamentale: les fonctions, comme pred et minustwo, sont équipées de règles de calcul -- e.g., la définition de pred dit que pred 2 se simplifie en 1 -- alors que la définition de S n'est pas attachée à de telles règles. Bien qu'elle soit une fonction, en ce sens qu'on peut lui appliquer un argument, elle ne fait rien du tout. Pour la plupart des définitions de fonctions sur les entiers, le raisonnement par cas ne suffit pas: on a en plus besoin de la récursion. Par exemple, pour vérifier qu'un entier n est pair, on peut avoir besoin de vérifier récursivement que n-2 l'est. Pour écrire de telles fonctions, on utilise le mot-clef Fixpoint.

On peut définir oddb à l'aide d'une déclaration Fixpoint similaire, mais on préfère une définition plus simple d'utilisation:

Bien sûr, on peut aussi définir récursivement des fonctions à plusieurs arguments. (On utilise à nouveau un module pour éviter de polluer l'espace de noms.)

Additionner trois et deux donne maintenant bien cinq.

La simplification effectuée par Coq pour arriver à ce résultat peut être vue comme ceci: plus (S (S (S O))) (S (S O)) ==> S (plus (S (S O)) (S (S O))) par la seconde clause du match ==> S (S (plus (S O) (S (S O)))) par la seconde clause du match ==> S (S (S (plus O (S (S O))))) par la seconde clause du match ==> S (S (S (S (S O)))) par la première clause du match Pour gagner en lisibilité, si deux arguments ou plus ont le même type, on peut les grouper. Dans la définition suivante, (n m : nat) pourrait s'écrire (n : nat) (m : nat).

On peut aussi raisonner par cas sur deux expressions d'un coup, en utilisant une virgule:

Le _ sur la première ligne est un cas joker. Écrire _ dans un cas revient à écrire une variable non utilisée dans le membre droit. Cela évite d'avoir à un inventer un nom de variable inutilement.

Exercice : 1 étoile (factorielle)

Rappelons la fonction factorielle habituelle:

    factorial(0)  =  1 
    factorial(n)  =  n * factorial(n-1)     (if n>0)

Traduisons-la en Coq.

☐ On peut rendre les expressions numériques légèrement plus lisibles et plus faciles à écrire en introduisant des «notations» pour l'addition, la multiplication et la soustraction.

(Les annotations level, associativity et nat_scope contrôlent le traitement de ces notations par le parser de Coq. Les détails importent peu, mais le lecteur intéressé peut se référer à la partie «Supplément sur les notations» dans la partie «Contenu optionnel» à la fin de ce chapitre.) Observons que ces notations ne changent pas les définitions déjà entées: ce sont simplement des instructions au parser de Coq pour accepter x + y à la place de just plus x y et, de même, à l'afficheur de Coq pour afficher x + y plutôt que plus x y. Quand on dit que Coq n'a rien de built-in, c'est pour de vrai: même le test d'égalité entre entiers est une opération définie au niveau utilisateur! La fonction beq_nat teste l'égalité (eq) entre entiers naturels et renvoie un booléen. Notons l'utilisation de définitions par cas (match) imbriquées (on aurait aussi pu utiliser un match simultané, comme pour minus.)

De la même manière, la fonction ble_nat compare les entiers naturels (on écrit ble pour boolean less or equal).

Exercice : 2 étoiles (blt_nat)

La fonction blt_nat compare les entiers naturels au sens strict et renvoie un booléen. Plutôt que de refaire une définition par Fixpoint, la définir en utilisant une fonction définie précédemment. Remarque: si la tactique simpl vous pose problème, vous pouvez essayer compute, qui est une sorte de simpl dopé aux anabolisants. Néanmoins, il y a une solution simple et élégante utilisant juste simpl.

☐

Preuve par simplification

Maintenant qu'on a défini quelques types de données et fonctions, examinons comment énoncer et démontrer des résultats sur leur comportement. En un sens, on a déjà commencé à le faire: chaque Example de la partie précédente postule un fait précis sur le comportement de fonctions sur des arguments particuliers. Ces preuves sont toutes les mêmes: on utilise la définition de la fonction pour simplifier les expressions des deux côtés du = et on constate qu'elles deviennent identiques. Le même genre de «preuve par simplification» peut servir à démontrer des propriétés plus intéressantes. Par exemple, le fait que 0 est un «élément neutre» à gauche pour + peut se démontrer en observant simplement que 0 + n se réduit à n, quel que soit n, puisque la définition de + est récursive en son premier argument.

(Remarque: l'énoncé précédent apparaît peut-être différent dans le fichier source original et dans l'affichage par Coq. Dans les fichiers Coq, on écrit le quantificateur universel forall en utilisant le mot-clef « forall ». Ce dernier est affiché comme un «A» avec la tête en bas, le symbole habituel en logique. ) La forme de ce théorème et de cette démonstration sont presque les même que dans les exemples précédents: les seules différences sont qu'on a ajouté le quantificateur forall n : nat et qu'on a utilisé le mot-clef Theorem plutôt qu'Example. En fait, cette seconde différence relève uniquement du style; les mots-clef Example et Theorem (ainsi que quelques autres comme Lemma, Fact et Remark) signifie exactement la même chose en Coq. Les mots-clef simpl et reflexivity sont des exemples de tactiques. Une tactique est une commande utilisée entre Proof et Qed pour expliquer à Coq comment vérifier la correction d'un énoncé. Nous verrons plusieurs autres tactiques dans la suite de cette séance et d'autres encore dans les séances suivantes. (Au passage, il sera utile plus tard de savoir que reflexivity fait en réalité un peu plus que simpl -- par exemple, elle essaie de «déplier» les termes définis en remplaçant les termes par leurs définitions. Cette différence est due au fait que, si reflexivity réussit, le but entier est atteint et on n'a pas besoin de lire les expressions, quelles qu'elles soient, auxquelles reflexivity est arrivée; au contraire, simpl s'utilise dans des cas où on peut avoir à lire et comprendre le nouveau but, donc on n'a pas envie qu'elle déplie aveuglément les définitions.)

Exercice : 1 étoile (simpl_plus)

Qu'affichera Coq en réponse à cette demande ?

Et à celle-ci ?

Expliquer la différence. ☐

La tactique intros

A part les tests unitaires, qui appliquent des fonctions à des arguments particuliers, la plupart des propriétés qu'on essaiera de prouver sur les programmes commenceront par des quantificateurs (par exemple, «pour tout entier n, ...») et/ou des hypothèses («supposons m=n, ...»). Dans ce cas, nous aurons besoin de raisonner en supposant l'hypothèse -- i.e., nous commencerons par dire «OK, supposons que n est un entier arbitraire,» ou «OK, supposons que m=n». La tactique intros nous permet de faire ceci en déplaçant un ou plusieurs quantificateurs ou hypothèses depuis le but vers un «contexte» contenant les hypothèses courantes. Par exemple, voilà une preuve légèrement différente du même théorème.

Jouer cette preuve étape par étape en Coq et observer comment le but et le contexte changent.

Le suffixe _l dans les noms de ces théorèmes se prononce «à gauche».

Preuve par récriture

Voilà un théorème un peu plus intéressant:

Plutôt que d'énoncer quelque chose d'entièrement universel en les entiers n et m, ce théorème porte sur une propriété plus spécialisée, vraie seulement si n = m. La flèche se prononce «implique». Comme n et m sont des entiers arbitraires, la simplification ne suffit pas à démontrer ce théorème. Il se démontre en effet en observant que, en supposant n=m, on peut remplacer n par m dans le but, pour obtenir une égalité avec la même expression des deux côtés. La tactique pour demander à Coq de faire ce remplacement s'appelle rewrite.

La première ligne de la preuve déplace les variables n et m, quantifiées universellement, dans le contexte. La deuxième déplace l'hypothèse n=m dans le contexte et la nomme H. La troisième demande à Coq de récrire le but courant (n+n=m+m) en remplaçant le membre gauche de l'hypothèse d'égalité H par son membre droit. (La flèche dans le rewrite n'a rien à voir avec l'implication: il demande à Coq de récrire de gauche à droite. Pour récrire de droite à gauche, on utilise rewrite <-. Essayer de faire ce changement dans la preuve ci-dessus et observer la différence dans le comportement de Coq.)

Exercice : 1 étoile (plus_id_exercise)

Effacer «Admitted.» et faire la preuve.

☐ Comme nous l'avons vu dans les exemples précédents, la commande Admitted demande à Coq de passer sur la preuve de ce théorème et de l'accepter comme tel. Cela peut se révéler utile lors du développement de preuves plus longues : on peut énoncer des faits auxiliaires dont on espère se servir dans une argumentation plus large, utiliser Admitted pour repousser leur preuve à plus tard et continuer l'argumentation plus large, pour y revenir quand on est sûr que cela fait sens ; on peut alors remplir les trous. Il faut néanmoins faire attention: à chaque Admitted (ou admit), on laisse une porte ouverte à toutes les absurdités possibles, qui peuvent ainsi s'introduire dans le monde rigoureux et formellement vérifié de Coq ! On peut aussi utiliser la tactique rewrite avec un théorème précédent plutôt qu'une hypothèse du contexte.

Exercice : 2 étoiles (mult_1_plus)

☐

Preuve par cas

Bien sûr, on ne peut pas tout démontrer juste par le calcul : en général, la présence de valeurs hypothétiques, inconnues (entiers arbitraires, booléens, listes, etc...) peut bloquer le calcul. Par exemple, si on tente de prouver le fait suivant en utilisant la tactique simpl comme ci-dessus, on est coincé.

La cause de ce comportement est que les définitions de beq_nat et + commencent par un raisonnement par cas sur leur premier argument. Mais ici, le premier argument de + est l'entier inconnu n et l'argument de beq_nat est l'expression composée n+1; aucun des deux ne se simplifie. Il nous manque ici un moyen de considérer les différentes formes possibles de n séparément. Si n est O, alors on peut calculer le résultat final de beq_nat (n+1) 0 et vérifier que c'est en effet false. De plus, si n=S n' pour un certain n', alors, bien qu'on ne connaisse pas exactement le nombre n+1, on peut au moins calculer qu'il commence par un S, ce qui suffit à calculer que, ici encore, beq_nat (n+1) 0 renvoie false. La tactique qui demande à Coq de considérer séparément les cas n=0 et n=S n' s'appelle destruct.

Le destruct engendre deux sous-buts, que nous devons ensuite prouver séparément pour que Coq reconnaisse que le théorème est prouvé. (Il n'y a pas besoin de commande pour bouger d'un sous-but à l'autre. Lorsque le premier sous-but est prouvé, il disparaît et on se retrouve avec l'autre.) Dans cette preuve, chaque sous-but se prouve facilement en une invocation de reflexivity. L'annotation «as [| n']» s'appelle un motif d'introduction. Elle dit à Coq comment nommer les variables introduites dans chaque sous-but. En général, on écrit entre les crochets une liste de listes de noms, séparés par |. Ici, la première composante est vide, puisque le constructeur 0 est zéro-aire (il ne contient aucune donnée). La seconde composant donne un seul nom, n', car S est un constructeur unaire. La tactique destruct peut s'utiliser avec n'importe quel type de données inductif. Par exemple, utilisons-le pour démontrer que la négation booléenne est involutive, i.e., qu'elle est sa propre inverse.

Observons que le destruct n'a ici pas de clause as, parce qu'aucun de ses sous-cas n'a de variables à lier; il n'a donc besoin de lier aucun nom. (On aurait aussi pu écrire as [|], ou as [].) En fait, on peut omettre la clause as de n'importe quel destruct, auquel cas Coq inventera des noms de variables automatiquement. Bien que ce soit confortable, on peut arguer que c'est une mauvaise pratique, les choix faits automatiquement par Coq étant souvent contre-intuitifs.

Exercice : 1 étoile (zero_nbeq_plus_1)

☐

Encore des exercices

Exercice : 2 étoiles (fonctions booléennes)

Utiliser les tactiques apprises jusqu'ici pour démontrer le théorème suivant sur les fonctions booléennes.

Énoncer à présent, puis démontrer, un théorème negation_fn_applied_twice similaire au précédent mais où la deuxième hypothèse demande que la fonction f vérifie f x = negb x pour tout x.

Exercice : 2 étoiles (andb_eq_orb)

Démontrer le théorème suivant. (Vous pourrez avoir besoin de démontrer un ou deux lemmes auxiliaires.)

Exercice : 3 étoiles (binaire)

Considérons une représentation différente, plus efficace, des entiers naturels utilisant un système binaire plutôt qu'unaire. C'est-à-dire, plutôt que de dire que chaque entier est soit zéro soit le successeur d'un entier, nous pouvons dire que chaque entier binaire est soit

• zéro,
• le double d'un nombre binaire, ou
• un de plus que le double d'un entier binaire.
  (a) Écrire d'abord une définition inductive du type bin correspondant à cette description des entiers binaires.
  (Indication: Rappelons que la définition de nat vue en cours Inductive nat : Type := | O : nat | S : nat -> nat. ne dit rien sur ce que O et S «signifient». Elle dit uniquement «O est dans l'ensemble nat et si n est dans cet ensemble, alors S n aussi». L'interprétation de O comme zéro et de S comme la fonction successeur/plus un vient de l' utilisation qu'on fait des valeurs de type nat, en écrivant des fonctions pour opérer dessus, en en démontrant des propriétés et ainsi de suite. Votre définition de bin doit rester aussi simple; seules les fonctions que vous écrirez juste après lui donneront du sens mathématique.)
  (b) Ensuite, écrire une fonction d'incrémentation pour les entiers binaires et une fonction pour convertir les entiers binaires en entiers unaires.
  (c) Écrire des tests unitaires pour vos fonctions d'incrémentation et de traduction binaire vers unaire. Observons qu'incrémenter un entier binaire puis le convertir en unaire doit donner le même résultat que le convertir d'abord puis l'incrémenter.

☐

Contenu optionnel

Notations supplémentaires

Pour chaque symbole de notation en Coq on peut spécifier son «niveau de priorité» et son «associativité». Le niveau de priorité n peut être spécifié par les mots at level n et il aide à lever des ambiguïtés dans les expressions composées. L'associativité sert à lever des ambiguïtés dans les expressions contenant plusieurs occurrences du même symbole. Par exemple, les paramètres spécifiés ci-dessus pour + et * disent que l'expression 1+2*3*4 est un raccourci pour l'expression (1+((2*3)*4)). Coq utilise les niveaux de priorité de 0 à 100 et les associativités left, right et no. Chaque symbole de notation en Coq n'est de plus actif que dans sa portée de notation. Coq tente de deviner quelle portée l'utilisateur a en tête, donc quand on écrit S (0*0), il devine nat_scope, mais quand on écrit le type produit (le type des n-uplets) bool * bool il devine type_scoe. Occasionnellement, il faut aider Coq en utilisant la notation «pour cent» en écrivant (x*y)%nat et il arrive que Coq affiche %nat pour indiquer la portée d'une notation. Les portées de notations s'appliquent aussi à la notation numérique (3,4,5, etc...), de sorte qu'on peut parfois voir 0%nat, qui signifie O, ou 0%Z, qui dénote l'entier relatif zéro.

Fixpoints et récursion structurelle

Quand Coq vérifie cette définition, il observe que plus' est «décroissante en son premier argument». Cela signifie qu'on effectue une récursion structurelle sur l'argument n -- i.e., que tous nos appels récursifs portent sur des valeurs strictement plus petites que n. Cela implique que tous les appels à plus' finissent par terminer. Coq exige que l'un des arguments de chaque définition par Fixpoint soit «décroissant». Cette exigence est un aspect fondamental de la conception de Coq : en particulier, elle garantit que toutes les fonctions définissables en Coq terminent sur tous les arguments possibles. Néanmoins, l'«analyse de décroissance» de Coq étant limitée, il est parfois nécessaire d'écrire des fonctions de manière peu naturelle.

Exercice : 2 étoiles (décroissance)

Pour concrétiser un peu ce point, trouver un moyen d'écrire une définition Fixpoint sensée (par exemple, d'une fonction simple sur les entiers) qui termine vraiment sur tous les arguments, mais que Coq n'accepte pas à cause de cette restriction.

☐