Une application d'un logiciel de démonstration assistée à un résultat d'algèbre

Frédéric RUYER

DEA Logique et fondements de l'informatique 01/02

Resume :

Table des matières

1 Le système

1.1 Sortes.

1.2 Expressions

1.3 Unification

1.4 Démonstrations

1.5 Logiques d'ordre supérieur et sémantique

2 Le logiciel PhoX

2.1 Exemple , présentation des preuves et commandes.

2.1.1Exemple

2.1.2 Présentation des preuves.

2.3 commandes

2.4 Réutilisation de théories

3 Un peu d'algèbre

3.1 Enoncé du théorème et quelques corollaires

3.2 Elements de preuve

3.3 Stratégie adoptée

4 Conclusion

1 Le système

Il s'agit d'une généralisation du système AF2 ,qui permet de quantifier sur des objets d' ordre arbitrairement grand.

1.1 Sortes.

L'idée intuitive est de distinguer les types d'objets mathématiques (formules, entiers,ensemble d'entiers,fonctions...), qu'on appellera des sortes.

On se donne quatre ensembles disjoints:

{o}, ensemble formé de la sorte o des propositions

,ensemble des sortes de base (nat , bool , ...)

,ensemble des variables de sortes (notées 'a,'b,...)

,ensemble des sortes paramétrées

(notées nom_de_paramètre['a1,'a2,...'ak] ,par exemple list ['a])

Et on définit comme la réunion de ces quatre ensembles.

L'ensemble S des sortes est défini par la grammaire : S = | .

La flèche est notée de façon usuelle : . pour .

On définit la substitution de manière usuelle, en s'autorisant à substituer à l'intérieur des crochets d'une sorte paramétrée.

On appelle sorte close une sorte dans laquelle n'intervient aucune variable de sorte.

On appelle sorte polymorphe une sorte qui n'est pas close.

1.2 Expressions

Comme on peut s'en douter, les termes de notre système incluent les formules.

Si A et un symbole et s une sorte, j'appelle symbole sorté le couple (A,s), que je note

Un langage d'ordre supérieur L est un ensemble fini de symboles sortés.

Le langage de base (qu'on enrichit par la suite...) est défini par trois fonctions:

.

.

On se donne, de plus, pour chaque sorte s un ensemble dénombrable de variables , noté , dont les éléments sont notés ,...

Un contexte est un ensemble formé de symboles sortés de L et d'un ensemble fini de variables telles que si et alors

Les règles de sortage des expressions sont les suivantes :

axiome :

abstraction :si alors si A est une variable

application : si et alors ,avec la condition qu'une même variable n'apparaisse pas dans les deux contextes avec deux sortes distinctes.

substitutions : dans le cas d'une sorte s polymorphe, on a :pour toute sorte s' et toute

variable de sorte 'a :

Si alors : si A est une constante

si A est une variable

Exemples:

Par contre ,le terme n'est pas sortable si X est une variable;si on déclare par contre X comme une constante de sorte 'a->prop, il le devient...

Si on oublie les types, on a donc des règles de dérivation de termes du -calcul pur.

Lemme: Si t est un terme du -calcul dont la dérivation ne contient pas de règles de substitution, et dont la sorte s n'est pas close , alors pour toute variable de sorte 'a et pour toute sorte s'',on peut étendre L de façon à ce qu' il existe un terme t' dont la dérivation a la même forme que celle de t et où sa sorte soit s['a:=s''].

preuve: Par induction sur la hauteur de la dérivation.

On notele contexte obtenu à partir de en ajoutant si besoin est des symboles de constantes, et en changeant les sortes des variables

* règle axiome , on remplace par: si A est une constante(on enrichit (éventuellement) le langage en rajoutant le couple (A',s['a:=s']))

Si A est une variable,il n'y a pas de problème: on change sa sorte....

*règle application : on applique simplement l'hypothèse d'induction.

*règle abstraction : par hypothèse d'induction,on a nécessairement que la sorte de A est bien substituée.

Lemme: Si t est un terme dérivable de sorte s, alors pour toute sorte s'' on peut étendre L de façon à ce qu' il existe un terme t' de sorte s['a:=s'']. dont la dérivation a la même forme que celle de t et dont la dérivation n'utilise pas de règles de substitution.

Preuve:induction sur la hauteur de la dérivation.

*règle de substitution : on la remplace par une règle axiome comme précedemment.

*règle axiome:pas de souci.

*règle d'abstraction :par hypothèse d'induction en utilisant la construction du lemme précédent et en remarquant que le contexte a été changé.

*règle d'application:par hypothèse d'induction.

On obtient ainsi des dérivations où un même symbole du langage peut avoir plusieurs sortes(closes) , par exemple dans (0::nil)::nil. (on note :: pour cons, en notation infixe).

Le terme t' obtenu est clairement simplement typé, et est donc fortement normalisable.

Si on regarde de plus près la transformation, on s'aperçoit que les termes t et t' ne diffèrent que par leurs constantes, car on ne peut abstraire que sur les variables.Il vient donc (presque) immédiatement le :

Théorème:Tout terme est fortement normalisable.

1.3 Unification

L'unification de deux termes du premier ordre consiste à trouver une substitution appelée unificateur rendant, si celà est possible, ces deux termes égaux.Le problème est décidable, et on dispose d'algorithmes qui donnent un unificateur le plus général i.e une substitution qui permet d'obtenir tous les unificateurs par composition.

L'unification de deux termes d'ordre supérieur consiste à trouver une substitution appelée unificateur rendant, si celà est possible, ces deux termes égaux modulo .Le problème de trouver un unificateur le plus général est indécidable dans le cas général.

Par exemple :

si t = A B et t' = C (A,B et C étant des variables),on a

s=[C:=A B] et s'[A:=,B:=D],D étant un terme quelconque qui conviennent toutes les deux.

Si p est un un unificateur principal pour t et t', il existe deux substitutions r et r' telles que

r o p =s et r' o p = s'.

On pose p = [A:=A';B:=B';C:=C'].rop=s impose par structure que A' et B' soient des variables. et r'op=s' impose de même que C' soit une variable.Ainsi,on a A' B' =C', ce qui est impossible par unicité de la forme normale.

1.4 Démonstrations

Les jugements portent sur les propositions, i.e. les objets de sorte o.

Les règles de typage sont celles de AF2 , avec une précision sur les sortes au lieu de se limiter à l'arité :

axiome :

-intro (abstraction ): si alors

-elim (application) : si et alors

-intro : si et x de sorte s n'est pas libre dans alors

-elim : si alors , où t est une expression de sorte s.

=-intro : si alors

=-elim : si alors

: si et si alors

Remarques:

*Les règles sur l'égalité sont celles de l'égalité de Leibnitz, qui signifie que deux objets sont égaux ssi aucun prédicat ne peut les distinguer.On vérifie facilement qu'elle a les propriétés d'une relation d'équivalence.

*On définit l'absurde par , ce qui donne immédiatement LI.

*LC est donnée par la loi de Pierce .

On se donne deux axiomes utiles pour l'égalité:

Extensionnalité:

Egalité des propositions:

Ces axiomes ne sont pas dérivables dans le système précédent.

Le principe de définition, et l'axiome du choix

On rajoute un symbole de constante au langage, noté .Ce symbole est parfois appelé epsilon de Hilbert.Il sert à définir une fonction en nommant l'image dans son graphe.

On a l'axiome suivant:

Principe de definition:.

Un exemple d'application dans les entiers:

Notations:

*on note / \ pour le et \ pour le

* /\a:X P est une abréviation pour /\a(X a -> P))

*/\a,b,c P est une abréviation pour /\a/\b/\c P

*\x,y,z f est une abréviation pour \x\y\z f.

*Def est la notation pour

On définit d'abord notre sorte et nos constantes , ainsi que le prédicat entier:

Sort nat.

Cst N0 : nat.

Cst Prefix[2] "S" x : nat -> nat.

(* S x *)

def N x = /\X (X N0 -> /\y (X y -> X (S y)) -> X x).

def (* graph of a function defined by induction *)

def_rec_P.N a f n z = /\X (

X N0 a ->

/\y:N/\r (X y r -> X (S y) (f y r)) -> X n z).

lemma (* The predicate [ def_rec_P.N] defines a function *) def_rec_unique.N

/\a,f,n (N n -> \/!z def_rec_P.N a f n z).

On prouve le lemme.....puison définit :

def (* function defined by induction *)

def_rec.N a f n = Def \z (def_rec_P.N a f n z).

On peut ensuite définir par exemple l'addition...

def (* addition *) rInfix[3.5] x "+" y = def_rec.N y (\n,r S r) x.

L'axiome du choix est la formule:

AC:

On a simplement supprimé l'unicité.

(Celà correspond par exemple au raisonnement usuel que l'on peut faire lors d'une preuve sur les limites).

1.5 Logiques d'ordre supérieur et sémantique

Une logique d'ordre supérieur est un triplet (,L,G) où est défini comme ci-dessus avec ==,L est un langage pour l'ensemble des sortes correspondantes et G est un sous ensemble de S, qui détermine les sortes d'objets sur lesquels on peut quantifier.

Les jugements de dérivation des termes sont les mêmes, sauf que l'on a le droit d'introduire un seulement si la sorte du terme sur lequel on quantifie est dans G.

Exemple

PA2 est déterminée par , L=et

G=

Un prémodèle m d'une l.o.s est la donnée:

*pour chaque sorte s d'un ensemble Ds tel que Do={0;1} et si s = s1->s2, alors

s est inclus dans l'ensemble des fonctions de Ds1 dans Ds2.

*pour chaque élément (A,s) de L, d'un élément Am de Ds

Soit m un prémodèle.Un environnement e est la donnée pour chaque sorte s d'une fonction de Vs dans Ds.

On note e[xs:=v] l'environnement qui à la variable x de sorte s associe v, et est égal à e ailleurs.

La valeur Val(t,e) d'une expression t est définie inductivement de manière usuelle.

On dit qu'un modèle m satisfait une formule F si pour tout environnement e Val(F,e)=1.

On a un théorème de complétude:

Théorème Une formule F est prouvable ssi tout modèle satisfait F.

2 Le logiciel PhoX

C'est un logiciel de démonstration assistée qui implémente le système

Pour lancer le logiciel ouvrir un fichier .phx sous xemacs.

2.1 Exemple , présentation des preuves et commandes.

2.1.1Exemple

Entrons d'abord trois constantes:

Cst A : prop.

Cst B : prop.

Cst C : prop.

On veut prouver On tape la commande:

goal ((A & B) -> C) -> A -> B -> C.

Le logiciel répond :

|-((A & B) -> C) -> A -> B -> C

Il y a trois introductions de l'implication à faire.On tape

intro 3.

Le logiciel répond :

1 goal created.

New goal is:

H :=((A & B) -> C)

H0 := A

H1 := B

|-C

On veut maintenant prouver C en utilisant H.Il faut donc faire une élimination de l'implication.On tape:

elim H.

Le logiciel répond :

1 goal created.

New goal is:

H :=((A & B) -> C)

H0 := A

H1 := B

|-A & B

On fait maintenant un introduction de la conjonction.On tape:

intro .

Le logiciel répond :

2 goals created.

New goals are:

goal 2/2

H :=((A & B) -> C)

H0 := A

H1 := B

|-B

goal 1/2

H :=((A & B) -> C)

H0 := A

H1 := B

|-A

Il ne reste plus qu'à indiquer que l'on a des axiomes en tapant:

axiom H0.

Le logiciel répond :

0 goal created.

Old goal is:

goal 1/1

H :=((A & B) -> C)

H0 := A

H1 := B

|-B

Puis:

axiom H1.

Le logiciel répond :

0 goal created.

On peut maintenant sauvegarder la preuve en tapant:

save mon_theoreme.

Le logiciel répond :

Building proof...

Typing proof...

Verifying proof...

mon_theoreme =((A & B) -> C) -> A -> B -> C : Theorem.

On aurait eu la même chose en remplaçant le goal du début par fact mon_theoreme et en terminant par save tout court.

Cette preuve correspond à l'arbre suivant en déduction naturelle:

A,B|-A A,B|-B

-----------------------------&-intro

A,B|-A&B (A&B)->C|-(A&B)->C

------------------------------------------------------------------------------- -> elim

(A&B)->C,A,B|-C

---------------------- -> intro *3

|-((A&B)->)C->A->B->C

On a donc lu la preuve à partir de la racine : ce type de notation s'appelle une notation linéaire des preuves.

2.1.2 Présentation des preuves.

Un des intérêts du système est qu'il permet de définir des règles dérivèes;ainsi, au départ, les seules règles dont on dispose est l'introduction et l'élimination de la flèche:

G,A|-B G|-A B|-B

--------- (-> i) et -------------------------(->e)

G|-A->B G,A->B|-B

(Dans la règle d'élimination, le séquent de droite est en fait ignoré)

Règles d'introduction dérivées

Si on a construit une nouvelle dérivation:

.

.

.

-----------

A1,A2,...An|-B

--------------(->i)

|-A1->A2->...->B

Alors on peut en déduire une nouvelle règle d'introduction,que l'on peut définir dans notre système.

Une fois défini, si dans une preuve on arrive à:

goal 1/1

H :=.....

|-B

Si on tape intro.

Alors on obtient:

n goals created.

New goals are:

goal n/n

H :=.....

|-An

goal n-1/n

H :=.....

|-An-1

[...]

goal 1/n

H :=.....

|-A1

par exemples:

*introduction de la disjonction:

On définit

Def A "&" B = /\X((A->B->X)-> X).

Puis on prouve:

fact bonjour /\X,Y(X->Y-> X&Y).

A la fin de la preuve, après l'avoir vérifiée, on tape :

new_intro et-intro bonjour.

*introduction du constructeur S pour les entiers:

On a défini le prédicat N x tout à l'heure.

On prouve:

fact au_suivant /\x(N x -> N S x)

A la fin de la preuve, après l'avoir vérifiée, on tape :

new_intro -c Sint au_suivant.

-c indique que s est un constructeur.

Ainsi si on veut prouver N SSSS 0.:

|-N SSSS 0

intro.

|- N SSS 0.

intro.

etc....

La syntaxe est new_intro nom_de_la_nouvelle_règle nom_du_théorème

avec des options que je ne détaille pas...

Règles d'élimination dérivées

Si on a construit une nouvelle dérivation:

.

-----------

A1,A2,...An,B|-C

--------------(->i)

|-A1->A2->...->B -> C

Alors on peut en déduire une nouvelle règle d'élimination,que l'on peut définir dans notre système.

Une fois défini, si dans une preuve on arrive à:

goal 1/1

H :=.....

G :=B

|-C

Si on tape elim G.

Alors on obtient:

n goals created.

New goals are:

goal n/n

H :=.....

G :=B

|-An

goal n-1/n

H :=.....

G :=B

|-An-1

[...]

goal 1/n

G :=B

H :=.....

|-A1

par exemple :

*Dans N, on a prouvé :

fact (* Induction on $N *) rec.N

/\X (X N0 -> /\y:N (X y -> X (S y)) -> /\x:N X x).

On tape ensuite:

new_elim N rec rec.N.

Si on arrive à:

H :=N n

|-A[n]

On tape

elim H

Le logiciel répond:

2 goals created:

goal 2/2

H :=N y

H0 :=A[y]

|-A[S y]

goal 1/2

H :=...

|-A[N0]

En fait, c'est simplement le raisonnement par récurrence....

*Pour la conjonction, on a trois règles d'élimination,et on reconnaît dans la dernière une règle gauche:

fact et_elim_g /\X,Y(X&Y->X)

fact et_elim_d /\X,Y (X&Y->Y)

fact et_gauche /\X,Y,Z((Y-> Z-> X)->Y&Z->X)

La dernière règle sera utilisée en tapant left H,avec H:=A&B.

En résumé:ces règles permettent de faciliter l'utilisation de formules, et entrent aussi dans les tentatives de vérification automatiques faites par le logiciel.

2.3 commandes

On a déjà vu les commandes intro , elim et axiom.

*apply

On a:

H :=A->B

H0 :=A

|-C

On tape

apply H with H0.

Le logiciel répond:

H :=A->B

H0 :=A

|-C

Celà revient en fait à une coupure sur la formule B.

*use

On a prouvé le théorème Th précédemment.

On a:

H :=...

|-C

On tape:

Use Th.

Le logiciel répond:

H :=......

H0 :=Th

|-C

Celà revient en fait à une coupure sur la formule Th.

*trivial

permet d'éviter une preuve fastidieuse :si on tape cette commande, le logiciel essaie de la trouver "tout seul".Attention, celà peut s'avérer en fait plus long que prévu...

*from

Essaie d'unifier des termes .

Exemple:On a:

H :=...

|-A=x+(y+z)

On tape : from A = (x+y)+z.

Réponse:

H :=...

|-A = (x+y)+z.

Dans cet exemple, on a présupposé que l'associativité faisait partie des règles de réécriture déjà rentrées.Celà correspond à la commande suivante:

*new_rewrite

Permet de réutiliser de façon automatique une règle de réécriture donnée en axiome, ou prouvée par un théorème.

2.4 Réutilisation de théories

Ce qui nous intéresse plus particulièrement ici est la possibilité de réutiliser une théorie.

Ceci est réalisé dans PhoX avec le système des modules:

Il s'agit de fichiers réutilisables .Par exemple, on peut définir la notion de groupe et prouver des propriétés générales,puis réutiliser cette notion deux fois dans un espace vectoriel...le problème est que (pour l'instant) on ne peut pas quantifier dessus.

exemple:

Module semigroup.

Sort set 0.

Cst G : set -> prop.

Cst rInfix[3] x "op" y : set -> set -> set.

claim op_total /\x,y:G G (x op y).

claim assoc /\x,y,z:G x op (y op z) = (x op y) op z.

end

Module monoid.

Use semigroup.

Cst e : set.

claim neutre_total G e.

claim neutre_left /\x:G e op x = x.

claim neutre_right /\x:G x op e = x.

end.

Module group

Use monoid.

Cst Prefix[2] "i" x : set -> set.

claim inv_total /\x:G G (i x).

claim inv_left /\x:G (i x) op x = e.

fact neutre_right /\x:G (x op e = x).

fact inv_idempotent /\x:G (i i x = x).

etc....

Si on veut réutiliser une théorie dans un autre cadre, il faut renommer la sorte générique (ici"set") ,les opérateurs et vérifier que l'on a bien les bons axiomes.

Si on veut prouver par exemple que pour toute liste de groupes le produit est encore un groupe , il faut pouvoir réutiliser la théorie pour chaque groupe de la liste, ce qui est possible si la liste est fixée , mais pas dans le cas général. En effet le prédicat "être un groupe" ne peut pas s'exprimer dans ce cadre.

De plus,le passage au quotient fait passer de la sort g->prop à la sorte (g->prop)->prop.Si on fait une itération sur le quotient,elle ne peut être arbitrairement grande.

C'est la raison pour laquelle j'ai commencé par bâtir la preuve avec des prédicats...

exemples

fact groupe_passe_a_droite /\G,p,i,e,x,y (groupe G p i e -> G x -> G y -> x = y -> e = p y (i x)).

fact ideal_generateur_modulo_inversible /\x,b,b',A,p,m,i,z,u (anneau_principal A p m i z u -> \/u'(inversible u' u m & b' = m u' b) -> ideal_principal_engendre_par b I a p m i z u = ideal_principal_engendre_par b I a p m i z u ).

fact propositionV.3.2 /\M,P,O,Z,f,A,p,m,i,z,u (anneau_principal A p m i z u -> module M P O Z f A p m i z u -> ordre_element_de_torsion x o M P O Z f A p m i z u -> ordre_element_de_torsion x' o' M P O Z f A p m i z u -> premier_entre_eux o o' m u -> ordre_element_de_torsion (P x x') (m o o') M P O Z f A p m i z u ).

les énoncés devenaient très lourds à manier et malcommodes, ne pouvant utiliser sur les fonctions (qui étaient dans ce cadre des variables ) aucune règle de réécriture,ni aucune règle de totalité...

3 Un peu d'algèbre

3.1 Enoncé du théorème et quelques corollaires

On rappelle les définitions suivantes:

Un anneau principal est un anneau dans lequel tout idéal est principal.

Un anneau noethérien est un anneau dans lequel toute suite croissante d'idéaux est stationnaire.

Un anneau factoriel est un anneau dans lequel tout élément se décompose en un produit de puissances d'éléments premiers.

Si A est un anneau un A-module est un groupe commutatif d'ensemble sous-jacent M muni d'une loi externe AxM->M qui a les mêmes axiomes qu'un espace vectoriel sur un corps.

Un module cyclique est un module engendré par un seul de ses éléments.

Un élément a de A est un annulateur du A-module M si pour tout x de M a.x=0

Un élément a de A est un annulateur minimal du A-module M si tout annulateur de M est un multiple de a.

Un élément x d'un A-module est dit de torsion s'il existe un élément a de A tel que a.x=0

Un module de torsion est un module dont tous ses éléments sont de torsion.

Un module de type fini est un module engendré par une liste finie de ses éléments.

Un module noethérien est un module dans lequel toute suite croissante de sous modules est stationnaire.

Un module libre est un module qui admet une partie génératrice libre.

On vérifie facilement qu'un module cyclique engendré par un élément de torsion x d'ordre o alors o est un annulateur minimal du module;on dit alors que c'est l'ordre du module (défini à un inversible près).

Le résultat est le suivant:

Théorème: Tout module de torsion de type fini sur un anneau principal M est

isomorphe à un produit de modules cycliques C1,...Cn

d'ordres m1,...,mn, tels que m1 est un annulateur minimal de M et m(i+1) divise mi.

On a , de plus, l'unicité (que je ne montre pas).

Il y a deux corollaires importants de ce théorème :

*Facteurs invariants d'un groupe abélien.

A=Z

Un groupe abélien fini est un Z-module, de torsion car x |->n.x est surjective , et de type fini car fini.

Un Z-module cyclique d'ordre n est à isomorphisme près Z/nZ.

Ainsi, on a la caractérisation des groupes abéliens finis.On a de plus le fait que m1*m2*...mn=ordre(cardinal) du groupe.

L'unicité permet de parler des facteurs invariants.

On peut ainsi dresser la liste de tous les g.a.f d'ordre(cardinal) donné.

Par exemple Si n=45: Z45 , Z15+Z3 .Si n=36 : Z36, Z18+Z2, Z12+Z3,Z6+Z6.

Le théorème Chinois permet de donner ensuite les diviseurs élémentaires:

Z45 = Z9 + Z5, Z15+Z3=Z5+Z3+Z3,etc...

*Matrices semblables et matrices compagnon.

K est un corps commutatif, E un Kev de dimension n,et u un endomorphisme de E.

L'action P,x |-> P(u).x permet de "transformer" E en un K[X]-module ,le groupe de base étant le même.

E est de torsion car u admet un polynôme minimal P0, ce dernier étant de plus l'annulateur minimal de E.

E est de t.f car de dimension finie...

On sait que K[X] est principal.

Il reste donc à regarder de plus près la traduction de "sous module"

et de "module cyclique".

Un sous module est clairement un sous-ev u-invariant.

Un sous module cyclique est clairement un sous-ev u-cyclique

(i.e engendré par un vecteur unique et ses images par les puissances

successives de u).

Pour arriver à notre résultat,il faut regarder quelle peut être la forme d'une matrice d'un sous module cyclique.

Une matrice compagnon est une matrice de la forme :

0..........0 a1

1 0.......0 a2

0 1 0....0 a3

...

0 ........1 an

Si la matrice de v dans une base d'un sous module F est une matrice compagnon,il est clair que F est un sous module cyclique d'ordre Pcar(v).

Réciproquement,soit F un sous module cyclique d'ordre P(v) (unitaire).

On pose d = degP, et a un élément d'ordre P(v) de F.La suite a, v.a, v*v.a,... engendre F, et F est donc engendré par les d premiers éléments de cette suite.Par la minimalité de P, ils forment une base de F.Dans cette base, on voit bien que la matrice est la matrice compagnon de g.

Par suite, tout endomorphisme u sur E est tel qu'il existe une base de E dans laquelle

Mat(u)=M1+M2+...+Mk,

Les Mk étant les matrices-compagnon resp. de g1,..gk polynômes unitaires tels que chacun divise le précédent...

On appelle ces polynômes les facteurs invariants de u, et on a de plus:

g1 est le polynôme minimal de u et g1*g2*...gk=Pcar(u).

(et donc Cayley-Hamilton).

3.2 Elements de preuve

On peut voir la preuve de ce résultat comme le résultat de trois propositions:

*Tout A-module de type fini sur un anneau noethérien est noethérien

+ corollaire:Tout sous module d'un A-module de type fini sur un anneau noethérien

est de type fini.

*Tout A-module de torsion d'annulateur minimal o sur un anneau A admet un

élément d'ordre o .

*Si un A-module de torsion d'annulateur minimal o de type fini sur un anneau A principal admet un élément e d'ordre o , alors il se décompose en une somme directe <e>+M' où M'est un A-module de torsion d'annulateur minimal o'|o, de type fini (utilise la première proposition).

On voit bien que l'application répétée du troisième fait à l'aide des deux autres permet d'arriver à la décomposition voulue (on utilise d'ailleurs ici le principe de définition pour construire la suite).

Le premier résultat se montre d'abord sur les modules libres, par récurrence sur la dimension.

Le deuxième résultat nécessite l'utilisation de l'arsenal classique (Bezout,Gauss,factoriel).

Le troisième résultat fait largement appel aux quotients..

3.3 Stratégie adoptée

*Il faut d'abord montrer les propriétés algébriques usuelles.

*Pour le premier résultat, on raisonne sur les modules .La première idée est de définir les opérations sur les listes finies.Le problème est qu'à chaque étape de récurrence,il faut redéfinir les opérations, ce qui interdit d'utiliser le principe des modules.De plus,on a bien envie d'utiliser une seule loi, ce qui n'est pas possible avec les listes, à cause de l'élément neutre qui n'est pas unique (on peut additionner deux listes de longueur différente, de la façon naturelle [a;a';a'']+[b,b']=[a+b;a'+b';a''], on a ainsi une infinité d'éléments neutres,et pour avoir un groupe, il faut quotienter par la relation a~=b "il existe une liste z de zéros telle que a=z@b ou b=z@a"...).Pour faciliter les opérations, on se place dans l'espace des séries

A(X), et on définit les sous espaces comme les polynômes de degré <=n.

*Le deuxième résultat est en fait assez calculatoire. Cependant, on tombe sur des difficultés insoupçonnées (par moi...) lorsqu'il s'agit de manier la notion d'anneau factoriel : l'existence de la décomposition est chose aisée, mais la construction à partir de cette dernière d'une liste de puissances de premiers l'est moins ....Celle ci étant (me semble t'il ) nécessaire pour montrer le résultat.Il faut en effet pouvoir accéder à chaque élément de la décomposition,les manipuler...

*Le troisième résultat se montre en utilisant des quotients.Pour éviter d'alourdir, je le montre directement.

4 Conclusion

Les intérêts que représentent les logiciels de ce type pour l'évolution des mathématiques sont les suivants:

-pour la logique elle même : une nouvelle application concrète de ses théories au sein même des mathématiques.Applications de la correspondance de Curry-Howard à des résultats de plus en plus élevés : extraction de programmes et d'algorithmes "inédits"?

-pour le mathématicien : lui fournir un assistant de preuves clair, accessible à un non spécialiste en logique, et muni de bibliothèques suffisamment riches pour lui permettre de manipuler tous les objets usuels (en algèbre, analyse,etc...)

-pour l'enseignant : avoir un outil qui permette aux étudiants d'apprendre à construire leurs raisonnements.

-pour la communauté des mathématiciens : vérification de preuves longues et difficiles , qui peuvent comporter des erreurs délicates à déceler (pour les publications...)

-pour l'industrie : application à la preuve de programmes, et au model-checking.

Questions qui me sont apparues

Sur les produits : identifier la classe des relations (dans ZF) à deux arguments R(E,f) telles que f est une loi interne sur E qui a une propriété particulière (associativité, existence d'un neutre,integrité....), et telles que si R(E,f) et R(E',f') alors R(E*E',f*f')(la propriété passe au produit).Il y a peut être à réfléchir dans la succession des quantificateurs.

Sur les anneaux : quels sont les anneaux pour lesquels il existe un algorithme de décomposition en éléments premiers ?

Les résultats dans Z et Z[X] sont connus, et l'insolubilité par radicaux des polynômes réels de degré supérieur à 5 semble laisser supposer que le fait d'être euclidien n'est pas suffisant.On pourrait peut-être raisonner sur le temps de calcul d'un algorithme supposé exister pour définir une forme d'ordre sur l'anneau.Une condition suffisante "brutale"est que l'anneau soit euclidien"+" (avec non seulement l'existence du dividende et du reste, mais aussi procédé de calcul effectif) et que l'ensemble des premiers soit récursif.

Pour le logiciel lui-même : la commande Use, qui permet de réutiliser une théorie pourrait être accompagnée d'une option qui donne de façon automatique à l'utilisateur la liste des axiomes à vérifier, et éventuellement les lui propose en les renommant.

Le logiciel est un peu bridé par le raisonnement équationnel: il me semblerait intéressant pour éviter de perdre trop de temps dans les preuves d'y intégrer une partie qui fasse ce travail, car c'est parfois un peu fastidieux.

Difficultés rencontrées : lenteur humaine pour rentrer les preuves.

Le programme qui correspond à la preuve : le faire tourner comment?sur quoi?pourquoi?

Développer une nouvelle interface : quelque chose de plus proche de la vision arborescente d'une preuve, avec possibilité de "cliquer" sur telle ou telle partie de la preuve pour la développer ou la réduire.

Merci à mon tuteur P.Rozière et à l'auteur du logiciel C.Raffali pour leur aide, ainsi qu'à C.Berline pour m'avoir donné l'occasion de présenter mon travail.

Références

[1]René David Karim Nour Christophe Raffalli.Introduction à la logique-Théorie de la démonstration.Ed. DUNOD 2001.

[2]S.Mac LANE G.BIRKHOFF algèbre T1 et 2.Ed gauthier-villars 1968

[3]J.M Alliot T.Schiex .Intelligence artificielle et informatique théorique.Ed CEPADUES EDITIONS 1993.

[4]R Lalement.Logique,réduction,résolution.Ed

[5]R.Godement.Cours d'algèbre.Ed

[6]J-M Arnaudiès J.Bertin Groupes,algères et géométrie.Ed ellipses 1993

[7]W.Bibel Automatic theorem proving.Ed

[8]C.Berline.Cours de lamda-calcul.

[9]C.Raffalli.PhoX.www.lama.univ-savoie.fr/~RAFFALLI/phox.html