This course deals with formal proofs, as a discipline of computer science. It thus extends course "Foundations of proof systems", but with emphasis on the actual construction of formal proofs and their verification by a computer.
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 l'ordinateur: la capacité de la machine à manipuler rapidement de grosses expressions symboliques permet de formaliser entièrement des raisonnements non-triviaux. If mathematical logic, in other words the complete formalization of reasoning, is a discipline already relatively old, it was fairly upset by the arrival of the computer: the ability of the machine to handle rapidly large symbolic expressions used to entirely formalize non-trivial reasoning. La question que se pose le logicien n'est alors plus tant existe-t-il une formalisation de tel raisonnement ? » que de construire et d'exhiber cette formalisation. The question that arises to the logician is no longer "is there a formalization of such reasoning?" than to build and display this formalization.
C'est avec cette observation à l'esprit que nous chercherons à traiter des points suivants: With this observation in mind, we will seek to address the following:
Le
choix du formalisme est important pour la pratique des mathématiques
formelles. The formalism choice is important for the practice of
formal mathematics. 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. Not only must it be able to express the evidence
developed by mathematicians, but it must do so in the easiest and most
intuitive way. 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. In fact, recent developments in
the Calculus of Inductive Constructions have almost always been
motivated by the practice and came after the first implemetations of
Coq (intially called CoC).
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. Even more than in usual mathematics, knowing how to state properties that we set to prove is vital if we are to go for a formal proof. 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. If we make the analogy between proving and programming, then the choice of the model corresponds to the data-structure representation, with the immediate and obvious consequences on the architecture of the software obtained.
Plus généralement, il nous semble que les analogies entre les activités de preuves et de programmation sont nombreuses, et s'il existe un art » de la bonne programmation, il en va de même pour les preuves formelles. More generally, we believe that the similarities between the activities of proving and programming are numerous, and if there is an "art" of good programming, it is the same for formal proofs. De plus, à chaque couple formalisme/problème, correspond un, 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é. In addition, to each pair formalism / problem corresponds one or more good proof styles, as there are good programming styles for a problem and a particular programming language.
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. We will focus particularly on modeling and formalization of computer problems where safety is important, and the proof of correctness of programs.
Enfin nous chercherons à décrire les grands principes d'un logiciel d'assistant à la démonstration. Finally we will describe the main principles of a proof assistant. Poursuivant encore l'analogie avec la programmation, ceci correspondrait à la description d'un compilateur. Pursuing further the analogy with programming, this would correspond to the description of a compiler. Nous nous intéresserons principalement au système de preuves Coq. We are mainly interested in the Coq proof assistant.
Aujourd'hui, on désigne généralement par théorie des types » un formalisme logique dont les objets sont des λ-termes typés. Today, "Type Theory" refers generally to a logical formalism in which objects are typed λ-terms. 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. There are several formalisms in this category, and they are distinguished primarily by the type system more or less rich objects, as well as logic to talk about these objects. 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. These include in particular Church's higher-order logic, Martin-Löf's Type Theory, the logic of PVS and the Calculus of Inductive Constructions (CIC) which variants implemented by Coq will be the main topic of this course.
Les objets de la logique d'ordre supérieur de Church sont les λ-termes simplement typés. The objects of Church's higher-order logic are simply typed λ-terms. Les trois autres formalismes utilisent essentiellement des variantes (ou plutôt des fragments) du langage de programmation ML. The other three formalisms mainly use variants (or rather fragments) of the ML programming language. Ils se distinguent par leur logique: They are distinguished by their logic:
Sur tous ces points, nous renvoyons bien sûr au cours de tronc commun. On all these points, we refer to previous courses (for instance "Foundations of proof systems"). La plupart seront par ailleurs illustrés tout au long du cours. Most will also be shown throughout the course.
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. A key common property of CCI and Martin-Löf's Type Theory, is that they are built on the Curry-Howard correspondence. Rappelons que cela signifie que: Recall that this means that:
En simplifiant, on peut dire que les avantages informatiques de cette approche sont: To simplify, we can say that the benefits of this approach are:
Le système Coq est un système de traitement de preuves pour une version prédicative du Calcul des Constructions Inductives. The Coq system is a proof system for a version of the predicative Calculus of Inductive Constructions. Les composantes essentielles du système Coq sont: The essential components of the Coq system are:
Le formalisme implanté par Coq sera donc couramment appelé CCI. The formalism implemented by Coq is commonly called CIC. Il s'agit pour l'essentiel d'une extension du Calcul de Constructions (CC) traité en tronc commun. This is essentially an extension of the Calculus of Constructions (CC). Il nous faut dès maintenant signaler quelques différences de notations avec la syntaxe employée jusqu'ici. We must now point out some differences with the syntax notation used so far.
Tout d'abord, Coq est conçu pour pouvoir être utilisé par une interface en mode texte (ASCII ou Unicode). First, Coq is designed to be used by an interface in text mode (ASCII or Unicode). Les notations de Coq pour λ x : A . t et Π x : A . B sont: The notations in Coq for λ x: A. T and Π x: A. B are:
Par ailleurs, essentiellement pour des raisons historiques, les sortes portent d'autres noms en Coq que dans le cours de tronc commun. Moreover, mainly for historical reasons, the kinds of Coq have other names than in the original presentation of CC. Rappelons que les sortes sont des constantes particulières, qui sont les types des types. Recall that kinds are constants, which are types of 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 . In the "Foundations of proof systems" course, there was a kind Type which was the type of types, and a kind Kind which was the type of Type. Cette dernière servant essentiellement à énoncer les règles correspondant au polymorphisme . The latter serves mainly to set out the rules corresponding to polymorphism.
Dans les versions de Coq antérieures à la version 8.0, Type est remplacée par deux sortes jumelles », Prop et Set . In versions of Coq prior to version 8.0, Type is replaced by two "twin" kinds, Prop and 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). Intuitively, Set contains the types of data (computational objects) that are considered by the extraction process Coq programs and Prop (logical statements) which are erased by the extraction process.
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. Since version 8.0 of Coq, Prop plays the role of Type in the Calculus of Constructions. There is a sort named Set but it is a predicative version of Type. Typiquement, le type forall A:Set, A->A ne peut pas s'appliquer à lui-même en Coq version 8.0. Typically, the type forall A: Set, A-> A can not be applied to itself in Coq version 8.0.
Pour ne rien arranger, la sorte Kind se trouve renommée Type dans Coq. To make matters worse, CC's kind called Kind is called Type in Coq. Au lecteur qui serait tenté de 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… The reader who might find this confusing, just remember that IT is without doubt the science of bureaucracy and a somewhat tyrannical vision of order and especially renaming...
A partir de là, nous pouvons taper nos premières commandes pour utiliser le vérificateur de type. From there, we can type our first commands to use the type checker. En syntaxe Coq, l'identité polymorphe est donc notée fun (A:Type) (a:A) => a . In Coq syntax, the polymorphic identity is written fun (A : Type) (a : A) => 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: It tells the system to verify the correctness of an object by the command Check; Coq commands are always terminated by a period, this gives:
Toutes les opérations de typage de Coq ont lieu dans un environnement global. All typing operations of Coq take place in a global environment. Cet environnement correspond au contexte Γ des jugements de typage Γ ⊢ t : T . This environment is the context Γ of typing judgments Γ ⊢ t : T. Il est donc possible de pousser de nouvelles variables dans l'environnement: It is possible to add new variables to the environment:
De plus, l'environnement de Coq peut également contenir des constantes , ou abréviations. In addition, the environment of Coq can also contain constants, and abbreviations. Pour cela, on associe un terme à un nom; de plus, l'environnement mémorise aussi un des types du corps de la constante 1 . For this, we associate a term with a name again, saves the environment as one of the types of the body of the constant 1 .
Construire une preuve revient, dans notre formalisme, à exhiber un λ-terme du type attendu. Constructing a proof, in our formalism, consists in exhibiting a λ-term of the expected type. L'utilisateur dispose pour cela d'un mode de preuve interactif. To do so, the user has an interactive proof mode. Les commandes de ce mode interactif sont appelées tactiques de preuve. The commands of this interactive mode are called proof tactics. 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: Here is a rough illustration of the principles on a simple example; we are given three propositional variables A, B and C, then we try to prove the following tautology:
On a alors le lemme comme seul but courant, sous la double barre. The lemma statement is the only current goal, under the double bar. On peut commencer à construire la preuve: We can begin to build the proof:
On voit que (A->B)->C et B ont été poussées comme hypothèses dans le contexte local, au-dessus de la double barre. We see that (A-> B) -> C and B have been pushed as assumptions in the local context, over the double bar. Elles ont été nommées comme demandé. They were named as requested.
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. From the perspective of the construction of the proof, this tactic is the λ-abstraction as shown by displaying the partial proof constructed.
Une 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. Partial evidence may have several question marks, that is to say that we can have several sub-goals simultaneously, each with its local context.
La tactique apply correspond à l'application: The tactic apply corresponds to the application:
On
est alors passé au terme de preuve partiel fun
(c:(A->B)->C) (b:B) => c ?1 où le but courant est
maintenant A->C . The partial proof term is now fun
(c:(A->B)->C) (b:B) => c ?1 and the current goal is now
A-> C. On finit donc la preuve par
So we end the proof by
La commande Qed (ou Save ) permet alors d'ajouter à l'environnement global le terme exemp1 ainsi crée: The command Qed (or Save) can then be added to the global environment and creates the term examp1:
Rassurons enfin le lecteur: une preuve aussi simple peut, heureusement, également être trouvée automatiquement par les tactiques de preuve plus évoluées dont dispose le système. Finally we reassure the reader: a simple proof can fortunately be found automatically by the advanced proof tactics available. Plus généralement, ce document n'est d'ailleurs pas un manuel d'utilisateur, ni un cours de Coq. More generally, this document is not a user manual nor a course in Coq. Nous renvoyons pour cela à la documentation standard de Coq [ Coq07 ]. We refer to this in the standard documentation of Coq [ Coq07 ].
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 point fixe est appelée une définition inductive . The type of natural numbers is the smallest type containing 0 and closed under the successor S; such a definition by least fixed point is called an inductive definition.
La syntaxe en Coq d'une telle définition est: The syntax in Coq of such a definition is:
Cette commande ajoute à l'environnement du système les objets suivants: This command adds to the environment of the system the following items:
nat : Set
type nat : Set O :
nat et S : nat -> nat appelés constructeurs
de nat . the two objects O : nat and
S : nat -> nat called constructors of 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. In general, this definition (and most of those that follow) are already present in the initial environment.
Remarque
Informellemment, le plus petit type ainsi défini est celui dont les
habitants sont O , (SO) , (S (SO))
, etc. Note Informally, the smallest type with the above
closure conditions is the one which inhabitants are O , (S
O) , (S (S O)), etc.. On a
donc bien une représentation de la notion mathématique d'entier naturel.
Hence we have a representation of the mathematical concept of
non-negative integer.
Remarque
La vision informatique est que cette définition est la version Coq du
type concret ML bien connu: Note The computer vision is
that this definition is the Coq version of the well known ML concrete
type:
# type nat = O | S of nat;; # type nat = O | S of nat;;
On
peut remarquer au passage, qu'en Coq le constructeur S
est fonctionnel et peut donc exister sans son argument. It can
be noted that Coq' S constructor is functional and can
exist without its argument. Il s'agit là d'un point
syntaxique, d'importance marginale. This is a syntactic point,
of marginal importance.
Remarque
D'un point de vue ensembliste, les entiers naturels sont le plus petit
point fixe de l'opérateur suivant: Note From the
set-theoretical point of view, the natural numbers are the smallest
fixed point of the following operator:
| F ( X ) ≡ {0}⋃{( S x ), x ∈ X }. F (X) ≡ {0} ⋃ {(S x), x ∈ X}. |
Cet opérateur est monotone, et admet donc un plus petit point fixe. This operator is monotone, and therefore has a least fixpoint. En effet, l'univers des ensembles est un treillis complet par rapport à l'ordre d'inclusion. Indeed, the universe of sets is a complete lattice with respect to the order of inclusion.
Cette possibilité de voir la définition comme un plus petit point fixe sera commune à toutes les définitions inductives. This ability to see the definition as a least fixed point will be common to all inductive definitions. Par ailleurs on verra plus tard, comment ces points fixes apparaissent également dans la sémantique de la théorie. Furthermore we will see later how these fixed points also appear in the semantics of the theory.
Dans ce chapitre, nous n'expliciterons pas les règles de typage qui sous-tendent les définitions inductives. In this chapter we do not explain the typing rules underlying the inductive definitions. Elles seront explicitées en partie lors du cours 3. They will be explained in part during the course 3.
Par
défaut, les entiers de nat sont représentés en Coq via la
notation standard en base 10. By default, the integers are
represented in nat Coq via the standard notation in base 10.
Par
exemple, la notation 3 désigne l'entier naturel (S(S(SO)))
. For example, expression 3 denotes the integer
(S(S(S O))). 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. It should be made clear that the two
entries refer to the same term and are represented equally in the
system.
On verra plus loin que les symboles infixes + , * , <= , ... We will see later that, by default in Coq, the infix symbols +, *, <=, ... designate the arithmetic operations on nat. À tout moment lors d'une session Coq, on peut désactiver les notations évoluées telles que 3 , + , <= , ... At any time during a Coq session, we can disable advanced notations such as 3, +, <=, ... en utilisant la commande Set Printing All . using the command Set Printing All.
Les entiers sont l'archétype du type de données récursif. The integers are the archetype of the recursive data type. Tout comme en ML, l'on calcule sur ces entiers grâce à des fonctions définies par deux mécanismes fondamentaux: As in ML, we computed with them using features defined by two basic mechanisms:
Le premier exemple d'une telle fonction est en général l'addition. The first example of such a function is usually the addition. Voici sa définition en ML: Here is its definition in ML:
let rec plus n m =
match n with match n with
O -> m O -> m | (S p) -> S(plus pm);; | (S p) -> S (plus p m);
et l'équivalent en syntaxe Coq: and the equivalent in Coq syntax:
Et voici, de même, une définition de la multiplication: And here, likewise, a definition of multiplication:
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. We understand that Fixpoint corresponds to the definition of a recursive function, as well as ML's let rec. On note en revanche que le premier des deux arguments de chacune des deux fonctions est syntaxiquement distingué par l'emploi du mot-clé struct . We note however that the first two arguments of both functions are syntactically distinguished by the use of the keyword 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-à-dire de la terminaison des calculs. The reason is simple: when type theory, as here, is used as a logical formalism, consistency of the formalism is mainly provided by the property of normalization, i.e. the termination of the computations. Une sommaire justification informelle pourrait être donnée ainsi: supposons qu'il soit possible de définir la fonction suivante. An informal summary justification may be cited as follows: suppose it is possible to define the following function:
Il
est alors clair que l'objet (non_sens O) ne correspond
mathématiquement pas à un entier naturel, et ne saurait être accepté
dans le formalisme. It is then clear that the object (non_sense
O) is not mathematically an integer, and can not be accepted in
the formalism.
On reviendra par la suite à l'étude de la propriété de normalisation, et renverra, pour l'instant, au cours de tronc commun. We will return later to the study of standard properties, and refer, for now, to the "Foundations of proof systems" course. Retenons pour l'instant que: Remeber for now that:
Toutes les fonctions récursives acceptées par le système doivent terminer. All recursive functions accepted by the system must terminate.
Pour pouvoir définir des règles de typage, il importe donc d'isoler une classe de fonctions récursives terminantes. To define typing rules, it is important to isolate a class of terminating recursive functions. Pour ce faire, on généralise la classe des fonctions définissables dans le système T de Gödel: To do this, we generalize the class of functions definable in the system of Gödel T:
nat de la forme (S n
) . Definition 1 Consider a term of type nat
of the form (S n). Sont
considérés comme structurellement plus petit que (S n
) les termes suivants: Are regarded as
structurally smaller than (S n) the following
terms:
Une fonction est structurellement récursive si l'on peut distinguer l'un de ses arguments, qui décroit structurellement à chaque appel récursif. A function is structurally recursive if it can distinguish one of its arguments, which decreases structurally at each recursive call.
En Coq, seules des fonctions structurellement récursives peuvent être définies par Fixpoint . In Coq, only structurally recursive functions can be defined by Fixpoint.
Les fonctions plus et mult définies ci-dessus sont structurellement récursives par rapport à leur premier argument. Functions plus and mult defined above are structurally recursive according to their first argument. Bien sûr, la fonction non_sens est rejetée par le système. Of course, the function non_sense is rejected by the system.
Voici une définition alternative de l'addition, qui décroit par rapport à son second argument. Here is an alternative definition of the addition, which decreases from its second argument.
Dans le système T, seul n est considéré comme structurellement plus petit que (S n ) .In system T, only n is regarded as structurally smaller than (S n). La définition ci-dessus est plus souple, par exemple voici une définition possible en Coq du quotient de la division entière par deux: The above definition is more flexible, for example here is a possible definition in Coq of the quotient of the integer division by two:
Il faut noter que cette fonction pourrait également être définie dans le système T, mais de manière un peu plus lourde. Note that this function could also be defined in system T, but it is slightly heavier. Il s'agit donc là d'un aménagement du formalisme qui n'étend pas l'expressivité du formalisme, mais juste son confort d'utilisation. It is therefore an enhancement of the formalism that does not extend the its expressiveness, but just its usability.
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. On a different note, the mechanism of structural recursion allows the definition of complex logic functions, that is to say that grow very quickly. L'exemple le plus connu est la fonction due à Ackermann, dont voici la définition ML: The best known example is the function due to Ackermann, which ML definition is:
let rec ack = function let rec ack = function
O,m -> S(m) O, m -> S (m)
| S(n),O -> ack(n,(S(O))) | S (n), O -> ack (n, (S (O)))
| S(n),S(m) -> ack(n,ack(S(n),m));; | S (n), S (m) -> 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-à-vis de l'ordre lexicographique. Termination of this definition is justified by a decrease in the pair of arguments with respect to the lexicographic order. En terme de récursion structurelle, ceci est codé par l'utilisation de deux récursions emboîtées. In terms of structural recursion, this is coded by using two nested recursions. En Coq, la syntaxe est alors un peu plus complexe; la commande fix jouant le rôle d'un let rec…in : In Coq, the syntax is slightly more complex, fix expressions playing the role of a let rec ... in:
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 (SO) et S (S (S (SO))) .Let's give a simple (and classic) example of the use of the conversion rule: proving that 2+2 = 4, where + is the infix Coq notation for plus and 2 and 4 representations of S (S O) and S (S (S (S O))). Ici, cette proposition s'énonce: Here, the property reads:
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 : It suffices to observe that the term corresponding to 2+2 effectively reduces to 4, so that the proposition is logically identified with 4 = 4:
Remarquons que la tactique simpl , qui procède donc à la β-normalisation du but courant, ne construit pas de terme-preuve . Note that the simpl tactic, which proceeds to the β-normalization of the current goal, builds no proof-term. Cela est dû à la forme de la règle de conversion qui, rappelons-le est: This is due to the shape of the conversion rule, which we recall is:
|
On voit bien que les termes-preuves de la conclusion et de la prémisse principale sont identiques. It is clear that the proof terms of the conclusion and main premise are the same.
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é. Therefore, we could simply avoid using simpl and just use reflexivity, which builds the proof corresponding to the reflexivity of equality. La définition exacte du prédicat d'égalité sera détaillée plus tard. The exact definition of the equality predicate will be detailed later.
Le fait que nat est bien le plus petit type clos par ses deux constructeurs est exprimé par le schéma de récurrence . The fact that nat is the smallest type closed by the two constructors is expressed by the recurrence scheme. 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: This is a logical property which states: let P be a predicate on integers, so that the proposition P (n) is true for any integer n, it suffices that the two following conditions are satisfied:
Dans une logique d'ordre supérieur, ce schéma peut être exprimé comme une proposition. In a higher-order logic, this scheme can be expressed as a proposition. En syntaxe Coq: In Coq syntax:
forall (P: nat -> Prop), forall (P : nat -> Prop),
(PO) -> (P O) ->
(forall (m:nat), (P m)->(P (S m)))-> (forall (m : nat) (P m) -> (P (S m)))->
forall (n:nat), (P n) 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. In fact, the definition of an inductive type automatically generates a proof of the corresponding recurrence scheme. Si le type inductif est nommé I , la preuve du schéma de récurrence s'appellera I_ind ; par exemple: For each inductive type I, a proof of the recurrence scheme is called I_ind; for example:
L'utilisation du schéma de récurrence en Coq se fait grâce aux tactiques elim et induction . The recursion scheme is used by invoking the induction and elim tactics.
Voici un autre exemple simple, combinant le calcul et le raisonnement par récurrence. Here is another simple example, combining computation and mathematical induction. Il s'agit de prouver une première étape vers la commutativité de l'addition, à savoir: This is a first step towards proving the commutativity of addition, namely:
Cette preuve se fait bien sûr par récurrence sur n ; le cas de base est trivial: This proof is of course by induction on n, the base case is trivial:
Pour le cas par récurrence, on peut procéder à une étape de réduction: For the induction case, we can make a reduction step:
Il suffit alors d'utiliser l'hypothèse de récurrence pour remplacer dans le but courant, p+0 par p ; cela peut se faire par: It then suffices to use the induction hypothesis to replace the current goal, n+0 for n; this can be done by:
Comme en ML, le principe de définitions inductives permet la construction de types de données plus complexes que les entiers. As in ML, inductive definitions allows the construction of more complex data types than integers. Suivent quelques exemples courants. Here are some common examples.
Il est sans doute inutile de rappeler la structure des listes, avec leurs deux constructeurs nil et cons . It is perhaps worth recalling the structure of lists, with their two constructors nil and cons. La commande définissant les listes d'entiers naturels est bien sûr: The command defining the lists of natural numbers is, of course:
Une première remarque, marginale, est que contrairement à ML, les constructeurs peuvent avoir plusieurs arguments: ici cons est curryfié. A first remark, marginal, is that, unlike ML, constructors can have several arguments: here cons is curried.
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. It is best to replace the previous definition by another where the type of list elements is a parameter. La bonne définition des listes est: The correct definition of the lists is:
Il s'agit de la même définition, mais paramétrée par le type A . This is the same definition, but parameterized by the type A. Cette abstraction est possible grâce aux types fonctionnels: This abstraction is made possible by functional types:
A titre d'exemple, on écrira ainsi l'équivalent de l'objet ML [1;2;3]: For example, we write the equivalent of the ML list [1; 2; 3]:
À 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: Provided you use the definition set out in the List module of the standard library of Coq, we can also use the following notation:
Le schéma de récurrence structurelle sur les listes est: The recursion scheme on lists is:
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 . We recognize the same structure as for integers, but with the additional argument of cons and the parameterization with respect to A.
Un exemple courant de type paramétré est le type somme: A common example of parameterized type is the sum type:
Son schéma d'élimination est plus simple, puisque le type est non récursif; il s'agit juste d'exprimer que tout élément de (sum A B) ne peut être construit qu'à partir de l'un des deux constructeurs: Its elimination scheme is simpler, since the type is non-recursive, it is just to express that every element of (sum A B) can be built only from one of two constructors:
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. In all examples of recursive types seen so far, the order corresponding to the recursion (and recurrence) merged with the structural sub-term relationship. Le mécanisme des types inductifs autorise toutefois des constructions plus générales. The mechanism of inductive types, however, allows more general constructions.
La définition qui suit est souvent appelé type des ordinaux » par abus de langage. The following definition is often called "type of ordinals" by abuse of language. Il s'agit en fait d'une notation ordinale, qui ne permet que la représentation d'un fragment des ordinaux constructible dans CCI. It's actually an ordinal notation, which allows the representation of a fragment of ordinals constructible in CIC. Il s'agit d'une copie du type des entiers naturels, étendue par un nouveau constructeur correspondant à la limite ordinale: This is a copy of the type of natural numbers, extended by a new constructor corresponding to limit ordinals:
On remarque que le constructeur lim est récursif, mais que son argument est une suite entière d'ordinaux. Note that the constructor lim is recursive, but that his whole argument is a sequence of ordinals.
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 petit que ( limit f ). The order of structural recursion is then generalized as follows: any n terms of type nat and f type nat → ord (f n) is structurally smaller than (f limit).
Voici une définition légale de fonction sur ce type des ordinaux: Here's a legal definition based on this type of ordinals:
Cette vision de la récursion structurelle est également reflétée dans l'énoncé du schéma de récurrence du type: This vision of structural recursion is also reflected in the statement of the type of the recurrence scheme:
C'est-à-dire que pour appliquer le schéma spécialisé à un prédicat P , il faut vérifier que si: That is to say that to apply the scheme specialized to a predicate P, we must check whether:
alors (lim f ) vérifie également P . then (lim f) also satisfies P.
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. You can use the previous idea to define a very general type of trees: using polymorphism, sons of each node can be indexed by an arbitrary type.
Ce type est très peu intuitif. This is very intuitive. Il utilise et combine toutes les ressources du formalismes et permet ainsi la construction de très nombreux éléments. It uses and combines all the resources of the formalism and allows the construction of many elements. 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. In fact, the English logician Peter Aczel has shown that it is possible to encode the objects of set theory in this type.
Nous avons vu comment construire des objets concrets. We have seen how to build concrete objects. Le mécanisme de définitions inductives permet également la définition d'objets plus logiques, et en particulier de prédicats. The mechanism of inductive definitions allows the definition of more logical objects, and in particular predicates. 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. In particular, this is usually the most convenient way to discriminate some of the elements of an inductive type.
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: In set theory, a possible definition of the set of even numbers is said to be the smallest set such that:
La même définition est possible dans CCI. The same definition is possible in CIC. Le prédicat even , être pair », étant un objet de type nat →Prop. Predicate even, "being even" is an object of type nat → Prop. Les deux clauses de la définition ci-dessus correspondant aux deux constructeurs du prédicat inductif . The two clauses of the definition above for the two constructors of the inductive predicate. En Coq: In Coq:
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 . It is clear that the structure of a proof of "even-ness" is recursive, just like the structure of a term of type nat. Ceci est reflété dans le schéma de récurrence qui permet de prouver des propriétés d'entiers pairs: This is reflected in the recurrence scheme, used to prove properties of even numbers:
Un exemple essentiel est l'ordre sur les entiers: A key example is the order of the integers:
Son principe de récurrence: Its induction principle:
Exercice Prouver: Exercise Prove:
forall n m : nat, le n m -> le (S n) (S m) forall (n:nat), (le O n)forall n: nat, le O n forall (nm:nat), (le nm)->(le mp)->(le np)forall n m p: nat, le n m -> le m p -> le n p
Voici un exemple pour illustrer les subtilités propres aux mathématiques formelles. Here is an example to illustrate the intricacies specific to formal mathematics. On peut proposer une définition alternative à le : We can suggest an alternative definition to:
Or cette définition, qui semble raisonnable et est mathématiquement saine, est peu praticable telle quelle. But this definition, which seems reasonable and is mathematically sound, is not easy to use as it is. 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. In particular the proof of transitivity is very painful. You can use this definition, but for some properties, it is best to start by first proving the equivalence with the previous definition. L'on risque sinon de s'ensabler rapidement. Proofs might otherwise be much more complicated.