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ä^[1].

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

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 ${\textstyle x+0=x}$ kaikilla ${\textstyle 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.

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

• Coqin kotisivu