Algèbre linéaire en Coq

date: mars 2010

in English

Le système Coq est un système qui fournit à la fois un langage de programmation et la possibilité de faire des preuves mathématiques. Par exemple, il est possible de prouver que certains programmes respectent des propriétés attendues. Ces preuves font souvent appel à des résultats mathématiques, par exemple des résultats sur les polynômes, les matrices, etc. L'un des défis actuels du développement de Coq est de fournir des bibliothèques de résultats et de techniques de preuves qui couvrent la culture mathématique usuelle des premières années universitaires.

Nous voulons disposer de résultats en algèbre linéaire pour plusieurs objectifs, comme la robotique basée sur les robots parallèles ou l'étude des groupes finis. En particulier, nous proposons d'étudier dans le cadre d'un stage la démonstration du théorème de Perron-Frobénius.

Ce thèorème parle des valeurs propres d'une matrice dont tous les coefficients sont positifs. Ce résultat a aussi servi en informatique pour la mise au point d'outils comme les moteurs de recherche internet.

Dans le projet Marelle, nous nous intéressons à la description formelle de théorèmes mathématiques, avec une orientation vers les théorèmes intervenant en géométrie, en topologie, et sur le plus long terme en robotique. Ce théorème fait partie de notre chemin critique pour un théorème connu sous le nom de théorème de Rohn et utilisé en robotique. La formalisation se fera dans le cadre de l'extension ssreflect de Coq, qui est déjà utilisée massivement pour étudier les groupes finis. Des résultats ont déjà été obtenus en algèbre linéaire. Voir par exemple les liens suivants: http://hal.inria.fr/inria-00331193/.

Remarques : Le stage pourra être rémunéré. Le thème de la formalisation de résultats d'algèbre linéaire pourra donner lieu à une prolongation en thèse, en particulier dans le cadre d'un projet Européen avec l'Université de Göteborg, l'Université de Nijmegen, et l'Université de la Rioja.

Linear algebra in the Coq system

The Coq system is a tool that provides both a programming language and means to perform mathematical proofs. For instance, it is possible to prove that programs satisfy some expected properties. These proofs usually require mathematical results, for instance results about polynomial functions, matrices, and so on. One of the current challenges for the Coq system is to provide libraries of mathematical results and proof techniques that cover the usual mathematical knowledge of the first university years.

We want results in linear algebra for several domains of application, like robotics with parallel robots or the theory of finite groups. In particular, we propose to study the proof of the Perron-Frobenius theorem.

This theorem is about the eigenvalues of a matrix with positive coefficients. This result is also useful for Internet search engines.

In the Marelle project, we are interested in the formal description of mathematical theorems with a general orientation towards theorems that are useful for geometry, topology, and in the long run for robotics. this theorem is on our critical paths for a theorem known as Rohn's theorem and used in robotics. The formal work will be done using the ssreflect extension of Coq. Some results have already been obtained in linear algebra, see for instance the following link: http://hal.inria.fr/inria-00331193/.


Last modified: Tue Mar 2 14:50:43 CET 2010