Coq

Coq is een interactieve stellingbewijzer die voor het eerst werd uitgebracht in 1989. Het maakt het uitdrukken van wiskundige beweringen mogelijk, het controleert mechanisch de bewijzen van deze beweringen, het helpt bij het vinden van wiskundige bewijzen en het extraheert een gecertificeerd programma uit het constructieve bewijs van de formele specificatie ervan. Coq werkt binnen de theorie van de calculus van inductieve constructies, een afgeleide van de calculus van constructies. Coq is geen geautomatiseerde stellingbewijzer, maar omvat automatische stellingenbewijstactieken (procedures) en verschillende beslissingsprocedures. De Curry-Howard-correspondentie is de directe relatie tussen computerprogramma's en wiskundige bewijzen.

De naam "Coq" is een woordspeling op de naam van Thierry Coquand, Calculus of Constructions of "CoC" en volgt de Franse computerwetenschappelijke traditie van het vernoemen van software naar dieren (coq betekent in het Frans haan). Het ontwikkelingsteam maakte op 11 oktober 2023 bekend dat de naam Coq de komende maanden in The Rocq Prover zal worden veranderd.

Overzicht

Wanneer het wordt gezien als een programmeertaal, implementeert Coq een dependent getypeerde functionele programmeertaal. Wanneer het wordt gezien als een logisch systeem, implementeert het een hogere-orde typetheorie. De ontwikkeling van Coq werd begonnen door Gérard Huet en Thierry Coquand. Coq wordt voornamelijk geïmplementeerd in Ocaml met een beetje C. Het kernsysteem kan worden uitgebreid door middel van een plug-in-mechanisme.

Coq biedt een specificatietaal genaamd Gallina ("hen" in het Latijn, Spaans, Italiaans en Catalaans). Programma's geschreven in Gallina hebben de zwakke normalisatie-eigenschap, wat impliceert dat ze altijd eindigen. Dit is een onderscheidende eigenschap van de taal, aangezien oneindige lussen (niet-beëindigende programma's) gebruikelijk zijn in andere programmeertalen en een manier is om het stopprobleem te omzeilen.

Als voorbeeld een bewijs van commutativiteit van optelling op natuurlijke getallen in Coq:

plus_comm =
fun n m : nat =>
nat_ind (fun n0 : nat => n0 + m = m + n0)
  (plus_n_0 m)
  (fun (y : nat) (H : y + m = m + y) =>
   eq_ind (S (m + y))
     (fun n0 : nat => S (y + m) = n0)
     (f_equal S H)
     (m + S y)
     (plus_n_Sm m y)) n
     : forall n m : nat, n + m = m + n

nat_ind staat voor wiskundige indcutie.

Tactiektaal

Naast het expliciet construeren van Gallina-termen, ondersteunt Coq het gebruik van tactieken die zijn geschreven in de ingebouwde taal Ltac of in OCaml. Deze tactieken automatiseren de constructie van bewijzen, waarbij triviale of voor de hand liggende stappen in bewijzen worden uitgevoerd. Verschillende tactieken implementeren beslissingsprocedures voor verschillende theorieën. De 'ring'-tactiek bepaalt bijvoorbeeld de theorie van gelijkheid modulo ring- of semiring-axioma's via associatief-commutatief herschrijven. Het volgende bewijs vestigt bijvoorbeeld in slechts één bewijsregel een complexe gelijkheid in de ring van gehele getallen:

Require Import ZArith.
Open Scope Z_scope.
Goal forall a b c:Z,
    (a + b + c) ^ 2 =
     a * a + b ^ 2 + c * c + 2 * a * b + 2 * a * c + 2 * b * c.
  intros; ring.
Qed.

Ingebouwde beslissingsprocedures zijn ook beschikbaar voor de lege theorie ("congruentie"), propositionele logica ("tauto"), kwantificatorvrije lineaire rekenkunde met gehele getallen ("lia") en lineaire rationele / reële rekenkunde ("lra"). Verdere beslissingsprocedures zijn ontwikkeld als bibliotheken, waaronder één voor Kleene-algebra's en een andere voor bepaalde meetkundige doelen.

Bronvermelding

• Dit artikel of een eerdere versie ervan is een (gedeeltelijke) vertaling van het artikel Coq (software) op de Engelstalige Wikipedia, dat onder de licentie Creative Commons Naamsvermelding/Gelijk delen valt. Zie de bewerkingsgeschiedenis aldaar.