Coq

Coq on funktionaalisen ohjelmointiin perustuva todistusapuri. Sen avulla voidaan laatia formaaleja matemaattisia todistuksia, jotka tarkistetaan automaattisesti. Todistukset esitetään induktiivisten konstruktioiden kalkyyliin perustuvalla Gallina-ohjelmointikielellä.

Coqia käytetään mm. ohjelmistojen verifiointiin ja matematiikan formalisointiin. Coq on toteutettu OCaml-kielellä.

Koodiesimerkkejä

Määritellään luonnollisten lukujen tyyppi:

Inductive nat : Type :=
  | O : nat
  | S : nat -> nat.

Määritellään luonnollisten lukujen yhteenlasku:

Fixpoint plus (n m : nat) : nat :=
  match n with
  | O => m
  | S p => S (plus p m)
  end.

Osoitetaan, että määritellylle yhteenlaskufunktiolle pätee

$x+0=x$

kaikilla

$x$

.

Theorem plus_n_O: forall n: nat, plus n O = n.
Proof.
  intros n.
  induction n.
  - simpl. reflexivity.
  - trivial. simpl. rewrite IHn. reflexivity.
Qed.

Merkittäviä sovellutuksia

• Neliväriteoreeman Coq-todistus (2005)
• Feitin-Thompsonin lauseen Coq-todistus (2012)
• CompCert: Coqilla toteutettu ja verifioitu C-ohjelmointikielen kääntäjä.

Aiheesta muualla

• Coqin kotisivu