Kirjoittaja: map_ (07.12.2009)
Coq on funktionaaliseen ohjelmointiin perustuva todistusapuri. Sen avulla voidaan kirjoittaa formaaleja matemaattisia todistuksia, jotka järjestelmä tarkistaa automaattisesti.
Coq perustuu ohjelmointikielten tyyppiteorian tulokseen nimeltä Curry-Howard -isomorfismi, joka on vastaavuus logiikan ja ohjelmoinnin välillä. Se kertoo, että tietyllä tavalla rakennetun ohjelmointikielen tietotyyppejä voidaan pitää loogisina väitteinä ja näiden tietotyyppien arvoja väitteiden todistuksina.
Esimerkiksi funktio A:lta B:lle, eli A -> B, vastaa loogista väitettä "A:sta seuraa B". Konjunktioa "A ja B" vastaa pari (vrt. kahden alkion struct tai tuple). Disjunktio "A tai B" ilmaistaan tietotyypillä, jonka arvo on joko A tai B -tyyppinen (vrt. C-kielen union).
Väitteet todistetaan keksimällä jokin arvo, jolla on tarvittava tyyppi. Esimerkiksi implikaatio (A ja B) -> (A tai B) todistetaan kirjoittamalla funktio, joka ottaa parametriksi parin ja palauttaa vaikkapa sen ensimmäisen alkion. Toisaalta implikaation (A tai B) -> (A ja B) todistaminen mielivaltaisille A ja B on mahdotonta - sen tyyppistä funktiota ei Coq:ssa voida kirjoittaa.
Edellä kuvatun funktionaalisen ohjelmointikielen päälle on Coq:ssa rakennettu myös interaktiivinen todistustaktiikkakieli. Siinä ei kirjoiteta funktioita suoraan, vaan annetaan käskyjä, kuten "pura konjunktio", "siirrä implikaation etujäsen oletukseksi", "tee induktio x:n suhteen", ...
(* Kuten nähdään, Coq ei ole optimoitu Hello Worldin kirjoittamiseen. *) Require Import String. Local Open Scope string_scope. Check "Todistettavasti hauskaa joulua!".
Tulostus:
"Todistettavasti hauskaa joulua!"
: stringSeuraava ohjelma tulostaa Fibonaccin lukuja:
Require Import List.
Fixpoint fibo (montako : nat) (a : nat) (b : nat) : list nat :=
match montako with
| 0 => nil
| S n => cons a (fibo n b (a + b))
end.
Eval compute in (fibo 11 1 1).Tulostus:
= 1 :: 1 :: 2 :: 3 :: 5 :: 8 :: 13 :: 21 :: 34 :: 55 :: 89 :: nil
: list nat(* Alussa mainittu esimerkki: *)
Definition a_ja_b__a_tai_b :
(* Väitetään, että kaikille propositioille A ja B pätee:
jos A ja B niin A tai B.
*)
forall A B : Prop, A /\ B -> A \/ B :=
(* Todistus on funktio, joka ottaa propositiot A ja B
sekä A /\ B-tyyppisen arvon (parin).
*)
fun A B a_ja_b =>
match a_ja_b with (* Puretaan annettu pari *)
| conj a b => (* Nimetään parin alkiot a:ksi ja b:ksi. *)
@or_introl A B a (* Rakennetaan disjunktio A \/ B antamalla a *)
end.
(* Coq:ssa mahdottomuus ilmaistaan tyypillä False. Falsen tyyppisiä
arvoja ei ole olemassa.
A:n negaatio "ei A" ilmaistaan tyypillä A -> False, eli
"A:sta seuraa mahdottomuus".
*)
(* Osoitetaan, että implikaatio A \/ B -> A /\ B on mahdoton.
Tämä tehdään tuottamalla funktio, joka
ottaa virheellisen implikaation A \/ B -> A /\ B
todistuksen ja rakentaa sen avulla todistuksen mahdottomuudelle.
*)
Definition ei__a_tai_b__a_ja_b :
(forall A B : Prop, A \/ B -> A /\ B) -> False :=
(* Tehdään vastaoletus:
Oletetaan, että A \/ B -> A /\ B pätee ja
johdetaan siitä mahdottomuus.
*)
fun kummallinen =>
(* Meillä on siis nyt käytössä funktio "kummallinen",
joka tekee disjunktiosta konjunktion.
Osaamme luoda disjunktion True \/ False, missä "True"
on triviaalisti todistuva väite, joka todistetaan
yksinkertaisesti termillä "I".
*)
let true_tai_false := @or_introl True False I
(* Nyt voimme antaa disjunktion funktiolle "kummallinen"
ja saamme ulos konjunktion True /\ False.
Tämä on jo selkeä ristiriita.
*)
in let true_ja_false := kummallinen True False true_tai_false
(* Nyt riitää enää purkaa konjunktio ja palauttaa sen
oikea puoli.
*)
in match true_ja_false with
| conj t f => f
end.
(* Tässä vielä esimerkin vuoksi todistustaktiikoilla kirjoitettu
hyvin lyhyt todistus sille, että 0 ei ole 1.
*)
Theorem nolla_ei_ole_yksi : 0 = 1 -> False.
Proof.
intro vastaoletus. (* Otetaan implikaation etujäsen oletukseksi. *)
(* Nyt meillä on yksi oletus nimeltä "vastaoletus", jonka tyyppi on
0 = 1. Todistettavana on enää False. *)
(* Annetaan Coq:n päätellä, millä tavoilla
yhtäsuuruus 0 = 1 on voitu rakentaa.
Coq huomaa helposti, että moisen yhtäsuuruuden rakentaminen
on mahdotonta, joten todistus on valmis.
*)
inversion vastaoletus.
Qed.Coq:ssa on mahdotonta kirjoittaa ikuista silmukkaa.
Ikuinen silmukka vastaisi Coq:ssa kehäpäätelmää, jonka avulla voitaisiin todistaa mitä tahansa.