Bécassine à la chasse au Coq (démonstration)

Valentin Blot (1) , Louise Dubois de Prisque (1) , Chantal Keller (2) , Pierre Vial (1)

1 DEDUCTEAM - Deduction modulo, interopérabilité et démonstration automatique
2 LMF - Laboratoire Méthodes Formelles

Nous présentons une nouvelle tactique Coq (snipe) permettant de prouver automatiquement des butsCoq en les envoyant à des prouveurs automatiques externes du premier ordre via des plugins. Pour ce faire, la tactique snipe réduit le but à un énoncé du premier ordre et enrichit le contexte local avec des énoncés explicitant pour le prouveur la sémantique du but. Nous combinons des transformations modulaires et indépendantes permettant chacune de réduire un aspect spécifique du langage de Coq au langage (plussimple) d’un prouveur automatique. A l’heure actuelle, snipe utilise des transformations simples mais cruciales qui explicitent des définitions et des types algébriques. Ceci permet de prouver automatiquement des buts mêlant raisonnement au premier ordre, types de données et polymorphisme. Ce prototype de tactique automatique est un premier pas vers l’implantation et la combinaison de transformations plus complexes, qui rendront Coq plus facile d’accès.

Domaines: Logique en informatique [cs.LO]

Valentin Blot, Louise Dubois de Prisque, Chantal Keller, Pierre Vial. Bécassine à la chasse au Coq (démonstration). JFLA 2022 - Journées Francophones des Langages Applicatifs, Jun 2022, Saint-Médard-d'Excideuil, France. ⟨hal-03604902⟩