SMTCoq: automatisation expressive et extensible dans Coq

Valentin Blot (1, 2, 3) , Amina Bousalem (1) , Quentin Garchery (1, 4, 5) , Chantal Keller (1)

1 LRI - Laboratoire de Recherche en Informatique
2 IRIF (UMR_8243) - Institut de Recherche en Informatique Fondamentale
3 LSV - Laboratoire Spécification et Vérification [Cachan]
4 UPD7 - Université Paris Diderot - Paris 7
5 TOCCATA - Formally Verified Programs, Certified Tools and Numerical Computations

Les assistants de preuve basés sur la Théorie des Types, tels que Coq, permettent l'implantation de tactiques automatiques efficaces reposant sur la réflexion calculatoire (ex : lia, ring). Malheureusement, celles-ci sont généralement limitées à un domaine mathématique particulier (ex : l'arithmétique linéaire entière, la théorie des anneaux). A contrario, SMTCoq est un outil modulaire et extensible, faisant appel à des prouveurs externes, qui généralise ces approches calculatoires pour combiner les raisonnements issus de multiples domaines. Pour cela, il repose sur une interface de haut niveau, qui offre une plus grande expressivité, au prix d'une automatisation plus complexe. Dans cet article, nous détaillons deux améliorations : la possibilité de faire appel à des lemmes quantifiés, et celle d'utiliser plusieurs représentations d'une même structure de données. Elles permettent de construire une tactique automatique basée sur SMTCoq qui soit expressive sans remettre en cause la modularité ni l'efficacité de ce dernier. Une telle tactique permet ainsi une automatisation extensible, à faible coût, à de nouveaux domaines supportés par les prouveurs automatiques de l'état de l'art.

Domaines: Logique en informatique [cs.LO]

Valentin Blot, Amina Bousalem, Quentin Garchery, Chantal Keller. SMTCoq: automatisation expressive et extensible dans Coq. JFLA 2019 - Journées Francophones des Langages Applicatifs, Jan 2019, Les Rousses, France. ⟨hal-02369249⟩