Speciaal voor NWT maakte Russell O'Connor van de Radboud Universiteit Nijmegen een nieuw formeel bewijs van de oude stelling van Euclides dat er oneindig veel priemgetallen zijn (zie kader, het oudste bewijs). Dit bewijs heeft hij geverifieerd met Coq. O'Connors bewijs ziet er zo uit:
***
Theorem NotFinitePrimes : forall l:list nat, ~(forall x, Prime x <-> In x l).
Proof.
intros l H.
cut (Prime 1).
unfold Prime; auto with *.
assert (H':=fun x => (proj1 (H x))).
assert (H0:Prime (product l + 1)).
apply primepropdiv.
firstorder using plus_lt_compat_r ZeroProduct.
intros q Hq H0.
replace q with 1 in Hq by eauto with *.
firstorder.
replace 1 with (product l + 1); eauto with *.
Qed.
***
Zo'n bewijs is voor mensen nauwelijks te lezen en ook de lijn die het bewijs volgt is heel anders dan de redenering van Euclides. In dit formele bewijs wordt bewezen dat als er een eindige lijst met precies alle priemgetallen bestaat, dat het getal 1 dan een priemgetal moet zijn. Omdat 1 geen priemgetal is, kan die eindige lijst met alle priemgetallen niet bestaan. Er zijn dus oneindig veel priemgetallen. Qed: quod erat demonstrandum, ofwel ‘hetgeen bewezen moest worden.’
Als je het bewijs in Coq draait, dan gaat het bewijs door verschillende toestanden. Aan het begin is de toestand:
***
1 subgoal
============================
forall l : list nat, ~ (forall x : nat, Prime x <-> In x l)
***
(Er is één doel, namelijk bewijzen dat er geen eindige lijst met alle priemgetallen bestaat.)
Aan het eind is de toestand:
***
Proof completed.
***
(Het bewijs is klaar en correct bevonden.)
Het programma verandert de toestand na elke stap. Neem bijvoorbeeld de stap “apply primepropdiv” in het bewijs. Daar wordt het volgende lemma gebruikt
***
primepropdiv
: forall n : nat,
n > 1 ->
(forall q : nat, Prime q -> Divides q n -> q * q > n) -> Prime n
***
(Laat n een positief geheel getal zijn dat groter is dan 1. Als elk priemgetal q dat n deelt groter is dan wortel(n), dan is n een priemgetal.)
Voor deze stap staat dit doel in de toestand van het bewijs:
***
subgoal 1 is:
l : list nat
H : forall x : nat, Prime x <-> In x l
H' : forall x : nat, Prime x -> In x l
============================
Prime (product l + 1)
***
Na deze stap is dit doel veranderd in:
***
subgoal 1 is:
l : list nat
H : forall x : nat, Prime x <-> In x l
H' : forall x : nat, Prime x -> In x l
============================
product l + 1 > 1
subgoal 2 is:
forall q : nat,
Prime q -> Divides q (product l + 1) -> q * q > product l + 1
***
Wat is er gebeurd in deze stap? Eerst was het doel om te bewijzen dat product l + 1 een priemgetal is. Na toepassing van het lemma zijn er twee doelen: laten zien dat product l + 1 groter is dan 1 en laten zien dat elke deler van product l + 1 groter is dan wortel(product l + 1 ). Het lemma zegt immers dat deze twee doelen samen betekenen dat product l + 1 een priemgetal is. Coq houdt zo steeds bij wat er nodig is om de bewering te bewijzen.
(Met dank aan Freek Wiedijk voor de uitleg van Coq.)
