Implementation du Calcul des Constructions Inductive Presburger

Pierre-Yves Strub

Description

Niveau: Supérieur
Implementation du Calcul des Constructions Inductive/Presburger Pierre-Yves Strub FORMES, INRIA - Tsinghua Universisity - Beijing 7 Octobre 2009

• procedure de decision pour l'arithmetique lineaire


• modification du noyau de coq permettant l'introduction dynamiquement de procedures de decision dans la conversion


• formalisation en coq


• calcul des constructions inductives


• procedure de decision

Informations

• Publié par: profil-nechor-2012
• Publié le: 01 octobre 2009
• Nombre de lectures: 15
• Langue: Français

Extrait

Impl´ementationduCalculdes Constructions Inductive / Presburger

Pierre-Yves Strub

FORMES, INRIA - Tsinghua Universisity - Beijing

7 Octobre 2009

Le Calcul des Constructions Inductives/Presburger CoqMT:uneimpl´ementationdeCIC/N

Certificationd’uneproce´dureded´ecision(avecA.Mahboubi) Une formalisation en Coq + Ssreflect Ge´n´erationdecertificats

CIC/N

Calcul des Constructions Inductive / Presburger :

I unCalcul des Constructions Inductives I uneisecd´deredu´eocrpoiniren´eauelietiqht´ma’iruolrp dans la conversion

Avantages:

I Plus d’automatisation I Preuves plus courtes... I `id´eavfierir...maispasfro´cmeneptulrspa e I Prargoremmsulpicaftspyceeltnvaelemsdantepenesd´

CIC/N

I

I

Modificationdelare`gledeconversion:

Une conversion entre 2termesairm´thiqetsue feraappela`uneorpde´cureded´ecision

E.g., list (x + (f y))≡list ((f (y + 0)) + x)

Car z = z’⇒x + z = z’ + x (avec z→(f y), z’→(f (y + 0)))

CoqMT:

I Une modification du noyau deCoqpermettant l’introduction dynamiquementdeproce´duresded´ecisiondanslaconversion.

I ´ndOceiritic

I Comment charger de telles boites noires I Comment le noyau les utilise

Roadmapdel’ajoutd’unethe´orie

Pouruneint´egrationeffectived’uneproce´duredede´cision:

1.Chargement, au sein du noyau, d’uneboite noire:

I eeDrcistpirdnoitaleoe´h I deCoecefffdti´ecisionlea’glrotimhdede

2.Etablissement ded´eseltrontiniefinesneiltealCsqoeobti noire(e.g. mapping des symboles au premier ordre sur Coq)

Chargement d’une boite noire (1/2)

I

I

The´orieT= (Σ,A,solve)→puatnaraudse`rtenoboˆı´eclired noyau 1.une sorte de travail (e.g.nat)→stermesmonosort´e 2.dysselobm(Σsenscouctrurteudso0g.e.)(isfin´e [C,0] , + [D,2] ) 3.une axiomatiqueA(e.g.∀xy,x+S(y) =S(x+y),∙ ∙ ∙) I Soit via une AST interne I Soit via un langage pour la logique de premier ordre 4.d´deontinioiseccnofenusolve(fonctionO’Caml)

Un contrat→ solvelatiasce´dredivadiliedt´laecsuseedoHnrpourT.

Chargement d’une boite noire (2/2)

I

I

Possibilit´ed’ins´ererplusieursthe´ories I Doivent travailler sur des sortes disjointes I Ne peuvent pas partager de variables

Th´ ies = codeO’Caml eor ⇒ierte´snevueeˆtnueiqntmerdreamyn`tmedeeivlasesyp chargement de code deCoq(Declare ML Module)

Lieruneth´eorie(1/3)

I Une boite noire estinerteuatpard´ef I Elle ne sait pas comment interagir avec les termes Coq

I Il faut I oqsContinifie´dsedruserdroremieauprolessymblrseLei I uvroPtasinoiixa’tamoifiebienlefiniv´erpaipgn´dreuqleme

I iaslonisusPlurieblsiosspetunureseiroe´h

Lierunethe´orie(2/3)

Pour Presburger, on peut e.g.

I Lier la sortenatsur l’inductif Inductivenat: Type :=0: nat|S: nat→nat .

I Lier les symboles0etSsur les constructeurs0etSden

0etSdenat.

I Lier le symbole+tionsurlad´efiniCoqstandardPeano.plus de l’addition.

Lierunethe´orie(3/3)

Lesystemedemanderaalorsdeve´rifier,dansCoq, que: `

I natest de typeType,eobmylseleuqtsselctentl’ai´esrepeir´te des symboles deT(e.g.0:nat,S:nat→nat).

I que les symbolesCoqurtsuetcossrtni´eslcsnoobelssmya`ed injectifs (ici, queSest injectif).

I ysseda`socselobmteuctrnsonessnurptsauqelessymbolesli´e confondus (ici, que 0et (Stuotourtauxpnse´seogntp)at).

I que les axiomes deTsselrapse´tcepsenrietbonsi´es.ymbolesl E.g., de∀x y,x+S(y) =S(x+y), il sera demande ´

forall (x y : nat), x

+ (Sy) =S(x + y)