Coq

Coq


Tyyppi	Lauseen todistaja
Kehittäjä	INRIA ; kehitystiimi
Sisään kirjoitettu	OCaml ; C
Käyttöjärjestelmä	cross-platform
Ensimmäinen painos	1. toukokuuta 1989
Laitteistoalusta	cross-platform
uusin versio	8.16.0 ( 5. syyskuuta 2022 ) [1]
Osavaltio	aktiivinen
Lisenssi	LGPL 2.1
Verkkosivusto	coq.inria.fr
Mediatiedostot Wikimedia Commonsissa

Coq ( fr. coq - rooster ) on interaktiivinen ohjelmistolauseen todistaja, joka käyttää omaa toiminnallista ohjelmointikieltä ( Gallina ) [2] riippuvaisilla tyypeillä . Voit kirjoittaa muistiin matemaattisia lauseita ja niiden todisteita , muokata niitä kätevästi, tarkistaa niiden oikeellisuuden. Käyttäjä luo vuorovaikutteisesti todisteen ylhäältä alas, alkaen tavoitteesta (eli todistettavasta hypoteesista). Coq voi automaattisesti löytää todisteita joistakin rajoitetuista teorioista käyttämällä niin kutsuttua taktiikkaa. Coqia käytetään ohjelman varmentamiseen .

Coq kehitettiin Ranskassa osana TypiCal -projektia (entinen LogiCal ) [3] , jota hallinnoivat yhdessä INRIA , Ecole Polytechnique , Paris-South XI -yliopisto ja National Center for Scientific Research . Aiemmin korkeakoulussa oli oma ryhmä. Normaali Lyonin koulu .

Coqin teoreettinen perusta on rakennuslaskenta ; sen lyhenne on piilotettu nimeen ( CoC , eng. calculus of constructions ) ja lyhenne laskennan luojan Thierry Cocanin nimestä .

Esimerkkejä

Funktiokokoonpanon assosiatiivisuus

Todiste "paperille" funktion koostumuksen assosiatiivisuudesta :

(f \circ g) \circ h

= \lambda x. (f \circ g) (h~x)

; δ-ekvivalenssi

= \lambda x. (\lambda y. f (g~y)) (h~x)

; δ-ekvivalenssi

= \lambda x. (f(g(h~x)))

; β-ekvivalenssi

f \circ (g \circ h)

= \lambda x. f ((g\circ h)~x)

; δ-ekvivalenssi

= \lambda x. f ((\lambda y. g (h~y))~x)

; δ-ekvivalenssi

= \lambda x. f(g(h~x))

; β-ekvivalenssi

Tasa-arvon transitiivisuudella:

(f \circ g) \circ h = f \circ (g \circ h)

Todiste Coqissa:

Määritelmä cf := fun t0 t1 t2 : Tyyppi => hauskaa (f : t1 -> t2) (g : t0 -> t1) => hauskaa x => f (gx). Implisiittiset argumentit vrt. [t0 t1 t2]. Merkintä "f @ g" := (vrt. fg) (tasolla 65, assosiatiivisuus vasemmalla). Määritelmä cf_assoc := hauskaa (t0 t1 t2 t3 : tyyppi) (f : t2 -> t3) (g : t1 -> t2) (h : t0 -> t1) => (refl_equal _) : (f @ g) @ h = f @ (g @ h).

cf - toimintojen koostumuksen määrittely. Notationottaa käyttöön infix-merkinnän @funktion koostumukselle.

cf_assoc - todellinen todiste. Coq perustuu Curry-Howard-isomorfismiin , joten todiste on lambda -lasken termi .

fun … => …Coq tarkoittaa lambda-abstraktiota . Funktiot on nimetty f, g, hja niiden laajuudet ja alueet on nimetty t0, t1, t2, t3.

Todistus koostuu lambda-abstraktion lisäksi refl_equal tasa-arvon refleksiivisyysaksioomasta. Meidän on vähennettävä yhtälön vasen ja oikea osa βδ-pelkistysten avulla yhdeksi lausekkeeksi. Coq suorittaa itse βδ-pelkistyksen, joten todistus on käytännössä tyhjä.

Ymmärtääksesi roolin refl_equal, suorita Check (refl_equal 2).Coq näyttää tämän termin automaattisesti päätellyn tyypin, nimittäin 2 = 2. Mutta todistuksessa cf_assocargumentti refl_equalkorvataan alleviivauksella. Coq itse voi päätellä tämän argumentin (katso " Argumenttiarvojen päättäminen tyypeistä "). Tämä vähentää todisteiden määrää. Suorittamalla Print cf_assoc., voit varmistaa, että Coq tulostaa termin (f @ g) @ halaviivan sijaan.

Kertolaskujen kommutatiivisuus Peano-aritmetiikassa

Luonnollisten lukujen tyyppi määritellään standardikirjastossa induktiivisesti:

Induktiivinen nat : Set := | O: nat | S: nat -> nat.

Rakentajat ja ovat nolla ja funktio, joka palauttaa seuraavan luvun. $O$ $S$

Se on tarpeen todistaa . Kommutatiivisuuden todiste Peanon aritmetiikassa on rakennettu käyttämällä matemaattista induktiota yhdelle tekijästä. $n \cdot m = m \cdot n$

Todiste "paperilla"

Coqissa käytettyä merkintää käytetään helpottamaan molempien todisteiden vertailua.

Tehdään induktio päälle . $n$

Induktion perusta: todistaa . Lausuma seuraa βδι-muunnoksesta. todistetaan erillisellä lemmalla (katso Coq.Init.Peano.mult_n_O). $O \cdot m = m \ cdot O$ $O \ cdot m = O$ $O = m \cdot O$

Vaihe induktio: ottaa induktiivinen hypoteesi , todistaa . βδι-muunnoksesta seuraa, että . On lemma (katso Coq.Init.Peano.mult_n_Sm), jossa todetaan . Käytämme summauksen kommutatiivisuutta ja induktiivista hypoteesia. $n \cdot m = m \cdot n$ $(S~n) \cdot m = m \cdot (S~n)$ $(S~n) \cdot m = m + n \cdot m$ $m \cdot n + m = m \cdot (S~n)$

Todistus Coqissa

Seuraava todistus on kopioitu pienin muutoksin vakiokirjastosta. Se käyttää taktiikkaa.

Taktiikka tuottaa automaattisesti todisteen (tai osan siitä) tavoitteen (mitä on todistettava) perusteella. Tietenkin, jotta taktiikka toimisi, on oltava algoritmi todisteiden löytämiseksi. Joissakin tapauksissa taktiikka voi vähentää todisteiden määrää huomattavasti.

Taktiikkaa varten sinun on määritettävä tyyppi Määritelmän jälkeen (tavoite, todistettava väite), mutta jätetään pois lambda-termi eli itse todistus. Sitten Coq siirtyy todisteen muokkaustilaan, jossa voit rakentaa todisteen taktiikalla.

Jos taktiikka pystyi täysin todistamaan maalin, se tuottaa nollan välimaaleja. Jos taktiikka ei onnistunut viimeistelemään todistetta, vaikka se suoritti joitakin vaiheita, taktiikka tuottaa nollasta poikkeavan määrän alitavoitteita. Todistuksen suorittamiseksi on todistettava osatavoitteet muilla taktiikoilla. Voit siis yhdistää erilaisia taktiikoita.

Vedosmuokkaustila ei estä vedoksen rakentamista lambda- termiksi . Taktiikka (katso " #Kertolaskun kommutatiivisuus Grothendieck-renkaassa ") on todistaa tavoite käyttämällä sen jälkeen merkittyä lambda-termiä. on seuraava lisäominaisuus: jos lambda-termissä on alaviiva joidenkin aliehtojen sijaan ja Coq ei voi päätellä aliehtojen arvoa automaattisesti, tämä alaviiva luo alakohteen. Siten se voi luoda mielivaltaisen määrän alitavoitteita. refinerefinerefinerefine

Vaadi Import Coq.Arith.Plus. Määritelmä mult_comm : kaikille nm, n * m = m * n. todiste. intros. Elim n. auto arithin kanssa. intros. yksinkertainen |- *. elim mult_n_Sm. elim H. apply plus_comm. Qed.

introsesittelee edellytykset ( nja m). elimsoveltaa matemaattista induktiota, jonka jälkeen todistuksen tavoite jaetaan kahteen osatavoitteeseen: induktion kanta ja askel. auto with arithosoittaa induktion perustan; Taktiikka autoetsii lausetietokannasta sopivan lauseen yksinkertaisella luettelolla ja korvaa sen todistuksessa. Tässä tapauksessa hän löytää lemman mult_n_O. Tämä voidaan varmistaa suorittamalla Show Proof.lemmat mult_n_Sm, plus_comm, ja induktiivinen hypoteesi H. Induktiivisen hypoteesin nimi syntyi automaattisesti taktiikalla intros, taktiikan toinen esiintyminen. simpl in |- *suorittaa kohteen βδι-muunnoksen. Vaikka se ei tuota todisteita, se tuo kohteen sellaiseen muotoon, jota tarvitaan taktiikan argumenttien päättelemiseksi apply plus_comm.

Sama todiste voidaan ilmaista lambda-termillä.

Määritelmä mult_comm := hauskaa n:nat => fix rec (m : nat) : n * m = m * n := täsmää m:ksi m palauttaa n * m = m * n kanssa | O => sym_eq(mult_n_O_) | S pm => match pm in _ = dep return _ = n + dep kanssa refl_equal => vastaa mult_n_Sm _ _ in _ = dep return dep = _ jossa refl_equal => plus_comm _ _ end loppu loppu.

elim nkirjeenvaihto fix … match … as …. Loput elimsopivat match … in _=dep …. Taktiikkatodistuksessa ei tarvitse määritellä Oja konstruktoreita S, koska ne on johdettu nat.

Määritelmä mult_comm := hauskaa n:nat => nat_ind(hauska m => n * m = m * n) (sym_eq(mult_n_O_)) (fun_rec => eq_ind _ (hauska dep => _ = n + dep) (eq_ind _ (hauska dep => dep = _) (plus_comm _ _) _ (mult_n_Sm _ _)) _rec).

Tämä on kompaktimpi, vaikkakin vähemmän visuaalinen merkintä. nat_indja eq_indniitä kutsutaan induktioperiaatteiksi ja ne ovat induktiivisten tyyppien rakenteen mukaan generoituja funktioita ( nat, if nat_ind, ja eq, if eq_ind). Taktikot lisäävät juuri nämä funktiot todisteeseen.

Kuten näet, taktiikan avulla voit jättää pois monia termejä, jotka voidaan päätellä automaattisesti.

Kertolaskun kommutatiivisuus Grothendieckin renkaassa

Tämä on esimerkki erikoistaktiikkojen käytöstä ring. Se suorittaa muunnoksia kaavoista, jotka on rakennettu puoli- tai rengasoperaatioista .

Grothendieckin rengas on rakennettu puolirenkaasta seuraavasti. int_bipart - renkaan kantaja - on toinen karteesinen aste nat - puolirenkaan kantaja.

Record int_bipart : Set := {pneg : nat; ppos: nat}.

Tietue ei ainoastaan konstruoi joukoista karteesista tuloa, vaan myös generoi vasemman (nimetty pneg) ja oikean (nimetty ppos) projektioita. Joukon arvo voidaan ymmärtää ratkaisuna yhtälöön , jossa on tuntematon suure. Jos , niin ratkaisu on negatiivinen. $i$ int_bipart $x + (pneg~i) = (ppos~j)$ $x$ $(pneg~i) > (ppos~j)$

Summa renkaassa määritellään komponenttikohtaiseksi lisäykseksi, eli pnegvasen termi lisätään pnegoikeaan termiin, pposvasen termi lisätään pposoikeaan termiin.

Merkintä "a !+ b" := (Peano.plus ab) (tasolla 50, vasen assosiaatio). Määritelmä plus ab := Build_int_bipart (pneg a !+ pneg b) (ppos a !+ ppos b). Merkintä "a + b" := (plus ab).

Merkitsemme lisäystä puolirenkaassa " !+" ja lisäystä renkaassa " +".

Kertominen määritellään seuraavasti: osa pneg(tämä on ensimmäinen argumentti Build_int_bipart) on eri komponenttien tulos, osa ppos(tämä on toinen argumentti Build_int_bipart) on samojen komponenttien tulos.

Merkintä "a !* b" := (Peano.mult ab) (tasolla 40, vasen assosiaatio). Määritelmä multab := Build_int_bipart (pneg a !* ppos b !+ ppos a !* pneg b) (pneg a !* pneg b !+ ppos a !* ppos b). Merkintä "a * b" := (mult ab) (tasolla 40, vasen assosiaatio).

Merkitsemme kertolaskua puolirenkaassa nimellä " !*" ja kertolaskua renkaalla nimellä " *".

Ensin todistetaan lemma "jos molemmat komponentit int_bipartovat yhtä suuret, ne int_bipartovat yhtä suuret".

Määritelmä int_bipart_eq_part : kaikille an bn, an = bn -> kaikille ap bp, ap = bp -> Build_int_bipart an ap = Build_int_bipart bn bp. todiste. tarkentaa (hauskaa _ _ eqn _ _ eqp => _). tarkentaa (eq_ind _ (hauska n => _ = Build_int_bipart n _) _ _ eqn). refine(f_equal_eqp). Qed.

Todistetaan nyt kertolaskun kommutatiivisuus renkaassa, eli n * m = m * n.

Vaadi Tuo ArithRing. Määritelmä mult_comm : kaikille nm, n * m = m * n. todiste. refine(fun nm => int_bipart_eq_part _ _ _ _ _ _); yksinkertainen; rengas. Qed.

Meidän on todistettava, että kaksi on yhtä suuri int_bipart. Lemma int_bipart_eq_partjakaa tavoitteemme kahdeksi osamaaliksi. Ensimmäinen osatavoite on pneg-komponenttien yhtäläisyys, toinen osatavoite on ppos-komponenttien yhtäläisyys. Näet nämä alitavoitteet, jos suoritat Proof." refine (fun n m => int_bipart_eq_part _ _ _ _ _ _).;" välittömästi sen jälkeen refineja ( ) välillä simpl; ringtarkoittaa , että yhdistetty taktiikka ( simpl; ring) todistaa kaikki taktiikan luomat osatavoitteet refine.

Todistaaksesi "paperilla" sinun on sovellettava johdonmukaisesti semiring-toimintojen ominaisuuksia:

(pneg~n) \cdot (ppos~m) + (ppos~n) \cdot (pneg~m)

= (ppos~m) \cdot (pneg~n) + (ppos~n) \cdot (pneg~m)

; kertolaskujen kommutatiivisuus

= (ppos~m) \cdot (pneg~n) + (pneg~m) \cdot (ppos~n)

; kertolaskujen kommutatiivisuus

= (pneg~m) \cdot (ppos~n) + (ppos~m) \cdot (pneg~n)

; lisäyksen kommutatiivisuus

(pneg~n) \cdot (pneg~m) + (ppos~n) \cdot (ppos~m)

= (pneg~m) \cdot (pneg~n) + (ppos~n) \cdot (ppos~m)

; kertolaskujen kommutatiivisuus

= (pneg~m) \cdot (pneg~n) + (ppos~m) \cdot (ppos~n)

; kertolaskujen kommutatiivisuus

Tactics ringluo kaikki nämä muutokset automaattisesti.

Työkalut

Toteutuskieli - OCaml ja C
Lisenssi - GNU Lesser General Public License Versio 2.1
Kehitysympäristöt:
- coqc-kääntäjä ja työkalut monitiedostoisten projektien kanssa työskentelemiseen
- coqtop - konsoli interaktiivinen ympäristö
- Kehitysympäristöt graafisella käyttöliittymällä :
  - coqide
  - Eclipse Proof General
  - Tila Emacsille
coqdoc - kirjaston dokumentaatiogeneraattori, ulostulo LaTeX- ja HTML - muotoihin
Vie todisteita XML:ään HELM1- ja MoWGLI-projekteille
Konstruktiivinen matematiikka tunnetaan siitä, että suuren olemassaolon todistuksesta voidaan poimia algoritmi tämän suuren saamiseksi. Coq voi viedä algoritmeja ML- ja Haskell-kielille . Arvoja, joiden tyyppi kuuluu lajitteluun Prop, ei poimita; yleensä näillä arvoilla on näyttöä.
Coqia voidaan laajentaa luotettavuudesta tinkimättä. Todistustarkistuksen oikeellisuus riippuu vedostarkistajasta , joka on pieni osa koko projektia. Se tarkistaa taktikoiden tuottamat todisteet, joten virheellinen taktiikka ei johda virheellisen todisteen hyväksymiseen. Joten Coq noudattaa de Bruijnin periaatetta .

Kieli

Käyttäjä voi syöttää omat aksioominsa
Perustuu (ko)induktiivisten konstruktien predikatiiviseen laskentaan , mikä tarkoittaa:
- Kaikki rakennuslaskennan mahdollisuudet :
- Universumien kumulatiivinen hierarkia, joka koostuu propista, joukosta ja luonnollisilla luvuilla indeksoidusta sarjatyypistä
- Prop impredikatiivi, Set ja Type predikatiivi
- Induktiiviset tai algebralliset tietotyypit
- Koinduktiiviset tietotyypit
- On mahdollista asettaa vain yleisiä rekursiivisia funktioita , eli sellaisia funktioita, joiden laskenta pysähtyy, eli ei silmukkaa. Coqissa Ackermann-funktio voidaan kirjoittaa . Induktiivisten tietotyyppien (kuten kokonaislukujen ja listojen) rekursion pysäyttäminen taataan "tuhoajien vartioima" -nimisen funktiomääritelmän syntaktisella tarkistuksella. Koinduktiivisten tyyppien mallisovitusta käyttävien toimintojen pysäyttäminen on taattu "rakentajien vartioima" -ehdon avulla.
- Implisiittinen tyyppivalu tai periytyminen [4]
Automaattinen tyyppipäätelmä
Argumenttien arvojen johtaminen tyypeistä. Esimerkiksi funktion toisen argumentin tai tuloksen tyyppi riippuu ensimmäisen argumentin arvosta (eli funktiolla on riippuvainen tyyppi). Sitten ensimmäisen argumentin arvo voidaan päätellä toisen argumentin tai tuloksen tyypistä. Alaviiva argumentin tilalla osoittaa, että argumentti pitäisi päätellä automaattisesti. Jos argumentti julistetaan implisiittiseksi, se voidaan yleensä jättää pois funktion nimen jälkeen [5] . Coq voi automaattisesti havaita argumentit, jotka on järkevää julistaa implisiittisiksi $f$ $f$
Taktiikka voidaan kirjoittaa seuraavasti:
- ML- ohjelmointikieli [6]
- Erikoiskieli taktiikoita varten Ltac [7]
- Coq lainaustaktiikkaa käyttäen
Sillä on laaja valikoima primitiivisiä taktiikoita (esim. intro, elim) ja pienempi joukko kehittyneitä taktiikoita tietyille teorioille (esim. kenttä kenttään , omega Presburger-aritmetiikkaa varten )
Setoidiryhmän taktiikka tekijäjoukkojen jäljittelemiseksi : määritetään ekvivalenssisuhde; toiminnot, jotka säilyttävät tämän suhteen; niin voit korvata termeillä vastaavat (edellä olevan suhteen mukaisesti) arvot
Tyyppiluokat on integroitu ( Haskellin tyyliin versiosta 8.2 lähtien).
Ohjelma ja Russel vahvistettujen ohjelmien luomiseen vahvistamattomista [8]

Kirjastot ja sovellukset

Matematiikan eri alojen formalisointi :
- Yleisalgebra
- Aritmetiikka ja lukuteoria
- Geometria
- Kombinatoriikka
- lambda-laskenta
- Matemaattinen logiikka , mukaan lukien itse rakennuslaskenta ja Pure Type Systems
- Matemaattinen analyysi
- Graafiteoria , joka sisältää todisteen ratkaisun olemassaolosta neljän värin ongelmaan - "todiste on lähes mahdoton varmistaa ilman tietokonetta"
- Luokkateoria
- Joukkoteoria , klassinen ja intuitionistinen
- Muodolliset kielet ja automaatit
Informatiikka:
- Ohjelmointikielten semantiikka
- RSA -algoritmien , Huffman-algoritmien ja muiden oikeellisuus
- Rinnakkaisjärjestelmät ja protokollat
- Loogisia pelejä
Ohjelman vahvistus:
- Miksi ohjelman vahvistusalustaa käytetään:
  - Krakatoa on työkalu Java- ja Java-korttiohjelmien tarkistamiseen Java- mallinnuskielellä
  - Frama-C — työkalu C -ohjelmien todentamiseen
- Ynot [9] on kirjasto pakollisten ohjelmien tarkistamiseen. Käyttää IO -monadin kehitystä ( Haskellilta ), Hoaren logiikkaa , erottelulogiikkaa
- Coqia voidaan käyttää [10] vaihtoehtoisena todistusjärjestelmänä GNATprove-työkalussa, jota käytetään SPARK -kielellä ( Adan murre ) ohjelmien muodolliseen todentamiseen.

Muistiinpanot

↑ Julkaisu Coq 8.16.0 - 2022.
↑ Chlipala, 2013 .
↑ Arkistoitu kopio . Haettu 26. helmikuuta 2009. Arkistoitu alkuperäisestä 26. helmikuuta 2009. (määrätön)
↑ Manual, 2009 , "Implicit Coercions".
↑ Manual, 2009 , "Implicit arguments".
↑ Manual, 2009 , "Käyttäjätaktiikoilla laajennetun huipputason rakentaminen".
↑ Manuaali, 2009 , "Taktinen kieli".
↑ Manuaali, 2009 , Ohjelma.
↑ Ei . Haettu 26. helmikuuta 2009. Arkistoitu alkuperäisestä 25. helmikuuta 2009. (määrätön)
↑ Alternative Provers - SPARK 2014 Käyttöopas 22.0w . docs.adacore.com . Haettu 30. syyskuuta 2020. Arkistoitu alkuperäisestä 12. lokakuuta 2020. (määrätön)

Kirjallisuus

Bertot, Y. ja Pierre Castéran, P. Vuorovaikutteisen lauseen todistaminen ja ohjelman kehittäminen: Coq'Art: Induktiivisten rakenteiden laskenta. - Springer, 2004. - ISBN 9783540208549 .
Henri Habrias, Marc Frappier. Luku 16. Coq // Ohjelmiston määrittelymenetelmät. - John Wiley & Sons, 2006. - 418 s. — ISBN 978-1-905-20934-7 .
Chlipala, A. Sertifioitu ohjelmointi riippuvaisilla tyypeillä: käytännöllinen johdatus Coq Proof Assistantiin . - MIT Press, 2013. - 440 s. — ISBN 9780262026659 . - helppokäyttöinen esitys Coqin käytöstä näyttöön perustuvassa ohjelmoinnissa
Ilja Sergei. Ohjelmat ja todisteet: Matematiikan koneistaminen riippuvaisilla tyypeillä . - 2014. - (Luentomuistiinpanot).

Linkit

The Coq proof assistant Arkistoitu 25. elokuuta 2004 Wayback Machinessa - Coqin virallinen verkkosivusto
Cocorico!, Coq Wiki arkistoitu 21. heinäkuuta 2011 Wayback Machinessa
Coqin kehitystiimi. Coq Proof Assistantin käsikirja. Versio 8.2. (linkki ei saatavilla) . Haettu 26. helmikuuta 2009. Arkistoitu alkuperäisestä 26. maaliskuuta 2012. (määrätön)