Le but général de cette bibliothèque est d’utiliser le démonstrateur
automatique CiME pour produire des
preuves en Coq, entre autres
d’égalité modulo dans une algèbre de termes
quotient,
de terminaison d’un système de réécriture,
de confluence locale d’un tel système,
de convergence.
La méthodologie retenue est de produire des traces, mais il faut
d’une part modéliser les propriétés à prouver dans Coq, d’autre part pour
interpréter ces traces, il faut parfois prouver des propriétés sur
les algorithmes sous-jacents. Par exemple, pour prouver la confluence
locale d’un système de réécriture, il faut prouver que toutes les
paires critiques sont confluentes. CiME va fournir une trace de
réécriture des deux termes de chaque paire vers un réduit commun,
mais il faut être sûr de vérifier toutes les paires critiques,
et pour celà avoir une preuve de complétude de l’algorithme
d’unification qui calcule ces paires.
Ce développement se veut donc une image en Coq du démonstrateur automatique
CiME.
Résultats sur les listes, entre autres tri et permutation, utiles
pour le cas multiset du rpo et le traitement de l’égalité modulo AC.
term_algebra/
Définition d’algèbres de termes génériques (sur une signature
arbitraire), des terms, sous-terms, substitutions, bonne formation,
taille, divers principes d’induction sur les termes.
Égalité / réécriture modulo un ensemble d’axiomes
term_orderings/
Definition d’un ordre total sans propriétés additionelles,
utile pour mettre les termes modulo AC dans une forme canonique.
Rpo.
Définition inductive du rpo avec status pour les termes
génériques.
preuves que rpo est un préordre
preuves de monotonicité, stabilité par instanciation
preuves d’accessibilité si la précédence sous-jacente est bien
fondée.
ac_matching/
Définition de la théorie équationelle AC. Preuve du fait que l’égalité
modulo AC est équivalente à l’égalité syntaxique des formes
canoniques.
Définition d’un algorithme de matching modulo AC par règles
d’inférence, preuve de sa terminaison, de sa complétude et de sa correction.
unification/
Définition d’un algorithme d’unification syntaxique, preuve de sa
terminaison, de sa complétude et de sa correction (en cours).
