Joulukalenteri 2009: Coq

(* Kuten nähdään, Coq ei ole optimoitu Hello Worldin kirjoittamiseen. *)
Require Import String.
Local Open Scope string_scope.
Check "Todistettavasti hauskaa joulua!".

"Todistettavasti hauskaa joulua!"
     : string

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).

     = 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.