Je tiens, avant tout, à remercier le Responsable scientifique Yves Bertot, pour m'avoir prise en stage. Je souhaite aussi lui témoigner ma reconnaissance pour l'aide et les conseils qu'il m'a apportés dans la réalisation de mon stage et la patience dont il a fait preuve. Sa connaissance et son soutien m'ont indiscutablement été d'un grand secours.
J'aimerais aussi adresser de chaleureux remerciements au Responsable permanent Laurence Rideau, qui m'a aussi servi de guide dans mes premiers pas dans le domaine de la recherche, ses conseils et son soutien moral m'ont beaucoup aidé dans ce travail et ont été d'un grand réconfort dans les moments de doute.
Ma vive gratitude au Professeur Michel Rueher, qui m'a donné la chance d'étudier en France et de faire mes études supérieures à l'École Supérieure en Sciences Informatiques. Ses conseils m'ont été très précieux.
Que soit particulièrement remercié mon Professeur Emmanuel Kounalis, qui m'a fait l'honneur d'être le rapporteur de mon travail.
Mes remerciments les plus vifs à Francis Montagnac, qui m'a beaucoup aidée lors de mes problèmes techniques liés à ma faible connaissance initiale du système.
Je remercie également Yann Coscoy pour sa patience et sa gentillesse, qui combinées à son expérience m'ont beaucoup aidée dans la compréhension du sujet de mon stage.
Lorsqu'une personne arrive dans un pays étranger elle est confrontée à une nouvelle culture, à un langage différent et à des personnes nouvelles. Je tiens donc, à remercier l'ensemble de l'équipe CROAP qui m'a accueilli à l'INRIA-Sophia Antipolis, pour son amitié, sa patience, ses conseils et son humeur. Grâce à cette équipe mon stage s'est déroulé dans une ambiance remarquable.
Depuis plusieurs années, le projet CROAP s'intéresse à l'utilisation de systèmes de preuve pour les tâches de programmation. Ces recherches sont menées suivant deux lignes directrices:
Dans les cas où les outils de preuve sont accompagnés d'outils de production de programmes à partir des algorithmes décrits, ceci permet de développer des programmes absolument sans erreur.
Des chercheurs de CROAP ont développé des outils et des compétences dans ces deux directions autour du Système Coq.
Dans toutes ces tâches, on est amené à construire des fonctions mathématiques récursives. C'est pourquoi nous présentons ici ce type de fonctions.
En mathématiques, la récurrence est le nom donné au procédé qui définit une fonction ou un processus à l'aide de la valeur de cette fonction en un autre point.
Un bon exemple d'une fonction définie récursivement est la fonction factorielle avec argument positif et entier :
fact(0) = 1
fact(n) = n * fact(n -1) sin ≠0
Ici fact(n)est définie à l'aide de fact(n
-1), qui est définie à l'aide de fact(n -2),
jusqu'à ce que l'on atteigne fact(0)qui est explicitement
défini.
Toute définition récursive doit avoir une définition explicite pour une ou plusieurs valeurs des arguments, sinon la définition se refermerait sur elle-même.
En Coq, les fonctions peuvent être définies récursivement en respectant des contraintes: par récurrence primitive sur la structure des arguments ou par référence à un ordre bien fondé; c'est-à-dire que la fonction ne se rappelle récursivement que sur des valeurs décroissantes ordonnées par un ordre bien fondé (un ordre ne contenant pas de chaînes infinies décroissantes), assurant que la fonction ne pourra pas se rappeler indéfiniment.
Naturellement quand on parle de fonction récursive f, il
existe une équation de point fixe:
f x = F (f, x)
Où F est une fonctionnelle, c'est à dire une
fonction dont l'un des arguments est une fonction. Par exemple, la fonction
Factorielle est le point fixe d'une fonction F qui est
définie par:
F(f , a) = if a = 0 then 1
else a*f(a-1)
Le but final du stage est de trouver une méthode automatique qui aboutira aux preuves de l'équation de point fixe, pour n'importe quelle fonction définie sur un ordre bien fondé. Pour expliquer en détails l'équation de point fixe, il est indispensable de décrire la théorie des types.
Aujourd'hui, on désigne généralement par " Théorie des types " un formalisme logique dont les objets sont des λ-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 manipulés, 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 et le Calcul des Constructions Inductives.
Les objets de la logique d'ordre supérieur de Church sont les λ-termes simplement typés. Les deux autres formalismes utilisent essentiellement des variantes du langage de programmation ML.
Ils se distingent par la logique utilisée:
récurrence [DOWEK98].
Un point commun essentiel au Calcul des Constructions et à la théorie de Martin-Löf est bien sûr qu'ils sont construits sur l'isomorphisme de Curry-Howard. Rappelons que cela signifie que:
P est un objet p de
type P.
Par exemple: Pour prouver la propriété de la symétrie de
Plus, on a la preuve suivante:
plus_sym=[n, m:nat]nat_ind [n0:nat] (plus n0 m)= (plus m n0) (plus_n_0 m)[y:nat](H:(plus y m)=(plus m y)]
(eq_ind nat (S (plus m y)) [n0:nat] (S (plus y m))= n0
(eq_S (plus y m) (plus m y) H) (plus m (S y)) (plus_n_Sm m y)) n): (n,m:nat) (plus n m)=(plus m n)
(n,m:nat) (plus n m)=(plus m n),qui
signifie pour tous les entiers n et m la proposition (plus
n m)=(plus m n) est vraie. Cette proposition est le type de l'objet
plus_sym.
(n,m :nat) (plus n m)=(plus m n) est
l'objet plus_sym dont le type est égal à cette
proposition.
En simplifiant, on peut dire que les avantages informatiques de cette approche sont :
L'écriture de la fonctionnelle F de l'équation de
point fixe, est obtenue facilement quand on est dans le cas d'une fonction
structurellement récursive. Par exemple, nous avons donné sa
valeur pour la fonction Factorielle.
Par contre, l'écriture de F devient plus
compliquée quand on se retrouve avec des fonctions définies sur
un ordre bien fondé.
Dans le cas de récursion sur un ordre bien fondé, on impose
à F de prendre en premier argument la donnée
x de type A,(A étant un ensemble
prédéfini) et en deuxième argument une fonction f
qui ne pourra être appelée que sur des arguments plus
petits que x.
Ceci peut être exprimé en imposant à f le
type suivant :
f:(y:A)(y < x) -> B
Ce type exprime que f prend deux arguments, le premier argument
y de type A et le deuxième étant une
preuve que y est plus petit que x.On voit que le
type de f dépend de x et que le type du
deuxième argument de f dépend de y.
Cette caractéristique est permise par les types dépendants du
système Coq. C'est pour cette raison qu'on a été
obligé d'intervertir les arguments de F.
F doit donc avoir le type suivant: F:(x:A)(f:(y:A)(R y x)->
B)B.
Le système Coq fournit un opérateur appelé
well_founded_induction qui prend une preuve que l'ordre R
est bien fondé, une fonctionnelle F et retourne une
fonction de A dans B.
Le type de well_founded_induction est en fait plus
compliqué que nous le laisse entendre cette explication intuitive. Ce
type utilise la propriété well_founded et est
donné formellement par :
: (A:Set)
(R:A->A->Prop)
(well_founded A R)
->(P:A->Set) ((x:A) ((y:A) (R y x) -> (P y)) -> (P x)) -> (a:A) (P a).
Avec le théorème well_founded_induction,
l'équation de point fixe devrait avoir la forme suivante:
well_founded_induction F a = F a [y:A] [h:y<x](well_founded_induction
F)
La fonction retournée est le point fixe de F. Mais la
démonstration de cette équation est difficile à obtenir
et le sujet de ce stage est de fournir une approche systématique
à ce problème. Nous avons utilisé le système Coq
à cet effet. Pour cela, nous allons présenter dans la partie
suivante ce système avant de décrire son utilisation dans notre
travail.
Coq est un système d'aide à la preuve développé à l'INRIA-Rocquencourt et à l'Ecole Normale Supérieure de Lyon et depuis 1997 au L.R.I. à Orsay.
Ce système est écrit en Ocaml. Le langage Ocaml est un langage fonctionnel de la famille ML développé à l'INRIA-Rocquencourt.
(a:A) et se
lit " pour tout a dans A".
Les crochets définissent les fonctions (comme les lambda-abstractions du λ-calcul).
Par exemple :
[a:A]t est la fonction qui à a de type
A associe le terme t.
La quantification universelle est le pendant dans les types de la définition des fonctions:
Si t est de type B, alors [a:A]t est de
type (a:A)B.
Coq abrège (a:A)B en A->B quand
B ne dépend pas de la variable a, et on retrouve le
type des fonctions de A dans B.
Habituellement, un ensemble défini inductivement est le plus petit
ensemble vérifiant un certain nombre d'axiomes. Par exemple l'ensemble
des entiers naturels est le plus petit type clos par ses deux constructeurs
qui sont O et S (Successeur).
Coq permet ce genre de définition, pour cela on dispose du mot clef
Inductive. On définit donc les entiers par:
Inductive nat : Set :=
O : nat
| S : nat -> nat.
Ce qui construit effectivement les objets nat:Set, 0:nat,
S:nat -> nat, mais le système Coq fournit de plus un
théorème de récurrence qui a la forme suivante:
Etant donné un P qui est un prédicat sur les
entiers; pour que la proposition P(n) soit vraie pour tout n;
alors on a besoin de prouver que les deux conditions suivantes sont
vraies:
P(0) est vrai
P(n) est vraie alors P(S(n)) est
vraie aussi .
En syntaxe Coq, c'est à dire dans une logique d'ordre supérieur, ce schéma sera exprimé comme une proposition:
(P: nat -> Prop)(P 0) -> ((m: nat) (P m) -> (P (S m))) -> (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 < Check nat_ind.
nat_ind
: (P: nat -> Prop) (P 0) -> ((n: nat)(P n) -> (P (S n))) -> (n: nat) (P n).
Dans Coq il y a trois façons différentes de définir des fonctions:
Correspond à la définition de la fonction sans récursion.
Le λ-calcul, est la formalisation de la notation mathémathique usuelle pour définir des fonctions.
Par exemple: f: nat -> nat
x -> x+2
devient en utilisant la syntaxe de Coq:
Coq < Definition f := [x:nat] (S(S x)).
On peut alors calculer:
Coq < Compute (f (S O)).
= (S(S(S O)))
: nat.
On parle de λ-calcul, car en logique Mathémathique, on note en général λx: T.t
Pour ce qui s'écrit [x:T]t en Coq.
En plus du λ-calcul typé, on peut, définir en Coq, des fonctions par cas, sur les types inductifs. Par exemple, la fonction prédecesseur peut être définie grâce à la commande suivante:
Coq < Pred = [n:nat] <nat> Cases n of O -> O |(S u) -> u end. : nat -> nat.En mathématique usuelle, une fonction peut être définie par son graphe.
En Coq, une fonction est définie par un algorithme ou une méthode de calcul. Les fonctions de Coq sont donc à mi-chemin entre les programmes et les fonctions (ou plutôt les applications ).
On peut utiliser le même mécanisme pour définir des fonctions récursives.
Supposons par exemple, qu'on veut définir l'addition:
Sa définition en ML est :
let rec plus n m =
match n with
O -> m
|(S p) -> S (plus p m);;
La même fonction est définie en Coq en utilisant la construction
"Fixpoint" qui permet de définir des fonctions
récursives.:
Fixpoint plus [n: nat] : nat-> nat :=
[m: nat] Cases n of
O -> m
|(S p)-> (S ( plus p m))
end.
Cette fonction plus est une fonction structurellement
récursive par rapport à son premier argument n. La
fonction plus se rappelle sur l'argument p qui est
un sous terme du (S p) lors de son appel récursif. Toute
fonction structurellement récursive est acceptée par le
système Coq.
L'exemple suivant ne correspond à aucune fonction mathématique, car son algorithme ne termine pas. Il est refusé par le système :
Coq < Fixpoint foo [n: nat] : nat :=
Cases n of
O -> O
|(S a) -> (foo ( S a))
end.
Cette condition de terminaison est nécessaire pour assurer la cohérence logique du système.
Avec la définition par Fixpoint on aura une
vérification automatique de type et de la condition d'arrêt de la
fonction car Fixpoint permet seulement la récursion sur
des sous termes structurels. De plus, l'évaluation de la fonction est
bien intégrée au système.
Avec cette définition on est capable de calculer automatiquement que :
plus(O,O) = O.
Ce troisième choix de définition de fonction est le sujet de la troisième partie de ce rapport.
Un Ordre Bien Fondé est un ordre défini sur un ensemble tel qu'il n'existe pas de chaîne infinie décroissante.
Avec un tel ordre, on peut raisonner en utilisant un principe d'induction bien fondée qui a la forme suivante:
Soit < un ordre Bien Fondé sur un ensemble A.
Soit P une propriété sur les éléments de l'ensemble A.
On a alors:∀a∈A P(a)
Si et seulement si on a ∀a∈A.((∀b∈A. b<a ->P(b))->P(a)).
Signalons qu'avec une induction bien fondée, il s'agit d'une méthode de preuve par induction sur une relation bien fondée, qui généralise la récurrence sur les entiers et l'induction structurale sur les termes.
Un théorème important pour les ordres bien fondés est le suivant:
Un ordre R est un ordre bien fondé sur un ensemble A
Si et Seulement Si tout sous ensemble non vide Q de A a un élément minimal.
Avec l'Ordre Bien Fondé on peut prouver la terminaison d'une fonction.
Pour montrer qu'une fonction termine, on peut montrer que durant son execution elle fait décroître une valeur dans un ensemble bien fondé c'est à dire défini par un Ordre bien fondé et donc est appelée sur une suite décroissante non infinie par définition.
En Coq, la manipulation des fonctions définies par récursion primitive est particulièrement bien intégrée dans le moteur de raisonnement. En revanche, les fonctions définies par récurrence sur un ordre bien fondé sont plus difficiles à mettre en oeuvre.
Pour donner un exemple, une fonction "f" décrite par
récurrence bien fondée de A vers B est
décrite par une fonctionnelle F de type (A ->B) ->(A
->B) telle que f(x)=F(f,x).
Ce qui est dommage en Coq, c'est que cette égalité n'est pas fournie et difficilement prouvable.
On a choisi l'ordre bien fondé car il nous permet de vérifier si la fonction se rappelle sur un argument plus petit en utilisant des ordres plus généraux que l'ordre structurel. Par exemple, la fonction d'Ackermann ne se rappelle pas sur un argument structurellement plus petit mais sur un argument plus petit pour l'ordre lexicographique sur les paires d'entiers. Nous rappelons que la fonction d'Ackermann est définie en ML par :
let rec ack = function
(0, m) -> S(m)
| (S(n), 0) -> ack(n, (S 0))
| (S(n), S(m)) -> ack(n, ack(S(n), m));;
Parmi les ordres bien fondés utiles pour prouver certaines
propriétés de terminaison, il faut mentionner les ordres
définis lexicographiquement sur un produit cartésien.
Étant donnés deux ordres < 1 et
sur deux ensembles
et
, l'ordre lexicographique < sur
défini à partir des ordres < 1
et < 2
est défini par:
(x, y) < (x', y') Si et Seulement Si x < 1 x' ou (x = x' et y
< 2 y')
Il est assez facile de vérifier que si les ordres < 1
et
sont bien fondés, l'ordre < l'est également.
On peut par exemple utiliser l'ordre lexicographique sur les couples d'entiers naturels pour prouver la terminaison de la fonction d'Ackermann .
Le principe de preuve est le suivant :
Etant donnée une relation d'ordre bien fondé < sur un ensemble E, pour démontrer une propriété
∀ x P(x), il suffit de montrer
(∀y < x
P(y)) => P(x).
Par conséquent, pour démontrer que le calcul de
ack(m,n) termine pour tout couple (m,n) d'entiers
naturels, il suffit de montrer ce fait sous l'hypothèse que
ack(m',n') termine pour tout couple (m', n') plus
petit que (m,n). Dans le cas où m et n sont
différents de 0, on peut ainsi utiliser le fait que
(m,n-1) est plus petit que (m,n) pour conclure que
le calcul de ack(m,n-1) se termine. Si on appelle alors p la
valeur de cette expression , on peut de nouveau utiliser le fait que le couple
(m-1,p) est plus petit que (m,n) pour conclure que
le calcul de ack(m-1,p) se termine et que par conséquent
celui de ack(m,n) se termine aussi. On a donc établi que
la fonction ack est totale (sur les couples entiers
naturels).
L'intérêt de cette partie est de présenter ce qu'est la fonctionnelle associée à une définition récursive, de donner les différentes étapes à suivre pour définir une fonction basée sur un ordre bien fondé, de prouver l'équation de point fixe et de présenter deux exemples de preuves.
Les fonctions étant considérées comme des valeurs à part entière, il est naturel qu'elles puissent apparaître comme arguments ou résultats d'autres fonctions.
Les fonctions prenant des arguments fonctionnels ou rendant des résultats fonctionnels sont dites d'ordre supérieur [G.Cousineau].
Considérons par exemple la fonctionnelle h qui
à toute fonction f(x) associe la fonction
f(x)/x.
On peut la définir en ML par:
let h= (fun f -> (fun x -> f(x)/x));;
h:(float -> float) -> float -> float = <fun>.
Pour définir une fonction f basée sur un ordre bien
fondé et prouver l'équation de point fixe, on a besoin de:
F correspondante.
Soient A:Set un ensemble de départ, n une
fonction de A vers A et B:Set
l'ensemble d'arrivée. Dans notre premier essai, nous avons
supposé que R est un ordre bien fondé sur
l'ensemble A et que H_n_decrease est une preuve que
(n a)
a selon l'ordre R ainsi choisi.
Puis nous avons considéré une fonction f qui traite
deux cas qui sont définis à l'aide de la variable
base_dec:
base_dec: (a: A) {(base a)}+{~(base a)}
Qui se lit pour tout x élément de A,
soit x est le cas de base, soit x n'est pas le cas
de base.
Definition F:=
[a:A] [f:(y:A) (R y a) -> B]
<B> Case (base_dec a) of
[h: (base a)] (gb a)
[h:~(base a)] (gr (f (n a) (H_n_decrease a h)))
end.
Signalons que le cas de base est le cas d'arrêt de la fonction où
il n'apparaît aucun appel récursif et qui étant
donné un élément de type A retourne,
à l'aide de la fonction gb,un élément de
type B. Par contre, l'autre cas est le cas de la
récursivité, on a donc besoin d'une preuve supplémentaire
assurant que lors de l'appel récursif, on se rappelle sur un argument
plus petit suivant l'ordre choisi.
Dans notre premier exemple, l'argument sur lequel on se rappelle est (n
a) et H_n_decrease est la preuve que (n
a) est plus petit que a. La deuxième argument
"h" est donnée pour préciser que l'on est dans le
cas de ~(base a).
H_n_decrease:(a:A) ~(base a) -> (R (n a) a)
Durant la preuve de l'équation de point fixe, on a besoin du fait que
l'ordre ainsi choisi vérifie la propriété de
transivité; Ici on a donné la propriété de
transivité à R comme un axiome:
Axiom R_trans: (a, b, c:A) (R a b)->(R b c)->(R a c).
Après avoir prouvé l'équation de point fixe dans notre premier exemple, on a choisi la fonction d'Ackermann comme un deuxième exemple pour notre preuve, car c'est une fonction non primitive récursive. On a suivi les 6 étapes suivants:
A:Set qui est l'ensemble des
couples : nat*nat.
lex.
nat.
lex vérifie bien la transivité est
donnée par lex_trans.
F a la forme suivante:
Definition ackermann :=
(well_founded_induction nat*nat lex well_founded_lex [_:nat*nat]nat F).
Définition F:(a:nat * nat) ((b:nat * nat) (lex b a) -> nat) ->nat :=[a:nat * nat]<[a:nat * nat] (f:(b:nat * nat) (lex b a) ->nat)nat > Cases a of(pair O n) => [f:(b:nat * nat) (lex b (O,n)) ->nat] (S n)| (pair (S n) O) =>[f:(b:nat * nat) (lex b ((S n),O)) -> nat](f (n,(S O)) (th2 n O (S O)))|(pair (S n) (S m))=>[f:(b:nat * nat) (lex b ((S n),(S m))) -> nat](f(n,(f ((S n), m) (th3 (S n) m)))(th2 n (S m) (f ((S n),m) (th3 (S n) m)))end.
Pour définir la fonctionnelle F d'Ackermann, on a besoin
des théorèmes suivants:
Theorem th2: (n, m, p:nat) (lex (n, p) ((S n), p)).
C'est dans le cas où le premier argument du premier couple est inférieur au premier argument du deuxième couple.
Theorem th3: (n, m:nat) (lex (n, m) (n, (S m))).
C'est dans le cas où les deux premiers arguments des deux couples sont égaux alors il faut passer au deux autres arguments pour les comparer.
Les problèmes rencontrés lors de la définition de la
fonctionnelle F d'Ackermann sont les suivants:
Quand on utilise la définition par cas normalement toutes les parties droites (à droite de =>) des règles doivent être de même type.
Mais dans notre définition le Type Checker de Coq n'arrive pas à unifier ((S n) , 0) qui se trouve dans la partie droite du deuxième cas avec la paire a .
On a donc été obligé d'ajouter
< [a: nat * nat ].(f:(b: nat
*nat)(lex b a)-> nat) nat >
qui n'est autre que le type de retour de Cases a,pour
qu'on puisse changer le type de a (parties gauches) à
chaque cas. (On parle d'un type dépendant de la forme de
a).
Donc pour un certain couple donné on aura une fonction f
qui prend pour argument un deuxième couple qui vérifie
bien l'ordre lexicographique et son type de retour est bien un
nat.
Et on aura comme réponse :
(S n).
f appliquée au
couple (n ,(S 0))et une preuve que (n ,(S 0)) est
plus petit que ((S n),0) pour l'ordre
grâce au théorème th2.
f appliquée au couple
(n ,(f((S n ),m) et une preuve que ((S n),m)
((S n),(S m)) en utilisant le théorème th3; et une
preuve que le couple(n,(f((S n),m)))
((S n),(S m))en utilisant le théorème th2.
Donc on a permis au système Coq de bien vérifier dans chaque
cas que le deuxième couple de (lex b ...) est bien le
a dont on parle.
Dans chaque cas, f a besoin d'une preuve et d'un énoncé qui sont differents. Alors on peut dire que le type de f dépend de la valeur de a qui change à chaque cas.
Dans cette partie, nous présentons les scripts de preuve des deux exemples: wf_essai et Ackermann et nous terminons par une comparaison de ces deux exemples.
Lemma l1:
(a:A)
(well_founded_induction A R H_well_founded_R P F a) =
(F a [y:A] [h: (R y a)]
(well_founded_induction A R H_well_founded_R P F y)).
Intro.
Apply (well_founded_ind
A R H_well_founded_R
[a: A]
(well_founded_induction A R H_well_founded_R P F a) =
(F
a
[y: A] [_: (R y a)]
(well_founded_induction A R H_well_founded_R P F y)).
Intro x.
Unfold 3 well_founded_induction.
Elim (H_well_founded_R x) using Acc_ind2.
Simpl.
Intros x0 accessible H_rec_acc H_rec_well_founded.
Cut (y:A) (y0: (R y x0))
<(P y)>
(Acc_rec
A R P
[x:A] [_:(y1:A) (R y1 x) -> (Acc A R y1)]
[H2:(y1:A) (R y1 x) -> (P y1)]
(F x H2) y (accessible y y0)) =
(well_founded_induction A R H_well_founded_R P F y).
Intro H_rec_acc'. (* La partie qui suit le Unfold F est specifique à chaque fonction traitée:*)
(***************************************************************************) Unfold F.
Case (base_dec x0); Auto.
Intro.
Rewrite H_rec_acc';Auto. Intros y1 H';Try Assumption.
Rewrite H_rec_well_founded.
Apply H_rec_acc.
Intros. Apply H_rec_well_founded.
Apply R_trans with y:=y1; Auto. Exact H'
Qed.
Lemma l1:
(a:nat*nat)
(well_founded_induction
nat*nat lex H_well_founded_lex [_:nat*nat]nat F a) =
(F
a
[b:nat*nat] [h: (lex b a)]
(well_founded_induction
nat*nat lex H_well_founded_lex [_:nat*nat]nat F b)).
Intro.
Apply (well_founded_ind
nat*nat lex H_well_founded_lex
[a:nat*nat]
(well_founded_induction
nat*nat lex H_well_founded_lex [_:nat*nat]nat F a)=
(F
a
[y:nat*nat] [_: (lex y a)]
(well_founded_induction
nat*nat lex H_well_founded_lex [_:nat*nat]nat F y))).
Intro x.
Unfold 3 well_founded_induction.
Elim (H_well_founded_lex x) using Acc_ind2.
Simpl.
Intros x0 accessible H_rec_acc H_rec_well_founded.
Cut (y:nat*nat) (h: (lex y x0))
<nat>
(Acc_rec
nat*nat lex [_:nat*nat]nat
[x:nat*nat]
[_:(y0:nat*nat) (lex y0 x) -> (Acc nat*nat lex y0)]
[H2:(y0:nat*nat)(lex y0 x) -> nat]
(F x H2) y (accessible y h)) =
(F
y
[y1:nat*nat] [_:(lex y1 y)]
(well_founded_induction
nat*nat lex H_well_founded_lex [_:nat*nat]nat F y1))).
Intro H_rec_acc'.
2:Intros y y0.
2:Apply H_rec_acc.
2:Intros y1 H'.
2:Apply H_rec_well_founded.
2:Apply lex_trans with b:=y; Auto.
Generalize H_rec_well_founded H_rec_acc' accessible.
Cette partie qui suit le Unfold F est specifique à cette fonction
Unfold 7 9 F.
Case x0. Intro n; Case n. Intros n0 a1 H' H'0;Auto. Intros p n0; Case n0. Clear H_rec_acc' H_rec_well_founded H_rec_acc accessible. Intros accessible H_rec_well_founded H_rec_acc'. Rewrite H_rec_acc'. Rewrite H_rec_well_founded; Auto. Apply th2. Clear H_rec_acc' H_rec_well_founded H_rec_acc accessible. Repeat Rewrite H_rec_acc'. Repeat Rewrite H_rec_well_founded; Auto. Apply th3. Apply th2. Apply th3. Qed.
En comparant les deux preuves wf_essai et Ackermann, on a remarqué
qu'elles étaient comparables jusqu'à l'étape où
l'on s'interresse à la structure interne de la fonction traitée.
Dans le cas du wf_essai, juste après avoir remplacé la
fonctionnelle F par sa définition (en utilisant la
tactique Unfold F), on execute la tactique Case x0
et on traite les différents cas; alors que dans le cas d'Ackermann on a
remarqué que, lors de notre preuve, on a déjà fixé
x0 dans les hypothèses alors que le but courant est de
faire une preuve pour tout x0,c'est à dire x0
désigne n'importe quel objet. D'où si on execute Case
x0 directement après le Unfold F, comme dans le cas
de wf_essai, le système nous génère une erreur car on a
toujours des types dépendants sur les arguments. Pour résoudre
ce problème, on a introduit la tactique Generalize sur
toutes les hypothèses qui contiennent x0 qui sont:
accessible, H_rec_well_founded et
H_rec_acc' avant la tactique Unfold F.
accessible:∀y:A. (R y x0) => (Acc A R y)
H_rec_well_founded:∀y:A.(R y x0) =>
<P y>
(well_founded_induction A R H_well_founded_R P F y) =
(F
y
λy0:A.λ_:(R y0 y).
(well_founded_induction A R H_well_founded_R P F y0))
H_rec_acc':∀y:A.∀y0:(R y x0)
<P y>
(Acc_rec
A R P
λx:A
λ_:∀y1:A.(R y1 x) => (Acc A R y1).
λH2:∀y1:A.(R y1 x) => (P y1 x) =>(P y1).(F x H2) y (accessible y y0)) =
(F
y
λy1:A.λ_:(R y1 y).
(well_founded_induction A R H_well_founded_R P F y1))
Signalons que H_rec_well_founded et H_rec_acc' sont
deux hypothèses de récurrences. La première est
basée sur le fait que l'ordre qu'on a choisi est un ordre bien
fondé, d'où tout élément est accessible. La
deuxième, nous sommes obligés d'ajouter une preuve
(accessible y y0) qui est la preuve que y est
accessible car y est plus petit d'un certain x0 qui
lui, est accessible.
Un élément x est dit accessible si
et seulement si tout élément plus petit que x est
accessible (Il s'agit d'une définition récursive). Ainsi un
ordre est bien fondé si et seulement si tout élément est
accessible. En Coq, le théorème de well_founded est
basé sur le fait que tout élément est accessible.
Une fois qu'on applique le Unfold F la partie qui suit dans notre
preuve dépend de la structure de la fonction traitée. Il suffit
alors de regarder la structure de la fonction et appliquer les tactiques
correspondantes.
C'est pour cette raison qu'il faut généraliser notre preuve et faire une méthode automatique qui aboutira aux tactiques de preuves qu'il faut pour prouver l'équation de point fixe, pour n'importe quelle fonction définie sur un ordre bien fondé.
La première étape dans notre traitement était de préciser les différentes formes que peut prendre une expression. Une expression peut être:
| 1-QuestioM |
: C'est le système qui va essayer de déterminer le lambda terme
manquant par unification. |
| 2- Ident | : Un identificateur du type chaîne. |
| 3- App | : C'est une application d'une fonction sur une liste d'expressions. |
| 4- Cases | : Permet la définition d'une fonction par cas. |
| 5- Lambda | : Permet la définition d'une fonction. |
| 6- Forall | : C'est le type de la fonction. |
Les tactiques sont des règles de transformations logiques qui sont valides. Ceci assure la correction des preuves qui les utilisent. Néanmoins, toute preuve obtenue par une succession de tactiques est, avant d'être acceptée, formellement vérifiée par le mécanisme de typage de Coq: le type d'une preuve doit être le théorème qu'elle est censée démontrer.
Dans les exemples donnés dans la suite du rapport, les hypothèses sont au-dessus de la barre et le but à prouver en-dessous. Pour prouver le but, on dispose de "tactiques", qui transforment le but et les hypothèses. L'idée étant de simplifier le but jusqu'à le rendre trivial.
Auto.
Cette tactique s'applique à tous les buts. C'est une tactique
automatique qui essaie d'appliquer récursivement une base de
données (Hint) de théorèmes
précédemments prouvés.
Intros.
Elle ne s'applique pas à tous les buts, seulement aux produits.
Par exemple (x, y:A).B . Elle correspond à la
règle "Lam" du calcul des constructions qui n'est autre
que la règle qui transforme un but qui se trouve dans un contexte vide,
qui est de la forme A->B, en un but B avec A
dans le contexte.
Simpl.
Cette tactique s'applique à tous les buts. Elle applique la règle &&βϵτα;&ϵπσιϖ;&ταυ;&αλπηα;&σϵμι;&&ταυ;&αλπηα;&υπσι;&σϵμι;-réduction sur le but courant pour le transformer en un but plus réduit et plus simple.
Exemple:
Si notre but est de la forme: (n:nat)(plus O n)=n.
On se trouve dans le cas d'une quantification universelle, la tactique Intro
fait passer la variable quantifié n en hypothèse et
on aura comme but à prouver (plus O n)=n; En appliquant
Simpl sur ce but on aura à prouver n=n ce qui
est trivial.
Elim term.
Cette tactique s'applique à tous les buts. C'est la destruction d'un type inductif (pour faire l'étude des cas) et ça correspond au raisonnement par induction structurelle.
Exemple:
Si notre but est de la forme:
n:nat----------------------
n=O \/ (Ex [m:nat] n=(S m)).
Ce but est une disjonction, ce qui oblige à faire un choix, mais qui
dépend de n. Introduisons ce choix par la tactique
Elim appliquée à n. Et il faut pas
oublier que n est du type nat qui est un type inductif, alors on distingue
deux cas, donc deux nouveaux buts. Le premier est obtenu en remplaçant
n par O, le second par (S n'). En
regardant ces deux buts on remarque que: Le premier est le cas de base de la
récurrence, le second le cas général: on suppose que ce
que l'on veut montrer est vrai pour n, et on doit montrer que
c'est vrai pour (S n).
tout_entier_est_soit_O_soit_a_un_predecesseur < Elim n.
2 subgoals
n:nat-------------------
O=O \/ (Ex [m:nat] O=(S m))subgoal 2 is:
(n:nat)n=O \/ (Ex[m:nat]n=(S m))->(S n)=O \/(Ex [m:nat] (S n)=(S m))
Case term.
C'est une version plus faible d' Elim qui correspond à un
simple raisonnement par cas sans récurrence.
Apply term.
Cette tactique s'applique à tous les buts. Elle essaie de faire
correspondre le but courant avec la conclusion du type de term.
Si elle réussit, elle retourne autant de sous buts qu'il y a de
prémisses dans term.
Exemple:
Si notre but a la forme suivante:
H : A->B->C
H': A->B
H": A
-----------------------------
C
Coq < Apply H.
Le but courant est C, on peut appliquer la tactique Apply H, car
le but courant et la conclusion de H peuvent être unifiées (ils
sont les mêmes), on obtient alors deux sous buts, qui ne sont autres que
les premisses qui existent dans H, c'est à dire A et B.
2 subgoals
H : A->B->C
H': A->B
H": A
-----------------------------
A subgoal 2 is: B
Exact term.
Cette tactique s'applique à tous les buts. Elle donne exactement le
terme de preuve correspondant au but, qui peut être parmi les
hypothèses ou un terme déjà prouvé. Si T est le
but courant, et p un terme de type U, alors Exact p reussi
à résoudre le but si et seulement si T et U sont
convertibles.
Exemple: Si notre but a la forme suivante:
1 subgoal
H : A->B->C
H': A->B
H": A
-----------------------------
A
Coq < Exact H".
Cette tactique permet de le résoudre, car notre but et notre hypothèse H" sont les mêmes.
Generalize term.
Cette tactique s'applique à tous les buts. Elle permet d'ajouter au but
courant une quantification. Dans ce cas, il faut que le terme utilisé
soit une variable définie dans le contexte courant et dépendante
de ce but. Si le but courant est de la forme : (P x) et que
x est un objet défini de
type T. Generalize x: Transforme le but en
(x:T) (P x).
Rewrite term.
Cette tactique s'applique à tous les buts. Le termequ'on a
choisi doit avoir comme conclusion la formule terme1=terme2. Elle
remplace dans le but courant toutes les occurrences du term1 par
term2.
Exemple:
Si le but courant est de la forme:
H: (plus n1 (S m))=(S (plus n1 m))
--------------------------------
(S (plus n1 (S m)))=(S (S (plus n1 m)))
Coq < Rewrite H.
1 subgoal
n0: nat
m: nat
n1: nat
H: (plus n1 (S m))=(S (plus n1 m))
--------------------------------
(S (S (plus n1 m)))=(S (S (plus n1 m)))
Unfold ident.
Cette tactique s'applique à tous les buts. L'identificateur
donné comme argument à Unfold, doit être un
terme déjà défini (Definition). Cette
tactique permet de
remplacer tous les occurrences de ident qui existent dejà
dans le but par le terme qui lui est associé.
Cut term.
Cette tactique s'applique à tous les buts. Le Cut
correspond à la règle de coupure du calcul des séquents.
Si le but était B. Alors Cut A revient
à générer deux sous buts: Le premier est de prouver que
A->B et le deuxième revient à prouver A
même. C'est pour utiliser A dans la preuve du but
courant. Il faut bien choisir A car il faudra la prouver
après.
Une fois qu'on a terminé nos deux preuves, le but suivant est d'essayer
de généraliser notre preuve pour qu'elle s'applique sur
n'importe quelle fonction f définie sur un ordre bien
fondé.
Pour cela, nous avons utilisé le langage ML. Nous avons introduit des types de données: représentation des expressions et représentation des tactiques.
"fexp1" est le nom de la fonction qui traite la partie commune
à toutes les fonctions. Elle donne une séquence de tactiques
à appliquer dans notre preuve jusque là où on arrive
à la structure de la fonction récursive proprement dite donc on
applique la fonction "fexp".
"fexp" est le nom de la fonction récursive définie
par cas sur cette structure de données (expression); elle prend en
premier argument un string option qui distingue deux cas:
F où on ne connait pas encore le nom de
la fonction f qui sera appelée lors des appels
récursifs.
Comme deuxième argument fexp prend le corps de la
fonctionnelle F et selon la forme de l'expression qui se trouve
dans la fonctionnelle elle renvoie la tactique correspondant.
Par exemple, dans le cas où, la fonction contient un Cases
a alors la tactique correspondante, si f n'apparait pas
dans a, est de faire une séquence de tactiques:
Sequence[Case(a); Brackets(map (frule fname) rules)]
Intros sur les patterns et de réappliquer
fexp sur le corps de la règle.
On obtient autant de buts qu'on a de cas dans Case(a) et on
applique frule sur chacune de ces règles.
Dans notre étude, nous avons dû nous limiter au cas où
notre fonctionnelle F est une Lambda abstraction, nous ne
traitons pas les autres cas.
En ce qui concerne le contenu de la fonctionnelle, nous avons aussi quelques restrictions:
Cases(t, a, rules), on se limite au cas où
f n'apparait pas dans a.
Pat_ident qui est un constructeur et dans ce cas on ne fait pas
des Intros.
Pat_app est un constructeur appliqué à une liste
d'identificateurs. La fonction d'Ackermann ne marchera pas dans ce cas
là. Alors on a dû casser à la main le pattern et
construire des Cases imbriqués.
On se restreint au pattern primitif, car sinon, à chaque fois qu'on a un pattern, il faut vérifier si c'est un constructeur ou non et pour cela il faut avoir un tableau qui contient la liste de tous les constructeurs de tous les types récursifs connus dans le texte.
App(expression,[liste d'expressions]), la partie
gauche de App doit être un identificateur et les autres
types d'expression ne sont pas traités.
Cases a, il faut conserver l'ordre
des constructeurs des types inductifs donnés lors de la
définition.
En Coq, la manipulation des fonctions définies par récursion primitive est particulièrement bien intégrée dans le moteur de raisonnement. En revanche, les fonctions définies par récurrence sur un ordre bien fondé sont plus difficiles à mettre en oeuvre. En effet, en Coq la preuve de l'équation de point fixe de fonctions basées sur un ordre bien fondé n'était pas réalisée automatiquement.
L'objectif de mon stage est d'intégrer une méthode automatique qui aboutira aux tactiques de preuve qu'il faut pour prouver l'équation de point fixe, pour n'importe quelle fonction définie sur un ordre bien fondé.
Dans cet objectif, nous avons tout d'abord étudié deux preuves sur des cas particuliers et ensuite nous avons comparé leur scripts de preuve. Ceci nous a permis de généraliser une preuve et de définir une méthode automatique.
Comme nous avons cité dans le paragraphe précédent " Limitations ", certaines limitations ont été imposées dans notre méthode. Nous planifions de résoudre ces problèmes dans un travail ultérieur.
Une des perspectives directes de ce travail est de générer une
nouvelle hypothèse de récurrence qui unit les deux
hypothèses de récurrence H_rec_well_founded et
H_rec_acc', qui sont nécessaires dans notre preuve.